From a6e08b22f8d9d1ac28eb9c66f6b424314c665a77 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 14:54:20 -0800 Subject: [PATCH] add rewrites for band Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 29 +++++++++++++++++++++++++++ src/ast/rewriter/arith_rewriter.h | 1 + src/sat/smt/polysat/op_constraint.cpp | 14 ++++++------- 3 files changed, 37 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 44b91826f..ddfabed83 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -91,6 +91,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_SINH: SASSERT(num_args == 1); st = mk_sinh_core(args[0], result); break; case OP_COSH: SASSERT(num_args == 1); st = mk_cosh_core(args[0], result); break; case OP_TANH: SASSERT(num_args == 1); st = mk_tanh_core(args[0], result); break; + case OP_ARITH_BAND: SASSERT(num_args == 2); st = mk_band_core(f->get_parameter(0).get_int(), args[0], args[1], result); break; default: st = BR_FAILED; break; } CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m); @@ -1349,6 +1350,34 @@ app* arith_rewriter_core::mk_power(expr* x, rational const& r, sort* s) { return y; } +br_status arith_rewriter::mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result) { + numeral x, y, N; + bool is_num_x = m_util.is_numeral(arg1, x); + bool is_num_y = m_util.is_numeral(arg2, y); + N = rational::power_of_two(sz); + if (is_num_x) + x = mod(x, N); + if (is_num_y) + y = mod(y, N); + if (is_num_x && x.is_zero()) { + result = m_util.mk_int(0); + return BR_DONE; + } + if (is_num_y && y.is_zero()) { + result = m_util.mk_int(0); + return BR_DONE; + } + if (is_num_x && is_num_y) { + rational r(0); + for (unsigned i = 0; i < sz; ++i) + if (x.get_bit(i) && y.get_bit(i)) + r += rational::power_of_two(i); + result = m_util.mk_int(r); + return BR_DONE; + } + return BR_FAILED; +} + br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & result) { numeral x, y; bool is_num_x = m_util.is_numeral(arg1, x); diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index edc84b25a..548ab80db 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -159,6 +159,7 @@ public: br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result); + br_status mk_band_core(unsigned sz, expr* arg1, expr* arg2, expr_ref& result); void mk_div(expr * arg1, expr * arg2, expr_ref & result) { if (mk_div_core(arg1, arg2, result) == BR_FAILED) result = m.mk_app(get_fid(), OP_DIV, arg1, arg2); diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index 666d950a9..713b9d6ef 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -319,15 +319,12 @@ namespace polysat { // auto& m = p.manager(); - auto const pv = c.subst(p); - auto const qv = c.subst(q); - auto const rv = c.subst(r); unsigned const N = m.power_of_2(); auto& C = c.cs(); - c.add_clause("q >= N & p < 0 -> p << q = -1", {~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value())}, true); - c.add_clause("q >= N & p >= 0 -> p << q = 0", {~C.uge(q, N), ~C.sge(p, 0), C.eq(r)}, true); - c.add_clause("q = 0 -> p << q = p", { ~C.eq(q), C.eq(r, p) }, true); + c.add_clause("q >= N & p < 0 -> p << q = -1", {~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value())}, false); + c.add_clause("q >= N & p >= 0 -> p << q = 0", {~C.uge(q, N), ~C.sge(p, 0), C.eq(r)}, false); + c.add_clause("q = 0 -> p << q = p", { ~C.eq(q), C.eq(r, p) }, false); for (unsigned k = 0; k < N; ++k) { // c.add_clause("q = k & p >= 0 -> p << q = p / 2^k", {~C.eq(q, k), ~C.sge(p, 0), ... }, true); // c.add_clause("q = k & p < 0 -> p << q = (p / 2^k) -1 + 2^{N-k}", {~C.eq(q, k), ~C.slt(p, 0), ... }, true); @@ -338,6 +335,10 @@ namespace polysat { void op_constraint::activate_and(core& c, dependency const& d) { auto x = p, y = q; auto& C = c.cs(); + + c.add_clause("band-mask p&q <= p", { C.ule(r, p) }, false); + c.add_clause("band-mask p&q <= q", { C.ule(r, q) }, false); + if (x.is_val()) std::swap(x, y); if (!y.is_val()) @@ -356,7 +357,6 @@ namespace polysat { SASSERT(k < N); rational exp = rational::power_of_two(N - k); c.add_clause("band-mask 1", { C.eq(x * exp, r * exp) }, false); - c.add_clause("band-mask 2", { C.ule(r, y) }, false); // maybe always activate these constraints regardless? } }