From 3f3bd5948fbb2e20e5839d96ea32b8fcf8a01c30 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Nov 2021 14:48:19 -0700 Subject: [PATCH] fixes/debugging Signed-off-by: Nikolaj Bjorner --- src/math/polysat/explain.cpp | 4 +--- src/math/polysat/saturation.cpp | 20 +++++++++++------ src/math/polysat/saturation.h | 2 ++ src/math/polysat/solver.cpp | 5 +++-- src/test/polysat.cpp | 40 ++++++++++++++++++--------------- 5 files changed, 41 insertions(+), 30 deletions(-) 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/saturation.cpp b/src/math/polysat/saturation.cpp index dd6f621a1..67e023963 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); 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..d938dfcc4 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -489,7 +489,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 +518,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 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();