mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

retain default configuration between calls to SMT tactic so that values are not overwritten between calls to smt-setup. Fixes bug #196

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-25 11:09:10 -07:00
parent 8c11299be6
commit 7639eff29b
3 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/asserted_formulas.cpp
View file

@ -252,6 +252,7 @@ void asserted_formulas::reduce() {
TRACE("before_reduce", display(tout);); TRACE("before_reduce", display(tout););
CASSERT("well_sorted", check_well_sorted()); CASSERT("well_sorted", check_well_sorted());
#define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; } #define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; }
set_eliminate_and(false); // do not eliminate and before nnf. set_eliminate_and(false); // do not eliminate and before nnf.

1
src/smt/smt_setup.cpp
View file

@ -52,6 +52,7 @@ namespace smt {
// } // }
TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";); TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";);
m_already_configured = true; m_already_configured = true;
switch (cm) { switch (cm) {
case CFG_BASIC: setup_unknown(); break; case CFG_BASIC: setup_unknown(); break;
case CFG_LOGIC: setup_default(); break; case CFG_LOGIC: setup_default(); break;

8
src/smt/tactic/smt_tactic.cpp
View file

@ -161,9 +161,11 @@ public:
struct scoped_init_ctx { struct scoped_init_ctx {
smt_tactic & m_owner; smt_tactic & m_owner;
smt_params m_params; // smt-setup overwrites parameters depending on the current assertions.
scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) { scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
smt::kernel * new_ctx = alloc(smt::kernel, m, o.fparams()); m_params = o.fparams();
smt::kernel * new_ctx = alloc(smt::kernel, m, m_params);
TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";); TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
new_ctx->set_logic(o.m_logic); new_ctx->set_logic(o.m_logic);
if (o.m_callback) { if (o.m_callback) {
@ -199,7 +201,8 @@ public:
<< " PREPROCESS: " << fparams().m_preprocess << "\n"; << " PREPROCESS: " << fparams().m_preprocess << "\n";
tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n"; tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n";
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
tout << "params_ref: " << m_params_ref << "\n";); tout << "params_ref: " << m_params_ref << "\n";
tout << "nnf: " << fparams().m_nnf_cnf << "\n";);
TRACE("smt_tactic_detail", in->display(tout);); TRACE("smt_tactic_detail", in->display(tout););
TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
scoped_init_ctx init(*this, m); scoped_init_ctx init(*this, m);
@ -239,7 +242,6 @@ public:
else else
r = m_ctx->check(assumptions.size(), assumptions.c_ptr()); r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
m_ctx->collect_statistics(m_stats); m_ctx->collect_statistics(m_stats);
switch (r) { switch (r) {
case l_true: { case l_true: {
if (m_fail_if_inconclusive && !in->sat_preserved()) if (m_fail_if_inconclusive && !in->sat_preserved())