Eliminated the dependency of the macro-finder on the simplifier.

src/ast/macros/macro_finder.cpp

@@ -21,8 +21,9 @@ 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) {
+bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) const {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
@@ -32,30 +33,30 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
 }
 
 /**
-   \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) {
+bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
-    arith_simplifier_plugin * as = get_arith_simp();
+    arith_rewriter & arw = m_util.get_arith_rw();
-    arith_util & autil = as->get_arith_util();
+    arith_util & au = m_util.get_arith_util();
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
-    
+
-    if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
+    if (!au.is_le(body) && !au.is_ge(body) && !m_manager.is_eq(body))
         return false;
-    if (!as->is_add(to_app(body)->get_arg(0)))
+    if (!au.is_add(to_app(body)->get_arg(0)))
         return false;
     app_ref head(m_manager);
     expr_ref def(m_manager);
@@ -63,15 +64,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 (as->is_le(body))
+    else if (au.is_le(body))
-        new_body = autil.mk_ge(head, def);
+        new_body = au.mk_ge(head, def);
     else
-        new_body = autil.mk_le(head, def);
+        new_body = au.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()) {
@@ -82,16 +83,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);
-    as->mk_add(def, k_app, new_rhs2);
+    arw.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, as->mk_numeral(rational(0)));
+    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, au.mk_numeral(0, m_manager.get_sort(def)));
     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);
@@ -118,7 +119,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)))
 
@@ -126,13 +127,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) };
@@ -183,7 +184,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;

src/ast/macros/macro_finder.h

@@ -20,8 +20,7 @@ Revision History:
 #define MACRO_FINDER_H_
 
 #include "ast/macros/macro_manager.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
+#include "ast/macros/macro_util.h"
-
 
 bool is_macro_head(expr * n, unsigned num_decls);
 bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable<func_decl> const * forbidden_set, app * & head, expr * & def);
@@ -34,16 +33,15 @@ 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);
 
-    bool is_macro(expr * n, app_ref & head, expr_ref & def);
+    bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
-    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
+    bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) const;
-    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
+    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;
 
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
@@ -52,4 +50,3 @@ public:
 };
 
 #endif /* MACRO_FINDER_H_ */
-

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, s),
+    m_util(m),
     m_decls(m),
     m_macros(m),
     m_macro_prs(m),

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/simplifier/arith_simplifier_plugin.h"
+#include "ast/arith_decl_plugin.h"
-#include "ast/simplifier/bv_simplifier_plugin.h"
+#include "ast/bv_decl_plugin.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -29,96 +29,73 @@ Revision History:
 #include "ast/well_sorted.h"
 #include "ast/rewriter/bool_rewriter.h"
 
-macro_util::macro_util(ast_manager & m, simplifier & s):
+macro_util::macro_util(ast_manager & m):
     m_manager(m),
-    m_bv(m),
+    m_arith_rw(m),
-    m_simplifier(s),
+    m_arith_util(m_arith_rw.get_util()),
-    m_arith_simp(0),
+    m_bv_rw(m),
-    m_bv_simp(0),
+    m_bv_util(m_bv_rw.get_util()),
     m_forbidden_set(0),
     m_curr_clause(0) {
 }
 
-arith_simplifier_plugin * macro_util::get_arith_simp() const {
-    if (m_arith_simp == 0) {
-        const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(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<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(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.is_bv(n);
+    return m_bv_util.is_bv(n);
 }
 
 bool macro_util::is_bv_sort(sort * s) const {
-    return m_bv.is_bv_sort(s);
+    return m_bv_util.is_bv_sort(s);
 }
 
 bool macro_util::is_add(expr * n) const {
-    return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n);
+    return m_arith_util.is_add(n) || m_bv_util.is_bv_add(n);
 }
 
 bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
-    return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg);
+    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)));
 }
 
 bool macro_util::is_le(expr * n) const {
-    return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
+    return m_arith_util.is_le(n) || m_bv_util.is_bv_ule(n) || m_bv_util.is_bv_sle(n);
 }
 
 bool macro_util::is_le_ge(expr * n) const {
-    return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
+    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);
-
-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 {
-    poly_simplifier_plugin * ps = get_poly_simp_for(s);
+    if (is_bv_sort(s))
-    ps->set_curr_sort(s);
+        return m_bv_util.mk_numeral(rational(0), s);
-    return ps->mk_zero();
+    else
+        return m_arith_util.mk_numeral(0, s);
 }
 
 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);
+        r = m_bv_util.mk_bv_sub(t1, t2);
-    }
+    else
-    else {
+        r = m_arith_util.mk_sub(t1, t2);
-        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)) {
+    if (is_bv(t1))
-        r = m_bv.mk_bv_add(t1, t2);
+        r = m_bv_util.mk_bv_add(t1, t2);
-    }
+    else
-    else {
+        m_arith_util.mk_add(t1, t2, r);
-        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);
-        return;
+    else if (num_args == 1)
-    }
+        r = args[0];
-    poly_simplifier_plugin * ps = get_poly_simp_for(s);
+    else if (is_bv_sort(s))
-    ps->set_curr_sort(s);
+        m_bv_rw.mk_add(num_args, args, r);
-    ps->mk_add(num_args, args, r);
+    else
+        m_arith_rw.mk_add(num_args, args, r);
 }
 
 /**
@@ -241,13 +218,12 @@ 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
-    arith_simplifier_plugin * as = get_arith_simp();
+    if (!m_manager.is_eq(n) && !m_arith_util.is_le(n) && !m_arith_util.is_ge(n))
-    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 (!as->is_numeral(rhs))
+    if (!m_arith_util.is_numeral(rhs))
         return false;
 
     inv = false;
@@ -272,7 +248,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 && as->is_times_minus_one(arg, neg_arg) &&
+        else if (h == 0 && m_arith_util.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)) {
@@ -287,11 +263,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);
-    as->mk_add(args.size(), args.c_ptr(), tmp);
+    m_arith_rw.mk_add(args.size(), args.c_ptr(), tmp);
     if (inv)
-        as->mk_sub(tmp, rhs, def);
+        m_arith_rw.mk_sub(tmp, rhs, def);
     else
-        as->mk_sub(rhs, tmp, def);
+        m_arith_rw.mk_sub(rhs, tmp, def);
     return true;
 }
 

src/ast/macros/macro_util.h

@@ -22,12 +22,8 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/obj_hashtable.h"
-#include "ast/simplifier/simplifier.h"
+#include "ast/rewriter/arith_rewriter.h"
-
+#include "ast/rewriter/bv_rewriter.h"
-class poly_simplifier_plugin;
-class arith_simplifier_plugin;
-class bv_simplifier_plugin;
-class basic_simplifier_plugin;
 
 class macro_util {
 public:
@@ -62,10 +58,10 @@ public:
 
 private:
     ast_manager &               m_manager;
-    bv_util                     m_bv;
+    mutable arith_rewriter      m_arith_rw;
-    simplifier &                m_simplifier;
+    arith_util &                m_arith_util;
-    arith_simplifier_plugin *   m_arith_simp;
+    mutable bv_rewriter         m_bv_rw;
-    bv_simplifier_plugin    *   m_bv_simp;
+    bv_util &                   m_bv_util;
     obj_hashtable<func_decl> *  m_forbidden_set;
 
     bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
@@ -94,11 +90,13 @@ private:
 
 
 public:
-    macro_util(ast_manager & m, simplifier & s);
+    macro_util(ast_manager & m);
     void set_forbidden_set(obj_hashtable<func_decl> * s) { m_forbidden_set = s; }
 
-    arith_simplifier_plugin * get_arith_simp() const;
+    arith_util & get_arith_util() const { return m_arith_util; }
-    bv_simplifier_plugin * get_bv_simp() const;
+    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; }
 
     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;
@@ -137,7 +135,6 @@ 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

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<arith_rewriter_core> {
     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) { 
+    void mk_to_real(expr * arg, expr_ref & result) {
-        if (mk_to_real_core(arg, result) == BR_FAILED)  
+        if (mk_to_real_core(arg, result) == BR_FAILED)
-            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); 
+            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg);
     }
     br_status mk_is_int(expr * arg, expr_ref & result);
 
@@ -178,6 +178,8 @@ 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

src/ast/rewriter/poly_rewriter.h

@@ -159,6 +159,63 @@ 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<expr> 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;
+    }
 };
 
 

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;
+            arith_util &         m_arith_util;
-            bv_util              m_bv_util;
+            bv_util &            m_bv_util;
 
             quantifier_info *    m_info;
 
@@ -1897,14 +1897,12 @@ 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 get_arith_simp()->is_var_plus_ground(n, inv, v, t) || get_bv_simp()->is_var_plus_ground(n, inv, v, t);
+                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);
             }
 
-            bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) {
+            bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) const {
                 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";
@@ -1917,10 +1915,11 @@ namespace smt {
             }
 
             bool is_zero(expr * n) const {
-                if (get_bv_simp()->is_bv(n))
+                if (m_bv_util.is_bv(n))
-                    return get_bv_simp()->is_zero_safe(n);
+                    return m_bv_util.is_zero(n);
-                else
+                else {
-                    return get_arith_simp()->is_zero_safe(n);
+                    return m_arith_util.is_zero(n);
+                }
             }
 
             bool is_times_minus_one(expr * n, expr * & arg) const {
@@ -1939,7 +1938,7 @@ namespace smt {
                 return m_bv_util.is_bv_sle(n);
             }
 
-            expr * mk_one(sort * s) {
+            expr * mk_one(sort * s) const {
                 return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s);
             }
 
@@ -1951,7 +1950,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) const {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) {
                 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)) {
@@ -1986,12 +1985,12 @@ namespace smt {
                 return false;
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) {
                 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) const {
+            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) {
                 if (!is_app(n))
                     return false;
                 if (m_manager.is_eq(n))
@@ -2382,10 +2381,10 @@ namespace smt {
             quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s):
                 m_mf(mf),
                 m_manager(m),
-                m_mutil(m, s),
+                m_mutil(m),
                 m_array_util(m),
-                m_arith_util(m),
+                m_arith_util(m_mutil.get_arith_util()),
-                m_bv_util(m),
+                m_bv_util(m_mutil.get_bv_util()),
                 m_info(0) {
             }