From a4fc63c542256f78a62e9f2c03f97dbb36f6ab5d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Dec 2021 14:39:00 -0800 Subject: [PATCH] initial overflow test Signed-off-by: Nikolaj Bjorner --- src/math/polysat/constraint.cpp | 3 +++ src/math/polysat/constraint.h | 1 + src/math/polysat/mul_ovfl_constraint.cpp | 20 ++++++++++++++------ src/math/polysat/solver.h | 10 +++++++++- src/math/polysat/viable.cpp | 2 +- src/test/polysat.cpp | 19 +++++++++++++++++++ 6 files changed, 47 insertions(+), 8 deletions(-) diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 7bf6c97d3..dfa28a64b 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -202,6 +202,9 @@ namespace polysat { return ~ule(b, a); } + signed_constraint constraint_manager::mul_ovfl(pdd const& a, pdd const& b) { + return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true }; + } // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 8cead94e4..612eb5e94 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -94,6 +94,7 @@ namespace polysat { signed_constraint ult(pdd const& a, pdd const& b); signed_constraint sle(pdd const& a, pdd const& b); signed_constraint slt(pdd const& a, pdd const& b); + signed_constraint mul_ovfl(pdd const& p, pdd const& q); constraint *const* begin() const { return m_constraints.data(); } constraint *const* end() const { return m_constraints.data() + m_constraints.size(); } diff --git a/src/math/polysat/mul_ovfl_constraint.cpp b/src/math/polysat/mul_ovfl_constraint.cpp index 5ff5cb8a8..f0e32c011 100644 --- a/src/math/polysat/mul_ovfl_constraint.cpp +++ b/src/math/polysat/mul_ovfl_constraint.cpp @@ -18,7 +18,6 @@ namespace polysat { mul_ovfl_constraint::mul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q): constraint(m, ckind_t::mul_ovfl_t), m_p(p), m_q(q) { - simplify(); m_vars.append(m_p.free_vars()); for (auto v : m_q.free_vars()) @@ -33,6 +32,8 @@ namespace polysat { m_p = 0; return; } + if (m_p.index() > m_q.index()) + std::swap(m_p, m_q); } std::ostream& mul_ovfl_constraint::display(std::ostream& out, lbool status) const { @@ -104,8 +105,6 @@ namespace polysat { * TODO optimizations: * if p is constant, q variable, update viable for q * - * Use bounds on variables in p instead of current assignment as premise. - * This is a more general lemma */ bool mul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) { @@ -118,22 +117,31 @@ namespace polysat { // p * q >= max + 1 <=> q >= (max + 1)/p <=> q >= ceil((max+1)/p) auto bound = ceil((max + 1) / p.val()); + // // the clause that explains bound <= q or bound > q // // Ovfl(p, q) & p <= p.val() => q >= bound - // ~Ovfl(p, q) & p >= p.val() => q < bound + // ~Ovfl(p, q) & p >= p.val() => q < bound + // signed_constraint sc(this, is_positive); signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0); signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound); - SASSERT(premise.is_currently_false(s)); + //std::cout << premise << "\n"; + //std::cout << sc << "\n"; + //std::cout << conseq << "\n"; + //std::cout << "Already true " << conseq.is_currently_true(s) << "\n"; + + SASSERT(premise.is_currently_true(s)); clause_builder cb(s); cb.push_new(~sc); cb.push_new(~premise); cb.push_new(conseq); clause_ref just = cb.build(); - s.assign_propagate(conseq.blit(), *just); + s.add_lemma(*just); + s.propagate(); + SASSERT(s.m_bvars.is_true(conseq.blit())); return true; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ce2defd92..1cc5c30f4 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -289,6 +289,8 @@ namespace polysat { signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); } signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); } signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); } + signed_constraint mul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); } + signed_constraint mul_ovfl(rational const& p, pdd const& q) { return mul_ovfl(q.manager().mk_val(p), q); } /** Create and activate polynomial constraints. */ @@ -298,6 +300,8 @@ namespace polysat { void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ult(p, q), dep); } void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(sle(p, q), dep); } void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(slt(p, q), dep); } + void add_noovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); } + void add_ovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } void add_ule(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); } void add_ule(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); } @@ -307,7 +311,11 @@ namespace polysat { void add_ult(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); } void add_ult(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ult(p, rational(q), dep); } void add_ult(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ult(rational(p), q, dep); } - + void add_noovfl(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); } + void add_noovfl(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); } + void add_noovfl(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_noovfl(p, rational(q), dep); } + void add_noovfl(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); } + /** * Activate the constraint corresponding to the given boolean variable. * Note: to deactivate, use push/pop. diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 7a71a2d48..e429ae314 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -197,8 +197,8 @@ namespace polysat { rational lambda_l = floor(coeff_val / e->coeff); lo = val - lambda_l; } - SASSERT(hi <= s.var2pdd(v).max_value()); LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "["); + SASSERT(hi <= max_value); entry* ne = alloc_entry(); ne->src = e->src; ne->side_cond = e->side_cond; diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 65cac43f4..2bb1c124b 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -940,6 +940,22 @@ namespace polysat { } } + static void test_quot_rem(unsigned bw = 32) { + scoped_solver s(__func__); + auto a = s.var(s.add_var(bw)); + auto quot = s.var(s.add_var(bw)); + auto rem = s.var(s.add_var(bw)); + auto x = a * 123; + auto y = 123; + // quot = udiv(a*123, 123) + s.add_eq(quot * y + rem - x); + s.add_diseq(a - quot); + s.add_noovfl(quot, y); + // s.add_ult(rem, x); + s.check(); + s.expect_sat(); + } + // 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) @@ -1065,6 +1081,9 @@ namespace polysat { void tst_polysat() { + polysat::test_quot_rem(); + return; + polysat::test_ineq_axiom1(); polysat::test_ineq_axiom2(); polysat::test_ineq_axiom3();