mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

block flips to units

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-01 16:01:58 -08:00
parent cb61af0496
commit 814d7f4d0a
3 changed files with 15 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -106,8 +106,11 @@ namespace sls {
return false;
expr* e = vars[ctx.rand(vars.size())];
if (m.is_bool(e)) {
auto v = ctx.atom2bool_var(e);
if (ctx.is_unit(v))
return false ;
TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";);
ctx.flip(ctx.atom2bool_var(e));
ctx.flip(v);
return true;
}
SASSERT(bv.is_bv(e));
@ -126,7 +129,10 @@ namespace sls {
expr* e = vars[ctx.rand(vars.size())];
if (m.is_bool(e)) {
TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";);
ctx.flip(ctx.atom2bool_var(e));
auto v = ctx.atom2bool_var(e);
if (ctx.is_unit(v))
return false;
ctx.flip(v);
return true;
}
SASSERT(bv.is_bv(e));
@ -370,6 +376,8 @@ namespace sls {
}
double bv_lookahead::lookahead_flip(sat::bool_var v) {
if (ctx.is_unit(v))
return -100;
auto a = ctx.atom(v);
return lookahead_update(a, m_v_updated);
}
@ -541,6 +549,8 @@ namespace sls {
auto v = ctx.atom2bool_var(e);
auto v1 = m_ev.bval1(to_app(e));
if (v != sat::null_bool_var) {
if (ctx.is_unit(v))
continue;
if (ctx.is_true(v) == v1)
continue;
TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";);

2
src/ast/sls/sls_context.cpp
View file

@ -505,7 +505,7 @@ namespace sls {
if (clause.m_clause.size() == 1)
m_unit_literals.push_back(clause.m_clause[0]);
for (sat::literal lit : m_unit_literals)
m_unit_indices.insert(lit.index());
m_unit_indices.insert(lit.var());
IF_VERBOSE(3, verbose_stream() << "UNITS " << m_unit_literals << "\n");
for (unsigned i = 0; i < m_atoms.size(); ++i)

3
src/ast/sls/sls_context.h
View file

@ -181,7 +181,8 @@ namespace sls {
unsigned rand(unsigned n) { return m_rand(n); }
sat::literal_vector const& root_literals() const { return m_root_literals; }
sat::literal_vector const& unit_literals() const { return m_unit_literals; }
bool is_unit(sat::literal lit) const { return m_unit_indices.contains(lit.index()); }
bool is_unit(sat::literal lit) const { return is_unit(lit.var()); }
bool is_unit(sat::bool_var v) const { return m_unit_indices.contains(v); }
void reinit_relevant();
void force_restart() { s.force_restart(); }
bool include_func_interp(func_decl* f) const { return any_of(m_plugins, [&](plugin* p) { return p && p->include_func_interp(f); }); }