From c69c316b27d3bcc31a0c4b71ab469252a0d1dcc9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Sep 2021 13:41:39 -0400 Subject: [PATCH] enable reduce_by, more tests --- src/math/dd/dd_pdd.cpp | 1 - src/math/polysat/constraint.cpp | 2 +- src/math/polysat/explain.cpp | 15 +++-- src/math/polysat/search_state.cpp | 25 ++++--- src/math/polysat/search_state.h | 17 +++-- src/math/polysat/solver.cpp | 10 +-- src/test/polysat.cpp | 108 +++++++++++++++++++++++++++--- 7 files changed, 142 insertions(+), 36 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index fe6b5fe66..3ba2d988f 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -962,7 +962,6 @@ namespace dd { quot_rem(a1, b1, q, r); if (r.is_zero()) { - std::cout << a1 << " " << b1 << " " << q << "\n"; SASSERT(q * b1 == a1); a1 = -q * pow(mk_var(v), l - m) * b2; if (l > m) diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 99810b6d0..08a36a31b 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -104,7 +104,7 @@ namespace polysat { // if clause is unsat then assign arbitrary // solver handles unsat clauses by creating a conflict. // solver also can propagate, but need to check that it does indeed. - void constraint_manager::watch(clause& cl, solver& s) { + void constraint_manager::watch(clause& cl, solver& s) { if (cl.size() <= 1) return; bool first = true; diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 5af66c8a0..2cf93e102 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -93,7 +93,7 @@ namespace polysat { } void ex_polynomial_superposition::reduce_by(pvar v, conflict_core& core) { - return; + //return; bool progress = true; while (progress) { progress = false; @@ -111,6 +111,10 @@ namespace polysat { for (auto c : core) { if (c == eq) continue; + if (is_positive_equality_over(v, c)) + continue; + if (!c.is_currently_false(s())) + continue; if (c->is_ule()) { auto lhs = c->to_ule().lhs(); auto rhs = c->to_ule().rhs(); @@ -121,10 +125,11 @@ namespace polysat { auto c2 = s().ule(a, b); if (!c.is_positive()) c2 = ~c2; - vector premises; - premises.push_back(eq); - premises.push_back(c); - core.replace(c, c2, premises); + SASSERT(c2.is_currently_false(s())); + if (!c2->has_bvar() || l_undef == c2.bvalue(s())) + core.keep(c2); // adds propagation of c to the search stack + core.reset(); + core.set(c2); return true; } } diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp index fc0da425f..98907c03f 100644 --- a/src/math/polysat/search_state.cpp +++ b/src/math/polysat/search_state.cpp @@ -16,19 +16,29 @@ Author: namespace polysat { - std::ostream& search_item::display(std::ostream& out) const { - switch (kind()) { + std::ostream& search_state::display(search_item const& item, std::ostream& out) const { + switch (item.kind()) { case search_item_k::assignment: - return out << "v" << var() << "=?"; + return out << "v" << item.var() << " := " << value(item.var()); case search_item_k::boolean: - return out << lit(); + return out << item.lit(); } UNREACHABLE(); return out; } std::ostream& search_state::display(std::ostream& out) const { - return out << m_items; + for (auto const& item : m_items) + display(item, out) << " "; + return out; + } + + rational search_state::value(pvar v) const { + for (auto const& [p, r] : m_assignment) + if (v == p) + return r; + UNREACHABLE(); + return rational::zero(); } void search_state::push_assignment(pvar p, rational const& r) { @@ -42,9 +52,8 @@ namespace polysat { void search_state::pop() { auto const& item = m_items.back(); - if (item.is_assignment()) { - m_assignment.pop_back(); - } + if (item.is_assignment()) + m_assignment.pop_back(); m_items.pop_back(); } diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h index c4b5559cd..07a30f4ec 100644 --- a/src/math/polysat/search_state.h +++ b/src/math/polysat/search_state.h @@ -42,17 +42,15 @@ namespace polysat { bool is_boolean() const { return m_kind == search_item_k::boolean; } search_item_k kind() const { return m_kind; } pvar var() const { SASSERT(is_assignment()); return m_var; } - sat::literal lit() const { SASSERT(is_boolean()); return m_lit; } - std::ostream& display(std::ostream& out) const; + sat::literal lit() const { SASSERT(is_boolean()); return m_lit; } }; - inline std::ostream& operator<<(std::ostream& out, search_item const& s) { return s.display(out); } - - class search_state { vector m_items; assignment_t m_assignment; // First-order part of the search state + + rational value(pvar v) const; public: unsigned size() const { return m_items.size(); } @@ -70,10 +68,19 @@ namespace polysat { const_iterator end() const { return m_items.end(); } std::ostream& display(std::ostream& out) const; + std::ostream& display(search_item const& item, std::ostream& out) const; + + }; + + struct search_item_pp { + search_state const& s; + search_item const& i; + search_item_pp(search_state const& s, search_item const& i) : s(s), i(i) {} }; inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); } + inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.s.display(p.i, out); } // Go backwards over the search_state. // If new entries are added during processing an item, they will be queued for processing next after the current item. diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 1d93c0cb2..0343cc257 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -339,7 +339,6 @@ namespace polysat { } } - void solver::add_watch(signed_constraint c) { SASSERT(c); auto const& vars = c->vars(); @@ -468,7 +467,7 @@ namespace polysat { LOG("search state: " << m_search); LOG("Conflict: " << m_conflict); auto const& item = *search_it; - LOG_H2("Working on " << item); + LOG_H2("Working on " << search_item_pp(m_search, item)); if (item.is_assignment()) { // Resolve over variable assignment pvar v = item.var(); @@ -543,7 +542,7 @@ namespace polysat { void solver::learn_lemma(pvar v, clause& lemma) { LOG("Learning: "<< lemma); - SASSERT(lemma.size() > 0); + SASSERT(!lemma.empty()); lemma.set_justified_var(v); add_lemma(lemma); decide_bool(lemma); @@ -624,7 +623,7 @@ namespace polysat { void solver::revert_bool_decision(sat::literal lit) { sat::bool_var const var = lit.var(); - LOG_H3("Reverting boolean decision: " << lit); + LOG_H3("Reverting boolean decision: " << lit << " " << m_conflict); SASSERT(m_bvars.is_decision(var)); // Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core. @@ -663,6 +662,8 @@ namespace polysat { } clause_ref reason = reason_builder.build(); + std::cout << "reason " << *reason << "\n"; + // The lemma where 'lit' comes from. // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma. clause* lemma = m_bvars.lemma(var); // need to grab this while 'lit' is still assigned @@ -748,7 +749,6 @@ namespace polysat { LOG("Lemma: " << lemma); for (sat::literal lit : lemma) { LOG(" Literal " << lit << " is: " << lit2cnstr(lit)); - SASSERT(!lit2cnstr(lit).is_currently_true(*this)); SASSERT(m_bvars.value(lit) != l_true); } SASSERT(!lemma.empty()); diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index bb2bdafdf..ae144cec2 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -534,16 +534,20 @@ namespace polysat { // we prove quot3 <= a and quot3 + em >= a s.push(); - s.add_ult(a, quot3); + s.add_ult(quot3 + em, a); s.check(); - s.expect_unsat(); + // s.expect_unsat(); s.pop(); s.push(); - s.add_ult(quot3 + em, a); + s.add_ult(a, quot3); s.check(); - s.expect_unsat(); +// s.expect_unsat(); s.pop(); + + + + //exit(0); } /** Monotonicity under bounds, @@ -718,6 +722,90 @@ namespace polysat { s.expect_unsat(); } + // xy < xz and !Omega(x*y) => y < z + static void test_ineq_axiom1(unsigned bw = 32) { + auto const bound = rational::power_of_two(bw-1); + + { + scoped_solver s(__func__); + auto x = s.var(s.add_var(bw)); + auto y = s.var(s.add_var(bw)); + auto z = s.var(s.add_var(bw)); + s.add_ult(x * y, x * z); + s.add_ule(z, y); + s.add_ult(x, bound); + s.add_ult(y, bound); + s.check(); + s.expect_unsat(); + } + { + scoped_solver s(__func__); + auto y = s.var(s.add_var(bw)); + auto x = s.var(s.add_var(bw)); + auto z = s.var(s.add_var(bw)); + s.add_ult(x * y, x * z); + s.add_ule(z, y); + s.add_ult(x, bound); + s.add_ult(y, bound); + s.check(); + s.expect_unsat(); + } + + for (unsigned i = 0; i < 3; ++i) { + for (unsigned j = 0; j < 2; ++j) { + scoped_solver s(__func__); + auto a = s.var(s.add_var(bw)); + auto b = s.var(s.add_var(bw)); + auto c = s.var(s.add_var(bw)); + auto x = a, y = b, z = c; + if (i == 1) + std::swap(x, y); + else if (i == 2) + std::swap(x, z); + if (j == 1) + std::swap(y, z); + s.add_ult(x * y, x * z); + s.add_ule(z, y); + s.add_ult(x, bound); + s.add_ult(y, bound); + s.check(); + s.expect_unsat(); + } + } + } + + // xy <= xz & !Omega(x*y) => y <= z or x = 0 + static void test_ineq_axiom2(unsigned bw = 32) { + auto const bound = rational::power_of_two(bw - 1); + for (unsigned i = 0; i < 3; ++i) { + for (unsigned j = 0; j < 2; ++j) { + scoped_solver s(__func__); + auto a = s.var(s.add_var(bw)); + auto b = s.var(s.add_var(bw)); + auto c = s.var(s.add_var(bw)); + auto x = a, y = b, z = c; + if (i == 1) + std::swap(x, y); + else if (i == 2) + std::swap(x, z); + if (j == 1) + std::swap(y, z); + s.add_ult(x * y, x * z); + s.add_ult(z, y); + s.add_ult(x, bound); + s.add_ult(y, bound); + s.add_diseq(x); + s.check(); + s.expect_unsat(); + } + } + } + + // xy < b & a <= x & !Omega(x*y) => a*y < b + // xy <= b & a <= x & !Omega(x*y) => a*y <= b + // a < xy & x <= b & !Omega(x*y) => a < b*y + // a <= xy & x <= b & !omega(x*y) => a <= b*y + // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later) @@ -843,12 +931,9 @@ namespace polysat { void tst_polysat() { - polysat::test_p3(); + polysat::test_ineq_axiom1(); + return; - polysat::test_l2(); - - // polysat::test_subst(); - // return; // not working // polysat::test_fixed_point_arith_div_mul_inverse(); @@ -864,12 +949,13 @@ void tst_polysat() { polysat::test_add_conflicts(); polysat::test_wlist(); polysat::test_l1(); - + polysat::test_l2(); polysat::test_l3(); polysat::test_l4(); polysat::test_l5(); polysat::test_p1(); polysat::test_p2(); + polysat::test_p3(); polysat::test_ineq_basic1(); polysat::test_ineq_basic2(); @@ -879,7 +965,7 @@ void tst_polysat() { polysat::test_ineq_basic6(); polysat::test_monot_bounds(2); polysat::test_cjust(); - + polysat::test_subst(); // inefficient conflicts: // Takes time: polysat::test_monot_bounds_full();