pdate decl collection to include functions under arrays

Signedoff-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 12, 2022 · 88b6c4a · 88b6c4a
1 parent 72f4ee9
commit 88b6c4a
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 3 deletions.
diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
@@ -48,6 +48,7 @@ bool decl_collector::is_bool(sort * s) {
 }
 
 void decl_collector::visit_func(func_decl * n) {
+    func_decl* g;
     if (!m_visited.is_marked(n)) {
         family_id fid = n->get_family_id();
         if (fid == null_family_id) 
@@ -57,6 +58,8 @@ void decl_collector::visit_func(func_decl * n) {
             recfun::util u(m());
             m_todo.push_back(u.get_def(n).get_rhs());
         }
+        else if (m_ar_util.is_as_array(n, g)) 
+            m_todo.push_back(g);
         m_visited.mark(n, true);
         m_trail.push_back(n);
     }
@@ -65,7 +68,8 @@ void decl_collector::visit_func(func_decl * n) {
 decl_collector::decl_collector(ast_manager & m):
     m_manager(m),
     m_trail(m),
-    m_dt_util(m) {
+    m_dt_util(m),
+    m_ar_util(m) {
     m_basic_fid = m_manager.get_basic_family_id();
     m_dt_fid = m_dt_util.get_family_id();
     recfun::util rec_util(m);
@@ -156,8 +160,15 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
         for (unsigned i = 0; i < num_cnstr; i++) {
             func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
             set.insert(cnstr->get_range());
-            for (unsigned j = 0; j < cnstr->get_arity(); ++j) 
-                set.insert(cnstr->get_domain(j));
+            for (unsigned j = 0; j < cnstr->get_arity(); ++j) {
+                sort* n = cnstr->get_domain(j);
+                set.insert(n);
+                for (unsigned i = n->get_num_parameters(); i-- > 0; ) {
+                    parameter const& p = n->get_parameter(i);
+                    if (p.is_ast() && is_sort(p.get_ast()))
+                        set.insert(to_sort(p.get_ast()));
+                }
+            }
         }
     }
 

diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
@@ -23,6 +23,7 @@ Revision History:
 #include "util/lim_vector.h"
 #include "ast/ast.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
 
 class decl_collector {
     ast_manager &         m_manager;
@@ -35,6 +36,7 @@ class decl_collector {
     family_id             m_basic_fid;
     family_id             m_dt_fid;
     datatype_util         m_dt_util;
+    array_util            m_ar_util;
     family_id             m_rec_fid;
     ptr_vector<ast>       m_todo;