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

insert_eval

Browse source
This commit is contained in:
Jakob Rath 2022-12-07 18:41:42 +01:00
parent 93ee9c7f8e
commit 45e94ae7dd
2 changed files with 12 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -121,10 +121,9 @@ namespace polysat {
if (!is_forced_false(c))
return false;
// TODO: ??? this means that c is already on the search stack, so presumably the lemma won't help. Should check whether this case occurs.
// if (c.bvalue(s) == l_true)
// return false;
SASSERT(c.bvalue(s) != l_true);
// Constraint c is already on the search stack, so the lemma will not derive anything new.
if (c.bvalue(s) == l_true)
return false;
m_lemma.insert_eval(c);
core.add_lemma(m_rule, m_lemma.build());
@ -354,7 +353,7 @@ namespace polysat {
if (!is_non_overflow(x, y, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
if (!xy_l_xz.is_strict())
m_lemma.insert_eval(s.eq(x));
return add_conflict(core, xy_l_xz, ineq(xy_l_xz.is_strict(), y, z));
@ -397,7 +396,7 @@ namespace polysat {
return false;
pdd const& z_prime = l_y.lhs();
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
return add_conflict(core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x));
}
@ -437,7 +436,7 @@ namespace polysat {
if (!is_non_overflow(x, y_prime, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
return add_conflict(core, yx_l_zx, z_l_y, ineq(z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x));
}
@ -478,7 +477,7 @@ namespace polysat {
if (!is_non_overflow(a, z, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
return add_conflict(core, y_l_ax, x_l_z, ineq(x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z));
}
@ -602,9 +601,9 @@ namespace polysat {
if (!is_non_overflow(a, X, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~s.eq(b, rational(-1)));
m_lemma.insert(~s.eq(y));
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~s.eq(b, rational(-1)));
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~non_ovfl);
if (propagate(core, axb_l_y, s.eq(X, 1)))
return true;
if (propagate(core, axb_l_y, s.eq(a, 1)))

3
src/test/polysat.cpp
View file

@ -1591,7 +1591,7 @@ void tst_polysat() {
// test_polysat::test_ineq_axiom1(32, 1);
// test_polysat::test_pop_conflict();
// test_polysat::test_l2();
test_polysat::test_ineq1();
// test_polysat::test_ineq1();
// test_polysat::test_quot_rem();
// test_polysat::test_ineq_non_axiom1(32, 3);
// test_polysat::test_monot_bounds_full();
@ -1599,6 +1599,7 @@ void tst_polysat() {
// test_polysat::test_quot_rem_incomplete();
// test_polysat::test_monot();
// test_polysat::test_fixed_point_arith_div_mul_inverse();
test_polysat::test_monot_bounds_simple(8);
return;
#endif