From: Tim King <taking@cs.nyu.edu>
Date: Mon, 23 Jan 2012 21:13:08 +0000 (+0000)
Subject: Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanat... 
X-Git-Tag: cvc5-1.0.0~8350
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9df9a78b51bb4a455d15810924bc8b537934833;p=cvc5.git

Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanations from the theory that can explain them. This partially fixes bug 295.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0a9670678..f69fdddcb 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -630,16 +630,26 @@ Node TheoryEngine::getExplanation(TNode node)
   Node explanation;
 
   // The theory that has explaining to do
-  Theory* theory = theoryOf(atom);
+  Theory* theory;
+
+  //This is true if atom is a shared assertion
+  bool sharedAssertion = false;
+
+  SharedAssertionsMap::iterator find;
+  // "find" will have a value when sharedAssertion is true
   if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) {
-    SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
-    if (find == d_sharedAssertions.end()) {
-      theory = theoryOf(atom);
-    }
+    find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
+    sharedAssertion = (find != d_sharedAssertions.end());
   }
 
   // Get the explanation
-  explanation = theory->explain(node);
+  if(sharedAssertion){
+    theory = theoryOf((*find).second.theory);
+    explanation = theory->explain((*find).second.node);
+  } else {
+    theory = theoryOf(atom);
+    explanation = theory->explain(node);
+  }
 
   // Explain any shared equalities that might be in the explanation
   if (d_sharedTermsExist) {