mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

Weaken precondition for overflow narrow

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-25 14:51:26 +01:00
parent 8be6dcce31
commit 4cf24fb5fc
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -117,9 +117,13 @@ namespace polysat {
auto const& max = p.manager().max_value(); auto const& max = p.manager().max_value();
// p * q >= max + 1 <=> q >= (max + 1)/p <=> q >= ceil((max+1)/p) // p * q >= max + 1 <=> q >= (max + 1)/p <=> q >= ceil((max+1)/p)
auto bound = ceil((max + 1) / p.val()); auto bound = ceil((max + 1) / p.val());
SASSERT(bound.is_pos());
SASSERT(bound * p.val() > max); SASSERT(bound * p.val() > max);
SASSERT((bound - 1) * p.val() <= max); SASSERT((bound - 1) * p.val() <= max);
rational relaxed_p = p.val(); // Lowest value such that bound is correct
relaxed_p = ceil((max + 1) / bound);
SASSERT(relaxed_p <= p.val());
// //
// the clause that explains bound <= q or bound > q // the clause that explains bound <= q or bound > q
// //
@ -129,16 +133,16 @@ namespace polysat {
signed_constraint sc(this, is_positive); signed_constraint sc(this, is_positive);
if (is_positive) { if (is_positive) {
clause_builder lemma(s, "Ovfl(p, q) & p <= p.val() ==> q >= bound"); clause_builder lemma(s, "Ovfl(p, q) & p <= relaxed(p.val()) ==> q >= bound");
lemma.insert_eval(~sc); lemma.insert_eval(~sc);
lemma.insert_eval(~s.ule(p0, p.val())); lemma.insert_eval(~s.ule(p0, relaxed_p));
lemma.insert(s.ule(bound, q0)); lemma.insert(s.ule(bound, q0));
s.add_clause(lemma.build()); s.add_clause(lemma.build());
} }
else { else {
clause_builder lemma(s, "~Ovfl(p, q) & p >= p.val() ==> q < bound"); clause_builder lemma(s, "~Ovfl(p, q) & p >= relaxed(p.val()) ==> q < bound");
lemma.insert_eval(~sc); lemma.insert_eval(~sc);
lemma.insert_eval(~s.ule(p.val(), p0)); lemma.insert_eval(~s.ule(relaxed_p, p0));
lemma.insert(s.ult(q0, bound)); lemma.insert(s.ult(q0, bound));
s.add_clause(lemma.build()); s.add_clause(lemma.build());
} }