From 799fb4a0d1e9b21a8af15759ecae4353dbb5d6bd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 24 Aug 2017 21:26:09 +0100 Subject: [PATCH] Revert "Eliminated the dependency of the macro-finder on the simplifier." This reverts commit 8310b24c521b6dac99a97a61ab74115c377db1b2. --- src/ast/macros/macro_finder.cpp | 43 ++++++------ src/ast/macros/macro_finder.h | 17 +++-- src/ast/macros/macro_manager.cpp | 2 +- src/ast/macros/macro_util.cpp | 106 ++++++++++++++++++------------ src/ast/macros/macro_util.h | 25 +++---- src/ast/rewriter/arith_rewriter.h | 20 +++--- src/ast/rewriter/poly_rewriter.h | 57 ---------------- src/smt/smt_model_finder.cpp | 37 ++++++----- 8 files changed, 139 insertions(+), 168 deletions(-) diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp index 604d10b04..285c0e5fb 100644 --- a/src/ast/macros/macro_finder.cpp +++ b/src/ast/macros/macro_finder.cpp @@ -21,9 +21,8 @@ Revision History: #include "ast/occurs.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" -#include "ast/rewriter/arith_rewriter.h" -bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const { +bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) { if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) return false; TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";); @@ -33,30 +32,30 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const { } /** - \brief Detect macros of the form + \brief Detect macros of the form 1- (forall (X) (= (+ (f X) (R X)) c)) 2- (forall (X) (<= (+ (f X) (R X)) c)) 3- (forall (X) (>= (+ (f X) (R X)) c)) The second and third cases are first converted into (forall (X) (= (f X) (+ c (* -1 (R x)) (k X)))) - and + and (forall (X) (<= (k X) 0)) when case 2 (forall (X) (>= (k X) 0)) when case 3 For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs. */ -bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const { +bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { if (!is_quantifier(n) || !to_quantifier(n)->is_forall()) return false; - arith_rewriter & arw = m_util.get_arith_rw(); - arith_util & au = m_util.get_arith_util(); + arith_simplifier_plugin * as = get_arith_simp(); + arith_util & autil = as->get_arith_util(); expr * body = to_quantifier(n)->get_expr(); unsigned num_decls = to_quantifier(n)->get_num_decls(); - - if (!au.is_le(body) && !au.is_ge(body) && !m_manager.is_eq(body)) + + if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body)) return false; - if (!au.is_add(to_app(body)->get_arg(0))) + if (!as->is_add(to_app(body)->get_arg(0))) return false; app_ref head(m_manager); expr_ref def(m_manager); @@ -64,15 +63,15 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex if (!m_util.is_arith_macro(body, num_decls, head, def, inv)) return false; app_ref new_body(m_manager); - + if (!inv || m_manager.is_eq(body)) new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def); - else if (au.is_le(body)) - new_body = au.mk_ge(head, def); + else if (as->is_le(body)) + new_body = autil.mk_ge(head, def); else - new_body = au.mk_le(head, def); + new_body = autil.mk_le(head, def); - quantifier_ref new_q(m_manager); + quantifier_ref new_q(m_manager); new_q = m_manager.update_quantifier(to_quantifier(n), new_body); proof * new_pr = 0; if (m_manager.proofs_enabled()) { @@ -83,16 +82,16 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex return m_macro_manager.insert(head->get_decl(), new_q, new_pr); } // is ge or le - // + // TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";); func_decl * f = head->get_decl(); func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); app * k_app = m_manager.mk_app(k, head->get_num_args(), head->get_args()); expr_ref_buffer new_rhs_args(m_manager); expr_ref new_rhs2(m_manager); - arw.mk_add(def, k_app, new_rhs2); + as->mk_add(def, k_app, new_rhs2); expr * body1 = m_manager.mk_eq(head, new_rhs2); - expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, au.mk_numeral(0, m_manager.get_sort(def))); + expr * body2 = m_manager.mk_app(new_body->get_decl(), k_app, as->mk_numeral(rational(0))); quantifier * q1 = m_manager.update_quantifier(new_q, body1); expr * patterns[1] = { m_manager.mk_pattern(k_app) }; quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2); @@ -119,7 +118,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex n is of the form: (forall (X) (iff (= (f X) t) def[X])) Convert it into: - + (forall (X) (= (f X) (ite def[X] t (k X)))) (forall (X) (not (= (k X) t))) @@ -127,13 +126,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex The new quantifiers and proofs are stored in new_exprs and new_prs */ -static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, +static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { func_decl * f = head->get_decl(); func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range()); app * k_app = m.mk_app(k, head->get_num_args(), head->get_args()); app * ite = m.mk_ite(def, t, k_app); - app * body_1 = m.mk_eq(head, ite); + app * body_1 = m.mk_eq(head, ite); app * body_2 = m.mk_not(m.mk_eq(k_app, t)); quantifier * q1 = m.update_quantifier(q, body_1); expr * pats[1] = { m.mk_pattern(k_app) }; @@ -184,7 +183,7 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";); found_new_macro = true; } - else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { + else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";); pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs); found_new_macro = true; diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h index 0c292eab8..7f1b27f0e 100644 --- a/src/ast/macros/macro_finder.h +++ b/src/ast/macros/macro_finder.h @@ -20,7 +20,8 @@ Revision History: #define MACRO_FINDER_H_ #include "ast/macros/macro_manager.h" -#include "ast/macros/macro_util.h" +#include "ast/simplifier/arith_simplifier_plugin.h" + bool is_macro_head(expr * n, unsigned num_decls); bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable const * forbidden_set, app * & head, expr * & def); @@ -33,15 +34,16 @@ inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app * as macros. */ class macro_finder { - ast_manager & m_manager; + ast_manager & m_manager; macro_manager & m_macro_manager; macro_util & m_util; - + arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); } bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); - bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const; - bool is_macro(expr * n, app_ref & head, expr_ref & def) const; - bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t) const; - bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def) const; + bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); + + bool is_macro(expr * n, app_ref & head, expr_ref & def); + bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t); + bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def); public: macro_finder(ast_manager & m, macro_manager & mm); @@ -50,3 +52,4 @@ public: }; #endif /* MACRO_FINDER_H_ */ + diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index f26a87445..bd330a2de 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -28,7 +28,7 @@ Revision History: macro_manager::macro_manager(ast_manager & m, simplifier & s): m_manager(m), m_simplifier(s), - m_util(m), + m_util(m, s), m_decls(m), m_macros(m), m_macro_prs(m), diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 415e77d03..35f2fbcfb 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -20,8 +20,8 @@ Revision History: #include "ast/macros/macro_util.h" #include "ast/occurs.h" #include "ast/ast_util.h" -#include "ast/arith_decl_plugin.h" -#include "ast/bv_decl_plugin.h" +#include "ast/simplifier/arith_simplifier_plugin.h" +#include "ast/simplifier/bv_simplifier_plugin.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" @@ -29,73 +29,96 @@ Revision History: #include "ast/well_sorted.h" #include "ast/rewriter/bool_rewriter.h" -macro_util::macro_util(ast_manager & m): +macro_util::macro_util(ast_manager & m, simplifier & s): m_manager(m), - m_arith_rw(m), - m_arith_util(m_arith_rw.get_util()), - m_bv_rw(m), - m_bv_util(m_bv_rw.get_util()), + m_bv(m), + m_simplifier(s), + m_arith_simp(0), + m_bv_simp(0), m_forbidden_set(0), m_curr_clause(0) { } +arith_simplifier_plugin * macro_util::get_arith_simp() const { + if (m_arith_simp == 0) { + const_cast(this)->m_arith_simp = static_cast(m_simplifier.get_plugin(m_manager.mk_family_id("arith"))); + } + SASSERT(m_arith_simp != 0); + return m_arith_simp; +} + +bv_simplifier_plugin * macro_util::get_bv_simp() const { + if (m_bv_simp == 0) { + const_cast(this)->m_bv_simp = static_cast(m_simplifier.get_plugin(m_manager.mk_family_id("bv"))); + } + SASSERT(m_bv_simp != 0); + return m_bv_simp; +} + + bool macro_util::is_bv(expr * n) const { - return m_bv_util.is_bv(n); + return m_bv.is_bv(n); } bool macro_util::is_bv_sort(sort * s) const { - return m_bv_util.is_bv_sort(s); + return m_bv.is_bv_sort(s); } bool macro_util::is_add(expr * n) const { - return m_arith_util.is_add(n) || m_bv_util.is_bv_add(n); + return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n); } bool macro_util::is_times_minus_one(expr * n, expr * & arg) const { - return is_app(n) && to_app(n)->get_num_args() == 2 && - ((m_arith_rw.is_mul(n) && m_arith_rw.is_times_minus_one(to_app(n)->get_arg(0), arg)) || - (m_bv_rw.is_mul(n) && m_bv_rw.is_times_minus_one(to_app(n)->get_arg(0), arg))); + return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg); } bool macro_util::is_le(expr * n) const { - return m_arith_util.is_le(n) || m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n); + return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n); } bool macro_util::is_le_ge(expr * n) const { - return m_arith_util.is_le(n) || m_arith_util.is_ge(n) || - m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n); + return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n); +} + +poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const { + if (is_bv_sort(s)) + return get_bv_simp(); + else + return get_arith_simp(); } app * macro_util::mk_zero(sort * s) const { - if (is_bv_sort(s)) - return m_bv_util.mk_numeral(rational(0), s); - else - return m_arith_util.mk_numeral(0, s); + poly_simplifier_plugin * ps = get_poly_simp_for(s); + ps->set_curr_sort(s); + return ps->mk_zero(); } void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const { - if (is_bv(t1)) - r = m_bv_util.mk_bv_sub(t1, t2); - else - r = m_arith_util.mk_sub(t1, t2); + if (is_bv(t1)) { + r = m_bv.mk_bv_sub(t1, t2); + } + else { + get_arith_simp()->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_util.mk_bv_add(t1, t2); - else - m_arith_util.mk_add(t1, t2, r); + if (is_bv(t1)) { + r = m_bv.mk_bv_add(t1, t2); + } + else { + get_arith_simp()->mk_add(t1, t2, r); + } } void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const { - if (num_args == 0) + if (num_args == 0) { r = mk_zero(s); - else if (num_args == 1) - r = args[0]; - else if (is_bv_sort(s)) - m_bv_rw.mk_add(num_args, args, r); - else - m_arith_rw.mk_add(num_args, args, r); + return; + } + poly_simplifier_plugin * ps = get_poly_simp_for(s); + ps->set_curr_sort(s); + ps->mk_add(num_args, args, r); } /** @@ -218,12 +241,13 @@ bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) c bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const { // TODO: obsolete... we should move to collect_arith_macro_candidates - if (!m_manager.is_eq(n) && !m_arith_util.is_le(n) && !m_arith_util.is_ge(n)) + arith_simplifier_plugin * as = get_arith_simp(); + if (!m_manager.is_eq(n) && !as->is_le(n) && !as->is_ge(n)) return false; expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); - if (!m_arith_util.is_numeral(rhs)) + if (!as->is_numeral(rhs)) return false; inv = false; @@ -248,7 +272,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex !poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) { h = arg; } - else if (h == 0 && m_arith_util.is_times_minus_one(arg, neg_arg) && + else if (h == 0 && as->is_times_minus_one(arg, neg_arg) && is_macro_head(neg_arg, num_decls) && !is_forbidden(to_app(neg_arg)->get_decl()) && !poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) { @@ -263,11 +287,11 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex return false; head = to_app(h); expr_ref tmp(m_manager); - m_arith_rw.mk_add(args.size(), args.c_ptr(), tmp); + as->mk_add(args.size(), args.c_ptr(), tmp); if (inv) - m_arith_rw.mk_sub(tmp, rhs, def); + as->mk_sub(tmp, rhs, def); else - m_arith_rw.mk_sub(rhs, tmp, def); + as->mk_sub(rhs, tmp, def); return true; } diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index 3da8accc9..d76f2f0d3 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -22,8 +22,12 @@ Revision History: #include "ast/ast.h" #include "util/obj_hashtable.h" -#include "ast/rewriter/arith_rewriter.h" -#include "ast/rewriter/bv_rewriter.h" +#include "ast/simplifier/simplifier.h" + +class poly_simplifier_plugin; +class arith_simplifier_plugin; +class bv_simplifier_plugin; +class basic_simplifier_plugin; class macro_util { public: @@ -58,10 +62,10 @@ public: private: ast_manager & m_manager; - mutable arith_rewriter m_arith_rw; - arith_util & m_arith_util; - mutable bv_rewriter m_bv_rw; - bv_util & m_bv_util; + bv_util m_bv; + simplifier & m_simplifier; + arith_simplifier_plugin * m_arith_simp; + bv_simplifier_plugin * m_bv_simp; obj_hashtable * m_forbidden_set; bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); } @@ -90,13 +94,11 @@ private: public: - macro_util(ast_manager & m); + macro_util(ast_manager & m, simplifier & s); void set_forbidden_set(obj_hashtable * s) { m_forbidden_set = s; } - arith_util & get_arith_util() const { return m_arith_util; } - bv_util & get_bv_util() const { return m_bv_util; } - arith_rewriter & get_arith_rw() const { return m_arith_rw; } - bv_rewriter & get_bv_rw() const { return m_bv_rw; } + arith_simplifier_plugin * get_arith_simp() const; + bv_simplifier_plugin * get_bv_simp() const; bool is_macro_head(expr * n, unsigned num_decls) const; bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const; @@ -135,6 +137,7 @@ public: void mk_sub(expr * t1, expr * t2, expr_ref & r) const; void mk_add(expr * t1, expr * t2, expr_ref & r) const; void mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const; + poly_simplifier_plugin * get_poly_simp_for(sort * s) const; }; #endif diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 2342782c1..de849dbd7 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -29,10 +29,10 @@ protected: bool m_expand_power; bool m_mul2power; bool m_expand_tan; - + ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } - + bool is_numeral(expr * n) const { return m_util.is_numeral(n); } bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); } bool is_zero(expr * n) const { return m_util.is_zero(n); } @@ -77,7 +77,7 @@ class arith_rewriter : public poly_rewriter { br_status mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result); br_status mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result); br_status mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result); - + bool is_reduce_power_target(expr * arg, bool is_eq); expr * reduce_power(expr * arg, bool is_eq); br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); @@ -154,16 +154,16 @@ public: if (mk_rem_core(arg1, arg2, result) == BR_FAILED) result = m().mk_app(get_fid(), OP_REM, arg1, arg2); } - + br_status mk_to_int_core(expr * arg, expr_ref & result); br_status mk_to_real_core(expr * arg, expr_ref & result); - void mk_to_int(expr * arg, expr_ref & result) { + void mk_to_int(expr * arg, expr_ref & result) { if (mk_to_int_core(arg, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); + result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); } - void mk_to_real(expr * arg, expr_ref & result) { - if (mk_to_real_core(arg, result) == BR_FAILED) - result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); + void mk_to_real(expr * arg, expr_ref & result) { + if (mk_to_real_core(arg, result) == BR_FAILED) + result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); } br_status mk_is_int(expr * arg, expr_ref & result); @@ -178,8 +178,6 @@ public: br_status mk_sinh_core(expr * arg, expr_ref & result); br_status mk_cosh_core(expr * arg, expr_ref & result); br_status mk_tanh_core(expr * arg, expr_ref & result); - - arith_util & get_util() { return m_util; } }; #endif diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index 81c5ea132..5d38e4b10 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -159,63 +159,6 @@ public: expr* args[2] = { a1, a2 }; mk_sub(2, args, result); } - - bool is_times_minus_one(expr * n, expr * & r) const { - if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) { - r = to_app(n)->get_arg(1); - return true; - } - return false; - } - - /** - \brief Return true if n is can be put into the form (+ v t) or (+ (- v) t) - \c inv = true will contain true if (- v) is found, and false otherwise. - */ - bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) { - if (!is_add(n) || is_ground(n)) - return false; - - ptr_buffer args; - v = 0; - expr * curr = to_app(n); - bool stop = false; - inv = false; - while (!stop) { - expr * arg; - expr * neg_arg; - if (is_add(curr)) { - arg = to_app(curr)->get_arg(0); - curr = to_app(curr)->get_arg(1); - } - else { - arg = curr; - stop = true; - } - if (is_ground(arg)) { - args.push_back(arg); - } - else if (is_var(arg)) { - if (v != 0) - return false; // already found variable - v = to_var(arg); - } - else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) { - if (v != 0) - return false; // already found variable - v = to_var(neg_arg); - inv = true; - } - else { - return false; // non ground term. - } - } - if (v == 0) - return false; // did not find variable - SASSERT(!args.empty()); - mk_add(args.size(), args.c_ptr(), t); - return true; - } }; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 0a80460f5..94a6a7267 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1873,12 +1873,12 @@ namespace smt { fill the structure quantifier_info. */ class quantifier_analyzer { - model_finder & m_mf; + model_finder& m_mf; ast_manager & m_manager; macro_util m_mutil; array_util m_array_util; - arith_util & m_arith_util; - bv_util & m_bv_util; + arith_util m_arith_util; + bv_util m_bv_util; quantifier_info * m_info; @@ -1897,12 +1897,14 @@ namespace smt { m_info->insert_qinfo(qi); } + arith_simplifier_plugin * get_arith_simp() const { return m_mutil.get_arith_simp(); } + bv_simplifier_plugin * get_bv_simp() const { return m_mutil.get_bv_simp(); } + bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) const { - return m_mutil.get_arith_rw().is_var_plus_ground(n, inv, v, t) || - m_mutil.get_bv_rw().is_var_plus_ground(n, inv, v, t); + return get_arith_simp()->is_var_plus_ground(n, inv, v, t) || get_bv_simp()->is_var_plus_ground(n, inv, v, t); } - bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) const { + bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) { bool inv; TRACE("is_var_plus_ground", tout << mk_pp(n, m_manager) << "\n"; tout << "is_var_plus_ground: " << is_var_plus_ground(n, inv, v, t) << "\n"; @@ -1915,11 +1917,10 @@ namespace smt { } bool is_zero(expr * n) const { - if (m_bv_util.is_bv(n)) - return m_bv_util.is_zero(n); - else { - return m_arith_util.is_zero(n); - } + if (get_bv_simp()->is_bv(n)) + return get_bv_simp()->is_zero_safe(n); + else + return get_arith_simp()->is_zero_safe(n); } bool is_times_minus_one(expr * n, expr * & arg) const { @@ -1938,7 +1939,7 @@ namespace smt { return m_bv_util.is_bv_sle(n); } - expr * mk_one(sort * s) const { + expr * mk_one(sort * s) { return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s); } @@ -1950,7 +1951,7 @@ namespace smt { m_mutil.mk_add(t1, t2, r); } - bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) { + bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) const { inv = false; // true if invert the sign TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";); if (is_var(lhs) && is_ground(rhs)) { @@ -1985,12 +1986,12 @@ namespace smt { return false; } - bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) { + bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const { bool inv; return is_var_and_ground(lhs, rhs, v, t, inv); } - bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) { + bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const { if (!is_app(n)) return false; if (m_manager.is_eq(n)) @@ -2381,10 +2382,10 @@ namespace smt { quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s): m_mf(mf), m_manager(m), - m_mutil(m), + m_mutil(m, s), m_array_util(m), - m_arith_util(m_mutil.get_arith_util()), - m_bv_util(m_mutil.get_bv_util()), + m_arith_util(m), + m_bv_util(m), m_info(0) { }