removing more dependencies

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

src/muz/base/dl_rule.cpp

@@ -44,6 +44,7 @@ Revision History:
 #include "tactic/filter_model_converter.h"
 #include "ast/scoped_proof.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/ast_util.h"
 
 namespace datalog {
 
@@ -757,7 +758,7 @@ namespace datalog {
             );
 
             proof_ref pr(m);
-            qe::expr_quant_elim_star1 simpl(m, m_ctx.get_fparams());
+            qe::simplify_rewriter_star simpl(m);
             simpl(quant_tail, fixed_tail, pr);
         }
         else {

src/muz/spacer/spacer_qe_project.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/expr_functors.h"
 #include "ast/expr_substitution.h"
+#include "ast/ast_util.h"
 
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/rewriter/expr_safe_replace.h"

src/qe/CMakeLists.txt

@@ -18,7 +18,6 @@ z3_add_component(qe
     qe_sat_tactic.cpp
     qe_tactic.cpp
     qsat.cpp
-    vsubst_tactic.cpp
   COMPONENT_DEPENDENCIES
     nlsat_tactic
     nlsat
@@ -31,5 +30,4 @@ z3_add_component(qe
     qe_sat_tactic.h
     qe_tactic.h
     qsat.h
-    vsubst_tactic.h
 )

src/qe/nlarith_util.cpp

@@ -11,7 +11,8 @@ Copyright (c) 2015 Microsoft Corporation
 #include "qe/qe.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/rewriter/arith_rewriter.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/expr_functors.h"
 
 namespace nlarith {
@@ -79,9 +80,8 @@ namespace nlarith {
         app_ref m_zero;
         app_ref m_one;
         smt_params m_params;
-        basic_simplifier_plugin m_bs;
+        bool_rewriter  m_bs;
-        arith_simplifier_plugin m_rw;
+        arith_rewriter m_rw;
-        arith_rewriter m_rw1;
         expr_ref_vector m_trail;
 
         ast_manager& m() const { return m_manager; }
@@ -105,8 +105,7 @@ namespace nlarith {
             m_enable_linear(false),
             m_zero(num(0),m), m_one(num(1),m), 
             m_bs(m),
-            m_rw(m, m_bs, m_params),
+            m_rw(m), m_trail(m) {
-            m_rw1(m), m_trail(m) {
         }
         
         //

src/qe/qe.cpp

@@ -1310,6 +1310,10 @@ namespace qe {
         m_s.mk_atom(e, p, result);
     }    
 
+    void i_solver_context::collect_statistics(statistics& st) const {
+       // tbd
+    }
+
     typedef ref_vector_ptr_hash<expr, ast_manager> expr_ref_vector_hash;
     typedef ref_vector_ptr_eq<expr, ast_manager>   expr_ref_vector_eq;
     typedef hashtable<expr_ref_vector*, expr_ref_vector_hash, expr_ref_vector_eq> clause_table;
@@ -2393,6 +2397,7 @@ namespace qe {
 
 
 
+#if 0
     // ------------------------------------------------
     // expr_quant_elim_star1
 
@@ -2433,13 +2438,7 @@ namespace qe {
         simplifier(m), m_quant_elim(m, p), m_assumption(m.mk_true())
     {
     }
-
+#endif
-    void expr_quant_elim_star1::reduce_with_assumption(expr* ctx, expr* fml, expr_ref& result) {
-        proof_ref pr(m);
-        m_assumption = ctx;
-        (*this)(fml, result, pr);
-        m_assumption = m.mk_true();
-    }
 
 
     void hoist_exists(expr_ref& fml, app_ref_vector& vars) {
@@ -2488,6 +2487,7 @@ namespace qe {
 
         virtual ~simplify_solver_context() { reset(); }    
         
+
         void solve(expr_ref& fml, app_ref_vector& vars) {
             init(fml, vars);
             bool solved  = true;
@@ -2580,6 +2580,10 @@ namespace qe {
             m_ctx.updt_params(p);
         }
 
+        void collect_statistics(statistics & st) const {
+            m_ctx.collect_statistics(st);
+        }
+
         bool reduce_quantifier(
             quantifier * old_q, 
             expr * new_body, 
@@ -2647,6 +2651,10 @@ namespace qe {
         imp->updt_params(p);
     }
 
+    void simplify_rewriter_cfg::collect_statistics(statistics & st) const {
+        imp->collect_statistics(st);
+    }
+
     bool simplify_rewriter_cfg::pre_visit(expr* e) {
         if (!is_quantifier(e)) return true;
         quantifier * q = to_quantifier(e);

src/qe/qe.h

@@ -26,7 +26,6 @@ Revision History:
 #include "util/statistics.h"
 #include "util/lbool.h"
 #include "ast/expr_functors.h"
-#include "ast/simplifier/simplifier.h"
 #include "ast/rewriter/rewriter.h"
 #include "model/model.h"
 #include "util/params.h"
@@ -106,6 +105,9 @@ namespace qe {
         i_expr_pred& get_is_relevant() { return m_is_relevant; }
         
         i_nnf_atom& get_mk_atom() { return m_mk_atom; }
+
+        void collect_statistics(statistics & st) const;
+
     };
 
     class conj_enum {
@@ -322,30 +324,6 @@ namespace qe {
         void init_qe();
     };
 
-    class expr_quant_elim_star1 : public simplifier {
-    protected:
-        expr_quant_elim m_quant_elim;
-        expr*       m_assumption;
-        virtual bool visit_quantifier(quantifier * q);
-        virtual void reduce1_quantifier(quantifier * q);
-        virtual bool is_target(quantifier * q) const { return q->get_num_patterns() == 0 && q->get_num_no_patterns() == 0; }
-    public:
-        expr_quant_elim_star1(ast_manager & m, smt_params const& p);
-        virtual ~expr_quant_elim_star1() {}
-
-        void collect_statistics(statistics & st) const {
-            m_quant_elim.collect_statistics(st);
-        }
-
-        void reduce_with_assumption(expr* ctx, expr* fml, expr_ref& result);
-
-        lbool first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) {
-            return m_quant_elim.first_elim(num_vars, vars, fml, defs);
-        }
-
-
-    };
-
     void hoist_exists(expr_ref& fml, app_ref_vector& vars);
 
     void mk_exists(unsigned num_vars, app* const* vars, expr_ref& fml);
@@ -372,6 +350,7 @@ namespace qe {
 
         void updt_params(params_ref const& p);
 
+        void collect_statistics(statistics & st) const;
     };
     
     class simplify_rewriter_star : public rewriter_tpl<simplify_rewriter_cfg> {
@@ -382,6 +361,11 @@ namespace qe {
             m_cfg(m) {}
          
         void updt_params(params_ref const& p) { m_cfg.updt_params(p); }
+
+        void collect_statistics(statistics & st) const {
+            m_cfg.collect_statistics(st);
+        }
+
     };
 
 };

src/qe/qe_cmd.cpp

@@ -44,9 +44,8 @@ public:
     }
     
     virtual void execute(cmd_context & ctx) {
-        smt_params par;
         proof_ref pr(ctx.m());
-        qe::expr_quant_elim_star1 qe(ctx.m(), par);
+        qe::simplify_rewriter_star qe(ctx.m());
         expr_ref result(ctx.m());
 
         qe(m_target, result, pr);            

src/qe/vsubst_tactic.cpp

@@ -1,169 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    vsubst_tactic.cpp
-
-Abstract:
-
-    Check satisfiability of QF_NRA problems using virtual subsititution quantifier-elimination.
-
-Author:
-
-    Nikolaj (nbjorner) 2011-05-16
-
-Notes:
-  Ported to tactic framework on 2012-02-28
-  It was qfnra_vsubst.cpp
-
-  This goal transformation checks satsifiability
-  of quantifier-free non-linear constraints using
-  virtual substitutions (applies to second-degree polynomials).
-  . identify non-linear variables
-  . use the identified variables as non-linear variables.
-  . give up if there are non-linear variables under uninterpreted scope.
-    give up if there are no non-linear variables.
-  . call quantifier elimination with 
-      - non-linear elimination option.
-      - get-first-branch option.
-  . if the first branch is linear, then done.
-    if the result is unsat, then done.
-    if the first branch is non-linear then, 
-    check candidate model,
-    perhaps iterate using rewriting or just give up.
-
-  . helpful facilities: 
-    . linearize_rewriter 
-        a*a*b + a*b = 0 <=> (b+1) = 0 \/ a = 0 \/ b = 0
-    . sign analysis:
-        a*a + b*b + c < 0  => c < 0
-
---*/
-#include "tactic/tactic.h"
-#include "qe/qe.h"
-#include "ast/arith_decl_plugin.h"
-#include "ast/for_each_expr.h"
-#include "tactic/extension_model_converter.h"
-#include "ast/ast_smt2_pp.h"
-
-class vsubst_tactic : public tactic {
-    params_ref m_params;
-
-    class get_var_proc {
-        arith_util       m_arith;
-        ptr_vector<app>& m_vars;
-    public:
-        get_var_proc(ast_manager & m, ptr_vector<app>& vars) : m_arith(m), m_vars(vars) {}
-        
-        void operator()(expr* e) {
-            if (is_app(e)) {
-                app* a = to_app(e);
-                if (m_arith.is_real(e) &&
-                    a->get_num_args() == 0 &&
-                    a->get_family_id() == null_family_id) {
-                    m_vars.push_back(a);
-                }
-            }
-        }
-    };
-
-    void get_vars(ast_manager & m, expr* fml, ptr_vector<app>& vars) {
-        get_var_proc proc(m, vars);
-        for_each_expr(proc, fml);        
-    }
-
-    void main(goal & s, model_converter_ref & mc, params_ref const & p) {
-        ast_manager & m = s.m();
-
-        ptr_vector<expr> fs;
-        for (unsigned i = 0; i < s.size(); ++i) {
-            fs.push_back(s.form(i));
-        }
-        app_ref f(m.mk_and(fs.size(), fs.c_ptr()), m);
-        TRACE("vsubst", 
-              s.display(tout);
-              tout << "goal: " << mk_ismt2_pp(f.get(), m) << "\n";);
-        ptr_vector<app> vars;
-        get_vars(m, f.get(), vars);
-        
-        if (vars.empty()) {
-            TRACE("vsubst", tout << "no real variables\n";);
-            throw tactic_exception("there are no real variables");
-        }
-
-        smt_params params;
-        params.updt_params(p);
-        params.m_model = false;
-        flet<bool> fl1(params.m_nlquant_elim, true);
-        flet<bool> fl2(params.m_nl_arith_gb, false);
-        TRACE("quant_elim", tout << "Produce models: " << params.m_model << "\n";);
-
-        qe::expr_quant_elim_star1 qelim(m, params);
-        expr_ref g(f, m);
-        qe::def_vector defs(m);
-        lbool is_sat = qelim.first_elim(vars.size(), vars.c_ptr(), g, defs);
-        if (is_sat == l_undef) {
-            TRACE("vsubst", tout << mk_ismt2_pp(g, m) << "\n";);
-            throw tactic_exception("elimination was not successful");
-        }
-        if (!defs.empty()) {
-            extension_model_converter * ev = alloc(extension_model_converter, m);
-            mc = ev;
-            for (unsigned i = defs.size(); i > 0; ) {
-                --i;
-                ev->insert(defs.var(i), defs.def(i));
-            }
-        }
-        
-        s.reset();
-        // TBD: wasteful as we already know it is sat or unsat.
-        // TBD: extract model from virtual substitution.
-        s.assert_expr(g);
-
-        TRACE("qfnra_vsubst", 
-              tout << "v-subst result:\n";
-              s.display(tout););
-    }
-
-
-public:
-    vsubst_tactic(params_ref const & p):m_params(p) {}
-
-    virtual tactic * translate(ast_manager & m) {
-        return alloc(vsubst_tactic, m_params);
-    }
-
-    virtual ~vsubst_tactic() {}
-    
-    virtual void updt_params(params_ref const & p) {
-        m_params = p;
-    }
-
-    /**
-       \brief Check satisfiability of an assertion set of QF_NRA
-       by using virtual substitutions.
-    */
-    virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
-                            proof_converter_ref & pc,
-                            expr_dependency_ref & core) {
-        SASSERT(g->is_well_sorted());
-        fail_if_proof_generation("vsubst", g);
-        fail_if_unsat_core_generation("vsubst", g);
-        fail_if_model_generation("vsubst", g); // disable for now due to problems with infinitesimals.
-        mc = 0; pc = 0; core = 0; result.reset();
-        
-        main(*(g.get()), mc, m_params);
-        
-        result.push_back(g.get());
-        SASSERT(g->is_well_sorted());
-    }
-
-    virtual void cleanup(void) {}
-};
-
-tactic * mk_vsubst_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(vsubst_tactic, p);
-}

src/qe/vsubst_tactic.h

@@ -1,33 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    vsubst_tactic.h
-
-Abstract:
-
-    Check satisfiability of QF_NRA problems using virtual subsititution quantifier-elimination.
-
-Author:
-
-    Nikolaj (nbjorner) 2011-05-16
-
-Notes:
-
-
---*/
-#ifndef VSUBST_TACTIC_H_
-#define VSUBST_TACTIC_H_
-
-#include "util/params.h"
-class ast_manager;
-class tactic;
-
-tactic * mk_vsubst_tactic(ast_manager & m, params_ref const & p = params_ref());
-/*
-  ADD_TACTIC("vsubst", "checks satsifiability of quantifier-free non-linear constraints using virtual substitution.", "mk_vsubst_tactic(m, p)")
-*/
-
-#endif
-

src/smt/CMakeLists.txt

@@ -2,7 +2,7 @@ z3_add_component(smt
   SOURCES
     arith_eq_adapter.cpp
     arith_eq_solver.cpp
-    asserted_formulas.cpp
+##  asserted_formulas.cpp
     asserted_formulas_new.cpp
     cached_var_subst.cpp
     cost_evaluator.cpp

src/smt/arith_eq_adapter.cpp

@@ -22,7 +22,6 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "util/stats.h"
-#include "ast/simplifier/simplifier.h"
 #include "ast/ast_smt2_pp.h"
 
 namespace smt {

src/smt/params/CMakeLists.txt

@@ -13,7 +13,6 @@ z3_add_component(smt_params
     ast
     bit_blaster
     pattern
-    simplifier
   PYG_FILES
     smt_params_helper.pyg
 )

src/smt/params/preprocessor_params.cpp

@@ -48,7 +48,6 @@ void preprocessor_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_pull_cheap_ite_trees);
     DISPLAY_PARAM(m_pull_nested_quantifiers);
     DISPLAY_PARAM(m_eliminate_term_ite);
-    //DISPLAY_PARAM(m_eliminate_and);
     DISPLAY_PARAM(m_macro_finder);
     DISPLAY_PARAM(m_propagate_values);
     DISPLAY_PARAM(m_propagate_booleans);

src/smt/params/preprocessor_params.h

@@ -39,7 +39,6 @@ struct preprocessor_params : public pattern_inference_params,
     bool            m_pull_cheap_ite_trees;
     bool            m_pull_nested_quantifiers;
     bool            m_eliminate_term_ite;
-//    bool            m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
     bool            m_macro_finder;
     bool            m_propagate_values;
     bool            m_propagate_booleans;
@@ -62,7 +61,6 @@ public:
         m_pull_cheap_ite_trees(false),
         m_pull_nested_quantifiers(false),
         m_eliminate_term_ite(false),
-       // m_eliminate_and(true),
         m_macro_finder(false),
         m_propagate_values(true),
         m_propagate_booleans(false), // TODO << check peformance

src/tactic/bv/elim_small_bv_tactic.cpp

@@ -24,9 +24,7 @@ Revision History:
 #include "ast/used_vars.h"
 #include "ast/well_sorted.h"
 #include "ast/rewriter/var_subst.h"
-#include "ast/simplifier/simplifier.h"
+#include "ast/rewriter/th_rewriter.h"
-#include "ast/simplifier/basic_simplifier_plugin.h"
-#include "ast/simplifier/bv_simplifier_plugin.h"
 
 #include "tactic/bv/elim_small_bv_tactic.h"
 
@@ -36,7 +34,7 @@ class elim_small_bv_tactic : public tactic {
         ast_manager               & m;
         params_ref                  m_params;
         bv_util                     m_util;
-        simplifier                  m_simp;
+        th_rewriter                 m_simp;
         ref<filter_model_converter> m_mc;
         goal *                      m_goal;
         unsigned                    m_max_bits;
@@ -56,14 +54,6 @@ class elim_small_bv_tactic : public tactic {
             updt_params(p);
             m_goal = 0;
             m_max_steps = UINT_MAX;
-
-            basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m);
-            // bsimp->set_eliminate_and(true);
-            m_simp.register_plugin(bsimp);
-
-            bv_simplifier_params bv_params;
-            bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, bv_params);
-            m_simp.register_plugin(bvsimp);
         }
 
         bool max_steps_exceeded(unsigned long long num_steps) const {