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

Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-03-07 15:21:53 +01:00
commit 6d0c3c0770
5 changed files with 31 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -584,7 +584,7 @@ namespace polysat {
}
}
}
for (unsigned d : deps)
out_deps.push_back(dependency(d));
if (!m_dep.is_null() && !deps.contains(m_dep.val()))

22
src/math/polysat/saturation.cpp
View file

@ -812,22 +812,31 @@ namespace polysat {
bool saturation::try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] 2^k*x = 2^k*y & x < 2^N-k => y = x or y >= 2^{N-k}");
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
unsigned const N = m.power_of_2();
pdd y = m.zero();
pdd a = y, b = y, a2 = y;
pdd X = s.var(x);
pdd const X = s.var(x);
// Match ax + b <= y with eval(y) = 0
if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
return false;
if (!a.is_val())
return false;
if (!a.val().is_power_of_two())
return false;
unsigned k = a.val().trailing_zeros();
unsigned const k = a.val().trailing_zeros();
if (k == 0)
return false;
// x*2^k = b, x <= a2 < 2^{N-k}
rational const bound = rational::power_of_two(N - k);
b = -b;
if (b.leading_coefficient() != a.val())
return false;
pdd Y = m.zero();
if (!b.try_div(b.leading_coefficient(), Y))
return false;
rational Y_val;
if (!s.try_eval(Y, Y_val) || Y_val >= bound)
return false;
for (auto c : core) {
if (!c->is_ule())
continue;
@ -836,15 +845,9 @@ namespace polysat {
continue;
if (!a2.is_val())
continue;
// x*2^k = b, x <= a2 < 2^{N-k}
rational bound = rational::power_of_two(N - k);
if (i.is_strict() && a2.val() >= bound)
continue;
if (!i.is_strict() && a2.val() > bound)
continue;
pdd Y = b.div(b.leading_coefficient());
rational Y_val;
if (!s.try_eval(Y, Y_val) || Y_val >= bound)
continue;
signed_constraint le = s.ule(Y, bound - 1);
m_lemma.reset();
@ -854,7 +857,6 @@ namespace polysat {
if (propagate(x, core, axb_l_y, s.eq(X, Y)))
return true;
}
return false;
}

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

@ -180,7 +180,7 @@ namespace polysat {
// Input literal contradicts current boolean state (e.g., opposite literals in the input)
// => conflict only flags the inconsistency
set_conflict_at_base_level(dep);
m_conflict.insert(~c); // ~c is true in the solver, need to track its original dependencies
m_conflict.insert(~c);
return;
}
m_bvars.assumption(lit, m_level, dep);

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;