mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

pick up log configuration consistently #3513

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-25 10:51:55 -07:00
parent e5e6f481f9
commit 145ec8f248
2 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/api/api_solver.cpp
View file

@ -151,6 +151,14 @@ extern "C" {
init_solver_core(c, s);
}
static void init_solver_log(Z3_context c, Z3_solver s) {
solver_params sp(to_solver(s)->m_params);
symbol smt2log = sp.smtlib2_log();
if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) {
to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str().c_str());
}
}
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_simple_solver(c);
@ -158,6 +166,7 @@ extern "C" {
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_solver_factory());
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
init_solver_log(c, r);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
@ -169,6 +178,7 @@ extern "C" {
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory());
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
init_solver_log(c, r);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
@ -187,6 +197,7 @@ extern "C" {
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic)));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
init_solver_log(c, r);
RETURN_Z3(r);
}
Z3_CATCH_RETURN(nullptr);
@ -199,6 +210,7 @@ extern "C" {
Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_tactic2solver_factory(to_tactic_ref(t)));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
init_solver_log(c, r);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
@ -213,6 +225,7 @@ extern "C" {
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
mk_c(target)->save_object(sr);
Z3_solver r = of_solver(sr);
init_solver_log(target, r);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
@ -343,19 +356,16 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p) {
Z3_TRY;
LOG_Z3_solver_set_params(c, s, p);
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);
@ -369,6 +379,8 @@ extern "C" {
}
to_solver(s)->m_params.append(to_param_ref(p));
init_solver_log(c, s);
Z3_CATCH;
}

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -190,7 +190,7 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref &
case EQ: result = m().mk_false(); return true;
}
}
expr * k = m_util.mk_numeral(c, is_int);
expr_ref k(m_util.mk_numeral(c, is_int), m());
switch (kind) {
case LE: result = m_util.mk_le(pp, k); return true;
case GE: result = m_util.mk_ge(pp, k); return true;