move it into substitution to handle dependencies

src/ast/rewriter/CMakeLists.txt

@@ -11,7 +11,6 @@ z3_add_component(rewriter
     cached_var_subst.cpp
     char_rewriter.cpp
     datatype_rewriter.cpp
-    demodulator_rewriter.cpp
     der.cpp
     distribute_forall.cpp
     dl_rewriter.cpp

src/ast/substitution/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(substitution
   SOURCES
+    demodulator_rewriter.cpp
     matcher.cpp
     substitution.cpp
     substitution_tree.cpp

src/ast/substitution/demodulator_rewriter.cpp

@@ -25,7 +25,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/var_subst.h"
-#include "ast/rewriter/demodulator_rewriter.h"
+#include "ast/substitution/demodulator_rewriter.h"
 
 demodulator_rewriter::demodulator_rewriter(ast_manager & m):
     m(m),
@@ -284,34 +284,31 @@ bool demodulator_rewriter::rewrite1(func_decl * f, expr_ref_vector const & args,
 }
 
 bool demodulator_rewriter::rewrite_visit_children(app * a) {
-    bool res=true;
+    bool res = true;
-    unsigned j = a->get_num_args();
+    for (expr* e : *a) {
-    while (j > 0) {
+        if (m_rewrite_cache.contains(e) && m_rewrite_cache.get(e).second)
-        expr * e = a->get_arg(--j);
+            continue;
-        if (!m_rewrite_cache.contains(e) || !m_rewrite_cache.get(e).second) {
+        bool recursive = false;
-            bool recursive = false;
+        unsigned sz = m_rewrite_todo.size();
-            unsigned sz = m_rewrite_todo.size();
+        expr * v = e;
-            expr * v = e;
+        if (m_rewrite_cache.contains(e)) {
-            if (m_rewrite_cache.contains(e)) {
+            expr_bool_pair const & ebp = m_rewrite_cache.get(e);
-                expr_bool_pair const & ebp = m_rewrite_cache.get(e);
+            if (ebp.second) 
-                if (ebp.second) {
+                v = ebp.first;
-                    v = ebp.first;
+        }
-                }
+        for (unsigned i = sz; i-- > 0;) {
-            }
+            if (m_rewrite_todo[i] == v) {
-            for (unsigned i = sz; i-- > 0;) {
+                recursive = true;
-                if (m_rewrite_todo[i] == v) {
+                TRACE("demodulator", tout << "Detected demodulator cycle: " <<
-                    recursive = true;
+                      mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;);
-                    TRACE("demodulator", tout << "Detected demodulator cycle: " <<
+                rewrite_cache(e, v, true);
-                        mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;);
+                break;
-                    rewrite_cache(e, v, true);
-                    break;
-                }
-            }
-            if (!recursive) {
-                m_rewrite_todo.push_back(e);
-                res = false;
             }
         }
+        if (!recursive) {
+            m_rewrite_todo.push_back(e);
+            res = false;
+        }
     }
     return res;
 }

src/tactic/ufbv/ufbv_rewriter_tactic.cpp

@@ -17,7 +17,7 @@ Notes:
 
 --*/
 #include "tactic/tactical.h"
-#include "ast/rewriter/demodulator_rewriter.h"
+#include "ast/substitution/demodulator_rewriter.h"
 #include "tactic/ufbv/ufbv_rewriter_tactic.h"
 
 class demodulator_rewriter_tactic : public tactic {
@@ -28,7 +28,7 @@ public:
     demodulator_rewriter_tactic(ast_manager & m, params_ref const & p):
         m_manager(m), m_params(p) {}
 
-    char const* name() const override { return "ufbv"; }
+    char const* name() const override { return "ufbv-rewriter"; }
 
     tactic * translate(ast_manager & m) override {
         return alloc(demodulator_rewriter_tactic, m, m_params);
@@ -63,8 +63,8 @@ public:
         dem(forms, new_forms);
 
         g->reset();
-        for (unsigned i = 0; i < new_forms.size(); i++)
+        for (expr* fml : new_forms)
-            g->assert_expr(new_forms.get(i), nullptr, nullptr);
+            g->assert_expr(fml, nullptr, nullptr);
 
         // CMW: Remark: The demodulator could potentially
         // remove all references to a variable.