Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.

12 files changed, 86 insertions, 60 deletions

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.
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 0100f1833..95d704a0e 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -191,7 +191,7 @@ void TheoryDatatypes::check(Effort e) {
           if( !hasLabel( eqc, n ) ){
             Trace("datatypes-debug") << "No constructor..." << std::endl;
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isUFinite() << " " << dt.isRecursiveSingleton() << std::endl;
+            Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isInterpretedFinite() << " " << dt.isRecursiveSingleton() << std::endl;
             bool continueProc = true;
             if( dt.isRecursiveSingleton() ){
               Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
@@ -252,7 +252,7 @@ void TheoryDatatypes::check(Effort e) {
                   if( consIndex==-1 ){
                     consIndex = j;
                   }
-                  if( options::finiteModelFind() ? !dt[ j ].isUFinite() : !dt[ j ].isFinite() ) {
+                  if( !dt[ j ].isInterpretedFinite() ) {
                     if( !eqc || !eqc->d_selectors ){
                       needSplit = false;
                     }
@@ -1497,7 +1497,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         if( neqc.isNull() ){
           for( unsigned i=0; i<pcons.size(); i++ ){
             //must try the infinite ones first
-            bool cfinite = options::finiteModelFind() ? dt[ i ].isUFinite() : dt[ i ].isFinite();
+            bool cfinite = dt[ i ].isInterpretedFinite();
             if( pcons[i] && (r==1)==cfinite ){
               neqc = DatatypesRewriter::getInstCons( eqc, dt, i );
               //for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 6c1155237..c0539743f 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -172,7 +172,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    Debug("dt-enum") << "datatype is " << d_type << std::endl;
    Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton();
    Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl;
-   Debug("dt-enum") << " " << d_datatype.isUFinite() << std::endl;
+   Debug("dt-enum") << " " << d_datatype.isInterpretedFinite() << std::endl;
 
    if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
      //start with uninterpreted constant
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index bbfd951b3..8473b5d69 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -159,7 +159,7 @@ public:
       }
       if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){
         //try next size limit as long as new terms were generated at last size, or other cases
-        if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || ( options::finiteModelFind() ? !d_datatype.isUFinite() : !d_datatype.isFinite() ) ){
+        if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite() ){
           d_size_limit++;
           d_ctor = d_zeroCtor;
           for( unsigned i=0; i<d_sel_sum.size(); i++ ){
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 9fb943e5e..5aff1a848 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,11 +48,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
       }else{
         int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isUFinite() ? 1 : -1;
+          score = dt.isInterpretedFinite() ? 1 : -1;
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
-          score = dt.isUFinite() ? 1 : -1;
+          score = dt.isInterpretedFinite() ? 1 : -1;
         }
-        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isUFinite() << " " << dt.isFinite() << ")" << std::endl;
+        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite() << " " << dt.isFinite() << ")" << std::endl;
         if( score>max_score ){
           max_index = i;
           max_score = score;
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;
-          }
         }
       }
     }
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index fa7e497e2..6889d1002 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -832,6 +832,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
           Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
           Node n;
           if (t.getCardinality().isInfinite()) {
+          // if (!t.isInterpretedFinite()) {
             bool success;
             do{
               Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl;
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 575aa4159..6e1c6e918 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -55,7 +55,8 @@ TESTS =	\
 	datatypes-ufinite-nested.smt2 \
 	ForElimination-scala-9.smt2 \
 	agree466.smt2 \
-	LeftistHeap.scala-8-ncm.smt2
+	LeftistHeap.scala-8-ncm.smt2 \
+	sc-crash-052316.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/sc-crash-052316.smt2 b/test/regress/regress0/fmf/sc-crash-052316.smt2
new file mode 100644
index 000000000..2fc86cbed
--- /dev/null
+++ b/test/regress/regress0/fmf/sc-crash-052316.smt2
@@ -0,0 +1,35 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+  (set-logic ALL_SUPPORTED)
+  (set-info :status unsat)
+  (declare-sort g_ 0)
+  (declare-fun __nun_card_witness_0_ () g_)
+  (declare-sort f_ 0)
+  (declare-fun __nun_card_witness_1_ () f_)
+  (declare-sort e_ 0)
+  (declare-fun __nun_card_witness_2_ () e_)
+(declare-datatypes ()
+ ((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_)))))
+  (declare-sort d_ 0)
+  (declare-fun __nun_card_witness_3_ () d_)
+  (declare-sort c_ 0)
+  (declare-fun __nun_card_witness_4_ () c_)
+  (declare-sort b_ 0)
+  (declare-fun __nun_card_witness_5_ () b_)
+  (declare-sort a_ 0)
+  (declare-fun __nun_card_witness_6_ () a_)
+(declare-datatypes ()
+ ((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_)))))
+  (declare-fun f1_ (prod_ c_ d_ prod1_) g_)
+  (declare-fun g1_ (prod_) c_)
+  (declare-fun h_ (prod_ d_) prod1_)
+  (declare-fun nun_sk_0_ () prod_)
+(declare-fun nun_sk_1_ (c_) d_)
+  (assert
+   (not
+    (exists ((v/72 c_))
+     (exists ((x/73 prod1_))
+      (= (f1_ nun_sk_0_ v/72 (nun_sk_1_ v/72) x/73)
+       (f1_ nun_sk_0_ (g1_ nun_sk_0_) (nun_sk_1_ v/72)
+        (h_ nun_sk_0_ (nun_sk_1_ v/72))))))))
+(check-sat)