mirror of
https://github.com/Z3Prover/z3
synced 2025-04-25 01:55:32 +00:00
forbidden interval update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
e6c4ae19c6
commit
a6643955e6
7 changed files with 192 additions and 242 deletions
|
|
@ -167,14 +167,8 @@ namespace polysat {
|
|||
void set_unit_clause(clause* cl);
|
||||
p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
|
||||
|
||||
/** Precondition: all variables other than v are assigned.
|
||||
*
|
||||
* \param[out] out_interval The forbidden interval for this constraint
|
||||
* \param[out] out_neg_cond Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant.
|
||||
* \returns True iff a forbidden interval exists and the output parameters were set.
|
||||
*/
|
||||
// TODO: we can probably remove this and unify the implementations for both cases by relying on as_inequality().
|
||||
virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) { return false; }
|
||||
|
||||
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
|
||||
|
|
|
|||
|
|
@ -120,66 +120,6 @@ namespace polysat {
|
|||
// }
|
||||
|
||||
|
||||
/// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality)
|
||||
bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
|
||||
{
|
||||
// Current only works when degree(v) is at most one
|
||||
unsigned const deg = p().degree(v);
|
||||
if (deg > 1)
|
||||
return false;
|
||||
|
||||
if (deg == 0) {
|
||||
return false;
|
||||
UNREACHABLE(); // this case is not useful for conflict resolution (but it could be handled in principle)
|
||||
// i is empty or full, condition would be this constraint itself?
|
||||
return true;
|
||||
}
|
||||
|
||||
unsigned const sz = s.size(v);
|
||||
dd::pdd_manager& m = s.sz2pdd(sz);
|
||||
|
||||
pdd p1 = m.zero();
|
||||
pdd e1 = m.zero();
|
||||
p().factor(v, 1, p1, e1);
|
||||
|
||||
pdd e2 = m.zero();
|
||||
|
||||
// Currently only works if coefficient is a power of two
|
||||
if (!p1.is_val())
|
||||
return false;
|
||||
rational a1 = p1.val();
|
||||
// TODO: to express the interval for coefficient 2^i symbolically, we need right-shift/upper-bits-extract in the language.
|
||||
// So currently we can only do it if the coefficient is 1.
|
||||
if (!a1.is_zero() && !a1.is_one())
|
||||
return false;
|
||||
/*
|
||||
unsigned j1 = 0;
|
||||
if (!a1.is_zero() && !a1.is_power_of_two(j1))
|
||||
return false;
|
||||
*/
|
||||
|
||||
// Concrete values of evaluable terms
|
||||
auto e1s = e1.subst_val(s.assignment());
|
||||
if (!e1s.is_val())
|
||||
return false;
|
||||
SASSERT(e1s.is_val());
|
||||
|
||||
// e1 + t <= 0, with t = 2^j1*y
|
||||
// condition for empty/full: 0 == -1, never satisfied, so we always have a proper interval!
|
||||
SASSERT(!a1.is_zero());
|
||||
pdd lo = 1 - e1;
|
||||
rational lo_val = (1 - e1s).val();
|
||||
pdd hi = -e1;
|
||||
rational hi_val = (-e1s).val();
|
||||
if (!is_positive) {
|
||||
swap(lo, hi);
|
||||
lo_val.swap(hi_val);
|
||||
}
|
||||
out_interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
out_neg_cond = nullptr;
|
||||
return true;
|
||||
}
|
||||
|
||||
inequality eq_constraint::as_inequality(bool is_positive) const {
|
||||
pdd zero = p() - p();
|
||||
if (is_positive)
|
||||
|
|
|
|||
|
|
@ -35,7 +35,6 @@ namespace polysat {
|
|||
bool is_currently_false(solver& s, bool is_positive) override;
|
||||
bool is_currently_true(solver& s, bool is_positive) override;
|
||||
void narrow(solver& s, bool is_positive) override;
|
||||
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) override;
|
||||
inequality as_inequality(bool is_positive) const override;
|
||||
unsigned hash() const override;
|
||||
bool operator==(constraint const& other) const override;
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ namespace polysat {
|
|||
LOG_H3("Computing forbidden interval for: " << c);
|
||||
eval_interval interval = eval_interval::full();
|
||||
signed_constraint neg_cond;
|
||||
if (c->forbidden_interval(s, c.is_positive(), v, interval, neg_cond)) {
|
||||
if (get_interval(s, c, v, interval, neg_cond)) {
|
||||
LOG("interval: " << interval);
|
||||
LOG("neg_cond: " << neg_cond);
|
||||
if (interval.is_currently_empty())
|
||||
|
|
@ -173,4 +173,192 @@ namespace polysat {
|
|||
return true;
|
||||
}
|
||||
|
||||
|
||||
// TODO:
|
||||
// review translation from is_positive to ineq.strict
|
||||
|
||||
/** Precondition: all variables other than v are assigned.
|
||||
*
|
||||
* \param[out] out_interval The forbidden interval for this constraint
|
||||
* \param[out] out_neg_cond Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant.
|
||||
* \returns True iff a forbidden interval exists and the output parameters were set.
|
||||
*/
|
||||
|
||||
bool forbidden_intervals::get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
|
||||
{
|
||||
inequality ineq = c.as_inequality();
|
||||
// Current only works when degree(v) is at most one on both sides
|
||||
pdd lhs = ineq.lhs;
|
||||
pdd rhs = ineq.rhs;
|
||||
if (ineq.is_strict)
|
||||
swap(lhs, rhs);
|
||||
unsigned const deg1 = lhs.degree(v);
|
||||
unsigned const deg2 = rhs.degree(v);
|
||||
if (deg1 > 1 || deg2 > 1)
|
||||
return false;
|
||||
|
||||
if (deg1 == 0 && deg2 == 0) {
|
||||
return false;
|
||||
UNREACHABLE(); // this case is not useful for conflict resolution (but it could be handled in principle)
|
||||
// i is empty or full, condition would be this constraint itself?
|
||||
return true;
|
||||
}
|
||||
|
||||
unsigned const sz = s.size(v);
|
||||
dd::pdd_manager& m = s.sz2pdd(sz);
|
||||
rational const pow2 = rational::power_of_two(sz);
|
||||
rational const minus_one = pow2 - 1;
|
||||
|
||||
pdd p1 = m.zero();
|
||||
pdd e1 = m.zero();
|
||||
if (deg1 == 0)
|
||||
e1 = lhs;
|
||||
else
|
||||
lhs.factor(v, 1, p1, e1);
|
||||
|
||||
pdd p2 = m.zero();
|
||||
pdd e2 = m.zero();
|
||||
if (deg2 == 0)
|
||||
e2 = rhs;
|
||||
else
|
||||
rhs.factor(v, 1, p2, e2);
|
||||
|
||||
// Interval extraction only works if v-coefficients are the same
|
||||
if (deg1 != 0 && deg2 != 0 && p1 != p2)
|
||||
return false;
|
||||
|
||||
// Currently only works if coefficient is a power of two
|
||||
if (!p1.is_val())
|
||||
return false;
|
||||
if (!p2.is_val())
|
||||
return false;
|
||||
rational a1 = p1.val();
|
||||
rational a2 = p2.val();
|
||||
// TODO: to express the interval for coefficient 2^i symbolically, we need right-shift/upper-bits-extract in the language.
|
||||
// So currently we can only do it if the coefficient is 1 or -1.
|
||||
if (!a1.is_zero() && !a1.is_one() && a1 != minus_one)
|
||||
return false;
|
||||
if (!a2.is_zero() && !a2.is_one() && a2 != minus_one)
|
||||
return false;
|
||||
/*
|
||||
unsigned j1 = 0;
|
||||
unsigned j2 = 0;
|
||||
if (!a1.is_zero() && !a1.is_power_of_two(j1))
|
||||
return false;
|
||||
if (!a2.is_zero() && !a2.is_power_of_two(j2))
|
||||
return false;
|
||||
*/
|
||||
|
||||
rational const y_coeff = a1.is_zero() ? a2 : a1;
|
||||
SASSERT(!y_coeff.is_zero());
|
||||
|
||||
// Concrete values of evaluable terms
|
||||
auto e1s = e1.subst_val(s.assignment());
|
||||
auto e2s = e2.subst_val(s.assignment());
|
||||
// TODO: this is not always true! cjust[v]/conflict may contain unassigned variables (they're coming from a previous conflict, but together they lead to a conflict. need something else to handle that.)
|
||||
if (!e1s.is_val())
|
||||
return false;
|
||||
if (!e2s.is_val())
|
||||
return false;
|
||||
SASSERT(e1s.is_val());
|
||||
SASSERT(e2s.is_val());
|
||||
|
||||
bool is_trivial;
|
||||
pdd condition_body = m.zero();
|
||||
pdd lo = m.zero();
|
||||
rational lo_val = rational::zero();
|
||||
pdd hi = m.zero();
|
||||
rational hi_val = rational::zero();
|
||||
|
||||
if (a2.is_zero()) {
|
||||
SASSERT(!a1.is_zero());
|
||||
// e1 + t <= e2, with t = 2^j1*y
|
||||
// condition for empty/full: e2 == -1
|
||||
is_trivial = (e2s + 1).is_zero();
|
||||
condition_body = e2 + 1;
|
||||
if (!is_trivial) {
|
||||
lo = e2 - e1 + 1;
|
||||
lo_val = (e2s - e1s + 1).val();
|
||||
hi = -e1;
|
||||
hi_val = (-e1s).val();
|
||||
}
|
||||
}
|
||||
else if (a1.is_zero()) {
|
||||
SASSERT(!a2.is_zero());
|
||||
// e1 <= e2 + t, with t = 2^j2*y
|
||||
// condition for empty/full: e1 == 0
|
||||
is_trivial = e1s.is_zero();
|
||||
condition_body = e1;
|
||||
if (!is_trivial) {
|
||||
lo = -e2;
|
||||
lo_val = (-e2s).val();
|
||||
hi = e1 - e2;
|
||||
hi_val = (e1s - e2s).val();
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(!a1.is_zero());
|
||||
SASSERT(!a2.is_zero());
|
||||
SASSERT_EQ(a1, a2);
|
||||
// e1 + t <= e2 + t, with t = 2^j1*y = 2^j2*y
|
||||
// condition for empty/full: e1 == e2
|
||||
is_trivial = e1s.val() == e2s.val();
|
||||
condition_body = e1 - e2;
|
||||
if (!is_trivial) {
|
||||
lo = -e2;
|
||||
lo_val = (-e2s).val();
|
||||
hi = -e1;
|
||||
hi_val = (-e1s).val();
|
||||
}
|
||||
}
|
||||
|
||||
if (condition_body.is_val()) {
|
||||
// Condition is trivial; no need to create a constraint for that.
|
||||
SASSERT(is_trivial == condition_body.is_zero());
|
||||
out_neg_cond = nullptr;
|
||||
}
|
||||
else if (is_trivial)
|
||||
out_neg_cond = ~s.m_constraints.eq(0, condition_body);
|
||||
else
|
||||
out_neg_cond = s.m_constraints.eq(0, condition_body);
|
||||
|
||||
if (is_trivial) {
|
||||
if (!ineq.is_strict)
|
||||
// TODO: we cannot use empty intervals for interpolation. So we
|
||||
// can remove the empty case (make it represent 'full' instead),
|
||||
// and return 'false' here. Then we do not need the proper/full
|
||||
// tag on intervals.
|
||||
out_interval = eval_interval::empty(m);
|
||||
else
|
||||
out_interval = eval_interval::full();
|
||||
}
|
||||
else {
|
||||
if (y_coeff == minus_one) {
|
||||
// Transform according to: y \in [l;u[ <=> -y \in [1-u;1-l[
|
||||
// -y \in [1-u;1-l[
|
||||
// <=> -y - (1 - u) < (1 - l) - (1 - u) { by: y \in [l;u[ <=> y - l < u - l }
|
||||
// <=> u - y - 1 < u - l { simplified }
|
||||
// <=> (u-l) - (u-y-1) - 1 < u-l { by: a < b <=> b - a - 1 < b }
|
||||
// <=> y - l < u - l { simplified }
|
||||
// <=> y \in [l;u[.
|
||||
lo = 1 - lo;
|
||||
hi = 1 - hi;
|
||||
swap(lo, hi);
|
||||
lo_val = mod(1 - lo_val, pow2);
|
||||
hi_val = mod(1 - hi_val, pow2);
|
||||
lo_val.swap(hi_val);
|
||||
}
|
||||
else
|
||||
SASSERT(y_coeff.is_one());
|
||||
|
||||
if (ineq.is_strict) {
|
||||
swap(lo, hi);
|
||||
lo_val.swap(hi_val);
|
||||
}
|
||||
out_interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ namespace polysat {
|
|||
|
||||
class forbidden_intervals : public variable_elimination_engine {
|
||||
void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, conflict_core& core);
|
||||
bool get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond);
|
||||
public:
|
||||
bool perform(solver& s, pvar v, conflict_core& core) override;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -113,177 +113,6 @@ namespace polysat {
|
|||
return p.is_val() && q.is_val() && p.val() > q.val();
|
||||
}
|
||||
|
||||
bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
|
||||
{
|
||||
// Current only works when degree(v) is at most one on both sides
|
||||
unsigned const deg1 = lhs().degree(v);
|
||||
unsigned const deg2 = rhs().degree(v);
|
||||
if (deg1 > 1 || deg2 > 1)
|
||||
return false;
|
||||
|
||||
if (deg1 == 0 && deg2 == 0) {
|
||||
return false;
|
||||
UNREACHABLE(); // this case is not useful for conflict resolution (but it could be handled in principle)
|
||||
// i is empty or full, condition would be this constraint itself?
|
||||
return true;
|
||||
}
|
||||
|
||||
unsigned const sz = s.size(v);
|
||||
dd::pdd_manager& m = s.sz2pdd(sz);
|
||||
rational const pow2 = rational::power_of_two(sz);
|
||||
rational const minus_one = pow2 - 1;
|
||||
|
||||
pdd p1 = m.zero();
|
||||
pdd e1 = m.zero();
|
||||
if (deg1 == 0)
|
||||
e1 = lhs();
|
||||
else
|
||||
lhs().factor(v, 1, p1, e1);
|
||||
|
||||
pdd p2 = m.zero();
|
||||
pdd e2 = m.zero();
|
||||
if (deg2 == 0)
|
||||
e2 = rhs();
|
||||
else
|
||||
rhs().factor(v, 1, p2, e2);
|
||||
|
||||
// Interval extraction only works if v-coefficients are the same
|
||||
if (deg1 != 0 && deg2 != 0 && p1 != p2)
|
||||
return false;
|
||||
|
||||
// Currently only works if coefficient is a power of two
|
||||
if (!p1.is_val())
|
||||
return false;
|
||||
if (!p2.is_val())
|
||||
return false;
|
||||
rational a1 = p1.val();
|
||||
rational a2 = p2.val();
|
||||
// TODO: to express the interval for coefficient 2^i symbolically, we need right-shift/upper-bits-extract in the language.
|
||||
// So currently we can only do it if the coefficient is 1 or -1.
|
||||
if (!a1.is_zero() && !a1.is_one() && a1 != minus_one)
|
||||
return false;
|
||||
if (!a2.is_zero() && !a2.is_one() && a2 != minus_one)
|
||||
return false;
|
||||
/*
|
||||
unsigned j1 = 0;
|
||||
unsigned j2 = 0;
|
||||
if (!a1.is_zero() && !a1.is_power_of_two(j1))
|
||||
return false;
|
||||
if (!a2.is_zero() && !a2.is_power_of_two(j2))
|
||||
return false;
|
||||
*/
|
||||
|
||||
rational const y_coeff = a1.is_zero() ? a2 : a1;
|
||||
SASSERT(!y_coeff.is_zero());
|
||||
|
||||
// Concrete values of evaluable terms
|
||||
auto e1s = e1.subst_val(s.assignment());
|
||||
auto e2s = e2.subst_val(s.assignment());
|
||||
// TODO: this is not always true! cjust[v]/conflict may contain unassigned variables (they're coming from a previous conflict, but together they lead to a conflict. need something else to handle that.)
|
||||
if (!e1s.is_val())
|
||||
return false;
|
||||
if (!e2s.is_val())
|
||||
return false;
|
||||
SASSERT(e1s.is_val());
|
||||
SASSERT(e2s.is_val());
|
||||
|
||||
bool is_trivial;
|
||||
pdd condition_body = m.zero();
|
||||
pdd lo = m.zero();
|
||||
rational lo_val = rational::zero();
|
||||
pdd hi = m.zero();
|
||||
rational hi_val = rational::zero();
|
||||
|
||||
if (a2.is_zero()) {
|
||||
SASSERT(!a1.is_zero());
|
||||
// e1 + t <= e2, with t = 2^j1*y
|
||||
// condition for empty/full: e2 == -1
|
||||
is_trivial = (e2s + 1).is_zero();
|
||||
condition_body = e2 + 1;
|
||||
if (!is_trivial) {
|
||||
lo = e2 - e1 + 1;
|
||||
lo_val = (e2s - e1s + 1).val();
|
||||
hi = -e1;
|
||||
hi_val = (-e1s).val();
|
||||
}
|
||||
}
|
||||
else if (a1.is_zero()) {
|
||||
SASSERT(!a2.is_zero());
|
||||
// e1 <= e2 + t, with t = 2^j2*y
|
||||
// condition for empty/full: e1 == 0
|
||||
is_trivial = e1s.is_zero();
|
||||
condition_body = e1;
|
||||
if (!is_trivial) {
|
||||
lo = -e2;
|
||||
lo_val = (-e2s).val();
|
||||
hi = e1 - e2;
|
||||
hi_val = (e1s - e2s).val();
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(!a1.is_zero());
|
||||
SASSERT(!a2.is_zero());
|
||||
SASSERT_EQ(a1, a2);
|
||||
// e1 + t <= e2 + t, with t = 2^j1*y = 2^j2*y
|
||||
// condition for empty/full: e1 == e2
|
||||
is_trivial = e1s.val() == e2s.val();
|
||||
condition_body = e1 - e2;
|
||||
if (!is_trivial) {
|
||||
lo = -e2;
|
||||
lo_val = (-e2s).val();
|
||||
hi = -e1;
|
||||
hi_val = (-e1s).val();
|
||||
}
|
||||
}
|
||||
|
||||
if (condition_body.is_val()) {
|
||||
// Condition is trivial; no need to create a constraint for that.
|
||||
SASSERT(is_trivial == condition_body.is_zero());
|
||||
out_neg_cond = nullptr;
|
||||
}
|
||||
else if (is_trivial)
|
||||
out_neg_cond = ~s.m_constraints.eq(level(), condition_body);
|
||||
else
|
||||
out_neg_cond = s.m_constraints.eq(level(), condition_body);
|
||||
|
||||
if (is_trivial) {
|
||||
if (is_positive)
|
||||
// TODO: we cannot use empty intervals for interpolation. So we
|
||||
// can remove the empty case (make it represent 'full' instead),
|
||||
// and return 'false' here. Then we do not need the proper/full
|
||||
// tag on intervals.
|
||||
out_interval = eval_interval::empty(m);
|
||||
else
|
||||
out_interval = eval_interval::full();
|
||||
} else {
|
||||
if (y_coeff == minus_one) {
|
||||
// Transform according to: y \in [l;u[ <=> -y \in [1-u;1-l[
|
||||
// -y \in [1-u;1-l[
|
||||
// <=> -y - (1 - u) < (1 - l) - (1 - u) { by: y \in [l;u[ <=> y - l < u - l }
|
||||
// <=> u - y - 1 < u - l { simplified }
|
||||
// <=> (u-l) - (u-y-1) - 1 < u-l { by: a < b <=> b - a - 1 < b }
|
||||
// <=> y - l < u - l { simplified }
|
||||
// <=> y \in [l;u[.
|
||||
lo = 1 - lo;
|
||||
hi = 1 - hi;
|
||||
swap(lo, hi);
|
||||
lo_val = mod(1 - lo_val, pow2);
|
||||
hi_val = mod(1 - hi_val, pow2);
|
||||
lo_val.swap(hi_val);
|
||||
}
|
||||
else
|
||||
SASSERT(y_coeff.is_one());
|
||||
|
||||
if (!is_positive) {
|
||||
swap(lo, hi);
|
||||
lo_val.swap(hi_val);
|
||||
}
|
||||
out_interval = eval_interval::proper(lo, lo_val, hi, hi_val);
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
inequality ule_constraint::as_inequality(bool is_positive) const {
|
||||
if (is_positive)
|
||||
return inequality(lhs(), rhs(), false, this);
|
||||
|
|
|
|||
|
|
@ -41,7 +41,6 @@ namespace polysat {
|
|||
bool is_currently_false(solver& s, bool is_positive) override;
|
||||
bool is_currently_true(solver& s, bool is_positive) override;
|
||||
void narrow(solver& s, bool is_positive) override;
|
||||
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) override;
|
||||
inequality as_inequality(bool is_positive) const override;
|
||||
unsigned hash() const override;
|
||||
bool operator==(constraint const& other) const override;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue