diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bf74cd016..c61879b6d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -50,6 +50,7 @@ #include "theory/relevance_manager.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_id.h" #include "theory/theory_model.h" #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" @@ -308,12 +309,13 @@ void TheoryEngine::preRegister(TNode preprocessed) { Assert(!expr::hasFreeVar(preprocessed)); // Pre-register the terms in the atom - Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run( + theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run( d_preRegistrationVisitor, preprocessed); - theories = Theory::setRemove(THEORY_BOOL, theories); + theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories); // Remove the top theory, if any more that means multiple theories were // involved - bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories); + bool multipleTheories = + TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories); if (Configuration::isAssertionBuild()) { TheoryId i; @@ -324,7 +326,7 @@ void TheoryEngine::preRegister(TNode preprocessed) { // even though arithmetic isn't actually involved. if (!options::finiteModelFind()) { - while ((i = Theory::setPop(theories)) != THEORY_LAST) + while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST) { if (!d_logicInfo.isTheoryEnabled(i)) { @@ -1074,9 +1076,11 @@ void TheoryEngine::assertFact(TNode literal) SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); for (; it != it_end; ++ it) { TNode term = *it; - Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); + theory::TheoryIdSet theories = + d_sharedTerms.getTheoriesToNotify(atom, term); for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) { - if (Theory::setContains(id, theories)) { + if (TheoryIdSetUtil::setContains(id, theories)) + { theoryOf(id)->addSharedTerm(term); } } |