summaryrefslogtreecommitdiff
path: root/src/theory/term_registration_visitor.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r--src/theory/term_registration_visitor.cpp340
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback