diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index d22254d65..c1f65969c 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -9,6 +9,15 @@ Author: Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09 +Notes: + +Additional possible functionality on constraints: + +- activate - when operation is first activated. It may be created and only activated later. +- bit-wise assignments - narrow based on bit assignment, not entire word assignment. +- integration with congruence tables +- integration with conflict resolution + --*/ #include "math/polysat/op_constraint.h" @@ -51,7 +60,19 @@ namespace polysat { default: return false; } } - + + 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_t const& a, bool is_positive) const { + return is_always_false(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a)); + } + + bool op_constraint::is_currently_true(assignment_t const& a, bool is_positive) const { + return is_always_true(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a)); + } + std::ostream& op_constraint::display(std::ostream& out, lbool status) const { switch (status) { case l_true: return display(out); @@ -60,7 +81,7 @@ namespace polysat { } } - std::ostream& operator<<(std::ostream & out, op_constraint::code c) { + std::ostream& operator<<(std::ostream& out, op_constraint::code c) { switch (c) { case op_constraint::code::ashr_op: return out << ">>a"; @@ -75,29 +96,31 @@ namespace polysat { case op_constraint::code::xor_op: return out << "^"; default: - return out << "?"; + UNREACHABLE(); + return out; } return out; } std::ostream& op_constraint::display(std::ostream& out) const { - return out << r() << " " << m_op << " " << p() << " << " << q(); + if (m_op == code::not_op) + return out << r() << " == ~" << p(); + else + return out << r() << " == " << p() << " " << m_op << " " << q(); } - 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_t const& a, bool is_positive) const { - return is_always_false(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a)); - } - - bool op_constraint::is_currently_true(assignment_t const& a, bool is_positive) const { - return is_always_true(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a)); - } + /** + * Propagate consequences or detect conflicts based on partial assignments. + * + * We can assume that op_constraint is only asserted positive. + */ void op_constraint::narrow(solver& s, bool is_positive) { SASSERT(is_positive); + + if (is_currently_true(s.assignment(), is_positive)) + return; + switch (m_op) { case code::lshr_op: narrow_lshr(s); @@ -106,6 +129,10 @@ namespace polysat { NOT_IMPLEMENTED_YET(); break; } + if (!s.is_conflict() && is_currently_false(s.assignment(), is_positive)) { + s.set_conflict(signed_constraint(this, is_positive)); + return; + } } unsigned op_constraint::hash() const { @@ -120,38 +147,61 @@ namespace polysat { } /** - * Enforce basic axioms, such as: + * Enforce basic axioms for r == p >> q, such as: * - * r = p >> q & q >= k -> r[i] = 0 for i > K - k - * r = p >> q & q >= K -> r = 0 - * r = p >> q & q = k -> r[i] = p[i+k] for k + i < K - * r = p >> q & q >= k -> r <= 2^{K-k-1} - * r = p >> q => r <= p - * r = p >> q & q != 0 => r < p - * r = p >> q & q = 0 => r = p + * q >= k -> r[i] = 0 for i > K - k + * q >= K -> r = 0 + * q = k -> r[i] = p[i+k] for k + i < K + * q >= k -> r <= 2^{K-k-1} + * r <= p + * q != 0 => r <= p + * q = 0 => r = p * * when q is a constant, several axioms can be enforced at activation time. * * Enforce also inferences and bounds * - * We can assume that op_constraint is only asserted positive. */ void op_constraint::narrow_lshr(solver& s) { + auto pv = p().subst_val(s.assignment()); + auto qv = q().subst_val(s.assignment()); + auto rv = r().subst_val(s.assignment()); + unsigned K = p().manager().power_of_2(); + signed_constraint lshl(this, true); + // r <= p + if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) { + s.add_clause(~lshl, s.ule(r(), p()), true); + return; + } + // q >= K -> r = 0 + if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) { + s.add_clause(~lshl, ~s.ule(K, q()), s.eq(r()), true); + return; + } + // q = 0 => r = p + if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv) { + s.add_clause(~lshl, ~s.eq(q()), s.eq(p(), r()), true); + return; + } + // q != 0 & p > 0 => r < p + if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && pv <= rv) { + s.add_clause(~lshl, s.eq(q()), s.ule(p, 0), s.ult(r(), p()), true); + return; + } NOT_IMPLEMENTED_YET(); } lbool op_constraint::eval_lshr(pdd const& p, pdd const& q, pdd const& r) const { - if (q.is_val() && r.is_val()) { - auto& m = p.manager(); - if (q.val() >= m.power_of_2()) - return r.is_zero() ? l_true : l_false; - if (p.is_val()) { - pdd rr = p * m.mk_val(rational::power_of_two(q.val().get_unsigned())); - return rr == r ? l_true : l_false; - } - // other cases when we know lower - // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant. - } + auto& m = p.manager(); + + if (p.is_val() && q.is_val() && r.is_val()) + return r == p * m.mk_val(rational::power_of_two(q.val().get_unsigned())) ? l_true : l_false; + + if (q.is_val() && q.val() >= m.power_of_2() && r.is_val()) + return r.is_zero() ? l_true : l_false; + + // other cases when we know lower + // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant. return l_undef; } } diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h index 265fda5f6..58ad50600 100644 --- a/src/math/polysat/op_constraint.h +++ b/src/math/polysat/op_constraint.h @@ -6,11 +6,11 @@ Module Name: Op constraint. lshr: r == p >> q - ashr: r == p >> q + ashr: r == p >>a q lshl: r == p << q and: r == p & q or: r == p | q - neg: r == ~p + not: r == ~p xor: r == p ^ q Author: diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 1a9b020b6..3c6cd2118 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -793,6 +793,34 @@ namespace polysat { add_clause(*clause); } + void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) { + clause_builder cb(*this); + if (!c1.is_always_false()) + cb.push(c1); + if (!c2.is_always_false()) + cb.push(c2); + if (!c3.is_always_false()) + cb.push(c3); + clause_ref clause = cb.build(); + clause->set_redundant(is_redundant); + add_clause(*clause); + } + + void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant) { + clause_builder cb(*this); + if (!c1.is_always_false()) + cb.push(c1); + if (!c2.is_always_false()) + cb.push(c2); + if (!c3.is_always_false()) + cb.push(c3); + if (!c4.is_always_false()) + cb.push(c4); + clause_ref clause = cb.build(); + clause->set_redundant(is_redundant); + add_clause(*clause); + } + void solver::insert_constraint(signed_constraints& cs, signed_constraint c) { SASSERT(c); LOG_V("INSERTING: " << c); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index c4ea836ad..19fa5b341 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -56,6 +56,7 @@ namespace polysat { friend class constraint; friend class ule_constraint; friend class mul_ovfl_constraint; + friend class op_constraint; friend class signed_constraint; friend class clause; friend class clause_builder; @@ -207,6 +208,8 @@ namespace polysat { void backjump(unsigned new_level); void add_clause(clause& lemma); void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant); + void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant); + void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant); signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }