From b13d2f7921a65b8921ef37b38a2d4579f7c911a2 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 23 May 2016 14:28:29 -0500
Subject: Fix related to parametric sorts whose interpretation is finite due to
 uninterpreted sorts + FMF.  Generalizes previous fix in term registration
 visitor.

---
 src/expr/datatype.cpp  | 19 +++++--------------
 src/expr/datatype.h    |  4 ++--
 src/expr/type_node.cpp | 21 +++++++++++++++++++++
 src/expr/type_node.h   |  7 +++++++
 4 files changed, 35 insertions(+), 16 deletions(-)

(limited to 'src/expr')

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index d14ac26d4..001f38a79 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool Datatype::isUFinite() const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
@@ -310,7 +310,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) {
   self.setAttribute(DatatypeUFiniteComputedAttr(), true);
   self.setAttribute(DatatypeUFiniteAttr(), false);
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).isUFinite()) {
+    if(! (*i).isInterpretedFinite()) {
       return false;
     }
   }
@@ -850,7 +850,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
@@ -859,18 +859,9 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
   if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
     return self.getAttribute(DatatypeUFiniteAttr());
   }
-  bool success = true;
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type t = (*i).getRangeType();
-    if( t.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)t).getDatatype();
-      if( !dt.isUFinite() ){
-        success = false;
-      }
-    }else if(!t.isSort() && !t.getCardinality().isFinite()) {
-      success = false;
-    }
-    if(!success ){
+    TypeNode t = TypeNode::fromType( (*i).getRangeType() );
+    if(!t.isInterpretedFinite()) {
       self.setAttribute(DatatypeUFiniteComputedAttr(), true);
       self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 1197b4a3b..dfd893fe8 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -342,7 +342,7 @@ public:
    * uninterpreted sorts are finite.  This function can
    * only be called for resolved constructors.
    */
-  bool isUFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite() const throw(IllegalArgumentException);
 
   /**
    * Returns true iff this Datatype constructor has already been
@@ -634,7 +634,7 @@ public:
    * datatype is  not well-founded, this function  returns false.  The
    * Datatype must be resolved or an exception is thrown.
    */
-  bool isUFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite() const throw(IllegalArgumentException);
 
   /**
    * Return true iff this datatype is well-founded (there exist ground
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 5d672e6ac..dc2370bea 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -21,6 +21,7 @@
 #include "expr/type_properties.h"
 #include "options/base_options.h"
 #include "options/expr_options.h"
+#include "options/quantifiers_options.h"
 
 using namespace std;
 
@@ -64,6 +65,26 @@ Cardinality TypeNode::getCardinality() const {
   return kind::getCardinality(*this);
 }
 
+bool TypeNode::isInterpretedFinite() const {
+  if( getCardinality().isFinite() ){
+    return true;
+  }else{
+    if( options::finiteModelFind() ){
+      if( isSort() ){
+        return true;
+      }else if( isDatatype() || isParametricDatatype() ){
+        const Datatype& dt = getDatatype();
+        return dt.isInterpretedFinite();
+      }else if( isArray() ){
+        return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite();
+      }else if( isSet() ) {
+        return getSetElementType().isInterpretedFinite();
+      }
+    }
+    return false;
+  }
+}
+
 bool TypeNode::isWellFounded() const {
   return kind::isWellFounded(*this);
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index cfb61a085..46fdaa143 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -419,6 +419,13 @@ public:
    * @return a finite or infinite cardinality
    */
   Cardinality getCardinality() const;
+  
+  /**
+   * Is this type interpreted as being finite.
+   * If finite model finding is enabled, this assumes all uninterpreted sorts 
+   *   are interpreted as finite.
+   */
+  bool isInterpretedFinite() const;
 
   /**
    * Returns whether this type is well-founded.
-- 
cgit v1.2.3