mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix regressions introduced when modifying macro_util

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-22 17:05:40 -07:00
parent e2b46257d6
commit f7ca7409ce
3 changed files with 41 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/macros/macro_util.cpp
View file

@ -105,19 +105,19 @@ app * macro_util::mk_zero(sort * s) const {
void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const { void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
if (is_bv(t1)) { if (is_bv(t1)) {
r = m_bv.mk_bv_sub(t1, t2); m_bv_rw.mk_sub(t1, t2, r);
} }
else { else {
r = m_arith.mk_sub(t1, t2); m_arith_rw.mk_sub(t1, t2, r);
} }
} }
void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const { void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
if (is_bv(t1)) { if (is_bv(t1)) {
r = m_bv.mk_bv_add(t1, t2); m_bv_rw.mk_add(t1, t2, r);
} }
else { else {
r = m_arith.mk_add(t1, t2); m_arith_rw.mk_add(t1, t2, r);
} }
} }
@ -312,9 +312,10 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
expr_ref tmp(m_manager); expr_ref tmp(m_manager);
tmp = m_arith.mk_add(args.size(), args.c_ptr()); tmp = m_arith.mk_add(args.size(), args.c_ptr());
if (inv) if (inv)
def = m_arith.mk_sub(tmp, rhs); mk_sub(tmp, rhs, def);
else else
def = m_arith.mk_sub(rhs, tmp); mk_sub(rhs, tmp, def);
TRACE("macro_util", tout << def << "\n";);
return true; return true;
} }

4
src/ast/macros/macro_util.h
View file

@ -60,8 +60,8 @@ private:
ast_manager & m_manager; ast_manager & m_manager;
bv_util m_bv; bv_util m_bv;
arith_util m_arith; arith_util m_arith;
arith_rewriter m_arith_rw; mutable arith_rewriter m_arith_rw;
bv_rewriter m_bv_rw; mutable bv_rewriter m_bv_rw;
obj_hashtable<func_decl> * m_forbidden_set; obj_hashtable<func_decl> * m_forbidden_set;
bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); } bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }

46
src/smt/smt_model_finder.cpp
View file

@ -755,11 +755,13 @@ namespace smt {
arith_rewriter arw(m); arith_rewriter arw(m);
bv_rewriter brw(m); bv_rewriter brw(m);
ptr_vector<expr> const & exceptions = n->get_exceptions(); ptr_vector<expr> const & exceptions = n->get_exceptions();
expr_ref e_minus_1(m), e_plus_1(m);
if (m_arith.is_int(s)) { if (m_arith.is_int(s)) {
expr_ref one(m_arith.mk_int(1), m); expr_ref one(m_arith.mk_int(1), m);
arith_rewriter arith_rw(m);
for (expr * e : exceptions) { for (expr * e : exceptions) {
expr_ref e_plus_1(m_arith.mk_add(e, one), m); arith_rw.mk_sub(e, one, e_minus_1);
expr_ref e_minus_1(m_arith.mk_sub(e, one), m); arith_rw.mk_add(e, one, e_plus_1);
TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";); TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";);
// Note: exceptions come from quantifiers bodies. So, they have generation 0. // Note: exceptions come from quantifiers bodies. So, they have generation 0.
n->insert(e_plus_1, 0); n->insert(e_plus_1, 0);
@ -768,9 +770,10 @@ namespace smt {
} }
else if (m_bv.is_bv_sort(s)) { else if (m_bv.is_bv_sort(s)) {
expr_ref one(m_bv.mk_numeral(rational(1), s), m); expr_ref one(m_bv.mk_numeral(rational(1), s), m);
bv_rewriter bv_rw(m);
for (expr * e : exceptions) { for (expr * e : exceptions) {
expr_ref e_plus_1(m_bv.mk_bv_add(e, one), m); bv_rw.mk_add(e, one, e_plus_1);
expr_ref e_minus_1(m_bv.mk_bv_sub(e, one), m); bv_rw.mk_sub(e, one, e_minus_1);
TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";); TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";);
// Note: exceptions come from quantifiers bodies. So, they have generation 0. // Note: exceptions come from quantifiers bodies. So, they have generation 0.
n->insert(e_plus_1, 0); n->insert(e_plus_1, 0);
@ -806,7 +809,7 @@ namespace smt {
numeral_lt(T& a): m_util(a) {} numeral_lt(T& a): m_util(a) {}
bool operator()(expr* e1, expr* e2) { bool operator()(expr* e1, expr* e2) {
rational v1, v2; rational v1, v2;
if (m_util.is_numeral(e1, v1) && m_util.is_numeral(e2, v1)) { if (m_util.is_numeral(e1, v1) && m_util.is_numeral(e2, v2)) {
return v1 < v2; return v1 < v2;
} }
else { else {
@ -1260,15 +1263,16 @@ namespace smt {
for (; it != end; it++) { for (; it != end; it++) {
enode * n = *it; enode * n = *it;
if (ctx->is_relevant(n)) { if (ctx->is_relevant(n)) {
arith_util arith(ctx->get_manager()); arith_rewriter arith_rw(ctx->get_manager());
bv_util bv(ctx->get_manager()); bv_util bv(ctx->get_manager());
bv_rewriter bv_rw(ctx->get_manager());
enode * e_arg = n->get_arg(m_arg_i); enode * e_arg = n->get_arg(m_arg_i);
expr * arg = e_arg->get_owner(); expr * arg = e_arg->get_owner();
expr_ref arg_minus_k(ctx->get_manager()); expr_ref arg_minus_k(ctx->get_manager());
if (bv.is_bv(arg)) if (bv.is_bv(arg))
arg_minus_k = bv.mk_bv_sub(arg, m_offset); bv_rw.mk_sub(arg, m_offset, arg_minus_k);
else else
arg_minus_k = arith.mk_sub(arg, m_offset); arith_rw.mk_sub(arg, m_offset, arg_minus_k);
S_j->insert(arg_minus_k, e_arg->get_generation()); S_j->insert(arg_minus_k, e_arg->get_generation());
} }
} }
@ -1291,17 +1295,29 @@ namespace smt {
instantiation_set const * from_s = from->get_instantiation_set(); instantiation_set const * from_s = from->get_instantiation_set();
obj_map<expr, unsigned> const & elems_s = from_s->get_elems(); obj_map<expr, unsigned> const & elems_s = from_s->get_elems();
arith_util arith(m_offset.get_manager()); arith_rewriter arith_rw(m_offset.get_manager());
bv_util bv(m_offset.get_manager()); bv_rewriter bv_rw(m_offset.get_manager());
bool is_bv = bv.is_bv_sort(from->get_sort()); bool is_bv = bv_util(m_offset.get_manager()).is_bv_sort(from->get_sort());
for (auto const& kv : elems_s) { for (auto const& kv : elems_s) {
expr * n = kv.m_key; expr * n = kv.m_key;
expr_ref n_k(m_offset.get_manager()); expr_ref n_k(m_offset.get_manager());
if (PLUS) if (PLUS) {
n_k = is_bv ? bv.mk_bv_add(n, m_offset) : arith.mk_add(n, m_offset); if (is_bv) {
else bv_rw.mk_add(n, m_offset, n_k);
n_k = is_bv ? bv.mk_bv_sub(n, m_offset) : arith.mk_sub(n, m_offset); }
else {
arith_rw.mk_add(n, m_offset, n_k);
}
}
else {
if (is_bv) {
bv_rw.mk_sub(n, m_offset, n_k);
}
else {
arith_rw.mk_sub(n, m_offset, n_k);
}
}
to->insert(n_k, kv.m_value); to->insert(n_k, kv.m_value);
} }
} }