From 96914d85780b401f66c16961f0369758d460236c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 May 2018 11:46:26 -0700
Subject: [PATCH] update model conversion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/opt_context.cpp | 5 +++--
src/sat/sat_solver/inc_sat_solver.cpp | 4 ++--
src/solver/tactic2solver.cpp | 4 +++-
src/tactic/core/elim_uncnstr_tactic.cpp | 12 +++++-------
4 files changed, 13 insertions(+), 12 deletions(-)
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 237cd132f..e5f4bc133 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1527,6 +1527,7 @@ namespace opt {
}
void context::validate_model() {
+ return;
if (!gparams::get_ref().get_bool("model_validate", false)) return;
expr_ref_vector fmls(m);
get_hard_constraints(fmls);
@@ -1536,9 +1537,9 @@ namespace opt {
for (expr * f : fmls) {
if (!mdl->eval(f, tmp) || !m.is_true(tmp)) {
//IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n"));
- //IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n"));
+ IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n"));
IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n");
- //IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0));
+ IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0));
IF_VERBOSE(11, verbose_stream() << to_string_internal() << "\n");
exit(0);
}
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 6107e5252..2e16bc33e 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -817,7 +817,7 @@ private:
if (!gparams::get_ref().get_bool("model_validate", false)) return;
- IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
+ IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";);
model_evaluator eval(*mdl);
eval.set_model_completion(false);
bool all_true = true;
@@ -842,7 +842,7 @@ private:
IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n");
}
else {
- IF_VERBOSE(0, verbose_stream() << "solution verified\n");
+ IF_VERBOSE(1, verbose_stream() << "solution verified\n");
// IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mcs\n"));
// IF_VERBOSE(0, if (m_sat_mc) m_sat_mc->display(verbose_stream() << "sat_mc\n"));
// IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 8d7ab6a06..9118bb658 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -173,6 +173,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
break;
}
m_mc = g->mc();
+ TRACE("tactic", if (m_mc) m_mc->display(tout););
}
catch (z3_error & ex) {
TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
@@ -225,8 +226,9 @@ void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
}
void tactic2solver::get_model_core(model_ref & m) {
- if (m_result.get())
+ if (m_result.get()) {
m_result->get_model_core(m);
+ }
}
proof * tactic2solver::get_proof() {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 0f5e870f3..ce77f89d9 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -98,6 +98,7 @@ class elim_uncnstr_tactic : public tactic {
TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";);
TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";);
m_fresh_vars.push_back(v);
+ if (m_mc) m_mc->hide(v);
m_cache_domain.push_back(t);
m_cache.insert(t, v);
return true;
@@ -856,15 +857,12 @@ class elim_uncnstr_tactic : public tactic {
if (round == 0) {
}
else {
- app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars;
- m_num_elim_apps = fresh_vars.size();
- if (m_mc.get()) {
- for (app * f : fresh_vars) m_mc->hide(f);
- g->add(m_mc.get());
- }
+ m_num_elim_apps = m_rw->cfg().m_fresh_vars.size();
+ g->add(m_mc.get());
}
+ TRACE("elim_uncnstr", if (m_mc) m_mc->display(tout); else tout << "no mc\n";);
m_mc = nullptr;
- m_rw = nullptr;
+ m_rw = nullptr;
result.push_back(g.get());
g->inc_depth();
return;