diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-23 14:28:29 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-23 14:28:29 -0500 |
commit | b13d2f7921a65b8921ef37b38a2d4579f7c911a2 (patch) | |
tree | df7e49fb4318fe58631ca4c4305125dd4fc32afe /src/theory/term_registration_visitor.cpp | |
parent | c254649c8dadd9f0d94f09bf46b21f93b2c67c07 (diff) |
Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
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; - } } } } |