3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00

remove separate API for setting solver log, use parameter setting instead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-09 09:00:49 -07:00
parent bc50b6bea2
commit 7a5ca96095
5 changed files with 8 additions and 24 deletions

View file

@ -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;
}

View file

@ -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:

View file

@ -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.

View file

@ -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);

View file

@ -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"),
))