diff options
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 40 |
1 files changed, 5 insertions, 35 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 830e7f809..6b268805a 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -64,14 +64,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -130,14 +124,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -222,14 +210,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -244,14 +226,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -297,14 +273,8 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } |