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

1 files changed, 16 insertions, 6 deletions

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