mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

add first test for band

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-18 12:28:59 -08:00
parent 8f8d88bc9d
commit c1d5111159
6 changed files with 81 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/constraint.cpp
View file

@ -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)

1
src/math/polysat/constraint.h
View file

@ -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(); }

7
src/math/polysat/op_constraint.cpp
View file

@ -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());

52
src/math/polysat/solver.cpp
View file

@ -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) {

6
src/math/polysat/solver.h
View file

@ -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.
*/

38
src/test/polysat.cpp
View file

@ -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;