mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

Strengthen umul_ovfl lemma

Browse source
This commit is contained in:
Jakob Rath 2022-12-14 11:07:16 +01:00
parent 1bc4313333
commit e978e4fc8e
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/umul_ovfl_constraint.cpp
View file

@ -90,8 +90,6 @@ namespace polysat {
return; return;
if (narrow_bound(s, is_positive, q(), p(), q1, p1)) if (narrow_bound(s, is_positive, q(), p(), q1, p1))
return; return;
} }
void umul_ovfl_constraint::activate(solver& s, bool is_positive) { void umul_ovfl_constraint::activate(solver& s, bool is_positive) {
@ -99,8 +97,10 @@ namespace polysat {
return; return;
if (!is_positive) { if (!is_positive) {
signed_constraint sc(this, is_positive); signed_constraint sc(this, is_positive);
s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(p(), p()*q()), false); // ¬Omega(p, q) ==> q = 0 \/ p <= p*q
s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(q(), p()*q()), false); // ¬Omega(p, q) ==> p = 0 \/ q <= p*q
s.add_clause(~sc, /* s.eq(p()), */ s.eq(q()), s.ule(p(), p()*q()), false);
s.add_clause(~sc, s.eq(p()), /* s.eq(q()), */ s.ule(q(), p()*q()), false);
} }
} }