diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 00659aa04..a7b17ddbd 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -191,7 +191,7 @@ namespace polysat { SASSERT(lit != sat::null_literal); SASSERT(~lit != sat::null_literal); - SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); })); + SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); })); SASSERT(contains_literal(lit)); SASSERT(std::count(cl.begin(), cl.end(), lit) > 0); SASSERT(!contains_literal(~lit)); @@ -219,7 +219,7 @@ namespace polysat { clause_builder conflict::build_lemma() { SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); })); - SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c) { return !c->has_bvar(); })); + SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); })); LOG_H3("Build lemma from core"); LOG("core: " << *this); diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index c345f21f8..83ad5b3b0 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -146,7 +146,7 @@ namespace polysat { if (!c2->has_bvar() || l_undef == c2.bvalue(s)) core.keep(c2); // adds propagation of c to the search stack core.reset(); - LOG("reduced to " << c2); + LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2); if (c2.bvalue(s) == l_false) { core.insert(eq); core.insert(c); @@ -161,12 +161,10 @@ namespace polysat { } bool ex_polynomial_superposition::try_explain(pvar v, conflict& core) { - LOG_H3("Trying polynomial superposition..."); reduce_by(v, core); lbool result = l_undef; while (result == l_undef) result = try_explain1(v, core); - LOG("success? " << result); return result == l_true; } diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index fa251d355..1464811b7 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -1335,7 +1335,7 @@ namespace polysat { template bool fixplex::propagate_strict_bounds(ineq const& i) { var_t v = i.v, w = i.w; - bool s = i.strict; + //bool s = i.strict; auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep; auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep; @@ -1363,7 +1363,7 @@ namespace polysat { template bool fixplex::propagate_non_strict_bounds(ineq const& i) { var_t v = i.v, w = i.w; - bool s = i.strict; + // bool s = i.strict; auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep; auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep; diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 7a716df0e..b4fa8f61b 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -13,11 +13,6 @@ Author: Jakob Rath 2021-04-6 -TODO: -compute forbidden interval coefficients a1, a2 modulo current assignment to handle pseudo-linear cases. -test_mont_bounds(8) produces constraint 13 <= v1*v2, where v2 = 1, then v1 is linear and is constrained above 13. - - --*/ #include "math/polysat/forbidden_intervals.h" @@ -175,6 +170,7 @@ namespace polysat { } + /** Precondition: all variables other than v are assigned. * * \param[out] out_interval The forbidden interval for this constraint @@ -186,6 +182,20 @@ namespace polysat { { if (!c->is_ule()) return false; + + struct backtrack { + bool released = false; + vector& side_cond; + unsigned sz; + backtrack(vector& s):side_cond(s), sz(s.size()) {} + ~backtrack() { + if (!released) + side_cond.shrink(sz); + } + }; + + backtrack _backtrack(out_side_cond); + // Current only works when degree(v) is at most one on both sides pdd lhs = c->to_ule().lhs(); pdd rhs = c->to_ule().rhs(); @@ -206,6 +216,16 @@ namespace polysat { rational const pow2 = rational::power_of_two(sz); rational const minus_one = pow2 - 1; + /** + * TODO: to express the interval for coefficient 2^i symbolically, + * we need right-shift/upper-bits-extract in the language. + * So currently we can only do it if the coefficient is 1 or -1. + */ + + auto coefficient_is_handled = [&](rational const& r) { + return r.is_zero() || r.is_one() || r == minus_one; + }; + pdd p1 = m.zero(); pdd e1 = m.zero(); if (deg1 == 0) @@ -247,13 +267,13 @@ namespace polysat { } rational a1 = p1.val(); rational a2 = p2.val(); - // TODO: to express the interval for coefficient 2^i symbolically, we need right-shift/upper-bits-extract in the language. - // So currently we can only do it if the coefficient is 1 or -1. + LOG("values " << a1 << " " << a2); - if (!a1.is_zero() && !a1.is_one() && a1 != minus_one) + if (!coefficient_is_handled(a1)) return false; - if (!a2.is_zero() && !a2.is_one() && a2 != minus_one) + if (!coefficient_is_handled(a2)) return false; + /* unsigned j1 = 0; unsigned j2 = 0; @@ -269,7 +289,9 @@ namespace polysat { // Concrete values of evaluable terms auto e1s = e1.subst_val(s.assignment()); auto e2s = e2.subst_val(s.assignment()); - // TODO: this is not always true! cjust[v]/conflict may contain unassigned variables (they're coming from a previous conflict, but together they lead to a conflict. need something else to handle that.) + // TODO: this is not always true! cjust[v]/conflict may contain unassigned variables + // (they're coming from a previous conflict, but together they lead to a conflict. + // need something else to handle that.) if (!e1s.is_val()) return false; if (!e2s.is_val()) @@ -280,9 +302,9 @@ namespace polysat { bool is_trivial; pdd condition_body = m.zero(); pdd lo = m.zero(); - rational lo_val = rational::zero(); + rational lo_val(0); pdd hi = m.zero(); - rational hi_val = rational::zero(); + rational hi_val(0); if (a2.is_zero()) { SASSERT(!a1.is_zero()); @@ -326,6 +348,8 @@ namespace polysat { } } + _backtrack.released = true; + if (condition_body.is_val()) { // Condition is trivial; no need to create a constraint for that. SASSERT(is_trivial == condition_body.is_zero()); diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index dd6f621a1..fa3aa44a6 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -147,20 +147,26 @@ namespace polysat { auto c2 = s.ule(y, pddm.mk_val(y_lo)); new_constraints.insert(c1); new_constraints.insert(c2); - LOG("bounded " << bound << " : " << c1 << " " << c2); + LOG("bounded " << bound << " : " << x << " " << x_max << " " << y << " " << y_max << " " << c1 << " " << c2); + } + + rational inf_saturate::max_value(pdd const& x) { + if (x.is_var()) + return s.m_viable.max_viable(x.var()); + else if (x.is_val()) + return x.val(); + else + return x.manager().max_value(); } // determine worst case upper bounds for x, y // then extract premises for a non-worst-case bound. void inf_saturate::push_omega(vector& new_constraints, pdd const& x, pdd const& y) { auto& pddm = x.manager(); - rational x_max = pddm.max_value(); - rational y_max = pddm.max_value(); + rational x_max = max_value(x); + rational y_max = max_value(y); - if (x.is_var()) - x_max = s.m_viable.max_viable(x.var()); - if (y.is_var()) - y_max = s.m_viable.max_viable(y.var()); + LOG("pushing " << x << " " << y); if (x_max * y_max > pddm.max_value()) push_omega_bisect(new_constraints, x, x_max, y, y_max); @@ -419,11 +425,13 @@ namespace polysat { new_constraints.push_back(c.as_signed_constraint()); if (c.is_strict) { new_constraints.push_back(s.ule(l_val, c.lhs)); - return propagate(core, c, c, s.ult(r_val, c.rhs), new_constraints); + auto conseq = s.ult(r_val, c.rhs); + return propagate(core, c, c, conseq, new_constraints); } else { new_constraints.push_back(s.ule(c.rhs, r_val)); - return propagate(core, c, c, s.ule(c.lhs, r_val), new_constraints); + auto conseq = s.ule(c.lhs, r_val); + return propagate(core, c, c, conseq, new_constraints); } } diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h index e8aee8be5..cf2cbd773 100644 --- a/src/math/polysat/saturation.h +++ b/src/math/polysat/saturation.h @@ -89,6 +89,8 @@ namespace polysat { // p := coeff*x*y where coeff_x = coeff*x, x a variable bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y); + rational max_value(pdd const& x); + public: inf_saturate(solver& s) : inference_engine(s) {} bool perform(pvar v, conflict& core) override; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index a115b716f..2bc9a4ee9 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -450,9 +450,7 @@ namespace polysat { continue; justification& j = m_justification[v]; LOG("Justification: " << j); - if (j.level() <= base_level()) - break; - if (!resolve_value(v) && j.is_decision()) { + if (j.level() > base_level() && !resolve_value(v) && j.is_decision()) { revert_decision(v); return; } @@ -464,8 +462,8 @@ namespace polysat { sat::bool_var const var = lit.var(); if (!m_conflict.is_bmarked(var)) continue; - if (m_bvars.level(var) <= base_level()) // TODO: this doesn't work with out-of-level-order iteration. - break; + if (m_bvars.level(var) <= base_level()) + continue; if (m_bvars.is_decision(var)) { revert_bool_decision(lit); return; @@ -489,7 +487,7 @@ namespace polysat { */ void solver::resolve_bool(sat::literal lit) { SASSERT(m_bvars.is_propagation(lit.var())); - clause other = *m_bvars.reason(lit.var()); + clause const& other = *m_bvars.reason(lit.var()); LOG_H3("resolve_bool: " << lit << " " << other); m_conflict.resolve(m_constraints, lit, other); } @@ -518,7 +516,8 @@ namespace polysat { SASSERT(!lemma.empty()); lemma.set_justified_var(v); add_lemma(lemma); - decide_bool(lemma); + if (!is_conflict()) + decide_bool(lemma); } // Guess a literal from the given clause; returns the guessed constraint @@ -623,7 +622,8 @@ namespace polysat { clause_builder reason_builder = m_conflict.build_lemma(); - bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit); + SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit)); +#if 0 if (!contains_lit) { // At this point, we do not have ~lit in the reason. // For now, we simply add it (thus weakening the reason) @@ -638,6 +638,7 @@ namespace polysat { std::cout << "ADD extra " << ~lit << "\n"; reason_builder.push(~lit); } +#endif clause_ref reason = reason_builder.build(); if (reason->empty()) { diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp index c6c4bf925..e0667ee26 100644 --- a/src/test/fixplex.cpp +++ b/src/test/fixplex.cpp @@ -389,7 +389,7 @@ namespace polysat { std::cout << " test_lp(rows, ineqs, bounds); \n }\n"; } - static unsigned num_test = 0; + // static unsigned num_test = 0; static void test_lp( vector>> const& rows, @@ -566,9 +566,9 @@ namespace polysat { static void test_lps() { random_gen r; - for (unsigned i = 0; i < 10000; ++i) + for (unsigned i = 0; i < 10000; ++i) test_lps(r, 6, 3, 3, 3); - return; + return; for (unsigned i = 0; i < 10000; ++i) test_lps(r, 6, 3, 3, 0); return; diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index c7d3970bf..40e46a473 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -876,23 +876,27 @@ namespace polysat { } // x*y <= b & a <= x & !Omega(x*y) => a*y <= b - static void test_ineq_non_axiom4(unsigned bw = 32) { + static void test_ineq_non_axiom4(unsigned bw, unsigned i) { auto const bound = rational::power_of_two(bw - 1); - for (unsigned i = 0; i < 24; ++i) { - scoped_solver s(__func__); - auto x = s.var(s.add_var(bw)); - auto y = s.var(s.add_var(bw)); - auto a = s.var(s.add_var(bw)); - auto b = s.var(s.add_var(bw)); - permute_args(i, x, y, a, b); - s.add_ule(x * y, b); - s.add_ule(a, x); - s.add_ult(x, bound); - s.add_ult(y, bound); - s.add_ult(b, a * y); - s.check(); - s.expect_sat(); - } + scoped_solver s(__func__); + LOG("permutation: " << i); + auto x = s.var(s.add_var(bw)); + auto y = s.var(s.add_var(bw)); + auto a = s.var(s.add_var(bw)); + auto b = s.var(s.add_var(bw)); + permute_args(i, x, y, a, b); + s.add_ule(x * y, b); + s.add_ule(a, x); + s.add_ult(x, bound); + s.add_ult(y, bound); + s.add_ult(b, a * y); + s.check(); + s.expect_sat(); + } + + static void test_ineq_non_axiom4(unsigned bw = 32) { + for (unsigned i = 0; i < 24; ++i) + test_ineq_non_axiom4(bw, i); } // a < xy & x <= b & !Omega(x*y) => a < b*y @@ -1063,8 +1067,8 @@ void tst_polysat() { // polysat::test_ineq_axiom1(); // polysat::test_ineq_axiom2(); // polysat::test_ineq_axiom3(); - polysat::test_ineq_non_axiom1(); - polysat::test_ineq_non_axiom4(); + // polysat::test_ineq_non_axiom1(); + polysat::test_ineq_non_axiom4(32, 5); polysat::test_ineq_axiom4(); polysat::test_ineq_axiom5(); polysat::test_ineq_axiom6();