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

Simplify constraint evaluation

Browse source
This commit is contained in:
Jakob Rath 2022-11-23 12:19:03 +01:00
parent e4999b07aa
commit fdc186b204
10 changed files with 95 additions and 113 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/constraint.cpp
View file

@ -24,8 +24,8 @@ Author:
namespace polysat {
bool constraint::is_currently_false(solver& s, bool is_positive) const {
return is_currently_false(s.assignment(), is_positive);
lbool constraint::eval(solver const& s) const {
return eval(s.assignment());
}
bool signed_constraint::is_eq() const {

32
src/math/polysat/constraint.h
View file

@ -83,12 +83,18 @@ namespace polysat {
virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
virtual bool is_always_false(bool is_positive) const = 0;
bool is_currently_false(solver& s, bool is_positive) const;
virtual bool is_currently_false(assignment const& a, bool is_positive) const = 0;
bool is_always_true(bool is_positive) const { return is_always_false(!is_positive); }
bool is_currently_true(solver& s, bool is_positive) const { return is_currently_false(s, !is_positive); }
bool is_currently_true(assignment const& a, bool is_positive) const { return is_currently_false(a, !is_positive); }
/** Evaluate the positive-polarity constraint under the empty assignment */
virtual lbool eval() const = 0;
/** Evaluate the positive-polarity constraint under the given assignment */
virtual lbool eval(assignment const& a) const = 0;
/** Evaluate the positive-polarity constraint under the solver's current assignment */
lbool eval(solver const& s) const;
bool is_always_true(bool is_positive) const { return eval() == to_lbool(is_positive); }
bool is_always_false(bool is_positive) const { return is_always_true(!is_positive); }
bool is_currently_true(assignment const& a, bool is_positive) const { return eval(a) == to_lbool(is_positive); }
bool is_currently_false(assignment const& a, bool is_positive) const { return is_currently_true(a, !is_positive); }
bool is_currently_true(solver const& s, bool is_positive) const { return eval(s) == to_lbool(is_positive); }
bool is_currently_false(solver const& s, bool is_positive) const { return is_currently_true(s, !is_positive); }
virtual void narrow(solver& s, bool is_positive, bool first) = 0;
virtual inequality as_inequality(bool is_positive) const = 0;
@ -147,12 +153,18 @@ namespace polysat {
bool is_positive() const { return m_positive; }
bool is_negative() const { return !is_positive(); }
/** Evaluate the constraint under the empty assignment */
lbool eval() const { return is_positive() ? get()->eval() : ~get()->eval(); }
/** Evaluate the constraint under the given assignment */
lbool eval(assignment const& a) const { return is_positive() ? get()->eval(a) : ~get()->eval(a); }
/** Evaluate the constraint under the solver's current assignment */
lbool eval(solver const& s) const { return is_positive() ? get()->eval(s) : ~get()->eval(s); }
bool is_always_false() const { return get()->is_always_false(is_positive()); }
bool is_always_true() const { return get()->is_always_false(is_negative()); }
bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
bool is_currently_true(solver& s) const { return get()->is_currently_false(s, is_negative()); }
bool is_always_true() const { return get()->is_always_true(is_positive()); }
bool is_currently_false(assignment const& a) const { return get()->is_currently_false(a, is_positive()); }
bool is_currently_true(assignment const& a) const { return get()->is_currently_false(a, is_negative()); }
bool is_currently_true(assignment const& a) const { return get()->is_currently_true(a, is_positive()); }
bool is_currently_false(solver const& s) const { return get()->is_currently_false(s, is_positive()); }
bool is_currently_true(solver const& s) const { return get()->is_currently_true(s, is_positive()); }
lbool bvalue(solver& s) const;
void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
inequality as_inequality() const { return get()->as_inequality(is_positive()); }

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

@ -51,6 +51,14 @@ namespace polysat {
SASSERT(c != code::not_op);
}
lbool op_constraint::eval() const {
return eval(p(), q(), r());
}
lbool op_constraint::eval(assignment const& a) const {
return eval(a.apply_to(p()), a.apply_to(q()), a.apply_to(r()));
}
lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
switch (m_op) {
case code::lshr_op:
@ -64,26 +72,6 @@ namespace polysat {
}
}
bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
switch (eval(p, q, r)) {
case l_true: return !is_positive;
case l_false: return is_positive;
default: return false;
}
}
bool op_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
return is_always_false(!is_positive, p, q, r);
}
bool op_constraint::is_always_false(bool is_positive) const {
return is_always_false(is_positive, p(), q(), r());
}
bool op_constraint::is_currently_false(assignment const& a, bool is_positive) const {
return is_always_false(is_positive, a.apply_to(p()), a.apply_to(q()), a.apply_to(r()));
}
std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
switch (status) {
case l_true: return display(out);
@ -399,4 +387,5 @@ namespace polysat {
break;
}
}
}

7
src/math/polysat/op_constraint.h
View file

@ -38,9 +38,6 @@ namespace polysat {
pdd m_r;
op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
void simplify() {}
bool is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
bool is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
void narrow_lshr(solver& s);
@ -59,8 +56,8 @@ namespace polysat {
pdd const& r() const { return m_r; }
std::ostream& display(std::ostream& out, lbool status) const override;
std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive) const override;
bool is_currently_false(assignment const& a, bool is_positive) const override;
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
unsigned hash() const override;

14
src/math/polysat/smul_fl_constraint.cpp
View file

@ -40,7 +40,7 @@ namespace polysat {
case l_true: return display(out);
case l_false: return display(out << "~");
case l_undef: return display(out << "?");
}
}
return out;
}
@ -48,12 +48,12 @@ namespace polysat {
if (m_is_overflow)
return out << "sovfl*(" << m_p << ", " << m_q << ")";
else
return out << "sudfl*(" << m_p << ", " << m_q << ")";
return out << "sudfl*(" << m_p << ", " << m_q << ")";
}
/**
* TODO - verify the rules for small bit-widths.
*
*
* sovfl(p,q) => p >= 2, q >= 2
* sovfl(p,q) => p >s 0 <=> q >s 0
* sovfl(p,q) & p >s 0 => p*q < 0 or ovfl(p,q)
@ -67,8 +67,8 @@ namespace polysat {
* sudfl(p, q) & p >s 0 => p*q > 0 or ovfl(p, -q)
* sudfl(p, q) & q >s 0 => p*q > 0 or ovfl(-p, q)
*
* ~sudfl(p, q) & p >s 0 & q <s 0 => ~ovfl(p, -q) & p*q <s 0
* ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0
* ~sudfl(p, q) & p >s 0 & q <s 0 => ~ovfl(p, -q) & p*q <s 0
* ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0
*/
void smul_fl_constraint::narrow(solver& s, bool is_positive, bool first) {
if (!first)
@ -103,8 +103,8 @@ namespace polysat {
s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.umul_ovfl(p(), -q()), false);
s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false);
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.umul_ovfl(-p(), q()), false);
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);
}
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);
}
}
}

6
src/math/polysat/smul_fl_constraint.h
View file

@ -26,7 +26,7 @@ namespace polysat {
void simplify();
smul_fl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow);
public:
~smul_fl_constraint() override {}
bool is_overflow() const { return m_is_overflow; }
@ -34,9 +34,9 @@ namespace polysat {
pdd const& q() const { return m_q; }
std::ostream& display(std::ostream& out, lbool status) const override;
std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive) const override { return false; }
lbool eval() const override { return l_undef; } // TODO
lbool eval(assignment const& a) const override { return l_undef; } // TODO
void narrow(solver& s, bool is_positive, bool first) override;
bool is_currently_false(assignment const& a, bool is_positive) const override { return false; }
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
unsigned hash() const override;

48
src/math/polysat/ule_constraint.cpp
View file

@ -189,36 +189,30 @@ namespace polysat {
s.m_viable.intersect(p, q, sc);
}
bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) {
// Evaluate lhs <= rhs
lbool ule_constraint::eval(pdd const& lhs, pdd const& rhs) {
// NOTE: don't assume simplifications here because we also call this on partially substituted constraints
if (is_positive) {
// lhs <= rhs
if (rhs.is_zero())
return lhs.is_never_zero(); // p <= 0 implies p == 0
return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val();
}
else {
// lhs > rhs
if (lhs.is_zero())
return true; // 0 > ... is always false
if (lhs == rhs)
return true; // p > p
if (rhs.is_max())
return true; // p > -1
if (lhs.is_one() && rhs.is_never_zero())
return true; // 1 > p implies p == 0
return lhs.is_val() && rhs.is_val() && lhs.val() <= rhs.val();
}
if (lhs.is_zero())
return l_true; // 0 <= p
if (lhs == rhs)
return l_true; // p <= p
if (rhs.is_max())
return l_true; // p <= -1
if (rhs.is_zero() && lhs.is_never_zero())
return l_false; // p <= 0 implies p == 0
if (lhs.is_one() && rhs.is_never_zero())
return l_true; // 1 <= p implies p != 0
if (lhs.is_val() && rhs.is_val())
return to_lbool(lhs.val() <= rhs.val());
return l_undef;
}
lbool ule_constraint::eval() const {
return eval(lhs(), rhs());
}
bool ule_constraint::is_always_false(bool is_positive) const {
return is_always_false(is_positive, lhs(), rhs());
}
bool ule_constraint::is_currently_false(assignment const& a, bool is_positive) const {
auto p = a.apply_to(lhs());
auto q = a.apply_to(rhs());
return is_always_false(is_positive, p, q);
lbool ule_constraint::eval(assignment const& a) const {
return eval(a.apply_to(lhs()), a.apply_to(rhs()));
}
inequality ule_constraint::as_inequality(bool is_positive) const {

8
src/math/polysat/ule_constraint.h
View file

@ -27,7 +27,9 @@ namespace polysat {
ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); }
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); }
static lbool eval(pdd const& lhs, pdd const& rhs);
public:
~ule_constraint() override {}
@ -36,8 +38,8 @@ namespace polysat {
static std::ostream& display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs);
std::ostream& display(std::ostream& out, lbool status) const override;
std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive) const override;
bool is_currently_false(assignment const& a, bool is_positive) const override;
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;

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

@ -40,15 +40,15 @@ namespace polysat {
case l_true: return display(out);
case l_false: return display(out << "~");
case l_undef: return display(out << "?");
}
}
return out;
}
std::ostream& umul_ovfl_constraint::display(std::ostream& out) const {
return out << "ovfl*(" << m_p << ", " << m_q << ")";
return out << "ovfl*(" << m_p << ", " << m_q << ")";
}
lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) const {
lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) {
if (p.is_zero() || q.is_zero() || p.is_one() || q.is_one())
return l_false;
@ -61,30 +61,18 @@ namespace polysat {
return l_undef;
}
bool umul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const {
switch (eval(p, q)) {
case l_true: return !is_positive;
case l_false: return is_positive;
default: return false;
}
lbool umul_ovfl_constraint::eval() const {
return eval(p(), q());
}
bool umul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const {
return is_always_false(!is_positive, p, q);
lbool umul_ovfl_constraint::eval(assignment const& a) const {
return eval(a.apply_to(p()), a.apply_to(q()));
}
bool umul_ovfl_constraint::is_always_false(bool is_positive) const {
return is_always_false(is_positive, m_p, m_q);
}
bool umul_ovfl_constraint::is_currently_false(assignment const& a, bool is_positive) const {
return is_always_false(is_positive, a.apply_to(p()), a.apply_to(q()));
}
void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {
void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {
auto p1 = s.subst(p());
auto q1 = s.subst(q());
if (is_always_false(is_positive, p1, q1)) {
s.set_conflict({ this, is_positive });
return;
@ -94,19 +82,19 @@ namespace polysat {
if (try_viable(s, is_positive, p(), q(), p1, q1))
return;
if (narrow_bound(s, is_positive, p(), q(), p1, q1))
return;
if (narrow_bound(s, is_positive, q(), p(), q1, p1))
return;
}
/**
* if p constant, q, propagate inequality
*/
bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive,
* if p constant, q, propagate inequality
*/
bool umul_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())
@ -118,13 +106,13 @@ namespace polysat {
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
//
// Ovfl(p, q) & p <= p.val() => q >= bound
// ~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 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);

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

@ -25,21 +25,21 @@ namespace polysat {
umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q);
void simplify();
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;
static bool is_always_true(bool is_positive, pdd const& p, pdd const& q) { return eval(p, q) == to_lbool(is_positive); }
static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
static lbool eval(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);
bool try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
lbool eval(pdd const& p, pdd const& q) const;
public:
~umul_ovfl_constraint() override {}
pdd const& p() const { return m_p; }
pdd const& q() const { return m_q; }
std::ostream& display(std::ostream& out, lbool status) const override;
std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive) const override;
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
bool is_currently_false(assignment const& a, bool is_positive) const override;
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
unsigned hash() const override;