mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

ensure statistics survive cancelation in tactics, fix propagation for smtfd

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-18 19:22:36 -07:00
parent 203ba12abc
commit 11736f078e
2 changed files with 15 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/solver/solver2tactic.cpp
View file

@ -111,10 +111,18 @@ public:
ref<solver> local_solver = m_solver->translate(m, m_params); ref<solver> local_solver = m_solver->translate(m, m_params);
local_solver->assert_expr(clauses); local_solver->assert_expr(clauses);
TRACE("solver2tactic", tout << "clauses asserted\n";); TRACE("solver2tactic", tout << "clauses asserted\n";);
lbool r = local_solver->check_sat(assumptions.size(), assumptions.c_ptr()); lbool r;
try {
r = local_solver->check_sat(assumptions.size(), assumptions.c_ptr());
}
catch (...) {
local_solver->collect_statistics(m_st);
throw;
}
TRACE("solver2tactic", tout << "check sat result " << r << "\n";); TRACE("solver2tactic", tout << "check sat result " << r << "\n";);
proof* pr = local_solver->get_proof(); proof* pr = local_solver->get_proof();
if (pr) in->set(proof2proof_converter(m, pr)); if (pr) in->set(proof2proof_converter(m, pr));
local_solver->collect_statistics(m_st);
switch (r) { switch (r) {
case l_true: case l_true:
if (in->models_enabled()) { if (in->models_enabled()) {
@ -160,7 +168,6 @@ public:
result.push_back(in.get()); result.push_back(in.get());
break; break;
} }
local_solver->collect_statistics(m_st);
} }
void collect_statistics(statistics & st) const override { void collect_statistics(statistics & st) const override {

8
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -584,6 +584,8 @@ namespace smtfd {
m_pinned.reset(); m_pinned.reset();
m_tables.reset(); m_tables.reset();
m_ast2table.reset(); m_ast2table.reset();
m_values.reset();
m_model = nullptr;
} }
}; };
@ -875,7 +877,7 @@ namespace smtfd {
expr_ref val2 = eval_abs(stored_value); expr_ref val2 = eval_abs(stored_value);
// A[i] = v // A[i] = v
if (val1 != val2) { if (val1 != val2) {
TRACE("smtfd", tout << "select/store: " << mk_pp(t, m) << "\n";); TRACE("smtfd", tout << "select/store: " << mk_bounded_pp(t, m, 2) << "\n";);
add_lemma(m.mk_eq(sel, stored_value)); add_lemma(m.mk_eq(sel, stored_value));
} }
m_pinned.push_back(sel); m_pinned.push_back(sel);
@ -1080,6 +1082,7 @@ namespace smtfd {
{} {}
void check_term(expr* t, unsigned round) override { void check_term(expr* t, unsigned round) override {
TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";);
switch (round) { switch (round) {
case 0: case 0:
if (m_autil.is_select(t)) { if (m_autil.is_select(t)) {
@ -1797,8 +1800,8 @@ namespace smtfd {
lbool refine_core(expr_ref_vector & core) { lbool refine_core(expr_ref_vector & core) {
lbool r = l_true; lbool r = l_true;
unsigned round = 0; unsigned round = 0;
m_context.reset(m_model);
while (true) { while (true) {
m_context.reset(m_model);
if (!m_context.add_theory_axioms(core, round)) { if (!m_context.add_theory_axioms(core, round)) {
break; break;
} }
@ -1822,6 +1825,7 @@ namespace smtfd {
case l_true: case l_true:
m_fd_sat_solver->get_model(m_model); m_fd_sat_solver->get_model(m_model);
m_model->set_model_completion(true); m_model->set_model_completion(true);
m_context.reset(m_model);
break; break;
default: default:
return r; return r;