From e978e4fc8e41b84aa21d093c6b6a301338c9e577 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 14 Dec 2022 11:07:16 +0100 Subject: [PATCH 1/8] Strengthen umul_ovfl lemma --- src/math/polysat/umul_ovfl_constraint.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp index 345541377..f1f980e20 100644 --- a/src/math/polysat/umul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -90,8 +90,6 @@ namespace polysat { return; if (narrow_bound(s, is_positive, q(), p(), q1, p1)) return; - - } void umul_ovfl_constraint::activate(solver& s, bool is_positive) { @@ -99,8 +97,10 @@ namespace polysat { return; if (!is_positive) { signed_constraint sc(this, is_positive); - s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(p(), p()*q()), false); - s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(q(), p()*q()), false); + // ¬Omega(p, q) ==> q = 0 \/ p <= p*q + // ¬Omega(p, q) ==> p = 0 \/ q <= p*q + s.add_clause(~sc, /* s.eq(p()), */ s.eq(q()), s.ule(p(), p()*q()), false); + s.add_clause(~sc, s.eq(p()), /* s.eq(q()), */ s.ule(q(), p()*q()), false); } } From 3d06a90e7f251a6eb31d25c4cb9584021f64d7ca Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 13:08:13 +0100 Subject: [PATCH 2/8] track refinement source --- src/math/polysat/viable.cpp | 4 ++++ src/math/polysat/viable.h | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index e1c1f17b2..ae8fea496 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -70,6 +70,7 @@ namespace polysat { auto* e = m_alloc.back(); e->side_cond.reset(); e->coeff = 1; + e->refined = nullptr; m_alloc.pop_back(); return e; } @@ -348,6 +349,7 @@ namespace polysat { pdd lop = s.var2pdd(v).mk_val(lo); pdd hip = s.var2pdd(v).mk_val(hi); entry* ne = alloc_entry(); + ne->refined = e; ne->src = e->src; ne->side_cond = e->side_cond; ne->coeff = 1; @@ -384,6 +386,7 @@ namespace polysat { pdd lop = s.var2pdd(v).mk_val(lo); pdd hip = s.var2pdd(v).mk_val(hi); entry* ne = alloc_entry(); + ne->refined = e; ne->src = e->src; ne->side_cond = e->side_cond; ne->coeff = 1; @@ -471,6 +474,7 @@ namespace polysat { pdd lop = s.var2pdd(v).mk_val(lo); pdd hip = s.var2pdd(v).mk_val(hi); entry* ne = alloc_entry(); + ne->refined = e; ne->src = e->src; ne->side_cond = e->side_cond; ne->coeff = 1; diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 8b2d2fa71..544082d34 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -38,7 +38,9 @@ namespace polysat { solver& s; forbidden_intervals m_forbidden_intervals; - struct entry final : public dll_base, public fi_record {}; + struct entry final : public dll_base, public fi_record { + entry const* refined = nullptr; + }; enum class entry_kind { unit_e, equal_e, diseq_e }; ptr_vector m_alloc; From 5de0007157c7ac02f4b2bfba27f21a2aa1f8bc5d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 13:39:48 +0100 Subject: [PATCH 3/8] very basic refinement loop breaking --- src/math/polysat/solver.cpp | 23 ++++-- src/math/polysat/viable.cpp | 138 +++++++++++++++++++++++++++++++----- src/math/polysat/viable.h | 23 +++++- 3 files changed, 158 insertions(+), 26 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index def600bad..dba5ba363 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -647,22 +647,29 @@ namespace polysat { rational val; justification j; switch (m_viable.find_viable(v, val)) { - case dd::find_t::empty: + case find_t::empty: // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) // (fail here in debug mode so we notice if we miss some) DEBUG_CODE( UNREACHABLE(); ); m_free_pvars.unassign_var_eh(v); set_conflict(v, false); return; - case dd::find_t::singleton: + case find_t::singleton: // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search // NOTE 2: probably not true anymore; viable::intersect should trigger all propagations now DEBUG_CODE( UNREACHABLE(); ); j = justification::propagation(m_level); break; - case dd::find_t::multiple: + case find_t::multiple: j = justification::decision(m_level + 1); break; + case find_t::resource_out: + // the value is not viable, so assign_verify will call the univariate solver. + j = justification::decision(m_level + 1); + break; + default: + UNREACHABLE(); + break; } assign_verify(v, val, j); } @@ -731,20 +738,24 @@ namespace polysat { } if (c) { LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!"); + LOG("Current assignment: " << assignments_pp(*this)); ++m_stats.m_num_viable_fallback; // Try to find a valid replacement value switch (m_viable_fallback.find_viable(v, val)) { - case dd::find_t::singleton: - case dd::find_t::multiple: + case find_t::singleton: + case find_t::multiple: LOG("Fallback solver: " << assignment_pp(*this, v, val)); SASSERT(!j.is_propagation()); // all excluded values are true negatives, so if j.is_propagation() the univariate solver must return unsat j = justification::decision(m_level + 1); break; - case dd::find_t::empty: + case find_t::empty: LOG("Fallback solver: unsat"); m_free_pvars.unassign_var_eh(v); set_conflict(v, true); return; + case find_t::resource_out: + UNREACHABLE(); // TODO: abort solving + return; } } if (j.is_decision()) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index ae8fea496..3b832b7cf 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -132,11 +132,11 @@ namespace polysat { if (intersect(v, sc)) { rational val; switch (find_viable(v, val)) { - case dd::find_t::singleton: + case find_t::singleton: propagate(v, val); prop = true; break; - case dd::find_t::empty: + case find_t::empty: s.set_conflict(v, false); return true; default: @@ -592,25 +592,45 @@ namespace polysat { return hi; } - dd::find_t viable::find_viable(pvar v, rational& lo) { - refined: + // template + find_t viable::query(query_t mode, pvar v, rational& lo, rational& hi) { + SASSERT(mode == query_t::find_viable); // other modes are TODO + + auto const& max_value = s.var2pdd(v).max_value(); + + // max number of interval refinements before falling back to the univariate solver + unsigned const refinement_budget = 1000; + unsigned refinements = refinement_budget; + + refined: + + if (!refinements) { + LOG("Refinement budget exhausted! Fall back to univariate solver."); + return find_t::resource_out; + } + + refinements--; + + // After a refinement, any of the existing entries may have been replaced + // (if it is subsumed by the new entry created during refinement). + // For this reason, we start chasing the intervals from the start again. lo = 0; + auto* e = m_units[v]; if (!e && !refine_viable(v, lo)) goto refined; if (!e && !refine_viable(v, rational::one())) goto refined; if (!e) - return dd::find_t::multiple; + return find_t::multiple; if (e->interval.is_full()) - return dd::find_t::empty; + return find_t::empty; entry* first = e; entry* last = first->prev(); // quick check: last interval does not wrap around // and has space for 2 unassigned values. - auto& max_value = s.var2pdd(v).max_value(); if (last->interval.lo_val() < last->interval.hi_val() && last->interval.hi_val() < max_value) { lo = last->interval.hi_val(); @@ -618,7 +638,7 @@ namespace polysat { goto refined; if (!refine_viable(v, max_value)) goto refined; - return dd::find_t::multiple; + return find_t::multiple; } // find lower bound @@ -633,7 +653,76 @@ namespace polysat { while (e != first); if (e->interval.currently_contains(lo)) - return dd::find_t::empty; + return find_t::empty; + + // find upper bound + hi = max_value; + e = last; + do { + if (!e->interval.currently_contains(hi)) + break; + hi = e->interval.lo_val() - 1; + e = e->prev(); + } + while (e != last); + if (!refine_viable(v, lo)) + goto refined; + if (!refine_viable(v, hi)) + goto refined; + + if (lo == hi) + return find_t::singleton; + else + return find_t::multiple; + } + + find_t viable::find_viable(pvar v, rational& lo) { +#if 1 + rational hi; + // return query(v, lo, hi); + return query(query_t::find_viable, v, lo, hi); +#else + refined: + lo = 0; + auto* e = m_units[v]; + if (!e && !refine_viable(v, lo)) + goto refined; + if (!e && !refine_viable(v, rational::one())) + goto refined; + if (!e) + return find_t::multiple; + if (e->interval.is_full()) + return find_t::empty; + + entry* first = e; + entry* last = first->prev(); + + // quick check: last interval does not wrap around + // and has space for 2 unassigned values. + auto& max_value = s.var2pdd(v).max_value(); + if (last->interval.lo_val() < last->interval.hi_val() && + last->interval.hi_val() < max_value) { + lo = last->interval.hi_val(); + if (!refine_viable(v, lo)) + goto refined; + if (!refine_viable(v, max_value)) + goto refined; + return find_t::multiple; + } + + // find lower bound + if (last->interval.currently_contains(lo)) + lo = last->interval.hi_val(); + do { + if (!e->interval.currently_contains(lo)) + break; + lo = e->interval.hi_val(); + e = e->next(); + } + while (e != first); + + if (e->interval.currently_contains(lo)) + return find_t::empty; // find upper bound rational hi = max_value; @@ -650,9 +739,10 @@ namespace polysat { if (!refine_viable(v, hi)) goto refined; if (lo == hi) - return dd::find_t::singleton; + return find_t::singleton; else - return dd::find_t::multiple; + return find_t::multiple; +#endif } bool viable::resolve(pvar v, conflict& core) { @@ -857,7 +947,7 @@ namespace polysat { return {}; } - dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) { + find_t viable_fallback::find_viable(pvar v, rational& out_val) { unsigned bit_width = s.m_size[v]; univariate_solver* us; @@ -884,14 +974,11 @@ namespace polysat { case l_true: out_val = us->model(); // we don't know whether the SMT instance has a unique solution - return dd::find_t::multiple; + return find_t::multiple; case l_false: - return dd::find_t::empty; + return find_t::empty; default: - // TODO: what should we do here? (SMT solver had resource-out ==> polysat should abort too?) - // can we pass polysat's resource limit to the univariate solver? - UNREACHABLE(); - return dd::find_t::empty; + return find_t::resource_out; } } @@ -905,5 +992,20 @@ namespace polysat { return cs; } + std::ostream& operator<<(std::ostream& out, find_t x) { + switch (x) { + case find_t::empty: + return out << "empty"; + case find_t::singleton: + return out << "singleton"; + case find_t::multiple: + return out << "multiple"; + case find_t::resource_out: + return out << "resource_out"; + } + UNREACHABLE(); + return out; + } + } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 544082d34..6588dcc18 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -32,6 +32,15 @@ namespace polysat { class univariate_solver; class univariate_solver_factory; + enum class find_t { + empty, + singleton, + multiple, + resource_out, + }; + + std::ostream& operator<<(std::ostream& out, find_t x); + class viable { friend class test_fi; @@ -67,6 +76,16 @@ namespace polysat { void propagate(pvar v, rational const& val); + enum class query_t { + has_viable, // currently only used internally in resolve_viable + min_viable, // currently unused + max_viable, // currently unused + find_viable, + }; + + // template + find_t query(query_t mode, pvar v, rational& out_lo, rational& out_hi); + public: viable(solver& s); @@ -112,7 +131,7 @@ namespace polysat { /** * Find a next viable value for variable. */ - dd::find_t find_viable(pvar v, rational & val); + find_t find_viable(pvar v, rational& out_val); /** * Retrieve the unsat core for v, @@ -255,7 +274,7 @@ namespace polysat { bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); } signed_constraint find_violated_constraint(assignment const& a, pvar v); - dd::find_t find_viable(pvar v, rational& out_val); + find_t find_viable(pvar v, rational& out_val); signed_constraints unsat_core(pvar v); }; From a6504785b5f8e7e967fa4144dee0f0a30339ab3b Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 13:43:09 +0100 Subject: [PATCH 4/8] print bitblasted constraints --- src/math/polysat/univariate/univariate_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index f9091fa1e..e00777ab8 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -85,7 +85,7 @@ namespace polysat { e = m.mk_not(e); expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort())); s->assert_expr(e, a); - // std::cout << "add: " << expr_ref(e, m) << " <== " << expr_ref(a, m) << "\n"; + IF_VERBOSE(10, verbose_stream() << "(assert (! " << expr_ref(e, m) << " :named " << expr_ref(a, m) << "))\n"); } void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { From 06a999e219ed599c2c57cf9df7b7ee71747f7e79 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 13:46:10 +0100 Subject: [PATCH 5/8] skip diseq when not using polysat --- src/sat/smt/bv_polysat.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 77e170e77..1345dde6a 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -218,6 +218,8 @@ namespace bv { } bool solver::polysat_diseq_eh(euf::th_eq const& ne) { + if (!use_polysat()) + return false; euf::theory_var v1 = ne.v1(), v2 = ne.v2(); pdd p = var2pdd(v1); pdd q = var2pdd(v2); From 37536425f42d4d2057554ab6b8101c6ec7b8388b Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 14:03:42 +0100 Subject: [PATCH 6/8] Encode 2^k*x as (bvshl x k) in the fallback solver --- .../polysat/univariate/univariate_solver.cpp | 35 ++++++++++++++++++- src/test/polysat.cpp | 3 +- 2 files changed, 36 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index e00777ab8..7c23b56ec 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -64,7 +64,8 @@ namespace polysat { return bv->mk_numeral(r, bit_width); } - // [d,c,b,a] ==> ((a*x + b)*x + c)*x + d +#if 0 + // [d,c,b,a] --> ((a*x + b)*x + c)*x + d expr* mk_poly(univariate const& p) const { if (p.empty()) { return mk_numeral(rational::zero()); @@ -79,6 +80,38 @@ namespace polysat { return e; } } +#else + // TODO: shouldn't the simplification step of the underlying solver already support this transformation? how to enable? + // 2^k*x --> x << k + // n*x --> n * x + expr* mk_poly_term(rational const& coeff, expr* xpow) const { + unsigned pow; + if (coeff.is_power_of_two(pow)) + return bv->mk_bv_shl(xpow, mk_numeral(rational(pow))); + else + return bv->mk_bv_mul(mk_numeral(coeff), xpow); + } + + // [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x) + expr* mk_poly(univariate const& p) const { + if (p.empty()) { + return mk_numeral(rational::zero()); + } + else { + expr* e = mk_numeral(p.back()); + expr* xpow = x; + for (unsigned i = p.size() - 1; i-- > 0; ) { + if (!p[i].is_zero()) { + expr* t = mk_poly_term(p[i], xpow); + e = bv->mk_bv_add(e, t); + } + if (i) + xpow = bv->mk_bv_mul(xpow, x); + } + return e; + } + } +#endif void add(expr* e, bool sign, dep_t dep) { if (sign) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index b81c66352..d96f20e60 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1661,7 +1661,8 @@ void tst_polysat() { // test_polysat::test_parity1b(); // test_polysat::test_parity2(); // test_polysat::test_parity3(); - test_polysat::test_parity4(); + // test_polysat::test_parity4(); + // test_polysat::test_parity4(32); test_polysat::test_parity4(256); // test_polysat::test_ineq2(); // test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop From 31e0add966e1121e72527c8db6d267f081c1e920 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 15:34:50 +0100 Subject: [PATCH 7/8] univariate::find_min --- .../polysat/univariate/univariate_solver.cpp | 34 +++++++- .../polysat/univariate/univariate_solver.h | 10 +++ src/test/viable.cpp | 79 ++++++++++++++++++- 3 files changed, 118 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index 7c23b56ec..5dd4f6963 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -98,14 +98,14 @@ namespace polysat { return mk_numeral(rational::zero()); } else { - expr* e = mk_numeral(p.back()); + expr* e = mk_numeral(p[0]); expr* xpow = x; - for (unsigned i = p.size() - 1; i-- > 0; ) { + for (unsigned i = 1; i < p.size(); ++i) { if (!p[i].is_zero()) { expr* t = mk_poly_term(p[i], xpow); e = bv->mk_bv_add(e, t); } - if (i) + if (i + 1 < p.size()) xpow = bv->mk_bv_mul(xpow, x); } return e; @@ -205,6 +205,34 @@ namespace polysat { return p.get_rational(); } + bool find_min(rational& val) override { + val = model(); + push(); + // try reducing val by setting bits to 0, starting at the msb. + for (unsigned k = bit_width; k-- > 0; ) { + if (!val.get_bit(k)) { + add_bit0(k, 0); + continue; + } + push(); + add_bit0(k, 0); + lbool result = check(); + if (result == l_true) { + SASSERT(model() < val); + val = model(); + } + pop(1); + if (result == l_true) + add_bit0(k, 0); + else if (result == l_false) + add_bit1(k, 0); + else + return false; + } + pop(1); + return true; + } + std::ostream& display(std::ostream& out) const override { return out << *s; } diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index 65bc9c65a..63099c618 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -41,9 +41,17 @@ namespace polysat { virtual void pop(unsigned n) = 0; virtual lbool check() = 0; + + // Precondition: check() returned l_false virtual dep_vector unsat_core() = 0; + + // Precondition: check() returned l_true virtual rational model() = 0; + // Precondition: check() returned l_true + // Returns false on resource out. + virtual bool find_min(rational& out_min) = 0; + virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; 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; @@ -65,6 +73,8 @@ namespace polysat { /// Assert i-th bit of x virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0; + void add_bit0(unsigned idx, dep_t dep) { add_bit(idx, true, dep); } + void add_bit1(unsigned idx, dep_t dep) { add_bit(idx, false, dep); } virtual std::ostream& display(std::ostream& out) const = 0; }; diff --git a/src/test/viable.cpp b/src/test/viable.cpp index 614255d16..ab03e72c6 100644 --- a/src/test/viable.cpp +++ b/src/test/viable.cpp @@ -117,8 +117,8 @@ namespace polysat { static void test_univariate() { std::cout << "\ntest_univariate\n"; - unsigned bw = 32; - rational modulus = rational::power_of_two(bw); + unsigned const bw = 32; + rational const modulus = rational::power_of_two(bw); auto factory = mk_univariate_bitblast_factory(); auto solver = (*factory)(bw); @@ -182,6 +182,80 @@ namespace polysat { std::cout << "status: " << solver->check() << "\n"; std::cout << "core: " << solver->unsat_core() << "\n"; } + + static void test_univariate_min() { + std::cout << "\ntest_univariate_min\n"; + unsigned const bw = 32; + auto factory = mk_univariate_bitblast_factory(); + auto solver = (*factory)(bw); + + vector lhs; + vector rhs; + rational min; + + solver->push(); + + // c0: 123 <= 2x + 10 + lhs.clear(); + lhs.push_back(rational(123)); + rhs.clear(); + rhs.push_back(rational(10)); + rhs.push_back(rational(2)); + solver->add_ule(lhs, rhs, false, 0); + std::cout << "status: " << solver->check() << "\n"; + std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); + std::cout << "find_min: " << min << "\n"; + VERIFY(min == 57); // 57*2 + 10 = 124; 56*2 + 10 = 122 + + solver->push(); + + // c1: 127 <= x + lhs.clear(); + lhs.push_back(rational(127)); + rhs.clear(); + rhs.push_back(rational(0)); + rhs.push_back(rational(1)); + solver->add_ule(lhs, rhs, false, 1); + std::cout << "status: " << solver->check() << "\n"; + std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); + std::cout << "find_min: " << min << "\n"; + VERIFY(min == 127); + + solver->pop(1); + + // c2: umul_ovfl(2, x) + lhs.clear(); + lhs.push_back(rational(2)); + rhs.clear(); + rhs.push_back(rational(0)); + rhs.push_back(rational(1)); + solver->add_umul_ovfl(lhs, rhs, false, 2); + std::cout << "status: " << solver->check() << "\n"; + std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); + std::cout << "find_min: " << min << "\n"; + solver->add_ule_const(min - 1, false, 3); + VERIFY(solver->check() == l_false); + + solver->pop(1); + + // c4: umul_ovfl(2, x) + lhs.clear(); + lhs.push_back(rational(2)); + rhs.clear(); + rhs.push_back(rational(0)); + rhs.push_back(rational(1)); + solver->add_umul_ovfl(lhs, rhs, false, 4); + std::cout << "status: " << solver->check() << "\n"; + std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); + std::cout << "find_min: " << min << "\n"; + solver->add_ule_const(min - 1, false, 5); + VERIFY(solver->check() == l_false); + } + } @@ -189,5 +263,6 @@ namespace polysat { void tst_viable() { polysat::test1(); polysat::test_univariate(); + polysat::test_univariate_min(); polysat::test2(); // takes long } From 8a5f1af3d1177f602ffa2101d3be6b1d66145103 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 15:59:15 +0100 Subject: [PATCH 8/8] univariate::find_max --- .../polysat/univariate/univariate_solver.cpp | 69 ++++++++++++++++--- .../polysat/univariate/univariate_solver.h | 24 +++++-- src/test/viable.cpp | 43 ++++++++++-- 3 files changed, 117 insertions(+), 19 deletions(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index 5dd4f6963..e66a521c3 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -35,6 +35,7 @@ namespace polysat { unsigned bit_width; func_decl_ref x_decl; expr_ref x; + vector model_cache; public: univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) : @@ -48,15 +49,30 @@ namespace polysat { s = mk_solver(m, p, false, true, true, symbol::null); x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width)); x = m.mk_const(x_decl); + model_cache.push_back(rational(-1)); } ~univariate_bitblast_solver() override = default; + void reset_cache() { + model_cache.back() = -1; + } + + void push_cache() { + model_cache.push_back(model_cache.back()); + } + + void pop_cache() { + model_cache.pop_back(); + } + void push() override { + push_cache(); s->push(); } void pop(unsigned n) override { + pop_cache(); s->pop(n); } @@ -114,6 +130,7 @@ namespace polysat { #endif void add(expr* e, bool sign, dep_t dep) { + reset_cache(); if (sign) e = m.mk_not(e); expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort())); @@ -194,15 +211,19 @@ namespace polysat { } rational model() override { - model_ref model; - s->get_model(model); - SASSERT(model); - app* val = to_app(model->get_const_interp(x_decl)); - SASSERT(val->get_decl_kind() == OP_BV_NUM); - SASSERT(val->get_num_parameters() == 2); - auto const& p = val->get_parameter(0); - SASSERT(p.is_rational()); - return p.get_rational(); + rational& cached_model = model_cache.back(); + if (cached_model.is_neg()) { + model_ref model; + s->get_model(model); + SASSERT(model); + app* val = to_app(model->get_const_interp(x_decl)); + SASSERT(val->get_decl_kind() == OP_BV_NUM); + SASSERT(val->get_num_parameters() == 2); + auto const& p = val->get_parameter(0); + SASSERT(p.is_rational()); + cached_model = p.get_rational(); + } + return cached_model; } bool find_min(rational& val) override { @@ -214,6 +235,7 @@ namespace polysat { add_bit0(k, 0); continue; } + // try decreasing k-th bit push(); add_bit0(k, 0); lbool result = check(); @@ -233,6 +255,35 @@ namespace polysat { return true; } + bool find_max(rational& val) override { + val = model(); + push(); + // try increasing val by setting bits to 1, starting at the msb. + for (unsigned k = bit_width; k-- > 0; ) { + if (val.get_bit(k)) { + add_bit1(k, 0); + continue; + } + // try increasing k-th bit + push(); + add_bit1(k, 0); + lbool result = check(); + if (result == l_true) { + SASSERT(model() > val); + val = model(); + } + pop(1); + if (result == l_true) + add_bit1(k, 0); + else if (result == l_false) + add_bit0(k, 0); + else + return false; + } + pop(1); + return true; + } + std::ostream& display(std::ostream& out) const override { return out << *s; } diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index 63099c618..904342a79 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -42,16 +42,32 @@ namespace polysat { virtual lbool check() = 0; - // Precondition: check() returned l_false + /** + * Precondition: check() returned l_false + */ virtual dep_vector unsat_core() = 0; - // Precondition: check() returned l_true + /** + * Precondition: check() returned l_true + */ virtual rational model() = 0; - // Precondition: check() returned l_true - // Returns false on resource out. + /** + * Find minimal model. + * + * Precondition: check() returned l_true + * Returns: true on success, false on resource out. + */ virtual bool find_min(rational& out_min) = 0; + /** + * Find maximal model. + * + * Precondition: check() returned l_true + * Returns: true on success, false on resource out. + */ + virtual bool find_max(rational& out_max) = 0; + virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; 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; diff --git a/src/test/viable.cpp b/src/test/viable.cpp index ab03e72c6..c2614854d 100644 --- a/src/test/viable.cpp +++ b/src/test/viable.cpp @@ -183,7 +183,7 @@ namespace polysat { std::cout << "core: " << solver->unsat_core() << "\n"; } - static void test_univariate_min() { + static void test_univariate_minmax() { std::cout << "\ntest_univariate_min\n"; unsigned const bw = 32; auto factory = mk_univariate_bitblast_factory(); @@ -192,6 +192,7 @@ namespace polysat { vector lhs; vector rhs; rational min; + rational max; solver->push(); @@ -204,10 +205,18 @@ namespace polysat { solver->add_ule(lhs, rhs, false, 0); std::cout << "status: " << solver->check() << "\n"; std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); std::cout << "find_min: " << min << "\n"; VERIFY(min == 57); // 57*2 + 10 = 124; 56*2 + 10 = 122 + VERIFY(solver->find_max(max)); + std::cout << "find_max: " << max << "\n"; + solver->push(); + solver->add_ugt_const(max, false, 5); + VERIFY(solver->check() == l_false); + solver->pop(1); + solver->push(); // c1: 127 <= x @@ -219,10 +228,16 @@ namespace polysat { solver->add_ule(lhs, rhs, false, 1); std::cout << "status: " << solver->check() << "\n"; std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); std::cout << "find_min: " << min << "\n"; VERIFY(min == 127); + VERIFY(solver->find_max(max)); + std::cout << "find_max: " << max << "\n"; + solver->add_ugt_const(max, false, 5); + VERIFY(solver->check() == l_false); + solver->pop(1); // c2: umul_ovfl(2, x) @@ -234,25 +249,41 @@ namespace polysat { solver->add_umul_ovfl(lhs, rhs, false, 2); std::cout << "status: " << solver->check() << "\n"; std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); std::cout << "find_min: " << min << "\n"; - solver->add_ule_const(min - 1, false, 3); + solver->push(); + solver->add_ult_const(min, false, 5); + VERIFY(solver->check() == l_false); + solver->pop(1); + + VERIFY(solver->find_max(max)); + std::cout << "find_max: " << max << "\n"; + solver->add_ugt_const(max, false, 5); VERIFY(solver->check() == l_false); solver->pop(1); - // c4: umul_ovfl(2, x) + // c3: umul_ovfl(2, x) lhs.clear(); lhs.push_back(rational(2)); rhs.clear(); rhs.push_back(rational(0)); rhs.push_back(rational(1)); - solver->add_umul_ovfl(lhs, rhs, false, 4); + solver->add_umul_ovfl(lhs, rhs, false, 3); std::cout << "status: " << solver->check() << "\n"; std::cout << "model: " << solver->model() << "\n"; + VERIFY(solver->find_min(min)); std::cout << "find_min: " << min << "\n"; - solver->add_ule_const(min - 1, false, 5); + solver->push(); + solver->add_ult_const(min, false, 5); + VERIFY(solver->check() == l_false); + solver->pop(1); + + VERIFY(solver->find_max(max)); + std::cout << "find_max: " << max << "\n"; + solver->add_ugt_const(max, false, 5); VERIFY(solver->check() == l_false); } @@ -263,6 +294,6 @@ namespace polysat { void tst_viable() { polysat::test1(); polysat::test_univariate(); - polysat::test_univariate_min(); + polysat::test_univariate_minmax(); polysat::test2(); // takes long }