update pretty printer for recursive function filtering

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/ast_pp_util.cpp

@@ -27,9 +27,8 @@ void ast_pp_util::collect(expr* e) {
 }
 
 void ast_pp_util::collect(unsigned n, expr* const* es) {
-    for (unsigned i = 0; i < n; ++i) {
+    for (unsigned i = 0; i < n; ++i) 
         coll.visit(es[i]);
-    }
 }
 
 void ast_pp_util::collect(expr_ref_vector const& es) {
@@ -38,31 +37,31 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
 
 void ast_pp_util::display_decls(std::ostream& out) {
     ast_smt_pp pp(m);
-    bool first = m_num_decls == 0;
-    coll.order_deps(m_num_sorts);
+    coll.order_deps(m_sorts);
     unsigned n = coll.get_num_sorts();
     ast_mark seen;
-    for (unsigned i = m_num_sorts; i < n; ++i) 
+    for (unsigned i = m_sorts; i < n; ++i) 
         pp.display_sort_decl(out, coll.get_sorts()[i], seen);
-    m_num_sorts = n;
+    m_sorts = n;
+
     n = coll.get_num_decls();
-    for (unsigned i = m_num_decls; i < n; ++i) {
+    for (unsigned i = m_decls; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
-        if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
+        if (f->get_family_id() == null_family_id && !m_removed.contains(f)) 
             ast_smt2_pp(out, f, m_env) << "\n";
-        }
     }
-    m_num_decls = n;
-    if (first) {
-        vector<std::pair<func_decl*, expr*>> recfuns;
-        recfun::util u(m);
-        func_decl_ref_vector funs = u.get_rec_funs();
-        if (funs.empty()) return;
-        for (func_decl * f : funs) {
-            recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
-        }
-        ast_smt2_pp_recdefs(out, recfuns, m_env);
+    m_decls = n;
+
+    n = coll.get_rec_decls().size();
+    vector<std::pair<func_decl*, expr*>> recfuns;
+    recfun::util u(m);
+    for (unsigned i = m_rec_decls; i < n; ++i) {
+        func_decl* f = coll.get_rec_decls()[i];
+        recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
     }
+    if (!recfuns.empty())
+        ast_smt2_pp_recdefs(out, recfuns, m_env);
+    m_rec_decls = n;
 }
 
 void ast_pp_util::remove_decl(func_decl* f) {
@@ -116,14 +115,14 @@ void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls
 
 void ast_pp_util::push() {
     coll.push();
-    m_num_sorts_trail.push_back(m_num_sorts);
-    m_num_decls_trail.push_back(m_num_decls);
+    m_rec_decls.push();
+    m_decls.push();
+    m_sorts.push();
 }
 
 void ast_pp_util::pop(unsigned n) {
     coll.pop(n);
-    m_num_sorts = m_num_sorts_trail[m_num_sorts_trail.size() - n];
-    m_num_decls = m_num_decls_trail[m_num_decls_trail.size() - n];
-    m_num_sorts_trail.shrink(m_num_sorts_trail.size() - n);
-    m_num_decls_trail.shrink(m_num_decls_trail.size() - n);
+    m_rec_decls.pop(n);
+    m_decls.pop(n);
+    m_sorts.pop(n);
 }

src/ast/ast_pp_util.h

@@ -21,22 +21,24 @@ Revision History:
 #include "ast/decl_collector.h"
 #include "ast/ast_smt2_pp.h"
 #include "util/obj_hashtable.h"
+#include "util/stacked_value.h"
 
 class ast_pp_util {
     ast_manager&        m;
     obj_hashtable<func_decl> m_removed;
     smt2_pp_environment_dbg m_env;
-    unsigned                m_num_sorts, m_num_decls;
-    unsigned_vector         m_num_sorts_trail, m_num_decls_trail;
+    stacked_value<unsigned> m_rec_decls;
+    stacked_value<unsigned> m_decls;
+    stacked_value<unsigned> m_sorts;
 
  public:        
 
     decl_collector      coll;
 
-    ast_pp_util(ast_manager& m): m(m), m_env(m), m_num_sorts(0), m_num_decls(0), coll(m) {}
-
-    void reset() { coll.reset(); m_removed.reset(); m_num_sorts = 0; m_num_decls = 0; }
+    ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_rec_decls(0), m_decls(0), m_sorts(0) {}
 
+    void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); }
+
 
     void collect(expr* e);
 

src/ast/decl_collector.cpp

@@ -19,6 +19,7 @@ Revision History:
 --*/
 #include "ast/decl_collector.h"
 #include "ast/ast_pp.h"
+#include "ast/recfun_decl_plugin.h"
 
 void decl_collector::visit_sort(sort * n) {
     SASSERT(!m_visited.is_marked(n));
@@ -49,8 +50,12 @@ bool decl_collector::is_bool(sort * s) {
 void decl_collector::visit_func(func_decl * n) {
     if (!m_visited.is_marked(n)) {
         family_id fid = n->get_family_id();
-        if (fid == null_family_id) {
+        if (fid == null_family_id) 
             m_decls.push_back(n);
+        else if (fid == m_rec_fid) {
+            m_rec_decls.push_back(n);
+            recfun::util u(m());
+            m_todo.push_back(u.get_def(n).get_rhs());
         }
         m_visited.mark(n, true);
         m_trail.push_back(n);
@@ -63,6 +68,8 @@ decl_collector::decl_collector(ast_manager & m):
     m_dt_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);
+    m_rec_fid = rec_util.get_family_id();
 }
 
 void decl_collector::visit(ast* n) {
@@ -143,9 +150,8 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
     set.insert(s);
     if (s->is_sort_of(m_dt_util.get_family_id(), DATATYPE_SORT)) {
         unsigned num_sorts = m_dt_util.get_datatype_num_parameter_sorts(s);
-        for (unsigned i = 0; i < num_sorts; ++i) {
+        for (unsigned i = 0; i < num_sorts; ++i) 
             set.insert(m_dt_util.get_datatype_parameter_sort(s, i));
-        }
         unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(s);
         for (unsigned i = 0; i < num_cnstr; i++) {
             func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
@@ -157,29 +163,27 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
 
     for (unsigned i = s->get_num_parameters(); i-- > 0; ) {
         parameter const& p = s->get_parameter(i);
-        if (p.is_ast() && is_sort(p.get_ast())) {
+        if (p.is_ast() && is_sort(p.get_ast())) 
             set.insert(to_sort(p.get_ast()));
-        }
     }
 }
 
 void decl_collector::push() {
     m_trail_lim.push_back(m_trail.size());
-    m_sorts_lim.push_back(m_sorts.size());
-    m_decls_lim.push_back(m_decls.size());
+    m_sorts.push_scope();
+    m_decls.push_scope();
+    m_rec_decls.push_scope();
 }
 
 void decl_collector::pop(unsigned n) {
     SASSERT(n > 0);
     unsigned sz = m_trail_lim[m_trail_lim.size() - n];
-    for (unsigned i = m_trail.size(); i-- > sz; ) {
+    for (unsigned i = m_trail.size(); i-- > sz; ) 
         m_visited.mark(m_trail.get(i), false);
-    }
     m_trail.shrink(sz);
-    m_sorts.shrink(m_sorts_lim[m_sorts_lim.size() - n]);
-    m_decls.shrink(m_decls_lim[m_decls_lim.size() - n]);
     m_trail_lim.shrink(m_trail_lim.size() - n);
-    m_sorts_lim.shrink(m_sorts_lim.size() - n);
-    m_decls_lim.shrink(m_decls_lim.size() - n);
+    m_sorts.pop_scope(n);
+    m_decls.pop_scope(n);
+    m_rec_decls.pop_scope(n);
 }
 

src/ast/decl_collector.h

@@ -20,21 +20,22 @@ Revision History:
 #pragma once
 
 #include "util/top_sort.h"
+#include "util/lim_vector.h"
 #include "ast/ast.h"
 #include "ast/datatype_decl_plugin.h"
 
 class decl_collector {
     ast_manager &         m_manager;
-    ptr_vector<sort>      m_sorts;
-    ptr_vector<func_decl> m_decls;
+    lim_svector<sort*>      m_sorts;
+    lim_svector<func_decl*> m_decls;
+    lim_svector<func_decl*> m_rec_decls;
     ast_mark              m_visited;
     ast_ref_vector        m_trail;
     unsigned_vector       m_trail_lim;
-    unsigned_vector       m_sorts_lim;
-    unsigned_vector       m_decls_lim;
     family_id             m_basic_fid;
     family_id             m_dt_fid;
     datatype_util         m_dt_util;
+    family_id             m_rec_fid;
     ptr_vector<ast>       m_todo;
 
     void visit_sort(sort* n);
@@ -64,7 +65,8 @@ class decl_collector {
     unsigned get_num_sorts() const { return m_sorts.size(); }
     unsigned get_num_decls() const { return m_decls.size(); }
 
-    ptr_vector<sort> const& get_sorts() const { return m_sorts; }
-    ptr_vector<func_decl> const& get_func_decls() const { return m_decls; }
+    lim_svector<sort*> const& get_sorts() const { return m_sorts; }
+    lim_svector<func_decl*> const& get_func_decls() const { return m_decls; }
+    lim_svector<func_decl*> const& get_rec_decls() const { return m_rec_decls; }
 };
 

src/util/stacked_value.h

@@ -20,23 +20,24 @@ Revision History:
 
 #pragma once
 // add to value the stack semantics
-#include <stack>
+#include "util/vector.h"
 template <typename T> class stacked_value {
     T m_value;    
-    std::stack<T> m_stack;
+    vector<T> m_stack;
 public:
 
 
     void push() {
-        m_stack.push(m_value);
+        m_stack.push_back(m_value);
     }
 
-    void clear() {
-        m_stack.clear();
+    void clear(T const& m) {
+        pop(m_stack.size());
+        m_value = m;
     }
 
     unsigned stack_size() const {
-        return static_cast<unsigned>(m_stack.size());
+        return m_stack.size();
     }
 
     void pop() {
@@ -46,8 +47,8 @@ template <typename T> class stacked_value {
         while (k-- > 0) {
             if (m_stack.empty())
                 return;
-            m_value = m_stack.top();
-            m_stack.pop();
+            m_value = m_stack.back();
+            m_stack.pop_back();
         }
     }