diff options
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 340 |
1 files changed, 132 insertions, 208 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index b4ad87f1e..82463367e 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -18,9 +18,9 @@ #include "options/quantifiers_options.h" #include "theory/theory_engine.h" -using namespace std; -using namespace CVC4; -using namespace theory; +using namespace CVC4::theory; + +namespace CVC4 { std::string PreRegisterVisitor::toString() const { std::stringstream ss; @@ -32,6 +32,47 @@ std::string PreRegisterVisitor::toString() const { return ss.str(); } +/** + * Return true if we already visited the term current with the given parent, + * assuming that the set of theories in visitedTheories has already processed + * current. This method is used by PreRegisterVisitor and SharedTermsVisitor + * below. + */ +bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent) +{ + TheoryId currentTheoryId = Theory::theoryOf(current); + if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + { + // current theory not visited, return false + return false; + } + + if (current == parent) + { + // top-level and current visited, return true + return true; + } + + // The current theory has already visited it, so now it depends on the parent + // and the type + TheoryId parentTheoryId = Theory::theoryOf(parent); + if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) + { + // parent theory not visited, return false + return false; + } + + // do we need to consider the type? + TypeNode type = current.getType(); + if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite()) + { + // current and parent are the same theory, and we are infinite, return true + return true; + } + TheoryId typeTheoryId = Theory::theoryOf(type); + return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories); +} + bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; @@ -47,62 +88,16 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "quantifier:true" << std::endl; return true; } - - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); - - 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; - TheoryId typeTheoryId = THEORY_LAST; - - if (current != parent) { - if (currentTheoryId != parentTheoryId) { - // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers - TypeNode type = current.getType(); - useType = true; - typeTheoryId = Theory::theoryOf(type); - } else { - TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); - if (typeTheoryId != currentTheoryId) { - if (type.isInterpretedFinite()) { - useType = true; - } - } - } - } // Get the theories that have already visited this node TNodeToTheorySetMap::iterator find = d_visited.find(current); if (find == d_visited.end()) { - if (useType) { - d_theories = TheoryIdSetUtil::setInsert(typeTheoryId, d_theories); - } + // not visited at all, return false return false; } 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 (TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) - { - if (useType) { - TheoryId typeTheoryId2 = Theory::theoryOf(current.getType()); - d_theories = TheoryIdSetUtil::setInsert(typeTheoryId2, d_theories); - return TheoryIdSetUtil::setContains(typeTheoryId2, visitedTheories); - } else { - return true; - } - } else { - return false; - } - } else { - return false; - } + return isAlreadyVisited(visitedTheories, current, parent); } void PreRegisterVisitor::visit(TNode current, TNode parent) { @@ -112,74 +107,96 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { Debug("register::internal") << toString() << std::endl; } - // Get the theories of the terms - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); - - // Should we use the theory of the type - bool useType = false; - TheoryId typeTheoryId = THEORY_LAST; - - if (current != parent) { - if (currentTheoryId != parentTheoryId) { - // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers - TypeNode type = current.getType(); - useType = true; - typeTheoryId = Theory::theoryOf(type); - } else { - TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); - if (typeTheoryId != currentTheoryId) { - if (type.isInterpretedFinite()) { - useType = true; - } - } - } - } - + // get the theories we already preregistered with TheoryIdSet visitedTheories = d_visited[current]; + + // call the preregistration on current, parent or type theories and update + // visitedTheories. + preRegister(d_engine, visitedTheories, current, parent); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent - << "): previously registered with " + << "): now registered with " << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; - if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) + // update the theories set for current + d_visited[current] = visitedTheories; + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); +} + +void PreRegisterVisitor::preRegister(TheoryEngine* te, + TheoryIdSet& visitedTheories, + TNode current, + TNode parent) +{ + // Preregister with the current theory, if necessary + TheoryId currentTheoryId = Theory::theoryOf(current); + preRegisterWithTheory(te, visitedTheories, currentTheoryId, current, parent); + + if (current != parent) { - 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; + // preregister with parent theory, if necessary + TheoryId parentTheoryId = Theory::theoryOf(parent); + preRegisterWithTheory(te, visitedTheories, parentTheoryId, current, parent); + + // Note that if enclosed by different theories it's shared, for example, + // in read(a, f(a)), f(a) should be shared with integers. + TypeNode type = current.getType(); + if (currentTheoryId != parentTheoryId || type.isInterpretedFinite()) + { + // preregister with the type's theory, if necessary + TheoryId typeTheoryId = Theory::theoryOf(type); + preRegisterWithTheory(te, visitedTheories, typeTheoryId, current, parent); + } } - if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) +} +void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te, + TheoryIdSet& visitedTheories, + TheoryId id, + TNode current, + TNode parent) +{ + if (TheoryIdSetUtil::setContains(id, 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; + // already registered + return; } - if (useType) { - if (!TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories)) + if (Configuration::isAssertionBuild()) + { + Debug("register::internal") + << "PreRegisterVisitor::visit(" << current << "," << parent + << "): adding " << id << std::endl; + // This should never throw an exception, since theories should be + // guaranteed to be initialized. + // These checks don't work with finite model finding, because it + // uses Rational constants to represent cardinality constraints, + // even though arithmetic isn't actually involved. + if (!options::finiteModelFind()) { - 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; + if (!te->isTheoryEnabled(id)) + { + const LogicInfo& l = te->getLogicInfo(); + LogicInfo newLogicInfo = l.getUnlockedCopy(); + newLogicInfo.enableTheory(id); + newLogicInfo.lock(); + std::stringstream ss; + ss << "The logic was specified as " << l.getLogicString() + << ", which doesn't include " << id + << ", but found a term in that theory." << std::endl + << "You might want to extend your logic to " + << newLogicInfo.getLogicString() << std::endl; + throw LogicException(ss.str()); + } } } - 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)); + // call the theory's preRegisterTerm method + visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories); + Theory* th = te->theoryOf(id); + th->preRegisterTerm(current); } +void PreRegisterVisitor::start(TNode node) {} + std::string SharedTermsVisitor::toString() const { std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); @@ -206,59 +223,14 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { return true; } TNodeVisitedMap::const_iterator find = d_visited.find(current); - // If node is not visited at all, just return false if (find == d_visited.end()) { Debug("register::internal") << "1:false" << std::endl; return false; } - TheoryIdSet theories = (*find).second; - - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); - - // Should we use the theory of the type - bool useType = false; - TheoryId typeTheoryId = THEORY_LAST; - - if (current != parent) { - if (currentTheoryId != parentTheoryId) { - // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers - TypeNode type = current.getType(); - useType = true; - typeTheoryId = Theory::theoryOf(type); - } else { - TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); - if (typeTheoryId != currentTheoryId) { - if (type.isInterpretedFinite()) { - useType = true; - } - } - } - } - - 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; - } + TheoryIdSet visitedTheories = (*find).second; + return isAlreadyVisited(visitedTheories, current, parent); } void SharedTermsVisitor::visit(TNode current, TNode parent) { @@ -267,66 +239,16 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { if (Debug.isOn("register::internal")) { Debug("register::internal") << toString() << std::endl; } - - // Get the theories of the terms - TheoryId currentTheoryId = Theory::theoryOf(current); - TheoryId parentTheoryId = Theory::theoryOf(parent); - - // Should we use the theory of the type - bool useType = false; - TheoryId typeTheoryId = THEORY_LAST; - - if (current != parent) { - if (currentTheoryId != parentTheoryId) { - // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers - TypeNode type = current.getType(); - useType = true; - typeTheoryId = Theory::theoryOf(type); - } else { - TypeNode type = current.getType(); - typeTheoryId = Theory::theoryOf(type); - if (typeTheoryId != currentTheoryId) { - if (type.isInterpretedFinite()) { - useType = true; - } - } - } - } - 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 (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories)) - { - visitedTheories = - TheoryIdSetUtil::setInsert(parentTheoryId, visitedTheories); - Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; - } - if (useType) { - 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 " - << TheoryIdSetUtil::setToString(visitedTheories) << std::endl; + + // preregister the term with the current, parent or type theories, as needed + PreRegisterVisitor::preRegister(d_engine, visitedTheories, current, parent); // 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 + TheoryId currentTheoryId = Theory::theoryOf(current); if (TheoryIdSetUtil::setDifference( visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId))) { @@ -338,7 +260,7 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { } void SharedTermsVisitor::start(TNode node) { - clear(); + d_visited.clear(); d_atom = node; } @@ -350,3 +272,5 @@ void SharedTermsVisitor::clear() { d_atom = TNode(); d_visited.clear(); } + +} // namespace CVC4 |