mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity

normalizing inequality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-27 22:23:01 -07:00
parent 9a5fa60e98
commit 7e9d0537d7
3 changed files with 38 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/ast/rewriter/bv2int_translator.cpp
View file

@ -183,6 +183,20 @@ void bv2int_translator::translate_app(app* e) {
set_translated(e, m.mk_app(f, m_args));
}
expr_ref bv2int_translator::mk_le(expr* x, expr* y) {
if (a.is_numeral(y))
return expr_ref(a.mk_le(x, y), m);
if (a.is_numeral(x))
return expr_ref(a.mk_ge(y, x), m);
return expr_ref(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), x->get_sort())), m);
}
expr_ref bv2int_translator::mk_lt(expr* x, expr* y) {
return expr_ref(m.mk_not(mk_le(y, x)), m);
}
void bv2int_translator::translate_bv(app* e) {
auto bnot = [&](expr* e) {
@ -229,35 +243,35 @@ void bv2int_translator::translate_bv(app* e) {
break;
case OP_ULEQ:
bv_expr = e->get_arg(0);
r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
r = mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_UGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
r = mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_ULT:
bv_expr = e->get_arg(0);
r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
r = mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_UGT:
bv_expr = e->get_arg(0);
r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
r = mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
break;
case OP_SLEQ:
bv_expr = e->get_arg(0);
r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
r = mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
r = mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SLT:
bv_expr = e->get_arg(0);
r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
r = mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_SGT:
bv_expr = e->get_arg(0);
r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
r = mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
break;
case OP_BNEG:
r = a.mk_uminus(arg(0));
@ -308,7 +322,7 @@ void bv2int_translator::translate_bv(app* e) {
}
case OP_BUMUL_NO_OVFL: {
bv_expr = e->get_arg(0);
r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
r = mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
break;
}
case OP_BSHL: {

5
src/ast/rewriter/bv2int_translator.h
View file

@ -47,6 +47,11 @@ class bv2int_translator {
expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
expr* amod(expr* bv_expr, expr* x, rational const& N);
rational bv_size(expr* bv_expr);
expr_ref mk_le(expr* a, expr* b);
expr_ref mk_lt(expr* a, expr* b);
expr_ref mk_ge(expr* a, expr* b) { return mk_le(b, a); }
expr_ref mk_gt(expr* a, expr* b) { return mk_lt(b, a); }
void translate_bv(app* e);
void translate_basic(app* e);

12
src/smt/theory_lra.cpp
View file

@ -2573,6 +2573,14 @@ public:
return true;
}
expr_ref mk_le(expr* x, expr* y) {
if (a.is_numeral(y))
return expr_ref(a.mk_le(x, y), m);
if (a.is_numeral(x))
return expr_ref(a.mk_ge(y, x), m);
return expr_ref(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), x->get_sort())), m);
}
void mk_bv_axiom(app* n) {
unsigned sz = 0;
expr* _x = nullptr, * _y = nullptr;
@ -2592,8 +2600,8 @@ public:
// x&y <= y
// TODO? x = y => x&y = x
ctx().mk_th_axiom(get_id(), mk_literal(a.mk_le(n, x)));
ctx().mk_th_axiom(get_id(), mk_literal(a.mk_le(n, y)));
ctx().mk_th_axiom(get_id(), mk_literal(mk_le(n, x)));
ctx().mk_th_axiom(get_id(), mk_literal(mk_le(n, y)));
}
else if (a.is_shl(n)) {
// y >= sz => n = 0