fix assert-and-track semantics for smt2 logging

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

src/api/api_solver.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "util/cancel_eh.h"
 #include "util/file_path.h"
 #include "util/scoped_timer.h"
+#include "util/file_path.h"
 #include "ast/ast_pp.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
@@ -30,11 +31,10 @@ Revision History:
 #include "api/api_model.h"
 #include "api/api_stats.h"
 #include "api/api_ast_vector.h"
-#include "solver/tactic2solver.h"
-#include "util/file_path.h"
 #include "smt/smt_solver.h"
 #include "smt/smt_implied_equalities.h"
 #include "solver/smt_logics.h"
+#include "solver/tactic2solver.h"
 #include "cmd_context/cmd_context.h"
 #include "parsers/smt2/smt2parser.h"
 #include "sat/dimacs.h"
@@ -55,28 +55,34 @@ extern "C" {
         m_pp_util.collect(t);
         m_pp_util.display_decls(m_out);
         m_pp_util.display_assert_and_track(m_out, e, t, true);
+        m_tracked.push_back(t);
     }
 
     void solver2smt2_pp::push() {
         m_out << "(push)\n";
         m_pp_util.push();
-    }
-
-    void solver2smt2_pp::reset() {
-        m_out << "(reset)\n";
-        m_pp_util.reset();
+        m_tracked_lim.push_back(m_tracked.size());
     }
 
     void solver2smt2_pp::pop(unsigned n) {
         m_out << "(pop " << n << ")\n";
         m_pp_util.pop(n);
+        m_tracked.shrink(m_tracked_lim[m_tracked_lim.size() - n]);
+        m_tracked_lim.shrink(m_tracked_lim.size() - n);
+    }
+
+    void solver2smt2_pp::reset() {
+        m_out << "(reset)\n";
+        m_pp_util.reset();        
     }
 
     void solver2smt2_pp::check(unsigned n, expr* const* asms) {
-        m_out << "(check-sat";
+        m_out << "(check-sat";        
         for (unsigned i = 0; i < n; ++i) {
-            m_out << "\n";
-            m_pp_util.display_expr(m_out, asms[i]);            
+            m_pp_util.display_expr(m_out << "\n", asms[i]);            
+        }
+        for (expr* e : m_tracked) {
+            m_pp_util.display_expr(m_out << "\n", e);
         }
         m_out << ")\n";
         m_out.flush();
@@ -98,7 +104,7 @@ extern "C" {
     }
 
 
-    solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) {
+    solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file), m_tracked(m) {
         if (!m_out) {
             throw default_exception("could not open " + std::string(file) + " for output");
         }

src/api/api_solver.h

@@ -24,6 +24,8 @@ Revision History:
 struct solver2smt2_pp {
     ast_pp_util m_pp_util;
     std::ofstream m_out;
+    expr_ref_vector m_tracked;
+    unsigned_vector m_tracked_lim;
     solver2smt2_pp(ast_manager& m, char const* file);
     void assert_expr(expr* e);
     void assert_expr(expr* e, expr* t);

src/ast/normal_forms/nnf.cpp

@@ -70,6 +70,8 @@ class skolemizer {
     bool          m_sk_hack_enabled;
     cache         m_cache;
     cache         m_cache_pr;
+    bool          m_proofs_enabled;
+
 
     void process(quantifier * q, expr_ref & r, proof_ref & p) {
         if (q->get_kind() == lambda_k) {
@@ -142,7 +144,7 @@ class skolemizer {
         }
         r = s(body, substitution.size(), substitution.c_ptr());
         p = nullptr;
-        if (m.proofs_enabled()) {
+        if (m_proofs_enabled) {
             if (q->get_kind() == forall_k) 
                 p = m.mk_skolemization(m.mk_not(q), m.mk_not(r));
             else
@@ -156,7 +158,8 @@ class skolemizer {
         m_sk_hack("sk_hack"),
         m_sk_hack_enabled(false),
         m_cache(m),
-        m_cache_pr(m) {
+        m_cache_pr(m),
+        m_proofs_enabled(m.proofs_enabled()) {
     }
 
     void set_sk_hack(bool f) {
@@ -167,13 +170,13 @@ class skolemizer {
         r = m_cache.find(q);
         if (r.get() != nullptr) {
             p = nullptr;
-            if (m.proofs_enabled())
+            if (m_proofs_enabled)
                 p = static_cast<proof*>(m_cache_pr.find(q));
         }
         else {
             process(q, r, p);
             m_cache.insert(q, r);
-            if (m.proofs_enabled())
+            if (m_proofs_enabled)
                 m_cache_pr.insert(q, p);
         }
     }
@@ -273,15 +276,13 @@ struct nnf::imp {
         updt_params(p);
         for (unsigned i = 0; i < 4; i++) {
             m_cache[i] = alloc(act_cache, m);
-            if (m.proofs_enabled())
+            if (proofs_enabled())
                 m_cache_pr[i] = alloc(act_cache, m);
         }
         m_name_nested_formulas = mk_nested_formula_namer(m, n);
         m_name_quant           = mk_quantifier_label_namer(m, n);
     }
 
-    // ast_manager & m() const { return m; }
-
     bool proofs_enabled() const { return m.proofs_enabled(); }
 
     ~imp() {

src/smt/smt_context.cpp

@@ -3240,7 +3240,7 @@ namespace smt {
                 else
                     assign(l, b_justification::mk_axiom());
                 m_assumptions.push_back(l);
-                get_bdata(l.var()).m_assumption = true;
+                get_bdata(l.var()).m_assumption = true;                
             }
         }
         m_search_lvl = m_scope_lvl;