mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 03:15:41 +00:00
Code Activity

fix #3022

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-16 08:14:51 -10:00
parent 19ba2948d1
commit 8c35b2092d
2 changed files with 71 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

138
src/ast/rewriter/bit2int.cpp
View file

@ -24,33 +24,30 @@ Revision History:
#include "ast/for_each_ast.h" #include "ast/for_each_ast.h"
#include "ast/rewriter/bit2int.h" #include "ast/rewriter/bit2int.h"
#define CHECK(_x_) if (!(_x_)) { UNREACHABLE(); }
bit2int::bit2int(ast_manager & m) : bit2int::bit2int(ast_manager & m) :
m_manager(m), m_bv_util(m), m_rewriter(m), m_arith_util(m), m_cache(m), m_bit0(m) { m(m), m_bv_util(m), m_rewriter(m), m_arith_util(m), m_cache(m, false), m_bit0(m) {
m_bit0 = m_bv_util.mk_numeral(0,1); m_bit0 = m_bv_util.mk_numeral(0,1);
} }
void bit2int::operator()(expr * m, expr_ref & result, proof_ref& p) { void bit2int::operator()(expr * n, expr_ref & result, proof_ref& p) {
flush_cache(); flush_cache();
expr_reduce emap(*this); expr_reduce emap(*this);
for_each_ast(emap, m); for_each_ast(emap, n);
result = get_cached(m); result = get_cached(n);
if (m_manager.proofs_enabled() && m != result.get()) { if (m.proofs_enabled() && n != result.get()) {
// TBD: rough // TBD: rough
p = m_manager.mk_rewrite(m, result); p = m.mk_rewrite(n, result);
} }
TRACE("bit2int", TRACE("bit2int",
tout << mk_pp(m, m_manager) << "======>\n" tout << mk_pp(n, m) << "======>\n" << result << "\n";);
<< mk_pp(result, m_manager) << "\n";);
} }
unsigned bit2int::get_b2i_size(expr* n) { unsigned bit2int::get_b2i_size(expr* n) {
SASSERT(m_bv_util.is_bv2int(n)); expr* arg = nullptr;
return m_bv_util.get_bv_size(to_app(n)->get_arg(0)); VERIFY(m_bv_util.is_bv2int(n, arg));
return m_bv_util.get_bv_size(arg);
} }
unsigned bit2int::get_numeral_bits(numeral const& k) { unsigned bit2int::get_numeral_bits(numeral const& k) {
@ -68,28 +65,26 @@ unsigned bit2int::get_numeral_bits(numeral const& k) {
void bit2int::align_size(expr* e, unsigned sz, expr_ref& result) { void bit2int::align_size(expr* e, unsigned sz, expr_ref& result) {
unsigned sz1 = m_bv_util.get_bv_size(e); unsigned sz1 = m_bv_util.get_bv_size(e);
SASSERT(sz1 <= sz); SASSERT(sz1 <= sz);
result = m_rewriter.mk_zero_extend(sz-sz1, e); result = m_rewriter.mk_zero_extend(sz - sz1, e);
} }
void bit2int::align_sizes(expr_ref& a, expr_ref& b) { void bit2int::align_sizes(expr_ref& a, expr_ref& b) {
unsigned sz1 = m_bv_util.get_bv_size(a); unsigned sz1 = m_bv_util.get_bv_size(a);
unsigned sz2 = m_bv_util.get_bv_size(b); unsigned sz2 = m_bv_util.get_bv_size(b);
expr_ref tmp(m_manager);
if (sz1 > sz2) { if (sz1 > sz2) {
tmp = m_rewriter.mk_zero_extend(sz1-sz2, b); b = m_rewriter.mk_zero_extend(sz1 - sz2, b);
b = tmp;
} }
else if (sz2 > sz1) { else if (sz2 > sz1) {
tmp = m_rewriter.mk_zero_extend(sz2-sz1, a); a = m_rewriter.mk_zero_extend(sz2-sz1, a);
a = tmp;
} }
} }
bool bit2int::extract_bv(expr* n, unsigned& sz, bool& sign, expr_ref& bv) { bool bit2int::extract_bv(expr* n, unsigned& sz, bool& sign, expr_ref& bv) {
numeral k; numeral k;
bool is_int; bool is_int;
if (m_bv_util.is_bv2int(n)) { expr* r = nullptr;
bv = to_app(n)->get_arg(0); if (m_bv_util.is_bv2int(n, r)) {
bv = r;
sz = m_bv_util.get_bv_size(bv); sz = m_bv_util.get_bv_size(bv);
sign = false; sign = false;
return true; return true;
@ -109,7 +104,7 @@ bool bit2int::extract_bv(expr* n, unsigned& sz, bool& sign, expr_ref& bv) {
bool bit2int::mk_add(expr* e1, expr* e2, expr_ref& result) { bool bit2int::mk_add(expr* e1, expr* e2, expr_ref& result) {
unsigned sz1, sz2; unsigned sz1, sz2;
bool sign1, sign2; bool sign1, sign2;
expr_ref tmp1(m_manager), tmp2(m_manager), tmp3(m_manager); expr_ref tmp1(m), tmp2(m), tmp3(m);
if (extract_bv(e1, sz1, sign1, tmp1) && !sign1 && if (extract_bv(e1, sz1, sign1, tmp1) && !sign1 &&
extract_bv(e2, sz2, sign2, tmp2) && !sign2) { extract_bv(e2, sz2, sign2, tmp2) && !sign2) {
@ -137,7 +132,7 @@ bool bit2int::mk_add(expr* e1, expr* e2, expr_ref& result) {
bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) { bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) {
unsigned sz1, sz2; unsigned sz1, sz2;
bool sign1, sign2; bool sign1, sign2;
expr_ref tmp1(m_manager), tmp2(m_manager), tmp3(m_manager); expr_ref tmp1(m), tmp2(m), tmp3(m);
if (extract_bv(e1, sz1, sign1, tmp1) && !sign1 && if (extract_bv(e1, sz1, sign1, tmp1) && !sign1 &&
extract_bv(e2, sz2, sign2, tmp2) && !sign2) { extract_bv(e2, sz2, sign2, tmp2) && !sign2) {
align_sizes(tmp1, tmp2); align_sizes(tmp1, tmp2);
@ -145,13 +140,13 @@ bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) {
switch(ty) { switch(ty) {
case lt: case lt:
tmp3 = m_rewriter.mk_ule(tmp2, tmp1); tmp3 = m_rewriter.mk_ule(tmp2, tmp1);
result = m_manager.mk_not(tmp3); result = m.mk_not(tmp3);
break; break;
case le: case le:
result = m_rewriter.mk_ule(tmp1, tmp2); result = m_rewriter.mk_ule(tmp1, tmp2);
break; break;
case eq: case eq:
result = m_manager.mk_eq(tmp1, tmp2); result = m.mk_eq(tmp1, tmp2);
break; break;
} }
return true; return true;
@ -162,8 +157,8 @@ bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) {
bool bit2int::mk_mul(expr* e1, expr* e2, expr_ref& result) { bool bit2int::mk_mul(expr* e1, expr* e2, expr_ref& result) {
unsigned sz1, sz2; unsigned sz1, sz2;
bool sign1, sign2; bool sign1, sign2;
expr_ref tmp1(m_manager), tmp2(m_manager); expr_ref tmp1(m), tmp2(m);
expr_ref tmp3(m_manager); expr_ref tmp3(m);
if (extract_bv(e1, sz1, sign1, tmp1) && if (extract_bv(e1, sz1, sign1, tmp1) &&
extract_bv(e2, sz2, sign2, tmp2)) { extract_bv(e2, sz2, sign2, tmp2)) {
@ -184,7 +179,7 @@ bool bit2int::mk_mul(expr* e1, expr* e2, expr_ref& result) {
bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) { bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
ptr_vector<expr> todo; ptr_vector<expr> todo;
expr_ref tmp(m_manager); expr_ref tmp(m);
numeral k; numeral k;
bool is_int; bool is_int;
todo.push_back(n); todo.push_back(n);
@ -193,41 +188,40 @@ bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
while (!todo.empty()) { while (!todo.empty()) {
n = todo.back(); n = todo.back();
todo.pop_back(); todo.pop_back();
expr* arg1 = nullptr, *arg2 = nullptr;
if (m_bv_util.is_bv2int(n)) { if (m_bv_util.is_bv2int(n)) {
CHECK(mk_add(n, pos, pos)); VERIFY(mk_add(n, pos, pos));
} }
else if (m_arith_util.is_numeral(n, k, is_int) && is_int) { else if (m_arith_util.is_numeral(n, k, is_int) && is_int) {
if (k.is_nonneg()) { if (k.is_nonneg()) {
CHECK(mk_add(n, pos, pos)); VERIFY(mk_add(n, pos, pos));
} }
else { else {
tmp = m_arith_util.mk_numeral(-k, true); tmp = m_arith_util.mk_numeral(-k, true);
CHECK(mk_add(tmp, neg, neg)); VERIFY(mk_add(tmp, neg, neg));
} }
} }
else if (m_arith_util.is_add(n)) { else if (m_arith_util.is_add(n)) {
for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) { for (expr* arg : *to_app(n)) {
todo.push_back(to_app(n)->get_arg(i)); todo.push_back(arg);
} }
} }
else if (m_arith_util.is_mul(n) && else if (m_arith_util.is_mul(n, arg1, arg2) &&
to_app(n)->get_num_args() == 2 && m_arith_util.is_numeral(arg1, k, is_int) && is_int && k.is_minus_one() &&
m_arith_util.is_numeral(to_app(n)->get_arg(0), k, is_int) && is_int && k.is_minus_one() && m_bv_util.is_bv2int(arg2)) {
m_bv_util.is_bv2int(to_app(n)->get_arg(1))) { VERIFY(mk_add(arg2, neg, neg));
CHECK(mk_add(to_app(n)->get_arg(1), neg, neg));
} }
else if (m_arith_util.is_mul(n) && else if (m_arith_util.is_mul(n, arg1, arg2) &&
to_app(n)->get_num_args() == 2 && m_arith_util.is_numeral(arg2, k, is_int) && is_int && k.is_minus_one() &&
m_arith_util.is_numeral(to_app(n)->get_arg(1), k, is_int) && is_int && k.is_minus_one() && m_bv_util.is_bv2int(arg1)) {
m_bv_util.is_bv2int(to_app(n)->get_arg(0))) { VERIFY(mk_add(arg1, neg, neg));
CHECK(mk_add(to_app(n)->get_arg(0), neg, neg));
} }
else if (m_arith_util.is_uminus(n) && else if (m_arith_util.is_uminus(n, arg1) &&
m_bv_util.is_bv2int(to_app(n)->get_arg(0))) { m_bv_util.is_bv2int(arg1)) {
CHECK(mk_add(to_app(n)->get_arg(0), neg, neg)); VERIFY(mk_add(arg1, neg, neg));
} }
else { else {
TRACE("bit2int", tout << "Not a poly: " << mk_pp(n, m_manager) << "\n";); TRACE("bit2int", tout << "Not a poly: " << mk_pp(n, m) << "\n";);
return false; return false;
} }
} }
@ -235,9 +229,9 @@ bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
} }
void bit2int::visit(quantifier* q) { void bit2int::visit(quantifier* q) {
expr_ref result(m_manager); expr_ref result(m);
result = get_cached(q->get_expr()); result = get_cached(q->get_expr());
result = m_manager.update_quantifier(q, result); result = m.update_quantifier(q, result);
cache_result(q, result); cache_result(q, result);
} }
@ -246,21 +240,21 @@ void bit2int::visit(app* n) {
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
m_args.reset(); m_args.reset();
for (unsigned i = 0; i < num_args; ++i) { for (expr* arg : *n) {
m_args.push_back(get_cached(n->get_arg(i))); m_args.push_back(get_cached(arg));
} }
expr* const* args = m_args.c_ptr(); expr* const* args = m_args.c_ptr();
bool has_b2i = bool has_b2i =
m_arith_util.is_le(n) || m_arith_util.is_ge(n) || m_arith_util.is_gt(n) || m_arith_util.is_le(n) || m_arith_util.is_ge(n) || m_arith_util.is_gt(n) ||
m_arith_util.is_lt(n) || m_manager.is_eq(n); m_arith_util.is_lt(n) || m.is_eq(n);
expr_ref result(m_manager); expr_ref result(m);
for (unsigned i = 0; !has_b2i && i < num_args; ++i) { for (unsigned i = 0; !has_b2i && i < num_args; ++i) {
has_b2i = m_bv_util.is_bv2int(args[i]); has_b2i = m_bv_util.is_bv2int(args[i]);
} }
if (!has_b2i) { if (!has_b2i) {
result = m_manager.mk_app(f, num_args, args); result = m.mk_app(f, num_args, args);
cache_result(n, result); cache_result(n, result);
return; return;
} }
@ -274,11 +268,11 @@ void bit2int::visit(app* n) {
// //
expr* e1 = nullptr, *e2 = nullptr; expr* e1 = nullptr, *e2 = nullptr;
expr_ref tmp1(m_manager), tmp2(m_manager); expr_ref tmp1(m), tmp2(m);
expr_ref tmp3(m_manager); expr_ref tmp3(m);
expr_ref pos1(m_manager), neg1(m_manager); expr_ref pos1(m), neg1(m);
expr_ref pos2(m_manager), neg2(m_manager); expr_ref pos2(m), neg2(m);
expr_ref e2bv(m_manager); expr_ref e2bv(m);
bool sign2; bool sign2;
numeral k; numeral k;
unsigned sz2; unsigned sz2;
@ -294,7 +288,7 @@ void bit2int::visit(app* n) {
e1 = result; e1 = result;
e2 = args[i]; e2 = args[i];
if (!mk_add(e1, e2, result)) { if (!mk_add(e1, e2, result)) {
result = m_manager.mk_app(f, num_args, args); result = m.mk_app(f, num_args, args);
cache_result(n, result); cache_result(n, result);
return; return;
} }
@ -307,14 +301,14 @@ void bit2int::visit(app* n) {
e1 = result; e1 = result;
e2 = args[i]; e2 = args[i];
if (!mk_mul(e1, e2, result)) { if (!mk_mul(e1, e2, result)) {
result = m_manager.mk_app(f, num_args, args); result = m.mk_app(f, num_args, args);
cache_result(n, result); cache_result(n, result);
return; return;
} }
} }
cache_result(n, result); cache_result(n, result);
} }
else if (m_manager.is_eq(n) && else if (m.is_eq(n) &&
is_bv_poly(e1, pos1, neg1) && is_bv_poly(e1, pos1, neg1) &&
is_bv_poly(e2, pos2, neg2) && is_bv_poly(e2, pos2, neg2) &&
mk_add(pos1, neg2, tmp1) && mk_add(pos1, neg2, tmp1) &&
@ -362,9 +356,9 @@ void bit2int::visit(app* n) {
// //
unsigned sz_p, sz_n, sz; unsigned sz_p, sz_n, sz;
bool sign_p, sign_n; bool sign_p, sign_n;
expr_ref tmp_p(m_manager), tmp_n(m_manager); expr_ref tmp_p(m), tmp_n(m);
CHECK(extract_bv(pos1, sz_p, sign_p, tmp_p)); VERIFY(extract_bv(pos1, sz_p, sign_p, tmp_p));
CHECK(extract_bv(neg1, sz_n, sign_n, tmp_n)); VERIFY(extract_bv(neg1, sz_n, sign_n, tmp_n));
SASSERT(!sign_p && !sign_n); SASSERT(!sign_p && !sign_n);
// pos1 mod e2 // pos1 mod e2
@ -404,17 +398,21 @@ void bit2int::visit(app* n) {
cache_result(n, result); cache_result(n, result);
} }
else { else {
result = m_manager.mk_app(f, num_args, args); result = m.mk_app(f, num_args, args);
cache_result(n, result); cache_result(n, result);
} }
} }
expr * bit2int::get_cached(expr * n) const { expr * bit2int::get_cached(expr * n) const {
return const_cast<bit2int*>(this)->m_cache.find(n); expr* r = nullptr;
proof* p = nullptr;
const_cast<bit2int*>(this)->m_cache.get(n, r, p);
CTRACE("bit2int", !r, tout << mk_pp(n, m) << "\n";);
return r;
} }
void bit2int::cache_result(expr * n, expr * r) { void bit2int::cache_result(expr * n, expr * r) {
TRACE("bit2int_verbose", tout << "caching:\n" << mk_ll_pp(n, m_manager) << TRACE("bit2int_verbose", tout << "caching:\n" << mk_pp(n, m) <<
"======>\n" << mk_ll_pp(r, m_manager) << "\n";); "======>\n" << mk_ll_pp(r, m) << "\n";);
m_cache.insert(n, r); m_cache.insert(n, r, nullptr);
} }

7
src/ast/rewriter/bit2int.h
View file

@ -21,7 +21,7 @@ Revision History:
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/act_cache.h" #include "ast/expr_map.h"
#include "ast/rewriter/bv_rewriter.h" #include "ast/rewriter/bv_rewriter.h"
class bit2int { class bit2int {
@ -55,8 +55,7 @@ protected:
}; };
typedef act_cache expr_map; ast_manager & m;
ast_manager & m_manager;
bv_util m_bv_util; bv_util m_bv_util;
bv_rewriter m_rewriter; bv_rewriter m_rewriter;
arith_util m_arith_util; arith_util m_arith_util;
@ -80,7 +79,7 @@ protected:
bool is_cached(expr * n) const { return get_cached(n) != nullptr; } bool is_cached(expr * n) const { return get_cached(n) != nullptr; }
void cache_result(expr * n, expr * r); void cache_result(expr * n, expr * r);
void reset_cache() { m_cache.reset(); } void reset_cache() { m_cache.reset(); }
void flush_cache() { m_cache.cleanup(); } void flush_cache() { m_cache.flush(); }
void align_size(expr* e, unsigned sz, expr_ref& result); void align_size(expr* e, unsigned sz, expr_ref& result);
void align_sizes(expr_ref& a, expr_ref& b); void align_sizes(expr_ref& a, expr_ref& b);