diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-02 00:44:40 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-02 00:44:40 +0000 |
commit | 8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (patch) | |
tree | 353b4a9d3163388aa6aef1c92aa0de5077888337 /src/theory | |
parent | 97555307af3415d6fbbac3fc9dccdafec51056b7 (diff) |
Changing d_sharedTermsExist to logicInfo.isSharingEnabled()
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 |
2 files changed, 7 insertions, 13 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a7e1f0cd7..314e3bdb3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -50,7 +50,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_possiblePropagations(), d_hasPropagated(context), d_inConflict(context, false), - d_sharedTermsExist(logicInfo.isSharingEnabled()), d_hasShutDown(false), d_incomplete(context, false), d_sharedLiteralsIn(context), @@ -149,7 +148,7 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory::assertions") << (*it).assertion << endl; } - if (d_sharedTermsExist) { + if (d_logicInfo.isSharingEnabled()) { Debug("theory::assertions") << "Shared terms of " << theory->getId() << ": " << std::endl; context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); for (unsigned i = 0; it != it_end; ++ it, ++i) { @@ -188,7 +187,7 @@ void TheoryEngine::check(Theory::Effort effort) { } // If in full check and no lemmas added, run the combination - if (Theory::fullEffort(effort) && d_sharedTermsExist) { + if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()) { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl; combineTheories(); @@ -625,7 +624,7 @@ void TheoryEngine::assertFact(TNode node) TNode atom = negated ? node[0] : node; Theory* theory = theoryOf(atom); - if (d_sharedTermsExist) { + if (d_logicInfo.isSharingEnabled()) { // If any shared terms, notify the theories if (d_sharedTerms.hasSharedTerms(atom)) { @@ -696,7 +695,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { TNode atom = negated ? literal[0] : literal; bool value; - if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL || + if (!d_logicInfo.isSharingEnabled() || atom.getKind() != kind::EQUAL || !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) { // If not an equality or if an equality between terms that are not both shared, // it must be a SAT literal so we enqueue it @@ -775,7 +774,7 @@ Node TheoryEngine::getExplanation(TNode node) { AssertedLiteralsOutMap::iterator find; // "find" will have a value when sharedAssertion is true - if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) { + if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) { find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST)); sharedLiteral = (find != d_assertedLiteralsOut.end()); } @@ -788,7 +787,7 @@ Node TheoryEngine::getExplanation(TNode node) { explanation = theory->explain(node); // Explain any shared equalities that might be in the explanation - if (d_sharedTermsExist) { + if (d_logicInfo.isSharingEnabled()) { explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId())); } } @@ -921,7 +920,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { << CheckSatCommand(conflict.toExpr()); } - if (d_sharedTermsExist) { + if (d_logicInfo.isSharingEnabled()) { // In the multiple-theories case, we need to reconstruct the conflict Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId)); Assert(properConflict(fullConflict)); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e353850aa..28a1000f1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -257,11 +257,6 @@ class TheoryEngine { context::CDO<bool> d_inConflict; /** - * Does the context contain terms shared among multiple theories. - */ - bool d_sharedTermsExist; - - /** * Explain the equality literals and push all the explaining literals * into the builder. All the non-equality literals are pushed to the * builder. |