From d9df9a78b51bb4a455d15810924bc8b537934833 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 23 Jan 2012 21:13:08 +0000 Subject: [PATCH] Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanations from the theory that can explain them. This partially fixes bug 295. --- src/theory/theory_engine.cpp | 22 ++++++++++++++++------ 1 file 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) { -- 2.30.2