mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

add review comment to bug location

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-24 12:40:47 -08:00
parent 48cd05c725
commit e978b81c7a
3 changed files with 15 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1199,7 +1199,6 @@ namespace polysat {
bool saturation::try_factor_equality2(pvar x, conflict& core, inequality const& a_l_b) { bool saturation::try_factor_equality2(pvar x, conflict& core, inequality const& a_l_b) {
set_rule("[x] ax + b = 0 & C[x] => C[-inv(a)*b]"); set_rule("[x] ax + b = 0 & C[x] => C[-inv(a)*b]");
auto& m = s.var2pdd(x); auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y = m.zero(); pdd y = m.zero();
pdd a = y, b = y, a1 = y, b1 = y; pdd a = y, b = y, a1 = y, b1 = y;
if (!is_AxB_eq_0(x, a_l_b, a, b, y)) if (!is_AxB_eq_0(x, a_l_b, a, b, y))
@ -1242,20 +1241,24 @@ namespace polysat {
auto const& ule = c->to_ule(); auto const& ule = c->to_ule();
auto p = replace(ule.lhs()); auto p = replace(ule.lhs());
auto q = replace(ule.rhs()); auto q = replace(ule.rhs());
if (!change)
continue;
m_lemma.reset(); m_lemma.reset();
m_lemma.insert(~c); m_lemma.insert(~c);
m_lemma.insert_eval(~s.eq(y)); m_lemma.insert_eval(~s.eq(y));
if (change && propagate(x, core, a_l_b, c.is_positive() ? s.ule(p, q) : ~s.ule(p, q))) if (propagate(x, core, a_l_b, c.is_positive() ? s.ule(p, q) : ~s.ule(p, q)))
prop = true; prop = true;
} }
else if (c->is_umul_ovfl()) { else if (c->is_umul_ovfl()) {
auto const& ovf = c->to_umul_ovfl(); auto const& ovf = c->to_umul_ovfl();
auto p = replace(ovf.p()); auto p = replace(ovf.p());
auto q = replace(ovf.q()); auto q = replace(ovf.q());
if (!change)
continue;
m_lemma.reset(); m_lemma.reset();
m_lemma.insert(~c); m_lemma.insert(~c);
m_lemma.insert_eval(~s.eq(y)); m_lemma.insert_eval(~s.eq(y));
if (change && propagate(x, core, a_l_b, c.is_positive() ? s.umul_ovfl(p, q) : ~s.umul_ovfl(p, q))) if (propagate(x, core, a_l_b, c.is_positive() ? s.umul_ovfl(p, q) : ~s.umul_ovfl(p, q)))
prop = true; prop = true;
} }
} }

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

@ -1060,6 +1060,8 @@ namespace polysat {
void solver::assign_eval(sat::literal lit) { void solver::assign_eval(sat::literal lit) {
signed_constraint const c = lit2cnstr(lit); signed_constraint const c = lit2cnstr(lit);
LOG_V(10, "Evaluate: " << lit_pp(*this ,lit)); LOG_V(10, "Evaluate: " << lit_pp(*this ,lit));
// assertion is false
if (!c.is_currently_true(*this)) IF_VERBOSE(0, verbose_stream() << c << " is not currently true\n");
SASSERT(c.is_currently_true(*this)); SASSERT(c.is_currently_true(*this));
VERIFY(c.is_currently_true(*this)); VERIFY(c.is_currently_true(*this));
unsigned level = 0; unsigned level = 0;

7
src/math/polysat/viable.cpp
View file

@ -169,6 +169,13 @@ namespace polysat {
// - side conditions // - side conditions
// - i.lo() == i.lo_val() for each unit interval i // - i.lo() == i.lo_val() for each unit interval i
// - i.hi() == i.hi_val() for each unit interval i // - i.hi() == i.hi_val() for each unit interval i
// NSB review:
// the bounds added by x < p and p < x in forbidden_intervals
// match_non_max
// use values that are approximations. Then the propagations in
// try_assign_eval are incorrect.
for (auto const& c : get_constraints(v)) { for (auto const& c : get_constraints(v)) {
s.try_assign_eval(c); s.try_assign_eval(c);
} }