From d913a55dfb6980f6c3589c1126c51de4078b5610 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Sep 2018 07:32:59 -0700
Subject: [PATCH] reset m_explanation (#82)

* reset m_explanation

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

* streamline handling of m_explanation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp        |  5 ++++-
 src/smt/theory_lra.cpp | 29 +++++++++++++++--------------
 2 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index b6f678fea..fa461aca5 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -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";);
         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", 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));
 
 #ifdef RECYCLE_FREE_AST_INDICES
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 819b5f6a4..a5c44b81a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2075,12 +2075,12 @@ public:
         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_a2 = alloc(scoped_anum, m_nra->am());
         switch (r) {
         case l_false:
-            set_conflict1();
+            set_conflict1(ex);
             break;
         case l_true:
             m_use_nra_model = true;
@@ -2096,7 +2096,7 @@ public:
         return r;
     }
 
-    void process_lemma(const niil::lemma& lemma) {
+    void process_lemma(lp::explanation& ex, const niil::lemma& lemma) {
         literal_vector core;
         for (auto const& ineq : lemma) {
             bool is_lower = true, pos = true, is_eq = false;
@@ -2122,13 +2122,13 @@ public:
             literal lit(ctx().get_bool_var(atom), pos);
             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) {
         case l_false:
-            process_lemma(lemma);
+            process_lemma(ex, lemma);
             break;
         case l_true:
             if (assume_eqs()) {
@@ -2151,8 +2151,9 @@ public:
         if (!m_switcher.need_check()) return l_true;
         m_a1 = nullptr; m_a2 = nullptr;
         niil::lemma lemma;
+        m_explanation.reset();
         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() {
         m_explanation.clear();
         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;
-        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_core.reset();
         m_params.reset();
         for (literal lit : core) {
             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_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););
-        for (auto const& ev : m_explanation) {
+        for (auto const& ev : ex) {
             if (!ev.first.is_zero()) { 
                 set_evidence(ev.second);
             }