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

add rewrites for band

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-15 14:54:20 -08:00
parent d0b03a1526
commit a6e08b22f8
3 changed files with 37 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ast/rewriter/arith_rewriter.cpp
View file

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

1
src/ast/rewriter/arith_rewriter.h
View file

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

14
src/sat/smt/polysat/op_constraint.cpp
View file

@ -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?
}
}