mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

reset m_explanation (#82)

Browse source 
* reset m_explanation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* streamline handling of m_explanation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-07 07:32:59 -07:00 • committed by Lev Nachmanson
parent 9b5996fcd5
commit d913a55dfb
2 changed files with 19 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/ast.cpp
View file

@ -1928,7 +1928,10 @@ void ast_manager::delete_node(ast * n) {
CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";); CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
TRACE("mk_var_bug", tout << "del_ast: " << " " << n->m_ref_count << "\n";); TRACE("mk_var_bug", tout << "del_ast: " << " " << n->m_ref_count << "\n";);
TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
TRACE("ast", tout << mk_pp(n, *this) << "\n";);
SASSERT(m_ast_table.contains(n));
m_ast_table.erase(n);
SASSERT(!m_ast_table.contains(n));
SASSERT(!m_debug_ref_count || !m_debug_free_indices.contains(n->m_id)); SASSERT(!m_debug_ref_count || !m_debug_free_indices.contains(n->m_id));
#ifdef RECYCLE_FREE_AST_INDICES #ifdef RECYCLE_FREE_AST_INDICES

29
src/smt/theory_lra.cpp
View file

@ -2075,12 +2075,12 @@ public:
return lia_check; return lia_check;
} }
lbool check_aftermath_nra(lbool r) { lbool check_aftermath_nra(lbool r, lp::explanation& ex) {
m_a1 = alloc(scoped_anum, m_nra->am()); m_a1 = alloc(scoped_anum, m_nra->am());
m_a2 = alloc(scoped_anum, m_nra->am()); m_a2 = alloc(scoped_anum, m_nra->am());
switch (r) { switch (r) {
case l_false: case l_false:
set_conflict1(); set_conflict1(ex);
break; break;
case l_true: case l_true:
m_use_nra_model = true; m_use_nra_model = true;
@ -2096,7 +2096,7 @@ public:
return r; return r;
} }
void process_lemma(const niil::lemma& lemma) { void process_lemma(lp::explanation& ex, const niil::lemma& lemma) {
literal_vector core; literal_vector core;
for (auto const& ineq : lemma) { for (auto const& ineq : lemma) {
bool is_lower = true, pos = true, is_eq = false; bool is_lower = true, pos = true, is_eq = false;
@ -2122,13 +2122,13 @@ public:
literal lit(ctx().get_bool_var(atom), pos); literal lit(ctx().get_bool_var(atom), pos);
core.push_back(~lit); core.push_back(~lit);
} }
set_conflict_or_lemma(core, false); set_conflict_or_lemma(ex, core, false);
} }
lbool check_aftermath_niil(lbool r, const niil::lemma & lemma) { lbool check_aftermath_niil(lbool r, lp::explanation& ex, const niil::lemma & lemma) {
switch (r) { switch (r) {
case l_false: case l_false:
process_lemma(lemma); process_lemma(ex, lemma);
break; break;
case l_true: case l_true:
if (assume_eqs()) { if (assume_eqs()) {
@ -2151,8 +2151,9 @@ public:
if (!m_switcher.need_check()) return l_true; if (!m_switcher.need_check()) return l_true;
m_a1 = nullptr; m_a2 = nullptr; m_a1 = nullptr; m_a2 = nullptr;
niil::lemma lemma; niil::lemma lemma;
m_explanation.reset();
lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, lemma); lbool r = m_nra? m_nra->check(m_explanation): m_niil->check(m_explanation, lemma);
return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r, lemma); return m_nra? check_aftermath_nra(r, m_explanation) : check_aftermath_niil(r, m_explanation, lemma);
} }
/** /**
@ -3191,27 +3192,27 @@ public:
void set_conflict() { void set_conflict() {
m_explanation.clear(); m_explanation.clear();
m_solver->get_infeasibility_explanation(m_explanation); m_solver->get_infeasibility_explanation(m_explanation);
set_conflict1(); set_conflict1(m_explanation);
} }
void set_conflict1() { void set_conflict1(lp::explanation& ex) {
literal_vector core; literal_vector core;
set_conflict_or_lemma(core, true); set_conflict_or_lemma(ex, core, true);
} }
void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) { void set_conflict_or_lemma(lp::explanation& ex, literal_vector const& core, bool is_conflict) {
m_eqs.reset(); m_eqs.reset();
m_core.reset(); m_core.reset();
m_params.reset(); m_params.reset();
for (literal lit : core) { for (literal lit : core) {
m_core.push_back(lit); m_core.push_back(lit);
} }
// m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed // m_solver->shrink_explanation_to_minimum(ex); // todo, enable when perf is fixed
++m_num_conflicts; ++m_num_conflicts;
++m_stats.m_conflicts; ++m_stats.m_conflicts;
TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); ); TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, ex); );
TRACE("arith", display(tout);); TRACE("arith", display(tout););
for (auto const& ev : m_explanation) { for (auto const& ev : ex) {
if (!ev.first.is_zero()) { if (!ev.first.is_zero()) {
set_evidence(ev.second); set_evidence(ev.second);
} }