diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 42d473657..0c8b418e6 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -1208,6 +1208,11 @@ namespace dd { return true; } + /** Return true iff p contains no variables other than v. */ + bool pdd_manager::is_univariate_in(PDD p, unsigned v) { + return (is_val(p) || var(p) == v) && is_univariate(p); + } + /** * Push coefficients of univariate polynomial in order of ascending degree. * Example: a*x^2 + b*x + c ==> [ c, b, a ] diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index de29ed600..12900b9c6 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -364,6 +364,7 @@ namespace dd { bool is_monomial(PDD p); bool is_univariate(PDD p); + bool is_univariate_in(PDD p, unsigned v); void get_univariate_coefficients(PDD p, vector& coeff); // create an spoly r if leading monomials of a and b overlap @@ -430,6 +431,7 @@ namespace dd { bool is_binary() const { return m.is_binary(root); } bool is_monomial() const { return m.is_monomial(root); } bool is_univariate() const { return m.is_univariate(root); } + bool is_univariate_in(unsigned v) const { return m.is_univariate_in(root, v); } void get_univariate_coefficients(vector& coeff) const { m.get_univariate_coefficients(root, coeff); } vector get_univariate_coefficients() const { vector coeff; m.get_univariate_coefficients(root, coeff); return coeff; } bool is_never_zero() const { return m.is_never_zero(root); } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index a54f649a7..a4f82b07d 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -114,9 +114,11 @@ namespace polysat { bool is_pwatched() const { return m_is_pwatched; } void set_pwatched(bool f) { m_is_pwatched = f; } - /// Assuming the constraint is univariate under the current assignment of 's', - /// adds the constraint to the univariate solver 'us'. - virtual void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0; + /** + * If the constraint is univariate in variable 'v' under the current assignment of 's', + * add the constraint to the univariate solver 'us'. + */ + virtual void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0; }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } @@ -161,7 +163,7 @@ namespace polysat { void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); } clause_ref produce_lemma(solver& s, assignment const& a) { return get()->produce_lemma(s, a, is_positive()); } - void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(s, us, dep, is_positive()); } + void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(v, s, us, dep, is_positive()); } unsigned_vector const& vars() const { return m_constraint->vars(); } unsigned var(unsigned idx) const { return m_constraint->var(idx); } diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 9c175570a..6f0752bd2 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -448,19 +448,25 @@ namespace polysat { return l_undef; } - void op_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { - auto p_coeff = s.subst(p()).get_univariate_coefficients(); - auto q_coeff = s.subst(q()).get_univariate_coefficients(); - auto r_coeff = s.subst(r()).get_univariate_coefficients(); + void op_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { + pdd pv = s.subst(p()); + if (!pv.is_univariate_in(v)) + return; + pdd qv = s.subst(q()); + if (!qv.is_univariate_in(v)) + return; + pdd rv = s.subst(r()); + if (!rv.is_univariate_in(v)) + return; switch (m_op) { case code::lshr_op: - us.add_lshr(p_coeff, q_coeff, r_coeff, !is_positive, dep); + us.add_lshr(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); break; case code::shl_op: - us.add_shl(p_coeff, q_coeff, r_coeff, !is_positive, dep); + us.add_shl(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); break; case code::and_op: - us.add_and(p_coeff, q_coeff, r_coeff, !is_positive, dep); + us.add_and(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); break; default: NOT_IMPLEMENTED_YET(); diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h index 23161f701..d1ed8d7c0 100644 --- a/src/math/polysat/op_constraint.h +++ b/src/math/polysat/op_constraint.h @@ -69,7 +69,7 @@ namespace polysat { bool operator==(constraint const& other) const override; bool is_eq() const override { return false; } - void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; + void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; }; struct op_constraint_args { diff --git a/src/math/polysat/smul_fl_constraint.cpp b/src/math/polysat/smul_fl_constraint.cpp index 98f76fac1..b80340348 100644 --- a/src/math/polysat/smul_fl_constraint.cpp +++ b/src/math/polysat/smul_fl_constraint.cpp @@ -119,13 +119,17 @@ namespace polysat { && q() == other.to_smul_fl().q(); } - void smul_fl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { - auto p_coeff = s.subst(p()).get_univariate_coefficients(); - auto q_coeff = s.subst(q()).get_univariate_coefficients(); + void smul_fl_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { + auto p1 = s.subst(p()); + if (!p1.is_univariate_in(v)) + return; + auto q1 = s.subst(q()); + if (!q1.is_univariate_in(v)) + return; if (is_overflow()) - us.add_smul_ovfl(p_coeff, q_coeff, !is_positive, dep); + us.add_smul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep); else - us.add_smul_udfl(p_coeff, q_coeff, !is_positive, dep); + us.add_smul_udfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep); } } diff --git a/src/math/polysat/smul_fl_constraint.h b/src/math/polysat/smul_fl_constraint.h index a8d2c2814..ea5ff9fa6 100644 --- a/src/math/polysat/smul_fl_constraint.h +++ b/src/math/polysat/smul_fl_constraint.h @@ -42,7 +42,7 @@ namespace polysat { bool operator==(constraint const& other) const override; bool is_eq() const override { return false; } - void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; + void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; }; } diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 57cf4b0e6..f6fd6cfdf 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -245,9 +245,16 @@ namespace polysat { return other.is_ule() && lhs() == other.to_ule().lhs() && rhs() == other.to_ule().rhs(); } - void ule_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { - auto p_coeff = s.subst(lhs()).get_univariate_coefficients(); - auto q_coeff = s.subst(rhs()).get_univariate_coefficients(); - us.add_ule(p_coeff, q_coeff, !is_positive, dep); + void ule_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { + pdd p = s.subst(lhs()); + pdd q = s.subst(rhs()); + bool p_ok = p.is_univariate_in(v); + bool q_ok = q.is_univariate_in(v); + if (!is_positive && !q_ok) // add p > 0 + us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, dep); + if (!is_positive && !p_ok) // add -1 > q <==> q+1 > 0 + us.add_ugt((q + 1).get_univariate_coefficients(), rational::zero(), false, dep); + if (p_ok && q_ok) + us.add_ule(p.get_univariate_coefficients(), q.get_univariate_coefficients(), !is_positive, dep); } } diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 87dea1179..8f120b216 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -44,7 +44,7 @@ namespace polysat { unsigned hash() const override; bool operator==(constraint const& other) const override; bool is_eq() const override { return m_rhs.is_zero(); } - void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; + void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; }; struct ule_pp { diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp index 78c133c26..210179210 100644 --- a/src/math/polysat/umul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -25,8 +25,7 @@ namespace polysat { } void umul_ovfl_constraint::simplify() { - if (m_p.is_zero() || m_q.is_zero() || - m_p.is_one() || m_q.is_one()) { + if (m_p.is_zero() || m_q.is_zero() || m_p.is_one() || m_q.is_one()) { m_q = 0; m_p = 0; return; @@ -158,9 +157,13 @@ namespace polysat { return other.is_umul_ovfl() && p() == other.to_umul_ovfl().p() && q() == other.to_umul_ovfl().q(); } - void umul_ovfl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { - auto p_coeff = s.subst(p()).get_univariate_coefficients(); - auto q_coeff = s.subst(q()).get_univariate_coefficients(); - us.add_umul_ovfl(p_coeff, q_coeff, !is_positive, dep); + void umul_ovfl_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { + pdd p1 = s.subst(p()); + if (!p1.is_univariate_in(v)) + return; + pdd q1 = s.subst(q()); + if (!q1.is_univariate_in(v)) + return; + us.add_umul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep); } } diff --git a/src/math/polysat/umul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h index 1595f0bd6..449cd767d 100644 --- a/src/math/polysat/umul_ovfl_constraint.h +++ b/src/math/polysat/umul_ovfl_constraint.h @@ -46,7 +46,7 @@ namespace polysat { bool operator==(constraint const& other) const override; bool is_eq() const override { return false; } - void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; + void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override; }; } diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index fc14fcabf..73a2702ce 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -103,6 +103,10 @@ namespace polysat { return true; } + bool is_zero(rational const& p) const { + return p.is_zero(); + } + #if 0 // [d,c,b,a] --> ((a*x + b)*x + c)*x + d expr* mk_poly(univariate const& p) const { @@ -154,6 +158,10 @@ namespace polysat { } return e; } + + expr_ref mk_poly(rational const& p) { + return {mk_numeral(p), m}; + } #endif void add(expr* e, bool sign, dep_t dep) { @@ -171,13 +179,18 @@ namespace polysat { } } - void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { + template + void add_ule_impl(lhs_t const& lhs, rhs_t const& rhs, bool sign, dep_t dep) { if (is_zero(rhs)) add(m.mk_eq(mk_poly(lhs), mk_poly(rhs)), sign, dep); else add(bv->mk_ule(mk_poly(lhs), mk_poly(rhs)), sign, dep); } + void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); } + void add_ule(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); } + void add_ule(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); } + void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add(bv->mk_bvumul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); } @@ -220,13 +233,13 @@ namespace polysat { void add_ule_const(rational const& val, bool sign, dep_t dep) override { if (val == 0) - add(m.mk_eq(x, mk_numeral(val)), sign, dep); + add(m.mk_eq(x, mk_poly(val)), sign, dep); else - add(bv->mk_ule(x, mk_numeral(val)), sign, dep); + add(bv->mk_ule(x, mk_poly(val)), sign, dep); } void add_uge_const(rational const& val, bool sign, dep_t dep) override { - add(bv->mk_ule(mk_numeral(val), x), sign, dep); + add(bv->mk_ule(mk_poly(val), x), sign, dep); } void add_bit(unsigned idx, bool sign, dep_t dep) override { diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index b2bf63d61..a90ebe825 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -80,7 +80,23 @@ namespace polysat { */ virtual bool find_two(rational& out1, rational& out2) = 0; + /** lhs <= rhs */ virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; + virtual void add_ule(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) = 0; + virtual void add_ule(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; + /** lhs >= rhs */ + void add_uge(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } + void add_uge(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } + void add_uge(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } + /** lhs < rhs */ + void add_ult(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } + void add_ult(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } + void add_ult(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } + /** lhs > rhs */ + void add_ugt(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } + void add_ugt(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } + void add_ugt(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } + virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 03d98f08f..f9ae8b359 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -344,9 +344,9 @@ namespace polysat { } }; do { - LOG("refine-equal-lin for src: " << lit_pp(s, e->src)); rational coeff_val = mod(e->coeff * val, mod_value); if (e->interval.currently_contains(coeff_val)) { + LOG("refine-equal-lin for src: " << lit_pp(s, e->src)); if (e->interval.lo_val().is_one() && e->interval.hi_val().is_zero() && e->coeff.is_odd()) { rational lo(1); @@ -730,6 +730,7 @@ namespace polysat { // First step: only query the looping constraints and see if they alone are already UNSAT. // The constraints which caused the refinement loop will be reached from m_units. + LOG_H3("Checking looping univariate constraints for v" << v << "..."); entry const* first = m_units[v]; entry const* e = first; do { @@ -740,7 +741,8 @@ namespace polysat { sat::literal const lit = c.blit(); if (!added.contains(lit)) { added.insert(lit); - c.add_to_univariate_solver(s, *us, lit.to_uint()); + LOG("Adding " << lit_pp(s, lit)); + c.add_to_univariate_solver(v, s, *us, lit.to_uint()); } e = e->next(); } @@ -759,13 +761,15 @@ namespace polysat { } // Second step: looping constraints aren't UNSAT, so add the remaining relevant constraints + LOG_H3("Checking all univariate constraints for v" << v << "..."); auto const& cs = s.m_viable_fallback.m_constraints[v]; for (unsigned i = cs.size(); i-- > 0; ) { sat::literal const lit = cs[i].blit(); if (added.contains(lit)) continue; + LOG("Adding " << lit_pp(s, lit)); added.insert(lit); - cs[i].add_to_univariate_solver(s, *us, lit.to_uint()); + cs[i].add_to_univariate_solver(v, s, *us, lit.to_uint()); } switch (us->check()) { @@ -1060,7 +1064,7 @@ namespace polysat { for (unsigned i = cs.size(); i-- > 0; ) { signed_constraint const c = cs[i]; LOG("Univariate constraint: " << c); - c.add_to_univariate_solver(s, *us, c.blit().to_uint()); + c.add_to_univariate_solver(v, s, *us, c.blit().to_uint()); } switch (us->check()) {