From 960147384b7953a352ca9c721f9b93bdac4ff178 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 28 Aug 2020 18:01:34 -0500 Subject: [PATCH] Replace Theory::Set with TheoryIdSet (#4959) This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine. This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h. It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h. This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory. --- src/theory/arith/congruence_manager.h | 1 + src/theory/model_manager.h | 1 + src/theory/quantifiers/first_order_model.h | 1 + src/theory/sets/cardinality_extension.cpp | 1 + src/theory/shared_terms_database.cpp | 41 ++++--- src/theory/shared_terms_database.h | 18 +-- src/theory/strings/solver_state.h | 4 +- src/theory/term_registration_visitor.cpp | 117 +++++++++++------- src/theory/term_registration_visitor.h | 36 +++--- src/theory/theory.h | 79 ------------- src/theory/theory_engine.cpp | 16 ++- src/theory/theory_id.cpp | 87 ++++++++++++++ src/theory/theory_id.h | 48 +++++++- src/theory/theory_model.cpp | 1 + src/theory/theory_model.h | 1 + src/theory/theory_model_builder.h | 3 + src/theory/uf/equality_engine.cpp | 131 +++++++++++++-------- src/theory/uf/equality_engine.h | 36 +++--- src/theory/uf/ho_extension.h | 1 + src/theory/uf/proof_equality_engine.h | 1 + 20 files changed, 392 insertions(+), 232 deletions(-) diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index d46346fd8..242d895fc 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -27,6 +27,7 @@ #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/partial_model.h" +#include "theory/ee_setup_info.h" #include "theory/uf/equality_engine.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index 9fc2e1156..9511f2779 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -19,6 +19,7 @@ #include +#include "theory/logic_info.h" #include "theory/theory_model.h" #include "theory/theory_model_builder.h" diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 4e1ef6d7f..bdf6d0607 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -17,6 +17,7 @@ #ifndef CVC4__FIRST_ORDER_MODEL_H #define CVC4__FIRST_ORDER_MODEL_H +#include "context/cdlist.h" #include "expr/attribute.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 4aa866d27..08410943f 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -18,6 +18,7 @@ #include "expr/emptyset.h" #include "expr/node_algorithm.h" #include "options/sets_options.h" +#include "smt/logic_exception.h" #include "theory/sets/normal_form.h" #include "theory/theory_model.h" #include "theory/valuation.h" diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 99584b167..a196d0ed0 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -50,9 +50,13 @@ void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { checkForConflict(); } - -void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { - Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; +void SharedTermsDatabase::addSharedTerm(TNode atom, + TNode term, + TheoryIdSet theories) +{ + Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " + << term << ", " << TheoryIdSetUtil::setToString(theories) + << ")" << std::endl; std::pair search_pair(atom, term); SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair); @@ -64,7 +68,8 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo d_termsToTheories[search_pair] = theories; } else { Assert(theories != (*find).second); - d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); + d_termsToTheories[search_pair] = + TheoryIdSetUtil::setUnion(theories, (*find).second); } } @@ -94,25 +99,27 @@ void SharedTermsDatabase::backtrack() { d_addedSharedTerms.resize(d_addedSharedTermsSize); } -Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) const { +TheoryIdSet SharedTermsDatabase::getTheoriesToNotify(TNode atom, + TNode term) const +{ // Get the theories that share this term from this atom std::pair search_pair(atom, term); SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair); Assert(find != d_termsToTheories.end()); // Get the theories that were already notified - Theory::Set alreadyNotified = 0; + TheoryIdSet alreadyNotified = 0; AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); if (theoriesFind != d_alreadyNotifiedMap.end()) { alreadyNotified = (*theoriesFind).second; } // Return the ones that haven't been notified yet - return Theory::setDifference((*find).second, alreadyNotified); + return TheoryIdSetUtil::setDifference((*find).second, alreadyNotified); } - -Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { +TheoryIdSet SharedTermsDatabase::getNotifiedTheories(TNode term) const +{ // Get the theories that were already notified AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); if (theoriesFind != d_alreadyNotifiedMap.end()) { @@ -142,15 +149,16 @@ bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNod return true; } -void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { - +void SharedTermsDatabase::markNotified(TNode term, TheoryIdSet theories) +{ // Find out if there are any new theories that were notified about this term - Theory::Set alreadyNotified = 0; + TheoryIdSet alreadyNotified = 0; AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term); if (theoriesFind != d_alreadyNotifiedMap.end()) { alreadyNotified = (*theoriesFind).second; } - Theory::Set newlyNotified = Theory::setDifference(theories, alreadyNotified); + TheoryIdSet newlyNotified = + TheoryIdSetUtil::setDifference(theories, alreadyNotified); // If no new theories were notified, we are done if (newlyNotified == 0) { @@ -160,11 +168,14 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl; // First update the set of notified theories for this term - d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified); + d_alreadyNotifiedMap[term] = + TheoryIdSetUtil::setUnion(newlyNotified, alreadyNotified); // Mark the shared terms in the equality engine theory::TheoryId currentTheory; - while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) { + while ((currentTheory = TheoryIdSetUtil::setPop(newlyNotified)) + != THEORY_LAST) + { d_equalityEngine.addTriggerTerm(term, currentTheory); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 05ce88d99..ca4f6c183 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -21,7 +21,7 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "theory/theory.h" +#include "theory/theory_id.h" #include "theory/uf/equality_engine.h" #include "util/statistics_registry.h" @@ -57,11 +57,15 @@ private: context::CDO d_addedSharedTermsSize; /** A map from atoms and subterms to the theories that use it */ - typedef context::CDHashMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; + typedef context::CDHashMap, + theory::TheoryIdSet, + TNodePairHashFunction> + SharedTermsTheoriesMap; SharedTermsTheoriesMap d_termsToTheories; /** Map from term to theories that have already been notified about the shared term */ - typedef context::CDHashMap AlreadyNotifiedMap; + typedef context::CDHashMap + AlreadyNotifiedMap; AlreadyNotifiedMap d_alreadyNotifiedMap; /** The registered equalities for propagation */ @@ -178,12 +182,12 @@ public: * Add a shared term to the database. The shared term is a subterm of the atom and * should be associated with the given theory. */ - void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories); + void addSharedTerm(TNode atom, TNode term, theory::TheoryIdSet theories); /** * Mark that the given theories have been notified of the given shared term. */ - void markNotified(TNode term, theory::Theory::Set theories); + void markNotified(TNode term, theory::TheoryIdSet theories); /** * Returns true if the atom contains any shared terms, false otherwise. @@ -203,12 +207,12 @@ public: /** * Get the theories that share the term in a given atom (and have not yet been notified). */ - theory::Theory::Set getTheoriesToNotify(TNode atom, TNode term) const; + theory::TheoryIdSet getTheoriesToNotify(TNode atom, TNode term) const; /** * Get the theories that share the term and have been notified already. */ - theory::Theory::Set getNotifiedTheories(TNode term) const; + theory::TheoryIdSet getNotifiedTheories(TNode term) const; /** * Returns true if the term is currently registered as shared with some theory. diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index fc27b847b..d9a67748d 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -19,12 +19,14 @@ #include +#include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" +#include "theory/strings/eqc_info.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" -#include "theory/strings/eqc_info.h" namespace CVC4 { namespace theory { diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index bf7cab4e3..b076e72a3 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -26,7 +26,8 @@ std::string PreRegisterVisitor::toString() const { std::stringstream ss; TNodeToTheorySetMap::const_iterator it = d_visited.begin(); for (; it != d_visited.end(); ++ it) { - ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second) + << std::endl; } return ss.str(); } @@ -50,8 +51,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); - d_theories = Theory::setInsert(currentTheoryId, d_theories); - d_theories = Theory::setInsert(parentTheoryId, d_theories); + d_theories = TheoryIdSetUtil::setInsert(currentTheoryId, d_theories); + d_theories = TheoryIdSetUtil::setInsert(parentTheoryId, d_theories); // Should we use the theory of the type bool useType = false; @@ -78,19 +79,21 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TNodeToTheorySetMap::iterator find = d_visited.find(current); if (find == d_visited.end()) { if (useType) { - d_theories = Theory::setInsert(typeTheoryId, d_theories); + d_theories = TheoryIdSetUtil::setInsert(typeTheoryId, d_theories); } return false; } - Theory::Set visitedTheories = (*find).second; - if (Theory::setContains(currentTheoryId, visitedTheories)) { + TheoryIdSet visitedTheories = (*find).second; + if (TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { // The current theory has already visited it, so now it depends on the parent and the type - if (Theory::setContains(parentTheoryId, visitedTheories)) { + if (TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { if (useType) { TheoryId typeTheoryId2 = Theory::theoryOf(current.getType()); - d_theories = Theory::setInsert(typeTheoryId2, d_theories); - return Theory::setContains(typeTheoryId2, visitedTheories); + d_theories = TheoryIdSetUtil::setInsert(typeTheoryId2, d_theories); + return TheoryIdSetUtil::setContains(typeTheoryId2, visitedTheories); } else { return true; } @@ -133,33 +136,45 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { } } } - - Theory::Set visitedTheories = d_visited[current]; - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; - if (!Theory::setContains(currentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories); + + TheoryIdSet visitedTheories = d_visited[current]; + Debug("register::internal") + << "PreRegisterVisitor::visit(" << current << "," << parent + << "): previously registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; + if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories); d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(currentTheoryId); th->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } - if (!Theory::setContains(parentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories); d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(parentTheoryId); th->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - if (!Theory::setContains(typeTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories); d_visited[current] = visitedTheories; Theory* th = d_engine->theoryOf(typeTheoryId); th->preRegisterTerm(current); Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } } - Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; + Debug("register::internal") + << "PreRegisterVisitor::visit(" << current << "," << parent + << "): now registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; Assert(d_visited.find(current) != d_visited.end()); Assert(alreadyVisited(current, parent)); @@ -169,7 +184,8 @@ std::string SharedTermsVisitor::toString() const { std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); for (; it != d_visited.end(); ++ it) { - ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second) + << std::endl; } return ss.str(); } @@ -197,7 +213,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { return false; } - Theory::Set theories = (*find).second; + TheoryIdSet theories = (*find).second; TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); @@ -239,16 +255,23 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } } - if (Theory::setContains(currentTheoryId, theories)) { - if (Theory::setContains(parentTheoryId, theories)) { - if (useType) { - return Theory::setContains(typeTheoryId, theories); - } else { - return true; - } - } else { - return false; + if (TheoryIdSetUtil::setContains(currentTheoryId, theories)) + { + if (TheoryIdSetUtil::setContains(parentTheoryId, theories)) + { + if (useType) + { + return TheoryIdSetUtil::setContains(typeTheoryId, theories); } + else + { + return true; + } + } + else + { + return false; + } } else { return false; } @@ -286,29 +309,43 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { } } - Theory::Set visitedTheories = d_visited[current]; - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; - if (!Theory::setContains(currentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories); + TheoryIdSet visitedTheories = d_visited[current]; + Debug("register::internal") + << "SharedTermsVisitor::visit(" << current << "," << parent + << "): previously registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; + if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(currentTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; } - if (!Theory::setContains(parentTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - if (!Theory::setContains(typeTheoryId, visitedTheories)) { - visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); + if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories)) + { + visitedTheories = + TheoryIdSetUtil::setInsert(typeTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl; } } - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl; + Debug("register::internal") + << "SharedTermsVisitor::visit(" << current << "," << parent + << "): now registered with " + << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; // Record the new theories that we visited d_visited[current] = visitedTheories; // If there is more than two theories and a new one has been added notify the shared terms database - if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) { + if (TheoryIdSetUtil::setDifference( + visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId))) + { d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories); } diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 6c6696f64..9772a6e34 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -42,7 +42,8 @@ class PreRegisterVisitor { /** The engine */ TheoryEngine* d_engine; - typedef context::CDHashMap TNodeToTheorySetMap; + typedef context::CDHashMap + TNodeToTheorySetMap; /** * Map from terms to the theories that have already had this term pre-registered. @@ -52,43 +53,43 @@ class PreRegisterVisitor { /** * A set of all theories in the term */ - theory::Theory::Set d_theories; + theory::TheoryIdSet d_theories; /** * String representation of the visited map, for debugging purposes. */ std::string toString() const; -public: - + public: /** Returned set tells us which theories there are */ - typedef theory::Theory::Set return_type; - + typedef theory::TheoryIdSet return_type; + PreRegisterVisitor(TheoryEngine* engine, context::Context* context) - : d_engine(engine) - , d_visited(context) - , d_theories(0) - {} + : d_engine(engine), d_visited(context), d_theories(0) + { + } /** - * Returns true is current has already been pre-registered with both current and parent theories. + * Returns true is current has already been pre-registered with both current + * and parent theories. */ bool alreadyVisited(TNode current, TNode parent); - + /** - * Pre-registeres current with any of the current and parent theories that haven't seen the term yet. + * Pre-registeres current with any of the current and parent theories that + * haven't seen the term yet. */ void visit(TNode current, TNode parent); - + /** * Marks the node as the starting literal. */ - void start(TNode node) { } + void start(TNode node) {} /** * Notifies the engine of all the theories used. */ - theory::Theory::Set done(TNode node) { return d_theories; } + theory::TheoryIdSet done(TNode node) { return d_theories; } }; @@ -105,7 +106,8 @@ class SharedTermsVisitor { /** * Cache from preprocessing of atoms. */ - typedef std::unordered_map TNodeVisitedMap; + typedef std::unordered_map + TNodeVisitedMap; TNodeVisitedMap d_visited; /** diff --git a/src/theory/theory.h b/src/theory/theory.h index 29a3a0998..c5fcf362c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -30,7 +30,6 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "lib/ffs.h" #include "options/options.h" #include "options/theory_options.h" #include "smt/command.h" @@ -799,84 +798,6 @@ class Theory { << " doesn't support Theory::setUserAttribute interface"; } - /** A set of theories */ - typedef uint32_t Set; - - /** A set of all theories */ - static const Set AllTheories = (1 << theory::THEORY_LAST) - 1; - - /** Pops a first theory off the set */ - static inline TheoryId setPop(Set& set) { - uint32_t i = ffs(set); // Find First Set (bit) - if (i == 0) { return THEORY_LAST; } - TheoryId id = (TheoryId)(i-1); - set = setRemove(id, set); - return id; - } - - /** Returns the size of a set of theories */ - static inline size_t setSize(Set set) { - size_t count = 0; - while (setPop(set) != THEORY_LAST) { - ++ count; - } - return count; - } - - /** Returns the index size of a set of theories */ - static inline size_t setIndex(TheoryId id, Set set) { - Assert(setContains(id, set)); - size_t count = 0; - while (setPop(set) != id) { - ++ count; - } - return count; - } - - /** Add the theory to the set. If no set specified, just returns a singleton set */ - static inline Set setInsert(TheoryId theory, Set set = 0) { - return set | (1 << theory); - } - - /** Add the theory to the set. If no set specified, just returns a singleton set */ - static inline Set setRemove(TheoryId theory, Set set = 0) { - return setDifference(set, setInsert(theory)); - } - - /** Check if the set contains the theory */ - static inline bool setContains(TheoryId theory, Set set) { - return set & (1 << theory); - } - - static inline Set setComplement(Set a) { - return (~a) & AllTheories; - } - - static inline Set setIntersection(Set a, Set b) { - return a & b; - } - - static inline Set setUnion(Set a, Set b) { - return a | b; - } - - /** a - b */ - static inline Set setDifference(Set a, Set b) { - return (~b) & a; - } - - static inline std::string setToString(theory::Theory::Set theorySet) { - std::stringstream ss; - ss << "["; - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { - if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) { - ss << (theory::TheoryId) theoryId << " "; - } - } - ss << "]"; - return ss.str(); - } - typedef context::CDList::const_iterator assertions_iterator; /** 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::run( + theory::TheoryIdSet theories = NodeVisitor::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); } } diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index 2c87458ef..a801e4abb 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -17,6 +17,9 @@ #include "theory/theory_id.h" +#include "base/check.h" +#include "lib/ffs.h" + namespace CVC4 { namespace theory { @@ -70,5 +73,89 @@ std::string getStatsPrefix(TheoryId theoryId) return "unknown"; } +TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set) +{ + uint32_t i = ffs(set); // Find First Set (bit) + if (i == 0) + { + return THEORY_LAST; + } + TheoryId id = static_cast(i - 1); + set = setRemove(id, set); + return id; +} + +size_t TheoryIdSetUtil::setSize(TheoryIdSet set) +{ + size_t count = 0; + while (setPop(set) != THEORY_LAST) + { + ++count; + } + return count; +} + +size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set) +{ + Assert(setContains(id, set)); + size_t count = 0; + while (setPop(set) != id) + { + ++count; + } + return count; +} + +TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set) +{ + return set | (1 << theory); +} + +TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set) +{ + return setDifference(set, setInsert(theory)); +} + +bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set) +{ + return set & (1 << theory); +} + +TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a) +{ + return (~a) & AllTheories; +} + +TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b) +{ + return a & b; +} + +TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b) +{ + return a | b; +} + +TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b) +{ + return (~b) & a; +} + +std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet) +{ + std::stringstream ss; + ss << "["; + for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId) + { + TheoryId tid = static_cast(theoryId); + if (setContains(tid, theorySet)) + { + ss << tid << " "; + } + } + ss << "]"; + return ss.str(); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h index 005380352..452dd09a9 100644 --- a/src/theory/theory_id.h +++ b/src/theory/theory_id.h @@ -23,7 +23,6 @@ #include namespace CVC4 { - namespace theory { /** @@ -58,6 +57,53 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId); std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; +/** + * A set of theories. Utilities for TheoryIdSet can be found below. + */ +typedef uint32_t TheoryIdSet; + +class TheoryIdSetUtil +{ + public: + /** A set of all theories */ + static const TheoryIdSet AllTheories = (1 << theory::THEORY_LAST) - 1; + + /** Pops a first theory off the set */ + static TheoryId setPop(TheoryIdSet& set); + + /** Returns the size of a set of theories */ + static size_t setSize(TheoryIdSet set); + + /** Returns the index size of a set of theories */ + static size_t setIndex(TheoryId id, TheoryIdSet set); + + /** Add the theory to the set. If no set specified, just returns a singleton + * set */ + static TheoryIdSet setInsert(TheoryId theory, TheoryIdSet set = 0); + + /** Add the theory to the set. If no set specified, just returns a singleton + * set */ + static TheoryIdSet setRemove(TheoryId theory, TheoryIdSet set = 0); + + /** Check if the set contains the theory */ + static bool setContains(TheoryId theory, TheoryIdSet set); + + /** Set complement of a */ + static TheoryIdSet setComplement(TheoryIdSet a); + + /** Set intersection of a and b */ + static TheoryIdSet setIntersection(TheoryIdSet a, TheoryIdSet b); + + /** Set union of a and b */ + static TheoryIdSet setUnion(TheoryIdSet a, TheoryIdSet b); + + /** Set difference of a and b */ + static TheoryIdSet setDifference(TheoryIdSet a, TheoryIdSet b); + + /** Convert theorySet to string (for debugging) */ + static std::string setToString(TheoryIdSet theorySet); +}; + } // namespace theory } // namespace CVC4 #endif diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 869e9100e..da9f28d01 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -16,6 +16,7 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "options/theory_options.h" #include "options/uf_options.h" #include "smt/smt_engine.h" diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index c31f208a0..aea3463c8 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -21,6 +21,7 @@ #include #include "smt/model.h" +#include "theory/ee_setup_info.h" #include "theory/rep_set.h" #include "theory/substitutions.h" #include "theory/type_enumerator.h" diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 898ca7dbc..32e2d1a90 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -23,6 +23,9 @@ #include "theory/theory_model.h" namespace CVC4 { + +class TheoryEngine; + namespace theory { /** TheoryEngineModelBuilder class diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 7bb857425..dd142edf4 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -17,6 +17,8 @@ #include "theory/uf/equality_engine.h" +#include "options/smt_options.h" +#include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" namespace CVC4 { @@ -386,13 +388,13 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); // Setup the new set - Theory::Set newSetTags = 0; + TheoryIdSet newSetTags = 0; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = THEORY_LAST; for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++currentTheory) { - newSetTags = Theory::setInsert(currentTheory, newSetTags); + newSetTags = TheoryIdSetUtil::setInsert(currentTheory, newSetTags); newSetTriggers[currentTheory] = tId; } // Add it to the list for backtracking @@ -534,17 +536,17 @@ bool EqualityEngine::assertEquality(TNode eq, TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef); // Go through and notify the shared dis-equalities - Theory::Set aTags = aTriggerTerms.d_tags; - Theory::Set bTags = bTriggerTerms.d_tags; - TheoryId aTag = Theory::setPop(aTags); - TheoryId bTag = Theory::setPop(bTags); + TheoryIdSet aTags = aTriggerTerms.d_tags; + TheoryIdSet bTags = bTriggerTerms.d_tags; + TheoryId aTag = TheoryIdSetUtil::setPop(aTags); + TheoryId bTag = TheoryIdSetUtil::setPop(bTags); int a_i = 0, b_i = 0; while (aTag != THEORY_LAST && bTag != THEORY_LAST) { if (aTag < bTag) { - aTag = Theory::setPop(aTags); + aTag = TheoryIdSetUtil::setPop(aTags); ++ a_i; } else if (aTag > bTag) { - bTag = Theory::setPop(bTags); + bTag = TheoryIdSetUtil::setPop(bTags); ++ b_i; } else { // Same tags, notify @@ -567,8 +569,8 @@ bool EqualityEngine::assertEquality(TNode eq, } } // Pop the next tags - aTag = Theory::setPop(aTags); - bTag = Theory::setPop(bTags); + aTag = TheoryIdSetUtil::setPop(aTags); + bTag = TheoryIdSetUtil::setPop(bTags); } } } @@ -618,12 +620,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Trigger set of class 1 TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; - Theory::Set class1Tags = class1triggerRef == null_set_id + TheoryIdSet class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).d_tags; // Trigger set of class 2 TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; - Theory::Set class2Tags = class2triggerRef == null_set_id + TheoryIdSet class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).d_tags; @@ -633,8 +635,10 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TaggedEqualitiesSet class1disequalitiesToNotify; // Individual tags - Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); - Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); + TheoryIdSet class1OnlyTags = + TheoryIdSetUtil::setDifference(class1Tags, class2Tags); + TheoryIdSet class2OnlyTags = + TheoryIdSetUtil::setDifference(class2Tags, class1Tags); // Only get disequalities if they are not both constant if (!class1isConstant || !class2isConstant) { @@ -760,17 +764,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef); // Initialize the merged set - Theory::Set newSetTags = - Theory::setUnion(class1triggers.d_tags, class2triggers.d_tags); + TheoryIdSet newSetTags = TheoryIdSetUtil::setUnion(class1triggers.d_tags, + class2triggers.d_tags); EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = 0; int i1 = 0; int i2 = 0; - Theory::Set tags1 = class1triggers.d_tags; - Theory::Set tags2 = class2triggers.d_tags; - TheoryId tag1 = Theory::setPop(tags1); - TheoryId tag2 = Theory::setPop(tags2); + TheoryIdSet tags1 = class1triggers.d_tags; + TheoryIdSet tags2 = class2triggers.d_tags; + TheoryId tag1 = TheoryIdSetUtil::setPop(tags1); + TheoryId tag2 = TheoryIdSetUtil::setPop(tags2); // Comparing the THEORY_LAST is OK because all other theories are // smaller, and will therefore be preferred @@ -780,12 +784,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // copy tag1 newSetTriggers[newSetTriggersSize++] = class1triggers.d_triggers[i1++]; - tag1 = Theory::setPop(tags1); + tag1 = TheoryIdSetUtil::setPop(tags1); } else if (tag1 > tag2) { // copy tag2 newSetTriggers[newSetTriggersSize++] = class2triggers.d_triggers[i2++]; - tag2 = Theory::setPop(tags2); + tag2 = TheoryIdSetUtil::setPop(tags2); } else { // copy tag1 EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = @@ -798,8 +802,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } } // Next tags - tag1 = Theory::setPop(tags1); - tag2 = Theory::setPop(tags2); + tag1 = TheoryIdSetUtil::setPop(tags1); + tag2 = TheoryIdSetUtil::setPop(tags2); } } @@ -1252,6 +1256,7 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, void EqualityEngine::explainLit(TNode lit, std::vector& assumptions) { + Assert(lit.getKind() != kind::AND); bool polarity = lit.getKind() != kind::NOT; TNode atom = polarity ? lit : lit[0]; std::vector tassumptions; @@ -1281,6 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector& assumptions) if (std::find(assumptions.begin(), assumptions.end(), a) == assumptions.end()) { + Assert(!a.isNull()); assumptions.push_back(a); } } @@ -1288,13 +1294,13 @@ void EqualityEngine::explainLit(TNode lit, std::vector& assumptions) Node EqualityEngine::mkExplainLit(TNode lit) { + Assert(lit.getKind() != kind::AND); std::vector assumptions; explainLit(lit, assumptions); Node ret; - NodeManager* nm = NodeManager::currentNM(); if (assumptions.empty()) { - ret = nm->mkConst(true); + ret = NodeManager::currentNM()->mkConst(true); } else if (assumptions.size() == 1) { @@ -1302,7 +1308,7 @@ Node EqualityEngine::mkExplainLit(TNode lit) } else { - ret = nm->mkNode(kind::AND, assumptions); + ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions); } return ret; } @@ -2267,11 +2273,11 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // uselists that have been asserted to false. All the representatives appearing on the other // side of such disequalities, that have the tag on, are put in a set. TaggedEqualitiesSet disequalitiesToNotify; - Theory::Set tags = Theory::setInsert(tag); + TheoryIdSet tags = TheoryIdSetUtil::setInsert(tag); getDisequalities(!d_isConstant[classId], classId, tags, disequalitiesToNotify); // Trigger data - Theory::Set newSetTags; + TheoryIdSet newSetTags; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize; @@ -2280,23 +2286,23 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Get the existing set TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); // Initialize the new set for copy/insert - newSetTags = Theory::setInsert(tag, triggerSet.d_tags); + newSetTags = TheoryIdSetUtil::setInsert(tag, triggerSet.d_tags); newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; - Theory::Set tags2 = newSetTags; + TheoryIdSet tags2 = newSetTags; TheoryId current; - while ((current = Theory::setPop(tags2)) != THEORY_LAST) + while ((current = TheoryIdSetUtil::setPop(tags2)) != THEORY_LAST) { // Remove from the tags - tags2 = Theory::setRemove(current, tags2); + tags2 = TheoryIdSetUtil::setRemove(current, tags2); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = current == tag ? eqNodeId : triggerSet.d_triggers[i++]; } } else { // Setup a singleton - newSetTags = Theory::setInsert(tag); + newSetTags = TheoryIdSetUtil::setInsert(tag); newSetTriggers[0] = eqNodeId; newSetTriggersSize = 1; } @@ -2326,8 +2332,9 @@ TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const EqualityNodeId classId = getEqualityNode(t).getFind(); const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]); unsigned i = 0; - Theory::Set tags = triggerSet.d_tags; - while (Theory::setPop(tags) != tag) { + TheoryIdSet tags = triggerSet.d_tags; + while (TheoryIdSetUtil::setPop(tags) != tag) + { ++ i; } return d_nodes[triggerSet.d_triggers[i]]; @@ -2381,7 +2388,11 @@ void EqualityEngine::getUseListTerms(TNode t, std::set& output) { } } -EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize) { +EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet( + TheoryIdSet newSetTags, + EqualityNodeId* newSetTriggers, + unsigned newSetTriggersSize) +{ // Size of the required set size_t size = sizeof(TriggerTermSet) + newSetTriggersSize*sizeof(EqualityNodeId); // Align the size @@ -2429,7 +2440,7 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId } Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end()) << "We propagated but there is no proof"; - bool result = Theory::setContains(tag, (*it).second); + bool result = TheoryIdSetUtil::setContains(tag, (*it).second); Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl; return result; } @@ -2446,12 +2457,12 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs EqualityPair pair2(rhsId, lhsId); // Store the fact that we've propagated this already - Theory::Set notified = 0; + TheoryIdSet notified = 0; PropagatedDisequalitiesMap::const_iterator find = d_propagatedDisequalities.find(pair1); if (find == d_propagatedDisequalities.end()) { - notified = Theory::setInsert(tag); + notified = TheoryIdSetUtil::setInsert(tag); } else { - notified = Theory::setInsert(tag, (*find).second); + notified = TheoryIdSetUtil::setInsert(tag, (*find).second); } d_propagatedDisequalities[pair1] = notified; d_propagatedDisequalities[pair2] = notified; @@ -2493,12 +2504,16 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs } } -void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out) { +void EqualityEngine::getDisequalities(bool allowConstants, + EqualityNodeId classId, + TheoryIdSet inputTags, + TaggedEqualitiesSet& out) +{ // Must be empty on input Assert(out.size() == 0); // The class we are looking for, shouldn't have any of the tags we are looking for already set Assert(d_nodeIndividualTrigger[classId] == null_set_id - || Theory::setIntersection( + || TheoryIdSetUtil::setIntersection( getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags, inputTags) == 0); @@ -2556,8 +2571,8 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // Tags of the other gey TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); // We only care if there are things in inputTags that is also in toCompareTags - Theory::Set commonTags = - Theory::setIntersection(inputTags, toCompareTriggerSet.d_tags); + TheoryIdSet commonTags = TheoryIdSetUtil::setIntersection( + inputTags, toCompareTriggerSet.d_tags); if (commonTags) { out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs)); } @@ -2573,8 +2588,11 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI } -bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) { - +bool EqualityEngine::propagateTriggerTermDisequalities( + TheoryIdSet tags, + TriggerTermSetRef triggerSetRef, + const TaggedEqualitiesSet& disequalitiesToNotify) +{ // No tags, no food if (!tags) { return !d_done; @@ -2592,8 +2610,8 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger const TaggedEquality& disequalityInfo = *it; const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.d_triggerSetRef); - Theory::Set commonTags = - Theory::setIntersection(disequalityTriggerSet.d_tags, tags); + TheoryIdSet commonTags = + TheoryIdSetUtil::setIntersection(disequalityTriggerSet.d_tags, tags); Assert(commonTags); // This is the actual function const FunctionApplication& fun = @@ -2608,7 +2626,10 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger } // Go through the tags, and add the disequalities TheoryId currentTag; - while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) { + while ( + !d_done + && ((currentTag = TheoryIdSetUtil::setPop(commonTags)) != THEORY_LAST)) + { // Get the tag representative EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag); EqualityNodeId myRep = triggerSet.getTrigger(currentTag); @@ -2636,6 +2657,16 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger return !d_done; } +TheoryIdSet EqualityEngine::TriggerTermSet::hasTrigger(TheoryId tag) const +{ + return TheoryIdSetUtil::setContains(tag, d_tags); +} + +EqualityNodeId EqualityEngine::TriggerTermSet::getTrigger(TheoryId tag) const +{ + return d_triggers[TheoryIdSetUtil::setIndex(tag, d_tags)]; +} + } // Namespace uf } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 91dae2509..19a10eba8 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -32,7 +32,7 @@ #include "expr/kind_map.h" #include "expr/node.h" #include "theory/rewriter.h" -#include "theory/theory.h" +#include "theory/theory_id.h" #include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine_iterator.h" #include "theory/uf/equality_engine_notify.h" @@ -500,18 +500,13 @@ private: /** Set of trigger terms */ struct TriggerTermSet { /** Set of theories in this set */ - Theory::Set d_tags; + TheoryIdSet d_tags; /** The trigger terms */ EqualityNodeId d_triggers[0]; /** Returns the theory tags */ - Theory::Set hasTrigger(TheoryId tag) const - { - return Theory::setContains(tag, d_tags); - } + TheoryIdSet hasTrigger(TheoryId tag) const; /** Returns a trigger by tag */ - EqualityNodeId getTrigger(TheoryId tag) const { - return d_triggers[Theory::setIndex(tag, d_tags)]; - } + EqualityNodeId getTrigger(TheoryId tag) const; };/* struct EqualityEngine::TriggerTermSet */ /** Are the constants triggers */ @@ -535,7 +530,9 @@ private: static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1); /** Create new trigger term set based on the internally set information */ - TriggerTermSetRef newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize); + TriggerTermSetRef newTriggerTermSet(TheoryIdSet newSetTags, + EqualityNodeId* newSetTriggers, + unsigned newSetTriggersSize); /** Get the trigger set give a reference */ TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) { @@ -607,7 +604,9 @@ private: /** * Map from equalities to the tags that have received the notification. */ - typedef context::CDHashMap PropagatedDisequalitiesMap; + typedef context:: + CDHashMap + PropagatedDisequalitiesMap; PropagatedDisequalitiesMap d_propagatedDisequalities; /** @@ -659,14 +658,19 @@ private: * @param inputTags the tags to filter the equalities * @param out the output equalities, as described above */ - void getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out); + void getDisequalities(bool allowConstants, + EqualityNodeId classId, + TheoryIdSet inputTags, + TaggedEqualitiesSet& out); /** * Propagates the remembered disequalities with given tags the original triggers for those tags, * and the set of disequalities produced by above. */ - bool propagateTriggerTermDisequalities(Theory::Set tags, - TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); + bool propagateTriggerTermDisequalities( + TheoryIdSet tags, + TriggerTermSetRef triggerSetRef, + const TaggedEqualitiesSet& disequalitiesToNotify); /** Name of the equality engine */ std::string d_name; @@ -792,8 +796,8 @@ private: */ void explainLit(TNode lit, std::vector& assumptions); /** - * Explain literal, return the conjunction. This method relies on the above - * method. + * Explain literal, return the explanation as a conjunction. This method + * relies on the above method. */ Node mkExplainLit(TNode lit); //--------------------------- end standard safe explanation methods diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index dc37808c9..25cb3623b 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -22,6 +22,7 @@ #include "context/cdo.h" #include "expr/node.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 2ee379509..b71f72c53 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -21,6 +21,7 @@ #include #include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof_node.h" -- 2.30.2