mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 18:36:41 +00:00
Code Activity

ovfl

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-09 13:15:59 -08:00
parent dcdbbfb925
commit 99e2247ccb
2 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/math/polysat/mul_ovfl_constraint.cpp
View file

@ -92,9 +92,9 @@ namespace polysat {
} }
if (is_always_true(is_positive, p1, q1)) if (is_always_true(is_positive, p1, q1))
return; return;
if (narrow_bound(s, is_positive, p1, q1)) if (narrow_bound(s, is_positive, p(), q(), p1, q1))
return; return;
if (narrow_bound(s, is_positive, q1, p1)) if (narrow_bound(s, is_positive, q(), p(), q1, p1))
return; return;
} }
@ -107,7 +107,8 @@ namespace polysat {
* Use bounds on variables in p instead of current assignment as premise. * Use bounds on variables in p instead of current assignment as premise.
* This is a more general lemma * This is a more general lemma
*/ */
bool mul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, pdd const& p, pdd const& q) { bool mul_ovfl_constraint::narrow_bound(solver& s, bool is_positive,
pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
if (!p.is_val()) if (!p.is_val())
return false; return false;
@ -118,17 +119,19 @@ namespace polysat {
auto bound = ceil((max + 1) / p.val()); auto bound = ceil((max + 1) / p.val());
// the clause that explains bound <= q or bound > q // the clause that explains bound <= q or bound > q
// is justified by the partial assignment to m_vars //
// Ovfl(p, q) & p <= p.val() => q >= bound
// ~Ovfl(p, q) & p >= p.val() => q < bound
signed_constraint sc(this, is_positive); signed_constraint sc(this, is_positive);
signed_constraint conseq = is_positive ? s.ule(bound, q) : s.ult(q, bound); signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0);
signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound);
SASSERT(premise.is_currently_false(s));
clause_builder cb(s); clause_builder cb(s);
cb.push_new(~sc); cb.push_new(~sc);
cb.push_new(~premise);
cb.push_new(conseq); cb.push_new(conseq);
for (auto v : m_vars)
if (s.is_assigned(v))
cb.push_new(~s.eq(s.var(v), s.get_value(v)));
clause_ref just = cb.build(); clause_ref just = cb.build();
s.assign_propagate(conseq.blit(), *just); s.assign_propagate(conseq.blit(), *just);
return true; return true;

2
src/math/polysat/mul_ovfl_constraint.h
View file

@ -25,7 +25,7 @@ namespace polysat {
void simplify(); void simplify();
bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const; bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const;
bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const; bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const;
bool narrow_bound(solver& s, bool is_positive, pdd const& p, pdd const& q); bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
public: public:
~mul_ovfl_constraint() override {} ~mul_ovfl_constraint() override {}