diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2014-11-07 12:31:26 -0500 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2014-11-10 14:09:59 -0500 |
commit | f9f3d26e4f34bfa0b03e05af6b827e7b72ea6ebd (patch) | |
tree | 5779409c1924886835ea667922ad70d61e1d0df9 /src | |
parent | be316870ef337a435d65f46a26f40ef0eab97934 (diff) |
Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 76 |
1 files changed, 72 insertions, 4 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 0e573ce62..7ece4594d 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -50,13 +50,36 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { d_theories = Theory::setInsert(parentTheoryId, d_theories); // Should we use the theory of the type - bool useType = current != parent && currentTheoryId != parentTheoryId; + 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 (options::finiteModelFind() && type.isSort()) { + // We're looking for finite models + useType = true; + } else { + Cardinality card = type.getCardinality(); + if (card.isFinite()) { + 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) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); d_theories = Theory::setInsert(typeTheoryId, d_theories); } return false; @@ -93,8 +116,32 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TheoryId parentTheoryId = Theory::theoryOf(parent); // Should we use the theory of the type - bool useType = current != parent && currentTheoryId != parentTheoryId; + 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 (options::finiteModelFind() && type.isSort()) { + // We're looking for finite models + useType = true; + } else { + Cardinality card = type.getCardinality(); + if (card.isFinite()) { + useType = 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)) { @@ -112,7 +159,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); if (!Theory::setContains(typeTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); d_visited[current] = visitedTheories; @@ -187,6 +233,28 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } } } + 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 (options::finiteModelFind() && type.isSort()) { + // We're looking for finite models + useType = true; + } else { + Cardinality card = type.getCardinality(); + if (card.isFinite()) { + useType = true; + } + } + } + } + } if (Theory::setContains(currentTheoryId, theories)) { if (Theory::setContains(parentTheoryId, theories)) { |