adding SMT2 log file for solver interaction #867

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

src/api/api_solver.cpp

@@ -44,6 +44,52 @@ Revision History:
 
 extern "C" {
 
+    void solver2smt2_pp::assert_expr(expr* e) {
+        m_pp_util.collect(e);
+        m_pp_util.display_decls(m_out);
+        m_pp_util.display_assert(m_out, e, true);
+    }
+
+    void solver2smt2_pp::assert_expr(expr* e, expr* t) {
+        m_pp_util.collect(e);
+        m_pp_util.collect(t);
+        m_pp_util.display_decls(m_out);
+        m_pp_util.display_assert_and_track(m_out, e, t, true);
+    }
+
+    void solver2smt2_pp::push() {
+        m_out << "(push)\n";
+    }
+
+    void solver2smt2_pp::pop(unsigned n) {
+        m_out << "(pop " << n << ")\n";
+    }
+
+    void solver2smt2_pp::check(unsigned n, expr* const* asms) {
+        m_out << "(check-sat";
+        for (unsigned i = 0; i < n; ++i) {
+            m_out << "\n";
+            m_pp_util.display_expr(m_out, asms[i]);            
+        }
+        m_out << ")\n";
+    }
+
+    solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) {
+        if (!m_out) {
+            throw default_exception("could not open file for output");
+        }
+    }
+
+    void Z3_solver_ref::assert_expr(expr * e) {
+        if (m_pp) m_pp->assert_expr(e);
+        m_solver->assert_expr(e);
+    }
+
+    void Z3_solver_ref::assert_expr(expr * e, expr* t) {
+        if (m_pp) m_pp->assert_expr(e, t);
+        m_solver->assert_expr(e, t);
+    }
+
     static void init_solver_core(Z3_context c, Z3_solver _s) {
         Z3_solver_ref * s = to_solver(_s);
         bool proofs_enabled, models_enabled, unsat_core_enabled;
@@ -85,6 +131,13 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    void Z3_API Z3_solver_open_smt2log(Z3_context c, Z3_solver s, Z3_string file) {
+        Z3_TRY;
+        LOG_Z3_solver_open_smt2log(c, s, file);
+        to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), file);
+        Z3_CATCH;
+    }
+
     Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic) {
         Z3_TRY;
         LOG_Z3_mk_solver_for_logic(c, logic);
@@ -154,7 +207,7 @@ extern "C" {
         if (!initialized)
             init_solver(c, s);
         for (expr * e : ctx->assertions()) {
-            to_solver_ref(s)->assert_expr(e);
+            to_solver(s)->assert_expr(e);
         }
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
     }
@@ -177,7 +230,7 @@ extern "C" {
         goal g(m);            
         s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
         for (unsigned i = 0; i < g.size(); ++i) {
-            to_solver_ref(s)->assert_expr(g.form(i));
+            to_solver(s)->assert_expr(g.form(i));
         }
     }
 
@@ -302,6 +355,7 @@ extern "C" {
         RESET_ERROR_CODE();
         init_solver(c, s);
         to_solver_ref(s)->push();
+        if (to_solver(s)->m_pp) to_solver(s)->m_pp->push();
         Z3_CATCH;
     }
 
@@ -314,8 +368,10 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return;
         }
-        if (n > 0)
+        if (n > 0) {
             to_solver_ref(s)->pop(n);
+            if (to_solver(s)->m_pp) to_solver(s)->m_pp->pop(n);
+        }
         Z3_CATCH;
     }
 
@@ -342,7 +398,7 @@ extern "C" {
         RESET_ERROR_CODE();
         init_solver(c, s);
         CHECK_FORMULA(a,);
-        to_solver_ref(s)->assert_expr(to_expr(a));
+        to_solver(s)->assert_expr(to_expr(a));
         Z3_CATCH;
     }
 
@@ -353,7 +409,7 @@ extern "C" {
         init_solver(c, s);
         CHECK_FORMULA(a,);
         CHECK_FORMULA(p,);
-        to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p));
+        to_solver(s)->assert_expr(to_expr(a), to_expr(p));
         Z3_CATCH;
     }
 
@@ -461,6 +517,7 @@ extern "C" {
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
+                if (to_solver(s)->m_pp) to_solver(s)->m_pp->check(num_assumptions, _assumptions); 
                 result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
             }
             catch (z3_exception & ex) {

src/api/api_solver.h

@@ -21,13 +21,28 @@ Revision History:
 #include "api/api_util.h"
 #include "solver/solver.h"
 
+struct solver2smt2_pp {
+    ast_pp_util m_pp_util;
+    std::ofstream m_out;
+    solver2smt2_pp(ast_manager& m, char const* file);
+    void assert_expr(expr* e);
+    void assert_expr(expr* e, expr* t);
+    void push();
+    void pop(unsigned n);
+    void check(unsigned n, expr* const* asms);
+};
+
 struct Z3_solver_ref : public api::object {
     scoped_ptr<solver_factory> m_solver_factory;
     ref<solver>                m_solver;
     params_ref                 m_params;
     symbol                     m_logic;
+    scoped_ptr<solver2smt2_pp> m_pp;
     Z3_solver_ref(api::context& c, solver_factory * f): api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null) {}
     ~Z3_solver_ref() override {}
+
+    void assert_expr(expr* e);
+    void assert_expr(expr* e, expr* t);
 };
 
 inline Z3_solver_ref * to_solver(Z3_solver s) { return reinterpret_cast<Z3_solver_ref *>(s); }

src/api/python/z3/z3.py

@@ -6436,7 +6436,7 @@ unknown = CheckSatResult(Z3_L_UNDEF)
 class Solver(Z3PPObject):
     """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc."""
 
-    def __init__(self, solver=None, ctx=None):
+    def __init__(self, solver=None, ctx=None, logFile=None):
         assert solver is None or ctx is not None
         self.ctx    = _get_ctx(ctx)
         self.backtrack_level = 4000000000
@@ -6446,6 +6446,8 @@ class Solver(Z3PPObject):
         else:
             self.solver = solver
         Z3_solver_inc_ref(self.ctx.ref(), self.solver)
+        if logFile is not None:
+            Z3_solver_open_smt2log(self.ctx.ref(), self.solver, logFile)
 
     def __del__(self):
         if self.solver is not None and self.ctx.ref() is not None:
@@ -6906,7 +6908,7 @@ class Solver(Z3PPObject):
             e = BoolVal(True, self.ctx).as_ast()
         return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
 
-def SolverFor(logic, ctx=None):
+def SolverFor(logic, ctx=None, logFile=None):
     """Create a solver customized for the given logic.
 
     The parameter `logic` is a string. It should be contains
@@ -6924,9 +6926,9 @@ def SolverFor(logic, ctx=None):
     """
     ctx = _get_ctx(ctx)
     logic = to_symbol(logic)
-    return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)
+    return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx, logFile)
 
-def SimpleSolver(ctx=None):
+def SimpleSolver(ctx=None, logFile=None):
     """Return a simple general purpose solver with limited amount of preprocessing.
 
     >>> s = SimpleSolver()
@@ -6936,7 +6938,7 @@ def SimpleSolver(ctx=None):
     sat
     """
     ctx = _get_ctx(ctx)
-    return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)
+    return Solver(Z3_mk_simple_solver(ctx.ref()), ctx, logFile)
 
 #########################################
 #
@@ -7662,7 +7664,7 @@ class Tactic:
         if self.tactic is not None and self.ctx.ref() is not None:
             Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
 
-    def solver(self):
+    def solver(self, logFile=None):
         """Create a solver using the tactic `self`.
 
         The solver supports the methods `push()` and `pop()`, but it
@@ -7677,7 +7679,7 @@ class Tactic:
         >>> s.model()
         [x = 1.4142135623?]
         """
-        return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx)
+        return Solver(Z3_mk_solver_from_tactic(self.ctx.ref(), self.tactic), self.ctx, logFile)
 
     def apply(self, goal, *arguments, **keywords):
         """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.

src/api/z3_api.h

@@ -6332,6 +6332,21 @@ extern "C" {
     */
     void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s);
 
+    /**
+       \brief Log solver interactions into an SMT2 file.
+       The tracked interactions are:
+       - Z3_solver_assert
+       - Z3_solver_assert_and_track
+       - Z3_solver_push
+       - Z3_solver_pop
+       - Z3_solver_check
+       - Z3_solver_check_assumptions
+       Assertions that are loaded from a file are also going to be tracked.
+
+       def_API('Z3_solver_open_smt2log', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING)))
+    */
+    void Z3_API Z3_solver_open_smt2log(Z3_context c, Z3_solver s, Z3_string file);
+    
     /**
        \brief Create a backtracking point.
 

src/ast/ast_pp_util.cpp

@@ -38,32 +38,63 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
 
 void ast_pp_util::display_decls(std::ostream& out) {
     ast_smt_pp pp(m);
-    coll.order_deps();
+    bool first = m_num_decls == 0;
+    coll.order_deps(m_num_sorts);
     unsigned n = coll.get_num_sorts();
-    for (unsigned i = 0; i < n; ++i) {
+    for (unsigned i = m_num_sorts; i < n; ++i) {
         pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr);
     }
+    m_num_sorts = n;
     n = coll.get_num_decls();
-    for (unsigned i = 0; i < n; ++i) {
+    for (unsigned i = m_num_decls; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
         if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
             ast_smt2_pp(out, f, m_env) << "\n";
         }
     }
-    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()));
+    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);
     }
-    ast_smt2_pp_recdefs(out, recfuns, m_env);
 }
 
 void ast_pp_util::remove_decl(func_decl* f) {
     m_removed.insert(f);
 }
 
+std::ostream& ast_pp_util::display_expr(std::ostream& out, expr* f, bool neat) {
+    if (neat) {
+        ast_smt2_pp(out, f, m_env);
+    }
+    else {
+        ast_smt_pp ll_smt2_pp(m);
+        ll_smt2_pp.display_expr_smt2(out, f);
+    }
+    return out;
+}
+
+void ast_pp_util::display_assert(std::ostream& out, expr* f, bool neat) {
+    display_expr(out << "(assert ", f, neat) << ")\n";
+}
+
+void ast_pp_util::display_assert_and_track(std::ostream& out, expr* f, expr* t, bool neat) {
+    if (neat) {
+        ast_smt2_pp(out << "(assert (=> ", t, m_env) << " ";
+        ast_smt2_pp(out, f, m_env) << "))\n";
+    }
+    else {
+        ast_smt_pp ll_smt2_pp(m);
+        ll_smt2_pp.display_expr_smt2(out << "(assert (=> ", t); out << " ";
+        ll_smt2_pp.display_expr_smt2(out, f); out << "))\n";
+    }
+}
 
 void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
     if (neat) {

src/ast/ast_pp_util.h

@@ -27,11 +27,13 @@ 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;
+    
  public:        
 
     decl_collector      coll;
 
-    ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m) {}
+ ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_num_sorts(0), m_num_decls(0) {}
 
     void collect(expr* e);
 
@@ -45,6 +47,12 @@ class ast_pp_util {
 
     void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);
 
+    void display_assert(std::ostream& out, expr* f, bool neat = true);
+
+    void display_assert_and_track(std::ostream& out, expr* f, expr* t, bool neat = true);
+
+    std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true);
+
     smt2_pp_environment& env() { return m_env; }
 };
 

src/ast/ast_smt_pp.cpp

@@ -957,7 +957,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
 #if 0
     decls.display_decls(strm);
 #else
-    decls.order_deps();
+    decls.order_deps(0);
     ast_mark sort_mark;
     for (sort* s : decls.get_sorts()) {
         if (!(*m_is_declared)(s)) {

src/ast/decl_collector.cpp

@@ -113,11 +113,14 @@ void decl_collector::visit(ast* n) {
     }
 }
 
-void decl_collector::order_deps() {
+void decl_collector::order_deps(unsigned n) {
     top_sort<sort> st;
-    for (sort * s : m_sorts) st.insert(s, collect_deps(s));
+    for (unsigned i = n; i < m_sorts.size(); ++i) {
+        sort* s = m_sorts.get(i);
+        st.insert(s, collect_deps(s));
+    }
     st.topological_sort();
-    m_sorts.reset();
+    m_sorts.shrink(n);
     for (sort* s : st.top_sorted()) m_sorts.push_back(s);
 }
 

src/ast/decl_collector.h

@@ -52,7 +52,7 @@ public:
     void visit(unsigned n, expr* const* es);
     void visit(expr_ref_vector const& es);
 
-    void order_deps();
+    void order_deps(unsigned n);
 
     unsigned get_num_sorts() const { return m_sorts.size(); }
     unsigned get_num_decls() const { return m_decls.size(); }