From f7ca7409cec5ce622725a9e35eb3ff935bdc890e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Aug 2017 17:05:40 -0700 Subject: [PATCH] fix regressions introduced when modifying macro_util Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_util.cpp | 13 +++++----- src/ast/macros/macro_util.h | 4 +-- src/smt/smt_model_finder.cpp | 48 +++++++++++++++++++++++------------ 3 files changed, 41 insertions(+), 24 deletions(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index b7eb9657f..6bc1ee66e 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -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 { if (is_bv(t1)) { - r = m_bv.mk_bv_sub(t1, t2); + m_bv_rw.mk_sub(t1, t2, r); } 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 { if (is_bv(t1)) { - r = m_bv.mk_bv_add(t1, t2); + m_bv_rw.mk_add(t1, t2, r); } 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); tmp = m_arith.mk_add(args.size(), args.c_ptr()); if (inv) - def = m_arith.mk_sub(tmp, rhs); + mk_sub(tmp, rhs, def); else - def = m_arith.mk_sub(rhs, tmp); + mk_sub(rhs, tmp, def); + TRACE("macro_util", tout << def << "\n";); return true; } diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index 91d96cc5e..3ab00df2a 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -60,8 +60,8 @@ private: ast_manager & m_manager; bv_util m_bv; arith_util m_arith; - arith_rewriter m_arith_rw; - bv_rewriter m_bv_rw; + mutable arith_rewriter m_arith_rw; + mutable bv_rewriter m_bv_rw; obj_hashtable * m_forbidden_set; bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 2e6a34557..f678ee3e7 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -755,11 +755,13 @@ namespace smt { arith_rewriter arw(m); bv_rewriter brw(m); ptr_vector const & exceptions = n->get_exceptions(); + expr_ref e_minus_1(m), e_plus_1(m); if (m_arith.is_int(s)) { expr_ref one(m_arith.mk_int(1), m); + arith_rewriter arith_rw(m); for (expr * e : exceptions) { - expr_ref e_plus_1(m_arith.mk_add(e, one), m); - expr_ref e_minus_1(m_arith.mk_sub(e, one), m); + arith_rw.mk_sub(e, one, e_minus_1); + 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";); // Note: exceptions come from quantifiers bodies. So, they have generation 0. n->insert(e_plus_1, 0); @@ -768,9 +770,10 @@ namespace smt { } else if (m_bv.is_bv_sort(s)) { expr_ref one(m_bv.mk_numeral(rational(1), s), m); + bv_rewriter bv_rw(m); for (expr * e : exceptions) { - expr_ref e_plus_1(m_bv.mk_bv_add(e, one), m); - expr_ref e_minus_1(m_bv.mk_bv_sub(e, one), m); + bv_rw.mk_add(e, one, e_plus_1); + 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";); // Note: exceptions come from quantifiers bodies. So, they have generation 0. n->insert(e_plus_1, 0); @@ -806,7 +809,7 @@ namespace smt { numeral_lt(T& a): m_util(a) {} bool operator()(expr* e1, expr* e2) { 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; } else { @@ -1260,15 +1263,16 @@ namespace smt { for (; it != end; it++) { enode * n = *it; 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_rewriter bv_rw(ctx->get_manager()); enode * e_arg = n->get_arg(m_arg_i); expr * arg = e_arg->get_owner(); expr_ref arg_minus_k(ctx->get_manager()); - if (bv.is_bv(arg)) - arg_minus_k = bv.mk_bv_sub(arg, m_offset); + if (bv.is_bv(arg)) + bv_rw.mk_sub(arg, m_offset, arg_minus_k); 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()); } } @@ -1291,17 +1295,29 @@ namespace smt { instantiation_set const * from_s = from->get_instantiation_set(); obj_map const & elems_s = from_s->get_elems(); - arith_util arith(m_offset.get_manager()); - bv_util bv(m_offset.get_manager()); - bool is_bv = bv.is_bv_sort(from->get_sort()); + arith_rewriter arith_rw(m_offset.get_manager()); + bv_rewriter bv_rw(m_offset.get_manager()); + bool is_bv = bv_util(m_offset.get_manager()).is_bv_sort(from->get_sort()); for (auto const& kv : elems_s) { expr * n = kv.m_key; expr_ref n_k(m_offset.get_manager()); - if (PLUS) - n_k = is_bv ? bv.mk_bv_add(n, m_offset) : arith.mk_add(n, m_offset); - else - n_k = is_bv ? bv.mk_bv_sub(n, m_offset) : arith.mk_sub(n, m_offset); + if (PLUS) { + if (is_bv) { + bv_rw.mk_add(n, m_offset, n_k); + } + 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); } }