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.
#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"
#include <memory>
+#include "theory/logic_info.h"
#include "theory/theory_model.h"
#include "theory/theory_model_builder.h"
#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"
#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"
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<TNode, TNode> search_pair(atom, term);
SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
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);
}
}
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<TNode, TNode> 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()) {
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) {
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);
}
#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"
context::CDO<unsigned> d_addedSharedTermsSize;
/** A map from atoms and subterms to the theories that use it */
- typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
+ typedef context::CDHashMap<std::pair<Node, TNode>,
+ theory::TheoryIdSet,
+ TNodePairHashFunction>
+ SharedTermsTheoriesMap;
SharedTermsTheoriesMap d_termsToTheories;
/** Map from term to theories that have already been notified about the shared term */
- typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
+ typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
+ AlreadyNotifiedMap;
AlreadyNotifiedMap d_alreadyNotifiedMap;
/** The registered equalities for propagation */
* 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.
/**
* 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.
#include <map>
+#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 {
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();
}
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;
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;
}
}
}
}
-
- 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));
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();
}
return false;
}
- Theory::Set theories = (*find).second;
+ TheoryIdSet theories = (*find).second;
TheoryId currentTheoryId = Theory::theoryOf(current);
TheoryId parentTheoryId = Theory::theoryOf(parent);
}
}
- 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;
}
}
}
- 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);
}
/** The engine */
TheoryEngine* d_engine;
- typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeToTheorySetMap;
+ typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
+ TNodeToTheorySetMap;
/**
* Map from terms to the theories that have already had this term pre-registered.
/**
* 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; }
};
/**
* Cache from preprocessing of atoms.
*/
- typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+ typedef std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>
+ TNodeVisitedMap;
TNodeVisitedMap d_visited;
/**
#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"
<< " 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<Assertion>::const_iterator assertions_iterator;
/**
#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"
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;
// 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))
{
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);
}
}
#include "theory/theory_id.h"
+#include "base/check.h"
+#include "lib/ffs.h"
+
namespace CVC4 {
namespace theory {
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<TheoryId>(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>(theoryId);
+ if (setContains(tid, theorySet))
+ {
+ ss << tid << " ";
+ }
+ }
+ ss << "]";
+ return ss.str();
+}
+
} // namespace theory
} // namespace CVC4
#include <iostream>
namespace CVC4 {
-
namespace theory {
/**
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
#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"
#include <unordered_set>
#include "smt/model.h"
+#include "theory/ee_setup_info.h"
#include "theory/rep_set.h"
#include "theory/substitutions.h"
#include "theory/type_enumerator.h"
#include "theory/theory_model.h"
namespace CVC4 {
+
+class TheoryEngine;
+
namespace theory {
/** TheoryEngineModelBuilder class
#include "theory/uf/equality_engine.h"
+#include "options/smt_options.h"
+#include "proof/proof_manager.h"
#include "smt/smt_statistics_registry.h"
namespace CVC4 {
// 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
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
}
}
// Pop the next tags
- aTag = Theory::setPop(aTags);
- bTag = Theory::setPop(bTags);
+ aTag = TheoryIdSetUtil::setPop(aTags);
+ bTag = TheoryIdSetUtil::setPop(bTags);
}
}
}
// 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;
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) {
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
// 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++] =
}
}
// Next tags
- tag1 = Theory::setPop(tags1);
- tag2 = Theory::setPop(tags2);
+ tag1 = TheoryIdSetUtil::setPop(tags1);
+ tag2 = TheoryIdSetUtil::setPop(tags2);
}
}
void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
{
+ Assert(lit.getKind() != kind::AND);
bool polarity = lit.getKind() != kind::NOT;
TNode atom = polarity ? lit : lit[0];
std::vector<TNode> tassumptions;
if (std::find(assumptions.begin(), assumptions.end(), a)
== assumptions.end())
{
+ Assert(!a.isNull());
assumptions.push_back(a);
}
}
Node EqualityEngine::mkExplainLit(TNode lit)
{
+ Assert(lit.getKind() != kind::AND);
std::vector<TNode> 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)
{
}
else
{
- ret = nm->mkNode(kind::AND, assumptions);
+ ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
}
return ret;
}
// 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;
// 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;
}
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]];
}
}
-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
}
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;
}
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;
}
}
-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);
// 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));
}
}
-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;
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 =
}
// 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);
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
#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"
/** 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 */
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) {
/**
* Map from equalities to the tags that have received the notification.
*/
- typedef context::CDHashMap<EqualityPair, Theory::Set, EqualityPairHashFunction> PropagatedDisequalitiesMap;
+ typedef context::
+ CDHashMap<EqualityPair, TheoryIdSet, EqualityPairHashFunction>
+ PropagatedDisequalitiesMap;
PropagatedDisequalitiesMap d_propagatedDisequalities;
/**
* @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;
*/
void explainLit(TNode lit, std::vector<TNode>& 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
#include "context/cdo.h"
#include "expr/node.h"
#include "theory/theory_model.h"
+#include "theory/theory_state.h"
namespace CVC4 {
namespace theory {
#include <vector>
#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
#include "expr/lazy_proof.h"
#include "expr/node.h"
#include "expr/proof_node.h"
projects / cvc5.git / commitdiff