mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

update model conversion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-03 11:46:26 -07:00
parent f59bf4c464
commit 96914d8578
4 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/opt/opt_context.cpp
View file

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

4
src/sat/sat_solver/inc_sat_solver.cpp
View file

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

4
src/solver/tactic2solver.cpp
View file

@ -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() {

12
src/tactic/core/elim_uncnstr_tactic.cpp
View file

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