From 7a5ca960951e56b8dbf0828d40f723c93d4ba4af Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 9 Oct 2019 09:00:49 -0700
Subject: [PATCH] remove separate API for setting solver log, use parameter
 setting instead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp       | 13 +++++--------
 src/api/python/z3/z3.py      |  2 +-
 src/api/z3_api.h             | 15 ---------------
 src/solver/solver.cpp        |  1 +
 src/solver/solver_params.pyg |  1 +
 5 files changed, 8 insertions(+), 24 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 0bf74b840..76dadae69 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -155,13 +155,6 @@ 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);
@@ -338,10 +331,13 @@ extern "C" {
         RESET_ERROR_CODE();
 
         symbol logic = to_param_ref(p).get_sym("smt.logic", symbol::null);
+        symbol smt2log = to_param_ref(p).get_sym("solver.smtlib2_log", symbol::null);
         if (logic != symbol::null) {
             to_solver(s)->m_logic = logic;
         }
-
+        if (smt2log != symbol::null && !to_solver(s)->m_pp) {
+            to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str().c_str());
+        }
         if (to_solver(s)->m_solver) {
             bool old_model = to_solver(s)->m_params.get_bool("model", true);
             bool new_model = to_param_ref(p).get_bool("model", true);
@@ -354,6 +350,7 @@ extern "C" {
             to_solver_ref(s)->updt_params(to_param_ref(p));
         }
         to_solver(s)->m_params.append(to_param_ref(p));
+        
         Z3_CATCH;
     }
     
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 07198bc91..e40f57fd7 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6447,7 +6447,7 @@ class Solver(Z3PPObject):
             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)
+            self.set("solver.smtlib2_log", logFile)
 
     def __del__(self):
         if self.solver is not None and self.ctx.ref() is not None:
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 127be301c..ed3f4b50d 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6331,21 +6331,6 @@ extern "C" {
        def_API('Z3_solver_dec_ref', VOID, (_in(CONTEXT), _in(SOLVER)))
     */
     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.
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index b93f8c658..ebb8e1723 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -227,6 +227,7 @@ void solver::assert_expr(expr* f, expr* t) {
 
 void solver::collect_param_descrs(param_descrs & r) {
     r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas");
+    r.insert("solver.smtlib2_log", CPK_SYMBOL, "(default: None) file to log solver interaction in smtlib2 format");
     insert_timeout(r);
     insert_rlimit(r);
     insert_max_memory(r);
diff --git a/src/solver/solver_params.pyg b/src/solver/solver_params.pyg
index 29690a164..04ffaf1c6 100644
--- a/src/solver/solver_params.pyg
+++ b/src/solver/solver_params.pyg
@@ -3,6 +3,7 @@ def_module_params('solver',
                   description='solver parameters',
                   export=True,
                   params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"),
+                          ('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
                           ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
                           ))