From 9acbfa392361e785365498cfe18e3276d8fa10fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Dec 2022 06:23:32 -0800
Subject: [PATCH] move it into substitution to handle dependencies

---
 src/ast/rewriter/CMakeLists.txt               |  1 -
 src/ast/substitution/CMakeLists.txt           |  1 +
 .../demodulator_rewriter.cpp                  | 51 +++++++++----------
 .../demodulator_rewriter.h                    |  0
 src/tactic/ufbv/ufbv_rewriter_tactic.cpp      |  8 +--
 5 files changed, 29 insertions(+), 32 deletions(-)
 rename src/ast/{rewriter => substitution}/demodulator_rewriter.cpp (95%)
 rename src/ast/{rewriter => substitution}/demodulator_rewriter.h (100%)

diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index 9eef651c8..c785804c1 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/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
diff --git a/src/ast/substitution/CMakeLists.txt b/src/ast/substitution/CMakeLists.txt
index 80e12c995..8dbf2c9e3 100644
--- a/src/ast/substitution/CMakeLists.txt
+++ b/src/ast/substitution/CMakeLists.txt
@@ -1,5 +1,6 @@
 z3_add_component(substitution
   SOURCES
+    demodulator_rewriter.cpp
     matcher.cpp
     substitution.cpp
     substitution_tree.cpp
diff --git a/src/ast/rewriter/demodulator_rewriter.cpp b/src/ast/substitution/demodulator_rewriter.cpp
similarity index 95%
rename from src/ast/rewriter/demodulator_rewriter.cpp
rename to src/ast/substitution/demodulator_rewriter.cpp
index f1fc6f969..6e79242e0 100644
--- a/src/ast/rewriter/demodulator_rewriter.cpp
+++ b/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;
-    unsigned j = a->get_num_args();
-    while (j > 0) {
-        expr * e = a->get_arg(--j);
-        if (!m_rewrite_cache.contains(e) || !m_rewrite_cache.get(e).second) {
-            bool recursive = false;
-            unsigned sz = m_rewrite_todo.size();
-            expr * v = e;
-            if (m_rewrite_cache.contains(e)) {
-                expr_bool_pair const & ebp = m_rewrite_cache.get(e);
-                if (ebp.second) {
-                    v = ebp.first;
-                }
-            }
-            for (unsigned i = sz; i-- > 0;) {
-                if (m_rewrite_todo[i] == v) {
-                    recursive = true;
-                    TRACE("demodulator", tout << "Detected demodulator cycle: " <<
-                        mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;);
-                    rewrite_cache(e, v, true);
-                    break;
-                }
-            }
-            if (!recursive) {
-                m_rewrite_todo.push_back(e);
-                res = false;
+    bool res = true;
+    for (expr* e : *a) {
+        if (m_rewrite_cache.contains(e) && m_rewrite_cache.get(e).second)
+            continue;
+        bool recursive = false;
+        unsigned sz = m_rewrite_todo.size();
+        expr * v = e;
+        if (m_rewrite_cache.contains(e)) {
+            expr_bool_pair const & ebp = m_rewrite_cache.get(e);
+            if (ebp.second) 
+                v = ebp.first;
+        }
+        for (unsigned i = sz; i-- > 0;) {
+            if (m_rewrite_todo[i] == v) {
+                recursive = true;
+                TRACE("demodulator", tout << "Detected demodulator cycle: " <<
+                      mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;);
+                rewrite_cache(e, v, true);
+                break;
             }
         }
+        if (!recursive) {
+            m_rewrite_todo.push_back(e);
+            res = false;
+        }
     }
     return res;
 }
diff --git a/src/ast/rewriter/demodulator_rewriter.h b/src/ast/substitution/demodulator_rewriter.h
similarity index 100%
rename from src/ast/rewriter/demodulator_rewriter.h
rename to src/ast/substitution/demodulator_rewriter.h
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index f374ea114..66d377491 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/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++)
-            g->assert_expr(new_forms.get(i), nullptr, nullptr);
+        for (expr* fml : new_forms)
+            g->assert_expr(fml, nullptr, nullptr);
 
         // CMW: Remark: The demodulator could potentially
         // remove all references to a variable.