diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-30 14:42:28 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-30 14:42:28 +0000 |
| commit | 97555307af3415d6fbbac3fc9dccdafec51056b7 (patch) | |
| tree | 56b47f809268d5b8ae21594d22cbec7ced8f46aa /src/theory/theory_engine.cpp | |
| parent | 9ac1cb18f03a5edf4b50532d29e195f74d6a83c2 (diff) | |
Added map from skolem variables to new ite formulas in ite removal.
d_sharedTermsExist is now set based on logicInfo instead of dynamically when
shared terms are found.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d5616221d..a7e1f0cd7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -50,7 +50,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_possiblePropagations(), d_hasPropagated(context), d_inConflict(context, false), - d_sharedTermsExist(context, false), + d_sharedTermsExist(logicInfo.isSharingEnabled()), d_hasShutDown(false), d_incomplete(context, false), d_sharedLiteralsIn(context), @@ -94,8 +94,6 @@ void TheoryEngine::preRegister(TNode preprocessed) { if (multipleTheories) { // Collect the shared terms if there are multipe theories NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); - // Mark the multiple theories flag - d_sharedTermsExist = true; } } @@ -627,7 +625,6 @@ void TheoryEngine::assertFact(TNode node) TNode atom = negated ? node[0] : node; Theory* theory = theoryOf(atom); - //TODO: there is probably a bug here if shared terms start to exist after some asseritons have been processed if (d_sharedTermsExist) { // If any shared terms, notify the theories |