diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index 55241f878..7a9e46a09 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -78,13 +78,13 @@ namespace polysat { SASSERT(is_propagation(lit)); } - void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dep_t dep) { + void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dependency dep) { LOG("Asserted " << lit << " @ " << lvl); assign(kind_t::decision, lit, lvl, nullptr, dep); SASSERT(is_decision(lit)); } - void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep) { + void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) { SASSERT(!is_assigned(lit)); SASSERT(k != kind_t::unassigned); m_value[lit.index()] = l_true; diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index 405722c43..2ef826779 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -29,7 +29,7 @@ namespace polysat { svector m_unused; // previously deleted variables that can be reused by new_var(); svector m_value; // current value (indexed by literal) unsigned_vector m_level; // level of assignment (indexed by variable) - svector m_deps; // dependencies of external asserts + dependency_vector m_deps; // dependencies of external asserts unsigned_vector m_activity; // svector m_kind; // decision or propagation? // Clause associated with the assignment (indexed by variable): @@ -40,7 +40,7 @@ namespace polysat { var_queue m_free_vars; // free Boolean variables vector> m_watch; // watch list for literals into clauses - void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep = null_dependency); + void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep = null_dependency); public: @@ -66,7 +66,7 @@ namespace polysat { unsigned level(sat::literal lit) const { return level(lit.var()); } clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; } clause* reason(sat::literal lit) const { return reason(lit.var()); } - dep_t dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; } + dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; } clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; } @@ -83,7 +83,7 @@ namespace polysat { void propagate(sat::literal lit, unsigned lvl, clause& reason); void decide(sat::literal lit, unsigned lvl, clause& lemma); void eval(sat::literal lit, unsigned lvl); - void asserted(sat::literal lit, unsigned lvl, dep_t dep); + void asserted(sat::literal lit, unsigned lvl, dependency dep); void unassign(sat::literal lit); std::ostream& display(std::ostream& out) const; diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 9586b820d..63b97ed5b 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -55,14 +55,7 @@ namespace polysat { _backtrack.released = true; - - // a*v <= 0, a odd - if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi)) - return true; - // v > q - // 2^k*a*v + b > 0 - // TODO: is !ok2 required? if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi)) return true; @@ -77,6 +70,14 @@ namespace polysat { SASSERT(b1.is_val()); SASSERT(b2.is_val()); + // a*v <= 0, a odd + if (match_zero(c, a1, b1, e1, a2, b2, e2, fi)) + return true; + + // a*v + b > 0, a odd + if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi)) + return true; + if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) return true; if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi)) @@ -271,6 +272,10 @@ namespace polysat { /** * a*v <= 0, a odd * forbidden interval for v is [1,0[ + * + * TODO: extend to + * 2^k*a*v <= 0, a odd + * (using periodic intervals?) */ bool forbidden_intervals::match_zero( signed_constraint const& c, @@ -294,6 +299,42 @@ namespace polysat { return false; } + /** + * a*v + b > 0, a odd + * + * TODO: extend to + * 2^k*a*v + b > 0, a odd + * (using periodic intervals?) + */ + bool forbidden_intervals::match_non_zero_linear( + signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi) { + if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) { + // a*v + b > 0 + // <=> a*v + b != 0 + // <=> v + a^-1 * b != 0 + // <=> v != - a^-1 * b + auto& m = e1.manager(); + rational const& mod_value = m.two_to_N(); + rational a1_inv; + VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv)); + rational lo_val(mod(-b1.val() * a1_inv, mod_value)); + auto lo = -e1 * a1_inv; + rational hi_val(mod(lo_val + 1, mod_value)); + auto hi = lo + 1; + fi.coeff = 1; + fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); + if (b1 != e1) + fi.side_cond.push_back(s.eq(b1, e1)); + if (b2 != e2) + fi.side_cond.push_back(s.eq(b2, e2)); + return true; + } + return false; + } + /** * v > q * forbidden interval for v is [0,1[ diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 4b8dc2d3e..2d88216d3 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -57,6 +57,11 @@ namespace polysat { rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi); + bool match_non_zero_linear(signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi); + bool match_non_zero(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, fi_record& fi); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d22965b4c..7ce32031f 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -170,7 +170,7 @@ namespace polysat { } - void solver::assign_eh(signed_constraint c, dep_t dep) { + void solver::assign_eh(signed_constraint c, dependency dep) { SASSERT(at_base_level()); SASSERT(c); if (is_conflict()) @@ -599,7 +599,7 @@ namespace polysat { SASSERT(!m_conflict.empty()); } - void solver::unsat_core(svector& deps) { + void solver::unsat_core(dependency_vector& deps) { deps.reset(); for (auto c : m_conflict) { auto d = m_bvars.dep(c.blit()); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 5776037d7..9fba3d07a 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -256,7 +256,7 @@ namespace polysat { /** * retrieve unsat core dependencies */ - void unsat_core(svector& deps); + void unsat_core(dependency_vector& deps); /** * Add variable with bit-size. @@ -316,6 +316,7 @@ namespace polysat { signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); } signed_constraint eq(pdd const& p, unsigned q) { return eq(p - q); } signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); } + signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); } signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); } signed_constraint ule(pdd const& p, rational const& q) { return ule(p, p.manager().mk_val(q)); } signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); } @@ -331,33 +332,39 @@ namespace polysat { signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } /** Create and activate polynomial constraints. */ - void add_eq(pdd const& p, dep_t dep = null_dependency) { assign_eh(eq(p), dep); } - void add_diseq(pdd const& p, dep_t dep = null_dependency) { assign_eh(diseq(p), dep); } - void add_ule(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ule(p, q), dep); } - void add_ult(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ult(p, q), dep); } - void add_sle(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(sle(p, q), dep); } - void add_slt(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(slt(p, q), dep); } - void add_noovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); } - void add_ovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } + void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); } + void add_eq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } + void add_eq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } + void add_eq(pdd const& p, unsigned q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } + void add_diseq(pdd const& p, dependency dep = null_dependency) { assign_eh(diseq(p), dep); } + void add_diseq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); } + void add_diseq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); } + void add_diseq(pdd const& p, unsigned q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); } + void add_ule(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(ule(p, q), dep); } + void add_ult(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(ult(p, q), dep); } + void add_sle(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(sle(p, q), dep); } + void add_slt(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(slt(p, q), dep); } + void add_noovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); } + void add_ovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } - void add_ule(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); } - void add_ule(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); } - void add_ule(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ule(p, rational(q), dep); } - void add_ule(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ule(rational(p), q, dep); } - void add_ult(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); } - void add_ult(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); } - void add_ult(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ult(p, rational(q), dep); } - void add_ult(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ult(rational(p), q, dep); } - void add_noovfl(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); } - void add_noovfl(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); } - void add_noovfl(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_noovfl(p, rational(q), dep); } - void add_noovfl(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); } + void add_ule(pdd const& p, rational const& q, dependency dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); } + void add_ule(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); } + void add_ule(pdd const& p, unsigned q, dependency dep = null_dependency) { add_ule(p, rational(q), dep); } + void add_ule(unsigned p, pdd const& q, dependency dep = null_dependency) { add_ule(rational(p), q, dep); } + void add_ult(pdd const& p, rational const& q, dependency dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); } + void add_ult(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); } + void add_ult(pdd const& p, unsigned q, dependency dep = null_dependency) { add_ult(p, rational(q), dep); } + void add_ult(unsigned p, pdd const& q, dependency dep = null_dependency) { add_ult(rational(p), q, dep); } + void add_noovfl(pdd const& p, rational const& q, dependency dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); } + void add_noovfl(rational const& p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); } + void add_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency) { add_noovfl(p, rational(q), dep); } + void add_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); } /** * Activate the constraint corresponding to the given boolean variable. * Note: to deactivate, use push/pop. */ - void assign_eh(signed_constraint c, dep_t dep); + void assign_eh(signed_constraint c, dependency dep); /** * Unit propagation accessible over API. diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 6c02b0dd6..e3c08434d 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -28,9 +28,29 @@ namespace polysat { typedef dd::pdd pdd; typedef dd::bdd bdd; typedef dd::bddv bddv; + typedef unsigned pvar; - typedef unsigned dep_t; - const dep_t null_dependency = std::numeric_limits::max();; - const pvar null_var = UINT_MAX; + inline const pvar null_var = UINT_MAX; + + class dependency { + unsigned m_val; + public: + explicit dependency(unsigned val): m_val(val) {} + unsigned val() const { return m_val; } + bool is_null() const { return m_val == UINT_MAX; } + unsigned hash() const { return val(); } + }; + + inline const dependency null_dependency = dependency(UINT_MAX); + typedef svector dependency_vector; + + inline bool operator<(dependency const& d1, dependency const& d2) { return d1.val() < d2.val(); } + inline bool operator==(dependency const& d1, dependency const& d2) { return d1.val() == d2.val(); } + inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); } + + inline std::ostream& operator<<(std::ostream& out, dependency const& d) { + out << "dep(" << d.val() << ")"; + return out; + } } diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 860a35daf..b8e3a3fa8 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -204,7 +204,7 @@ namespace bv { sat::literal lit(a->m_bv, sign); if (sign) sc = ~sc; - m_polysat.assign_eh(sc, 1 + 2*lit.index()); + m_polysat.assign_eh(sc, polysat::dependency(1 + 2*lit.index())); } bool solver::polysat_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { @@ -215,7 +215,7 @@ namespace bv { auto sc = m_polysat.eq(p, q); m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); ctx.push(value_trail(m_var_eqs_head)); - m_polysat.assign_eh(sc, 2 * m_var_eqs_head); + m_polysat.assign_eh(sc, polysat::dependency(2 * m_var_eqs_head)); m_var_eqs_head++; return true; } @@ -226,7 +226,7 @@ namespace bv { pdd q = var2pdd(v2); auto sc = ~m_polysat.eq(p, q); sat::literal neq = ~expr2literal(ne.eq()); - m_polysat.assign_eh(sc, 1 + 2 * neq.index()); + m_polysat.assign_eh(sc, polysat::dependency(1 + 2 * neq.index())); return true; } @@ -248,15 +248,15 @@ namespace bv { } void solver::polysat_core() { - svector deps; + polysat::dependency_vector deps; sat::literal_vector core; euf::enode_pair_vector eqs; m_polysat.unsat_core(deps); for (auto n : deps) { - if (0 != (n & 1)) - core.push_back(sat::to_literal(n / 2)); + if (0 != (n.val() & 1)) + core.push_back(sat::to_literal(n.val() / 2)); else { - auto [v1, v2] = m_var_eqs[n / 2]; + auto [v1, v2] = m_var_eqs[n.val() / 2]; eqs.push_back(euf::enode_pair(var2enode(v1), var2enode(v2))); } } @@ -321,4 +321,4 @@ namespace bv { VERIFY(m_polysat.try_eval(p, val)); values[n->get_root_id()] = bv.mk_numeral(val, get_bv_size(n)); } -} \ No newline at end of file +}