remove simplifier dependencies from cmakelist.txt files

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

src/ast/fpa/CMakeLists.txt

@@ -5,7 +5,7 @@ z3_add_component(fpa
     fpa2bv_rewriter.cpp
   COMPONENT_DEPENDENCIES
     ast
-    simplifier
+    rewriter
     model
     util
   PYG_FILES

src/ast/macros/CMakeLists.txt

@@ -5,5 +5,5 @@ z3_add_component(macros
     macro_util.cpp
     quasi_macros.cpp
   COMPONENT_DEPENDENCIES
-    simplifier
+    rewriter
 )

src/ast/pattern/CMakeLists.txt

@@ -29,7 +29,7 @@ z3_add_component(pattern
     ${CMAKE_CURRENT_BINARY_DIR}/database.h
   COMPONENT_DEPENDENCIES
     normal_forms
-    simplifier
+    rewriter
     smt2parser
   PYG_FILES
     pattern_inference_params_helper.pyg

src/ast/pattern/pattern_inference.cpp

@@ -89,6 +89,15 @@ bool smaller_pattern::operator()(unsigned num_bindings, expr * p1, expr * p2) {
     return process(p1, p2);
 }
 
+
+#ifdef _TRACE
+static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
+    for (app * e : v) 
+        out << mk_pp(e, m) << "\n";
+}
+#endif
+
+#if 0
 pattern_inference_old::pattern_inference_old(ast_manager & m, pattern_inference_params & params):
     simplifier(m),
     m_params(params),
@@ -470,12 +479,6 @@ void pattern_inference_old::reset_pre_patterns() {
     m_pre_patterns.reset();
 }
 
-#ifdef _TRACE
-static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
-    for (app * e : v) 
-        out << mk_pp(e, m) << "\n";
-}
-#endif
 
 bool pattern_inference_old::is_forbidden(app * n) const {
     func_decl const * decl = n->get_decl();
@@ -567,7 +570,6 @@ void pattern_inference_old::mk_patterns(unsigned num_bindings,
     m_candidates.reset();
 }
 
-#include "ast/pattern/database.h"
 
 void pattern_inference_old::reduce1_quantifier(quantifier * q) {
     TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
@@ -729,6 +731,9 @@ void pattern_inference_old::reduce1_quantifier(quantifier * q) {
     cache_result(q, new_q, pr);
 }
 
+#endif
+
+#include "ast/pattern/database.h"
 
 
 pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_params & params):

src/ast/pattern/pattern_inference.h

@@ -61,6 +61,7 @@ public:
     bool operator()(unsigned num_bindings, expr * p1, expr * p2);
 };
 
+#if 0
 class pattern_inference_old : public simplifier {
     pattern_inference_params & m_params;
     family_id                  m_bfid;
@@ -244,6 +245,7 @@ public:
 
     bool is_forbidden(app * n) const;
 };
+#endif
 
 class pattern_inference_cfg :  public default_rewriter_cfg {
     ast_manager&               m;

src/ast/rewriter/bit_blaster/CMakeLists.txt

@@ -4,5 +4,4 @@ z3_add_component(bit_blaster
     bit_blaster_rewriter.cpp
   COMPONENT_DEPENDENCIES
     rewriter
-    simplifier
 )

src/model/model_core.cpp

@@ -19,18 +19,14 @@ Revision History:
 #include "model/model_core.h"
 
 model_core::~model_core() {
-    decl2expr::iterator it1  = m_interp.begin();
+    for (auto & kv : m_interp) {
-    decl2expr::iterator end1 = m_interp.end();
+        m_manager.dec_ref(kv.m_key);
-    for (; it1 != end1; ++it1) {
+        m_manager.dec_ref(kv.m_value);
-        m_manager.dec_ref(it1->m_key);
-        m_manager.dec_ref(it1->m_value);
     }
 
-    decl2finterp::iterator it2  = m_finterp.begin();
+    for (auto & kv : m_finterp) {
-    decl2finterp::iterator end2 = m_finterp.end();
+        m_manager.dec_ref(kv.m_key);
-    for (; it2 != end2; ++it2) {
+        dealloc(kv.m_value);
-        m_manager.dec_ref(it2->m_key);
-        dealloc(it2->m_value);
     }
 }
 

src/muz/transforms/dl_mk_quantifier_instantiation.cpp

@@ -70,7 +70,7 @@ namespace datalog {
         if (q->get_num_patterns() == 0) {
             proof_ref new_pr(m);
             pattern_inference_params params;
-            pattern_inference_old infer(m, params);
+            pattern_inference_rw infer(m, params);
             infer(q, qe, new_pr);
             q = to_quantifier(qe);
         }

src/smt/proto_model/CMakeLists.txt

@@ -8,6 +8,6 @@ z3_add_component(proto_model
     value_factory.cpp
   COMPONENT_DEPENDENCIES
     model
-    simplifier
+    rewriter
     smt_params
 )