diff options
author | Tim King <taking@cs.nyu.edu> | 2012-01-23 21:13:08 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-01-23 21:13:08 +0000 |
commit | d9df9a78b51bb4a455d15810924bc8b537934833 (patch) | |
tree | 2e0ecfef8bfafa19b1fbfedaea7a53ddbc1e0714 /src | |
parent | 3b3c5597a926cf6f2056fe237bcac7c4d2596a75 (diff) |
Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanations from the theory that can explain them. This partially fixes bug 295.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 22 |
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) { |