diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-12 16:55:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-12 21:55:44 +0000 |
commit | 76f495646c0e3a95f2474c5d746bc61ece18f89f (patch) | |
tree | 5390007f4be229dfb18e641f34b9d9df6a9dea92 /src/theory/term_registration_visitor.cpp | |
parent | af398235ef9f3a909991fddbb71d43434d6cf3a1 (diff) |
Fix computation of whether a type is finite (#6312)
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index e546e6937..7f669e36d 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -41,7 +41,10 @@ std::string PreRegisterVisitor::toString() const { * current. This method is used by PreRegisterVisitor and SharedTermsVisitor * below. */ -bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent) +bool isAlreadyVisited(TheoryEngine* te, + TheoryIdSet visitedTheories, + TNode current, + TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories)) @@ -67,7 +70,7 @@ bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent) // do we need to consider the type? TypeNode type = current.getType(); - if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite()) + if (currentTheoryId == parentTheoryId && !te->isFiniteType(type)) { // current and parent are the same theory, and we are infinite, return true return true; @@ -100,7 +103,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { } TheoryIdSet visitedTheories = (*find).second; - return isAlreadyVisited(visitedTheories, current, parent); + return isAlreadyVisited(d_engine, visitedTheories, current, parent); } void PreRegisterVisitor::visit(TNode current, TNode parent) { @@ -149,7 +152,7 @@ void PreRegisterVisitor::preRegister(TheoryEngine* te, // 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()) + if (currentTheoryId != parentTheoryId || te->isFiniteType(type)) { // preregister with the type's theory, if necessary TheoryId typeTheoryId = Theory::theoryOf(type); @@ -244,7 +247,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } TheoryIdSet visitedTheories = (*find).second; - return isAlreadyVisited(visitedTheories, current, parent); + return isAlreadyVisited(d_engine, visitedTheories, current, parent); } void SharedTermsVisitor::visit(TNode current, TNode parent) { |