diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 90dd11ce2..b7035ef23 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -237,6 +237,10 @@ namespace polysat { return { dedup(alloc(op_constraint, *this, op_constraint::code::lshr_op, p, q, r)), true }; } + signed_constraint constraint_manager::band(pdd const& p, pdd const& q, pdd const& r) { + return { dedup(alloc(op_constraint, *this, op_constraint::code::and_op, p, q, r)), true }; + } + // To do signed comparison of bitvectors, flip the msb and do unsigned comparison: // // x <=s y <=> x + 2^(w-1) <=u y + 2^(w-1) diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index a1103bdad..3f8e9d73d 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -98,6 +98,7 @@ namespace polysat { signed_constraint mul_ovfl(pdd const& p, pdd const& q); signed_constraint bit(pdd const& p, unsigned i); signed_constraint lshr(pdd const& p, pdd const& q, pdd const& r); + signed_constraint band(pdd const& p, pdd const& q, pdd const& r); 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/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 76def0808..f62a76afa 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -191,6 +191,9 @@ namespace polysat { rv.val() > rational::power_of_two(K - qv.val().get_unsigned() - 1)) // q >= k -> r <= 2^{K-k-1} s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned() - 1)), true); + else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) + // q >= K -> r = 0 + s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true); // q = k -> r[i - k] = p[i] for K - k <= i < K else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) { unsigned k = qv.val().get_unsigned(); @@ -232,6 +235,10 @@ namespace polysat { * p = 0 => r = 0 * q = 0 => r = 0 * p[i] && q[i] = r[i] + * + * Possible other: + * p = max_value => q = r + * q = max_value => p = r */ void op_constraint::narrow_and(solver& s) { auto pv = p().subst_val(s.assignment()); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 3c6cd2118..0d3266f24 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -143,6 +143,14 @@ namespace polysat { return r; } + pdd solver::band(pdd const& p, pdd const& q) { + auto& m = p.manager(); + unsigned sz = m.power_of_2(); + pdd r = m.mk_var(add_var(sz)); + assign_eh(m_constraints.band(p, q, r), null_dependency); + return r; + } + void solver::assign_eh(signed_constraint c, unsigned dep) { SASSERT(at_base_level()); @@ -782,43 +790,33 @@ namespace polysat { propagate(); } - void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) { + void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) { clause_builder cb(*this); - if (!c1.is_always_false()) - cb.push(c1); - if (!c2.is_always_false()) - cb.push(c2); + for (unsigned i = 0; i < n; ++i) { + signed_constraint c = cs[i]; + if (c.is_always_false()) + continue; + m_constraints.ensure_bvar(c.get()); + cb.push(c); + } clause_ref clause = cb.build(); clause->set_redundant(is_redundant); add_clause(*clause); } + void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) { + signed_constraint cs[2] = { c1, c2 }; + add_clause(2, cs, is_redundant); + } + void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) { - clause_builder cb(*this); - if (!c1.is_always_false()) - cb.push(c1); - if (!c2.is_always_false()) - cb.push(c2); - if (!c3.is_always_false()) - cb.push(c3); - clause_ref clause = cb.build(); - clause->set_redundant(is_redundant); - add_clause(*clause); + signed_constraint cs[3] = { c1, c2, c3 }; + add_clause(3, cs, is_redundant); } void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant) { - clause_builder cb(*this); - if (!c1.is_always_false()) - cb.push(c1); - if (!c2.is_always_false()) - cb.push(c2); - if (!c3.is_always_false()) - cb.push(c3); - if (!c4.is_always_false()) - cb.push(c4); - clause_ref clause = cb.build(); - clause->set_redundant(is_redundant); - add_clause(*clause); + signed_constraint cs[4] = { c1, c2, c3, c4 }; + add_clause(4, cs, is_redundant); } void solver::insert_constraint(signed_constraints& cs, signed_constraint c) { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 90a4ccf9c..35231273c 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -210,6 +210,7 @@ namespace polysat { void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant); void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant); void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant); + void add_clause(unsigned n, signed_constraint* cs, bool is_redundant); signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); } @@ -275,6 +276,11 @@ namespace polysat { */ pdd lshr(pdd const& p, pdd const& q); + /** + * Create expression for bit-wise and of p by q. + */ + pdd band(pdd const& p, pdd const& q); + /** * Create polynomial constant. */ diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 181e92826..4a432401a 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -979,6 +979,34 @@ namespace polysat { s.check(); } + static void test_band(unsigned bw = 32) { + { + scoped_solver s(__func__); + auto p = s.var(s.add_var(bw)); + auto q = s.var(s.add_var(bw)); + s.add_ult(p, s.band(p, q)); + s.check(); + s.expect_unsat(); + } + { + scoped_solver s(__func__); + auto p = s.var(s.add_var(bw)); + auto q = s.var(s.add_var(bw)); + s.add_ult(q, s.band(p, q)); + s.check(); + s.expect_unsat(); + } + { + scoped_solver s(__func__); + auto p = s.var(s.add_var(bw)); + auto q = s.var(s.add_var(bw)); + s.add_ule(p, s.band(p, q)); + 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) @@ -1036,6 +1064,13 @@ namespace polysat { auto pb = to_pdd(m, s, expr2pdd, b); r = alloc(pdd, s.lshr(pa, pb)); } + else if (bv.is_bv_and(e) && to_app(e)->get_num_args() == 2) { + a = to_app(e)->get_arg(0); + b = to_app(e)->get_arg(1); + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + r = alloc(pdd, s.lshr(pa, pb)); + } else if (bv.is_numeral(e, n, sz)) r = alloc(pdd, s.value(n, sz)); else if (is_uninterp(e)) @@ -1106,6 +1141,9 @@ namespace polysat { void tst_polysat() { + polysat::test_band(); + return; + polysat::test_quot_rem(); return;