From 7639eff29b92b9a7ee3aa2af52af6985f44e18ab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Aug 2015 11:09:10 -0700
Subject: [PATCH] retain default configuration between calls to SMT tactic so
that values are not overwritten between calls to smt-setup. Fixes bug #196
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/asserted_formulas.cpp | 1 +
src/smt/smt_setup.cpp | 1 +
src/smt/tactic/smt_tactic.cpp | 8 +++++---
3 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index c02c6760a..bd5f53922 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -252,6 +252,7 @@ void asserted_formulas::reduce() {
TRACE("before_reduce", display(tout););
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; }
set_eliminate_and(false); // do not eliminate and before nnf.
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 98ad5e51a..b72ecbd84 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -52,6 +52,7 @@ namespace smt {
// }
TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";);
m_already_configured = true;
+
switch (cm) {
case CFG_BASIC: setup_unknown(); break;
case CFG_LOGIC: setup_default(); break;
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 725d38ed5..a42f00274 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -161,9 +161,11 @@ public:
struct scoped_init_ctx {
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) {
- 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";);
new_ctx->set_logic(o.m_logic);
if (o.m_callback) {
@@ -199,7 +201,8 @@ public:
<< " PREPROCESS: " << fparams().m_preprocess << "\n";
tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\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_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
scoped_init_ctx init(*this, m);
@@ -239,7 +242,6 @@ public:
else
r = m_ctx->check(assumptions.size(), assumptions.c_ptr());
m_ctx->collect_statistics(m_stats);
-
switch (r) {
case l_true: {
if (m_fail_if_inconclusive && !in->sat_preserved())