mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

polysat fixes

Browse source 
1. ensure that force_push is invoked before polysat updates state.
2. extract conflicts based on dependencies of both new literal that was conflicting with existing literal that had its value assigned based on dependencies.
This commit is contained in:
Nikolaj Bjorner 2023-03-06 17:35:39 -08:00
parent be0d0d5b9b
commit 6c00d40513
6 changed files with 34 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/polysat/conflict.cpp
View file

@ -167,6 +167,7 @@ namespace polysat {
void conflict::reset() {
m_literals.reset();
m_vars.reset();
m_dep_literal = sat::null_literal;
m_var_occurrences.reset();
m_vars_occurring.reset();
m_lemmas.reset();
@ -184,16 +185,21 @@ namespace polysat {
return contains(lit) || contains(~lit);
}
void conflict::init_at_base_level(dependency dep) {
void conflict::init_at_base_level(dependency dep, sat::literal lit) {
SASSERT(empty());
SASSERT(s.at_base_level());
m_level = s.m_level;
m_dep = dep;
m_dep_literal = lit;
SASSERT(!empty());
// TODO: logger().begin_conflict???
// TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
}
void conflict::init_at_base_level(dependency dep) {
init_at_base_level(dep, sat::null_literal);
}
void conflict::init(signed_constraint c) {
LOG("Conflict: constraint " << lit_pp(s, c));
SASSERT(empty());
@ -585,6 +591,9 @@ namespace polysat {
}
}
if (m_dep_literal != sat::null_literal)
enqueue_lit(m_dep_literal);
for (unsigned d : deps)
out_deps.push_back(dependency(d));
if (!m_dep.is_null() && !deps.contains(m_dep.val()))

3
src/math/polysat/conflict.h
View file

@ -102,6 +102,7 @@ namespace polysat {
// Level at which the conflict was discovered
unsigned m_level = UINT_MAX;
dependency m_dep = null_dependency;
sat::literal m_dep_literal = sat::null_literal;
public:
conflict(solver& s);
@ -128,6 +129,8 @@ namespace polysat {
/** conflict due to obvious input inconsistency */
void init_at_base_level(dependency dep);
/** conflict due to obvious input inconsistency with literal */
void init_at_base_level(dependency dep, sat::literal lit);
/** conflict because the constraint c is false under current variable assignment */
void init(signed_constraint c);
/** boolean conflict with the given clause */

3
src/math/polysat/solver.cpp
View file

@ -599,6 +599,7 @@ namespace polysat {
#if 0
m_fixed_bits.push();
#endif
display(verbose_stream() << "push\n");
}
void solver::pop_levels(unsigned num_levels) {
@ -710,6 +711,8 @@ namespace polysat {
m_trail.push_back(trail_instr_t::assign_bool_i);
LOG("Replay: " << lit);
}
display(verbose_stream());
}
bool solver::can_decide() const {

1
src/math/polysat/solver.h
View file

@ -263,6 +263,7 @@ namespace polysat {
void propagate_clause(clause& cl);
void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
void set_conflict_at_base_level(dependency dep, sat::literal lit) { m_conflict.init_at_base_level(dep, lit); }
void set_conflict(signed_constraint c) { m_conflict.init(c); }
void set_conflict(clause& cl) { m_conflict.init(cl); }
void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }

9
src/sat/smt/bv_polysat.cpp
View file

@ -205,6 +205,7 @@ namespace bv {
polysat::signed_constraint sc = a->m_sc;
if (!sc)
return;
force_push();
SASSERT(s().value(a->m_bv) != l_undef);
bool sign = l_false == s().value(a->m_bv);
sat::literal lit(a->m_bv, sign);
@ -216,6 +217,7 @@ namespace bv {
bool solver::polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
if (!use_polysat())
return false;
force_push();
pdd p = var2pdd(r1);
pdd q = var2pdd(r2);
auto sc = m_polysat.eq(p, q);
@ -229,11 +231,13 @@ namespace bv {
bool solver::polysat_diseq_eh(euf::th_eq const& ne) {
if (!use_polysat())
return false;
force_push();
euf::theory_var v1 = ne.v1(), v2 = ne.v2();
pdd p = var2pdd(v1);
pdd q = var2pdd(v2);
auto sc = ~m_polysat.eq(p, q);
sat::literal neq = ~expr2literal(ne.eq());
TRACE("bv", tout << neq << " := " << s().value(neq) << " @" << s().scope_lvl() << "\n");
m_polysat.assign_eh(sc, polysat::dependency(1 + 2 * neq.index()));
return true;
}
@ -241,6 +245,7 @@ namespace bv {
void solver::polysat_propagate() {
if (!use_polysat())
return;
force_push();
lbool r = m_polysat.unit_propagate();
if (r == l_false)
polysat_core();
@ -249,6 +254,7 @@ namespace bv {
lbool solver::polysat_final() {
if (!use_polysat())
return l_true;
force_push();
lbool r = m_polysat.check_sat();
if (r == l_false)
polysat_core();
@ -268,6 +274,9 @@ namespace bv {
eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2)));
}
}
for (auto lit : core) {
VERIFY(s().value(lit) == l_true);
}
auto ex = mk_bv2ext_justification(core, eqs);
ctx.set_conflict(ex);
}

9
src/sat/smt/bv_solver.cpp
View file

@ -247,10 +247,10 @@ namespace bv {
return;
if (s().is_probing())
return;
TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
if (polysat_diseq_eh(ne))
return;
TRACE("bv", tout << "diff: " << v1 << " != " << v2 << " @" << s().scope_lvl() << "\n";);
unsigned sz = m_bits[v1].size();
if (sz == 1)
return;
@ -801,6 +801,13 @@ namespace bv {
return out << "bv <- " << m_bits[v1] << " != " << m_bits[v2] << " @" << cidx;
case bv_justification::kind_t::bv2int:
return out << "bv <- v" << v1 << " == v" << v2 << " <== " << ctx.bpp(c.a) << " == " << ctx.bpp(c.b) << " == " << ctx.bpp(c.c);
case bv_justification::kind_t::bvext: {
for (unsigned i = 0; i < c.m_num_literals; ++i)
out << c.m_literals[i] << " ";
for (unsigned i = 0; i < c.m_num_eqs; ++i)
out << ctx.bpp(c.m_eqs[i].first) << " == " << ctx.bpp(c.m_eqs[i].second) << " ";
return out << "\n";
}
default:
UNREACHABLE();
break;