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

try_op bugfixes

Browse source
This commit is contained in:
Jakob Rath 2023-03-10 12:23:53 +01:00
parent dba8a4b73a
commit ffb7b5f85d
2 changed files with 13 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/op_constraint.cpp
View file

@ -256,18 +256,16 @@ namespace polysat {
else {
// forward propagation
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [>>] " << r() << " = " << (qv.val().is_unsigned() ? machine_div(pv.val(), rational::power_of_two(qv.val().get_unsigned())) : rational::zero()));
// LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [>>] " << r() << " = " << (qv.val().is_unsigned() ? machine_div2k(pv.val(), qv.val().get_unsigned()) : rational::zero()));
if (qv.is_val() && !rv.is_val()) {
const rational& qr = qv.val();
if (qr >= N)
return s.mk_clause(~lshr, ~s.ule(m.mk_val(m.power_of_2()), q()), s.eq(r()), true);
if (rv.is_val()) {
const rational& pr = pv.val();
return s.mk_clause(~lshr, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(
qr.is_unsigned()
? machine_div(pr, rational::power_of_two(qr.get_unsigned()))
: rational::zero())), true);
// q >= N -> r = 0
return s.mk_clause(~lshr, ~s.ule(m.mk_val(N), q()), s.eq(r()), true);
if (pv.is_val()) {
// p = pv & q = qv ==> r = rv
rational const rval = qr.is_unsigned() ? machine_div2k(pv.val(), qr.get_unsigned()) : rational::zero();
return s.mk_clause(~lshr, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), m.mk_val(rval)), true);
}
}
}

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

@ -35,7 +35,7 @@ namespace polysat {
void saturation::log_lemma(pvar v, conflict& core) {
IF_VERBOSE(2, {
clause* cl = core.lemmas().back();
verbose_stream() << m_rule << " v" << v << " ";
verbose_stream() << (m_rule ? m_rule : "m_rule is null!") << " v" << v << " ";
for (auto lit : *cl)
verbose_stream() << s.lit2cnstr(lit) << " ";
verbose_stream() << " " << *cl << "\n";
@ -226,10 +226,10 @@ namespace polysat {
}
bool saturation::try_op(pvar v, signed_constraint c, conflict& core) {
set_rule("try_op");
SASSERT(c->is_op());
SASSERT(c.is_positive());
op_constraint* op = ((op_constraint*)c.get());
clause_ref correction = op->produce_lemma(s, s.get_assignment(), c.is_positive());
clause_ref correction = c.produce_lemma(s, s.get_assignment());
if (correction) {
IF_LOGGING(
LOG("correcting op_constraint: " << *correction);
@ -238,9 +238,9 @@ namespace polysat {
}
);
for (const sat::literal& l : *correction)
if (!s.m_bvars.is_assigned(l))
s.assign_eval(~l);
for (sat::literal lit : *correction)
if (!s.m_bvars.is_assigned(lit) && s.lit2cnstr(lit).is_currently_false(s))
s.assign_eval(~lit);
core.add_lemma(correction);
log_lemma(v, core);
return true;