make smt2 log scope aware

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

src/api/api_solver.cpp

@@ -59,6 +59,7 @@ extern "C" {
 
     void solver2smt2_pp::push() {
         m_out << "(push)\n";
+        m_pp_util.push();
     }
 
     void solver2smt2_pp::reset() {
@@ -68,6 +69,7 @@ extern "C" {
 
     void solver2smt2_pp::pop(unsigned n) {
         m_out << "(pop " << n << ")\n";
+        m_pp_util.pop(n);
     }
 
     void solver2smt2_pp::check(unsigned n, expr* const* asms) {

src/ast/ast_pp_util.cpp

@@ -113,3 +113,17 @@ 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);
+}
+
+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);
+}

src/ast/ast_pp_util.h

@@ -28,6 +28,7 @@ class ast_pp_util {
     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;
     
  public:        
 
@@ -37,6 +38,7 @@ class ast_pp_util {
 
     void reset() { coll.reset(); m_removed.reset(); m_num_sorts = 0; m_num_decls = 0; }
 
+
     void collect(expr* e);
 
     void collect(unsigned n, expr* const* es);
@@ -55,6 +57,10 @@ class ast_pp_util {
 
     std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true);
 
+    void push();
+    
+    void pop(unsigned n);
+
     smt2_pp_environment& env() { return m_env; }
 };
 

src/ast/decl_collector.cpp

@@ -69,7 +69,6 @@ void decl_collector::visit(ast* n) {
     if (m_visited.is_marked(n)) 
         return;
     datatype_util util(m());
-    m_trail.push_back(n);
     m_todo.push_back(n);
     while (!m_todo.empty()) {
         n = m_todo.back();
@@ -114,6 +113,7 @@ void decl_collector::visit(ast* n) {
                 UNREACHABLE();
             }
             m_visited.mark(n, true);
+            m_trail.push_back(n);
         }
     }
 }
@@ -161,4 +161,23 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
     }
 }
 
+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());
+}
+
+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; ) {
+        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);
+}
 

src/ast/decl_collector.h

@@ -30,6 +30,9 @@ class decl_collector {
     ptr_vector<func_decl> m_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;
@@ -54,6 +57,9 @@ public:
     void visit(unsigned n, expr* const* es);
     void visit(expr_ref_vector const& es);
 
+    void push();
+    void pop(unsigned n);
+
     void order_deps(unsigned n);
 
     unsigned get_num_sorts() const { return m_sorts.size(); }