remove simplify dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/bmc/dl_bmc_engine.cpp

@@ -1139,7 +1139,7 @@ namespace datalog {
             md->eval(path, path);
             IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n";
                        for (unsigned i = 0; i < b.m_solver.size(); ++i) {
-                           verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n";
+                           verbose_stream() << mk_pp(b.m_solver.get_formula(i), m) << "\n";
                        });
             scoped_proof _sp(m);
             proof_ref pr(m);

src/muz/pdr/pdr_smt_context_manager.cpp

@@ -83,7 +83,7 @@ namespace pdr {
               {
                   ast_smt_pp pp(m);
                   for (unsigned i = 0; i < m_context.size(); ++i) {
-                      pp.add_assumption(m_context.get_formulas()[i]);
+                      pp.add_assumption(m_context.get_formula(i));
                   }
                   for (unsigned i = 0; i < assumptions.size(); ++i) {
                       pp.add_assumption(assumptions[i].get());

src/muz/spacer/spacer_virtual_solver.cpp

@@ -318,7 +318,7 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions,
             stopwatch sw2;
             smt::kernel kernel(m, p);
             for (unsigned i = 0, sz = m_context.size(); i < sz; ++i)
-            { kernel.assert_expr(m_context.get_formulas()[i]); }
+                { kernel.assert_expr(m_context.get_formula(i)); }
             sw2.start();
             kernel.check(num_assumptions, assumptions);
             sw2.stop();
@@ -450,7 +450,7 @@ void virtual_solver::to_smt2_benchmark(std::ostream &out,
 
 
     for (unsigned i = 0, sz = context.size(); i < sz; ++i) {
-        asserts.push_back(context.get_formulas()[i]);
+        asserts.push_back(context.get_formula(i));
         pp.collect(asserts.back());
     }
     pp.collect(num_assumptions, assumptions);

src/opt/opt_solver.cpp

@@ -161,7 +161,7 @@ namespace opt {
         TRACE("opt_verbose", {
             tout << "context size: " << m_context.size() << "\n";            
             for (unsigned i = 0; i < m_context.size(); ++i) {
-                tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
+                tout << mk_pp(m_context.get_formula(i), m_context.m()) << "\n";
             }
         });
         stopwatch w;
@@ -330,7 +330,7 @@ namespace opt {
     
     expr * opt_solver::get_assertion(unsigned idx) const {
         SASSERT(idx < get_num_assertions());
-        return m_context.get_formulas()[idx];
+        return m_context.get_formula(idx);
     }
         
     smt::theory_var opt_solver::add_objective(app* term) {

src/smt/asserted_formulas.cpp

@@ -47,6 +47,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
     m_params(p),
     m_pre_simplifier(m),
     m_simplifier(m),
+    m_rewriter(m),
     m_defined_names(m),
     m_static_features(m),
     m_asserted_formulas(m),

src/smt/asserted_formulas.h

@@ -30,6 +30,7 @@ Revision History:
 #include "ast/normal_forms/defined_names.h"
 #include "ast/pattern/pattern_inference.h"
 #include "smt/params/smt_params.h"
+#include "ast/rewriter/th_rewriter.h"
 
 class arith_simplifier_plugin;
 class bv_simplifier_plugin;
@@ -39,6 +40,7 @@ class asserted_formulas {
     smt_params &                 m_params;
     simplifier                   m_pre_simplifier;
     simplifier                   m_simplifier;
+    th_rewriter                  m_rewriter;
     basic_simplifier_plugin *    m_bsimp;
     bv_simplifier_plugin *       m_bvsimp;
     defined_names                m_defined_names;
@@ -121,7 +123,8 @@ public:
     proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
     void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
     void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); }
-    simplifier & get_simplifier() { return m_simplifier; }
+    // simplifier & get_simplifier() { return m_simplifier; }
+    th_rewriter& get_rewriter() { return m_rewriter; }
     void get_assertions(ptr_vector<expr> & result);
     bool empty() const { return m_asserted_formulas.empty(); }
     void collect_static_features();

src/smt/qi_queue.cpp

@@ -227,7 +227,7 @@ namespace smt {
         TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m_manager) << "\n";);
         expr_ref  s_instance(m_manager);
         proof_ref pr(m_manager);
-        simplifier & simp = m_context.get_simplifier();
+        th_rewriter & simp = m_context.get_rewriter();
         simp(instance, s_instance, pr);
         TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << mk_pp(s_instance, m_manager) << "\n";);
         if (m_manager.is_true(s_instance)) {

src/smt/smt_context.cpp

@@ -148,8 +148,8 @@ namespace smt {
         dst_ctx.set_logic(src_ctx.m_setup.get_logic());
         dst_ctx.copy_plugins(src_ctx, dst_ctx);
 
-        asserted_formulas& src_af = src_ctx.m_asserted_formulas;
+        asserted_formulas_new& src_af = src_ctx.m_asserted_formulas;
-        asserted_formulas& dst_af = dst_ctx.m_asserted_formulas;
+        asserted_formulas_new& dst_af = dst_ctx.m_asserted_formulas;
 
         // Copy asserted formulas.
         for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
@@ -224,20 +224,6 @@ namespace smt {
 
     void context::copy_plugins(context& src, context& dst) {
 
-        // copy missing simplifier_plugins
-        // remark: some simplifier_plugins are automatically created by the asserted_formulas class.
-        simplifier & src_s = src.get_simplifier();
-        simplifier & dst_s = dst.get_simplifier();
-        ptr_vector<simplifier_plugin>::const_iterator it1  = src_s.begin_plugins();
-        ptr_vector<simplifier_plugin>::const_iterator end1 = src_s.end_plugins();
-        for (; it1 != end1; ++it1) {
-            simplifier_plugin * p = *it1;
-            if (dst_s.get_plugin(p->get_family_id()) == 0) {
-                dst.register_plugin(p->mk_fresh());
-            }
-            SASSERT(dst_s.get_plugin(p->get_family_id()) != 0);
-        }
-
         // copy theory plugins
         for (theory* old_th : src.m_theory_set) {
             theory * new_th = old_th->mk_fresh(&dst);
@@ -2845,11 +2831,6 @@ namespace smt {
         return false;
     }
 
-    void context::register_plugin(simplifier_plugin * s) {
-        SASSERT(!already_internalized());
-        SASSERT(m_scope_lvl == 0);
-        m_asserted_formulas.register_simplifier_plugin(s);
-    }
 
 #ifdef Z3DEBUG
     /**

src/smt/smt_context.h

@@ -36,7 +36,7 @@ Revision History:
 #include "smt/smt_case_split_queue.h"
 #include "smt/smt_almost_cg_table.h"
 #include "smt/smt_failure.h"
-#include "smt/asserted_formulas.h"
+#include "smt/asserted_formulas_new.h"
 #include "smt/smt_types.h"
 #include "smt/dyn_ack.h"
 #include "ast/ast_smt_pp.h"
@@ -81,7 +81,7 @@ namespace smt {
         params_ref                  m_params;
         setup                       m_setup;
         timer                       m_timer;
-        asserted_formulas           m_asserted_formulas;
+        asserted_formulas_new       m_asserted_formulas;
         scoped_ptr<quantifier_manager>   m_qmanager;
         scoped_ptr<model_generator>      m_model_generator;
         scoped_ptr<relevancy_propagator> m_relevancy_propagator;
@@ -245,8 +245,8 @@ namespace smt {
             return m_manager;
         }
 
-        simplifier & get_simplifier() {
+        th_rewriter & get_rewriter() {
-            return m_asserted_formulas.get_simplifier();
+            return m_asserted_formulas.get_rewriter();
         }
 
         smt_params & get_fparams() {
@@ -1467,8 +1467,6 @@ namespace smt {
 
         bool set_logic(symbol const& logic) { return m_setup.set_logic(logic); }
 
-        void register_plugin(simplifier_plugin * s);
-
         void register_plugin(theory * th);
 
         void assert_expr(expr * e);
@@ -1540,9 +1538,9 @@ namespace smt {
 
         proof * get_asserted_formula_proof(unsigned idx) const { return m_asserted_formulas.get_formula_proof(idx); }
 
-        expr * const * get_asserted_formulas() const { return m_asserted_formulas.get_formulas(); }
+        void get_asserted_formulas(ptr_vector<expr>& r) const { m_asserted_formulas.get_assertions(r); }
 
-        proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
+        //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
 
         void get_assumptions_core(ptr_vector<expr> & result);
 

src/smt/smt_kernel.cpp

@@ -60,10 +60,10 @@ namespace smt {
             // m_kernel.display(out); <<< for external users it is just junk
             // TODO: it will be replaced with assertion_stack.display
             unsigned num = m_kernel.get_num_asserted_formulas();
-            expr * const * fms = m_kernel.get_asserted_formulas();
             out << "(kernel";
             for (unsigned i = 0; i < num; i++) {
-                out << "\n  " << mk_ismt2_pp(fms[i], m(), 2);
+                expr* f = m_kernel.get_asserted_formula(i);
+                out << "\n  " << mk_ismt2_pp(f, m(), 2);
             }
             out << ")";
         }
@@ -81,8 +81,12 @@ namespace smt {
             return m_kernel.get_num_asserted_formulas();
         }
         
-        expr * const * get_formulas() const {
+        void get_formulas(ptr_vector<expr>& fmls) const {
-            return m_kernel.get_asserted_formulas();
+            m_kernel.get_asserted_formulas(fmls);
+        }
+
+        expr* get_formula(unsigned i) const {
+            return m_kernel.get_asserted_formula(i);
         }
         
         void push() {
@@ -241,8 +245,8 @@ namespace smt {
         return m_imp->size();
     }
     
-    expr * const * kernel::get_formulas() const {
+    expr* kernel::get_formula(unsigned i) const {
-        return m_imp->get_formulas();
+        return m_imp->get_formula(i);
     }
 
 

src/smt/smt_kernel.h

@@ -85,7 +85,12 @@ namespace smt {
         /**
            \brief Return the array of asserted formulas.
         */
-        expr * const * get_formulas() const;
+        void get_formulas(ptr_vector<expr>& r) const;
+
+        /**
+           \brief return the formula at index idx.
+        */
+        expr* get_formula(unsigned idx) const;
         
         /**
            \brief Create a backtracking point (aka scope level).

src/smt/smt_quick_checker.cpp

@@ -164,7 +164,7 @@ namespace smt {
     quick_checker::quick_checker(context & c):
         m_context(c),
         m_manager(c.get_manager()),
-        m_simplifier(c.get_simplifier()),
+        m_simplifier(c.get_rewriter()),
         m_collector(c),
         m_new_exprs(m_manager) {
     }
@@ -411,7 +411,7 @@ namespace smt {
             }
         }
         expr_ref new_expr(m_manager);
-        m_simplifier.mk_app(to_app(n)->get_decl(), num_args, new_args.c_ptr(), new_expr);
+        new_expr = m_simplifier.mk_app(to_app(n)->get_decl(), num_args, new_args.c_ptr());
         m_new_exprs.push_back(new_expr);
         m_canonize_cache.insert(n, new_expr);
         return new_expr;

src/smt/smt_quick_checker.h

@@ -20,7 +20,7 @@ Revision History:
 #define SMT_QUICK_CHECKER_H_
 
 #include "ast/ast.h"
-#include "ast/simplifier/simplifier.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "util/obj_hashtable.h"
 
 namespace smt {
@@ -77,7 +77,7 @@ namespace smt {
 
         context &            m_context;
         ast_manager &        m_manager;
-        simplifier &         m_simplifier;
+        th_rewriter &        m_simplifier;
         collector            m_collector;
         expr_ref_vector      m_new_exprs;
         vector<enode_vector> m_candidate_vectors; 

src/smt/smt_setup.cpp

@@ -142,7 +142,9 @@ namespace smt {
         }
         else {
             IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
-            st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
+            ptr_vector<expr> fmls;
+            m_context.get_asserted_formulas(fmls);
+            st.collect(fmls.size(), fmls.c_ptr());
             IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
             if (m_logic == "QF_UF") 
                 setup_QF_UF(st);
@@ -742,7 +744,9 @@ namespace smt {
     void setup::setup_arith() {
         static_features    st(m_manager);
         IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
-        st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
+        ptr_vector<expr> fmls;
+        m_context.get_asserted_formulas(fmls);
+        st.collect(fmls.size(), fmls.c_ptr());
         IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
         bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
         bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
@@ -877,7 +881,9 @@ namespace smt {
 
     void setup::setup_unknown() {
         static_features st(m_manager);
-        st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
+        ptr_vector<expr> fmls;
+        m_context.get_asserted_formulas(fmls);
+        st.collect(fmls.size(), fmls.c_ptr());
         TRACE("setup", tout << "setup_unknown\n";);        
         setup_arith();
         setup_arrays();

src/smt/smt_solver.cpp

@@ -216,7 +216,7 @@ namespace smt {
 
         virtual expr * get_assertion(unsigned idx) const {
             SASSERT(idx < get_num_assertions());
-            return m_context.get_formulas()[idx];
+            return m_context.get_formula(idx);
         }
 
         struct collect_fds_proc {

src/smt/theory_arith_core.h

@@ -442,7 +442,7 @@ namespace smt {
     void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq) {
         ast_manager & m = get_manager();
         context & ctx   = get_context();
-        simplifier & s  = ctx.get_simplifier();
+        th_rewriter & s  = ctx.get_rewriter();
         expr_ref s_ante(m), s_conseq(m);
         expr* s_conseq_n, * s_ante_n;
         bool negated;

src/smt/theory_arith_int.h

@@ -455,9 +455,8 @@ namespace smt {
         pol = m_util.mk_add(_args.size(), _args.c_ptr());
         result = m_util.mk_ge(pol, m_util.mk_numeral(k, all_int));
         TRACE("arith_mk_polynomial", tout << "before simplification:\n" << result << "\n";);
-        simplifier & s = get_context().get_simplifier();
         proof_ref pr(m);
-        s(result, result, pr);
+        get_context().get_rewriter()(result, result, pr);
         TRACE("arith_mk_polynomial", tout << "after simplification:\n" << result << "\n";);
         SASSERT(is_well_sorted(get_manager(), result));
     }

src/smt/theory_arith_nl.h

@@ -2205,7 +2205,7 @@ namespace smt {
                 args.push_back(monomial2expr(eq->get_monomial(i), is_int));
         }
         context & ctx   = get_context();
-        simplifier & s  = ctx.get_simplifier();
+        th_rewriter& s = ctx.get_rewriter();
         expr_ref pol(get_manager());
         SASSERT(!args.empty());
         pol = mk_nary_add(args.size(), args.c_ptr());

src/smt/theory_array_full.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "smt/theory_array_full.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_util.h"
 #include "ast/ast_smt2_pp.h"
 #include "util/stats.h"
 
@@ -515,7 +516,7 @@ namespace smt {
 
         expr_ref sel1(m), sel2(m);
         sel1 = mk_select(args1.size(), args1.c_ptr());
-        m_simp->mk_app(f, args2.size(), args2.c_ptr(), sel2);
+        sel2 = ctx.get_rewriter().mk_app(f, args2.size(), args2.c_ptr());
         ctx.internalize(sel1, false);
         ctx.internalize(sel2, false);
         
@@ -553,7 +554,7 @@ namespace smt {
 
         expr* def1 = mk_default(map);
         expr_ref def2(get_manager());
-        m_simp->mk_app(f, args2.size(), args2.c_ptr(), def2);
+        def2 = ctx.get_rewriter().mk_app(f, args2.size(), args2.c_ptr());
         ctx.internalize(def1, false);
         ctx.internalize(def2, false);
         return try_assign_eq(def1, def2);
@@ -722,9 +723,7 @@ namespace smt {
             }
             
             expr_ref eq(m);
-            simplifier_plugin* p = m_simp->get_plugin(m.get_basic_family_id());
+            eq = mk_and(eqs);
-            basic_simplifier_plugin* bp = static_cast<basic_simplifier_plugin*>(p);
-            bp->mk_and(eqs.size(), eqs.c_ptr(), eq);
             expr* defA = mk_default(store_app->get_arg(0));
             def2 = m.mk_ite(eq, store_app->get_arg(num_args-1), defA); 
 #if 0

src/smt/theory_array_full.h

@@ -20,7 +20,6 @@ Revision History:
 #define THEORY_ARRAY_FULL_H_
 
 #include "smt/theory_array.h"
-#include "ast/simplifier/simplifier.h"
 #include "ast/ast_trail.h"
 
 namespace smt {
@@ -37,7 +36,6 @@ namespace smt {
         ptr_vector<var_data_full> m_var_data_full;
 
         ast2ast_trailmap<sort,app> m_sort2epsilon;
-        simplifier*                m_simp;
         obj_pair_map<expr,expr,bool> m_eqs;
         svector<literal>             m_eqsv;
 
@@ -100,7 +98,6 @@ namespace smt {
             // the parent class is theory_array.
             // theory::init(ctx); 
             theory_array::init(ctx); 
-            m_simp = &ctx->get_simplifier(); 
         }
 
     };

src/smt/theory_bv.cpp

@@ -28,7 +28,6 @@ namespace smt {
 
     void theory_bv::init(context * ctx) {
         theory::init(ctx);
-        m_simplifier    = &(ctx->get_simplifier());
     }
 
     theory_var theory_bv::mk_var(enode * n) {
@@ -300,7 +299,7 @@ namespace smt {
     void theory_bv::simplify_bit(expr * s, expr_ref & r) {
         // proof_ref p(get_manager());
         // if (get_context().at_base_level())
-        //    m_simplifier->operator()(s, r, p);
+        //    ctx.get_rewriter()(s, r, p);
         // else
         r = s;
     }
@@ -605,8 +604,9 @@ namespace smt {
             args.push_back(m.mk_ite(b, n, zero));
             num *= numeral(2);
         }
-        expr_ref sum(m);
+        expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
-        arith_simp().mk_add(sz, args.c_ptr(), sum);
+        arith_rewriter arw(m);
+        ctx.get_rewriter()(sum);
         literal l(mk_eq(n, sum, false));
         TRACE("bv", 
               tout << mk_pp(n, m) << "\n";
@@ -1366,7 +1366,6 @@ namespace smt {
         m_params(params),
         m_util(m),
         m_autil(m),
-        m_simplifier(0),
         m_bb(m, bb_params),
         m_trail_stack(*this),
         m_find(*this),

src/smt/theory_bv.h

@@ -24,10 +24,7 @@ Revision History:
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
 #include "util/trail.h"
 #include "util/union_find.h"
-#include "ast/simplifier/simplifier.h"
-#include "ast/simplifier/bv_simplifier_plugin.h"
 #include "ast/arith_decl_plugin.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
 #include "smt/proto_model/numeral_factory.h"
 
 namespace smt {
@@ -112,7 +109,6 @@ namespace smt {
         theory_bv_params const & m_params;
         bv_util                  m_util;
         arith_util               m_autil;
-        simplifier *             m_simplifier;
         bit_blaster              m_bb;
         th_trail_stack           m_trail_stack;
         th_union_find            m_find;
@@ -218,12 +214,6 @@ namespace smt {
         void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
         void assert_int2bv_axiom(app* n);
         void assert_bv2int_axiom(app* n);
-        arith_simplifier_plugin & arith_simp() const {
-            SASSERT(m_simplifier != 0);
-            arith_simplifier_plugin * as = static_cast<arith_simplifier_plugin*>(m_simplifier->get_plugin(m_autil.get_family_id()));
-            SASSERT(as != 0);
-            return *as;
-        }
 
     protected:
         virtual void init(context * ctx);

src/smt/theory_fpa.cpp

@@ -385,7 +385,7 @@ namespace smt {
     {
         ast_manager & m = get_manager();
         context & ctx = get_context();
-        simplifier & simp = ctx.get_simplifier();
+        th_rewriter & simp = ctx.get_rewriter();
 
         expr_ref res(m), t(m);
         proof_ref t_pr(m);