get rid of a simplifier dependency

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

contrib/cmake/src/ast/rewriter/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(rewriter
     bv_rewriter.cpp
     datatype_rewriter.cpp
     der.cpp
+    distribute_forall.cpp
     dl_rewriter.cpp
     enum2bv_rewriter.cpp
     expr_replacer.cpp

contrib/cmake/src/ast/simplifier/CMakeLists.txt

@@ -10,7 +10,6 @@ z3_add_component(simplifier
     bv_simplifier_params.cpp
     bv_simplifier_plugin.cpp
     datatype_simplifier_plugin.cpp
-    distribute_forall.cpp
     elim_bounds.cpp
     fpa_simplifier_plugin.cpp
     inj_axiom.cpp

src/ast/rewriter/distribute_forall.cpp

@@ -20,12 +20,12 @@ Revision History:
 --*/
 #include"var_subst.h"
 #include"ast_ll_pp.h"
-
+#include"ast_util.h"
 #include"distribute_forall.h"
+#include"bool_rewriter.h"
 
-distribute_forall::distribute_forall(ast_manager & m, basic_simplifier_plugin & p) :
+distribute_forall::distribute_forall(ast_manager & m) :
     m_manager(m),
-    m_bsimp(p),
     m_cache(m) {
 }
 
@@ -109,6 +109,8 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
 
     expr * e = get_cached(q->get_expr());
     if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) {
+        bool_rewriter br(m_manager);
+
         // found target for simplification
         // (forall X (not (or F1 ... Fn)))
         // -->
@@ -121,8 +123,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
         for (unsigned i = 0; i < num_args; i++) {
             expr * arg = or_e->get_arg(i);
             expr_ref not_arg(m_manager);
-            // m_bsimp.mk_not applies basic simplifications. For example, if arg is of the form (not a), then it will return a.
-            m_bsimp.mk_not(arg, not_arg);
+            br.mk_not(arg, not_arg);
             quantifier_ref tmp_q(m_manager);
             tmp_q = m_manager.update_quantifier(q, not_arg);
             expr_ref new_q(m_manager);
@@ -132,7 +133,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
         expr_ref result(m_manager);
         // m_bsimp.mk_and actually constructs a (not (or ...)) formula,
         // it will also apply basic simplifications.
-        m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result);
+        br.mk_and(new_args.size(), new_args.c_ptr(), result);
         cache_result(q, result);
     }
     else {

src/ast/rewriter/distribute_forall.h

@@ -22,7 +22,6 @@ Revision History:
 #define DISTRIBUTE_FORALL_H_
 
 #include"ast.h"
-#include"basic_simplifier_plugin.h"
 #include"act_cache.h"
 
 /**
@@ -47,7 +46,6 @@ Revision History:
 class distribute_forall {
     typedef act_cache expr_map;
     ast_manager &             m_manager;
-    basic_simplifier_plugin & m_bsimp; // useful for constructing formulas and/or/not in simplified form.
     ptr_vector<expr>          m_todo;
     expr_map                  m_cache;
     ptr_vector<expr>          m_new_args;
@@ -57,7 +55,7 @@ class distribute_forall {
 
 
 public:
-    distribute_forall(ast_manager & m, basic_simplifier_plugin & p);
+    distribute_forall(ast_manager & m);
 
     /**
        \brief Apply the distribute_forall transformation (when possible) to all universal quantifiers in \c f.

src/smt/asserted_formulas.cpp

@@ -505,7 +505,7 @@ void asserted_formulas::NAME() {
     TRACE(LABEL, display(tout););                                                                                       \
 }
 
-MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m, *m_bsimp), "distribute_forall", "distribute-forall");
+MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall");
 
 void asserted_formulas::reduce_and_solve() {
     IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";);