Minor cleanup related to codatatypes.

7 files changed, 54 insertions, 48 deletions

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 4f9e497ea..0f5e020d8 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -582,6 +582,9 @@ public:
   /** Is this a parameterized datatype type */
   bool isParametricDatatype() const;
 
+  /** Is this a codatatype type */
+  bool isCodatatype() const;
+
   /** Is this a fully instantiated datatype type */
   bool isInstantiatedDatatype() const;
 
@@ -985,6 +988,15 @@ inline bool TypeNode::isParametricDatatype() const {
     ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() );
 }
 
+/** Is this a codatatype type */
+inline bool TypeNode::isCodatatype() const {
+  if( isDatatype() ){
+    return getDatatype().isCodatatype();
+  }else{
+    return false;
+  }
+}
+
 /** Is this a constructor type */
 inline bool TypeNode::isConstructor() const {
   return getKind() == kind::CONSTRUCTOR_TYPE;
@@ -1004,7 +1016,7 @@ inline bool TypeNode::isTester() const {
     and <code>sig</code> significand bits */
 inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
   return
-    ( getKind() == kind::FLOATINGPOINT_TYPE && 
+    ( getKind() == kind::FLOATINGPOINT_TYPE &&
       getConst<FloatingPointSize>().exponent() == exp &&
       getConst<FloatingPointSize>().significand() == sig ) ||
     ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) );
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index c342e488a..4b60044d0 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -60,8 +60,9 @@ public:
       }
       if( in.isConst() ){
         Node inn = normalizeConstant( in );
+        Assert( !inn.isNull() );
         if( inn!=in ){
-          Trace("datatypes-rewrite-debug") << "Normalized constant " << in << " -> " << inn << std::endl;
+          Trace("datatypes-rewrite") << "Normalized constant " << in << " -> " << inn << std::endl;
           return RewriteResponse(REWRITE_DONE, inn);
         }
       }
@@ -399,8 +400,7 @@ private:
     Node ret = n;
     bool isCdt = false;
     if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      if( !dt.isCodatatype() ){
+      if( !tn.isCodatatype() ){
         //nested datatype within codatatype : can be normalized independently since all loops should be self-contained
         ret = normalizeConstant( n );
       }else{
@@ -592,10 +592,9 @@ public:
   }
   //normalize constant : apply to top-level codatatype constants
   static Node normalizeConstant( Node n ){
-    if( n.getType().isDatatype() ){
-      Assert( n.getType().isDatatype() );
-      const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
-      if( dt.isCodatatype() ){
+    TypeNode tn = n.getType();
+    if( tn.isDatatype() ){
+      if( tn.isCodatatype() ){
         return normalizeCodatatypeConstant( n );
       }else{
         std::vector< Node > children;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 72717f974..af8e5c503 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -190,6 +190,7 @@ void TheoryDatatypes::check(Effort e) {
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
             bool continueProc = true;
             if( dt.isRecursiveSingleton() ){
+              Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
               //handle recursive singleton case
               std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
               if( itrs!=rec_singletons.end() ){
@@ -230,6 +231,7 @@ void TheoryDatatypes::check(Effort e) {
               continueProc = ( getQuantifiersEngine()!=NULL );
             }
             if( continueProc ){
+              Trace("datatypes-debug") << "Get possible cons..." << std::endl;
               //all other cases
               std::vector< bool > pcons;
               getPossibleCons( eqc, n, pcons );
@@ -237,32 +239,30 @@ void TheoryDatatypes::check(Effort e) {
               // this is if there are no selectors for this equivalence class, its possible values are infinite,
               //  and we are not producing a model, then do not split.
               int consIndex = -1;
+              int fconsIndex = -1;
               bool needSplit = true;
               for( unsigned int j=0; j<pcons.size(); j++ ) {
                 if( pcons[j] ) {
                   if( consIndex==-1 ){
                     consIndex = j;
                   }
-                  if( !dt[ j ].isFinite() && ( !eqc || !eqc->d_selectors ) ) {
-                    needSplit = false;
+                  if( !dt[ j ].isFinite() ) {
+                    if( !eqc || !eqc->d_selectors ){
+                      needSplit = false;
+                    }
+                  }else{
+                    if( fconsIndex==-1 ){
+                      fconsIndex = j;
+                    }
                   }
                 }
               }
+              //if we want to force an assignment of constructors to all ground eqc
               //d_dtfCounter++;
               if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
-                //for the sake of termination, we must choose the constructor of a ground term
-                //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
-                // TODO: this is probably not good enough, actually need fair enumeration strategy
-                if( !n.getType().isRecord() ){ //FIXME
-                  Node groundTerm = n.getType().mkGroundTerm();
-                  if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME
-                    int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
-                    if( pcons[index] ){
-                      consIndex = index;
-                    }
-                    needSplit = true;
-                  }
-                }
+                Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl;
+                needSplit = true;
+                consIndex = fconsIndex!=-1 ? fconsIndex : consIndex;
               }
 
               if( needSplit && consIndex!=-1 ) {
@@ -1391,8 +1391,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
 
   for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){
     Node eqc = it->first;
-    const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
-    if( dt.isCodatatype() ){
+    if( eqc.getType().isCodatatype() ){
       //until models are implemented for codatatypes
       //throw Exception("Models for codatatypes are not supported in this version.");
       //must proactive expand to avoid looping behavior in model builder
@@ -1583,7 +1582,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     int index = getLabelIndex( eqc, n );
     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
     //must be finite or have a selector
-    //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment()
+    //if( eqc->d_selectors || dt[ index ].isFinite() ){
     //instantiate this equivalence class
     eqc->d_inst = true;
     Node tt_cons = getInstantiateCons( tt, dt, index );
@@ -1613,8 +1612,7 @@ void TheoryDatatypes::checkCycles() {
     Node eqc = (*eqcs_i);
     TypeNode tn = eqc.getType();
     if( DatatypesRewriter::isTypeDatatype( tn ) ) {
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      if( !dt.isCodatatype() ){
+      if( !tn.isCodatatype() ){
         if( options::dtCyclic() ){
           //do cycle checks
           std::map< TNode, bool > visited;
@@ -1846,8 +1844,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
   }else{
     TypeNode tn = nn.getType();
     if( DatatypesRewriter::isTypeDatatype( tn ) ) {
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      if( !dt.isCodatatype() ){
+      if( !tn.isCodatatype() ){
         return nn;
       }
     }
@@ -1855,15 +1852,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
   }
 }
 
-bool TheoryDatatypes::mustSpecifyAssignment(){
-  //FIXME: the condition finiteModelFind is an over-approximation in this function
-  //   we still may not want to specify assignments for datatypes that are truly infinite
-  //   the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
-  return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
-  //return options::produceModels();
-  //return false;
-}
-
 bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   //the datatypes decision procedure makes "internal" inferences apart from the equality engine :
   //  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index a221153a3..b452e02d1 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -277,11 +277,6 @@ private:
   void processNewTerm( Node n );
   /** check instantiate */
   void instantiate( EqcInfo* eqc, Node n );
-  /** must specify model
-    *  This returns true when the datatypes theory is expected to specify the constructor
-    *  type for all equivalence classes.
-    */
-  bool mustSpecifyAssignment();
   /** must communicate fact */
   bool mustCommunicateFact( Node n, Node exp );
   /** check clash mod eq */
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index da3c0cce0..3cf603100 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1044,8 +1044,15 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
 void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
   if( n.getNumChildren()>0 ){
     std::vector< int > vec;
+    std::vector< TypeNode > types;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       vec.push_back( 0 );
+      TypeNode tn = n[i].getType();
+      if( TermDb::isClosedEnumerableType( tn ) ){
+        types.push_back( tn );
+      }else{
+        return;
+      }
     }
     vec.pop_back();
     int size_limit = 0;
@@ -1059,7 +1066,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
         vec.push_back( size_limit );
       }else{
         //see if we can iterate current
-        if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( n[index].getType(), vec[index]+1 ).isNull() ){
+        if( vec_sum<size_limit && !getTermDatabase()->getEnumerateTerm( types[index], vec[index]+1 ).isNull() ){
           vec[index]++;
           vec_sum++;
           vec.push_back( size_limit - vec_sum );
@@ -1074,7 +1081,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
       }
       if( success ){
         if( vec.size()==n.getNumChildren() ){
-          Node lc = getTermDatabase()->getEnumerateTerm( n[vec.size()-1].getType(), vec[vec.size()-1] );
+          Node lc = getTermDatabase()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] );
           if( !lc.isNull() ){
             for( unsigned i=0; i<vec.size(); i++ ){
               Trace("sg-gt-enum-debug") << vec[i] << " ";
@@ -1087,7 +1094,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
             std::vector< Node > children;
             children.push_back( n.getOperator() );
             for( unsigned i=0; i<(vec.size()-1); i++ ){
-              Node nn = getTermDatabase()->getEnumerateTerm( n[i].getType(), vec[i] );
+              Node nn = getTermDatabase()->getEnumerateTerm( types[i], vec[i] );
               Assert( !nn.isNull() );
               Assert( nn.getType()==n[i].getType() );
               children.push_back( nn );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9985d3cdb..d076c6510 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -594,7 +594,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     Node mbt;
     if( tn.isInteger() || tn.isReal() ){
       mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-    }else if( !tn.isArray() && !tn.isSort() ){
+    }else if( isClosedEnumerableType( tn ) ){
       mbt = tn.mkGroundTerm();
     }else{
       if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
@@ -963,6 +963,9 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
   return d_enum_terms[tn][index];
 }
 
+bool TermDb::isClosedEnumerableType( TypeNode tn ) {
+  return !tn.isArray() && !tn.isSort() && !tn.isCodatatype();
+}
 
 Node TermDb::getFreeVariableForInstConstant( Node n ){
   return getFreeVariableForType( n.getType() );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 136d77268..fb80cb8a8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -282,6 +282,8 @@ private:
 public:
   //get nth term for type
   Node getEnumerateTerm( TypeNode tn, unsigned index );
+  //does this type have an enumerator that produces constants that are handled by ground theory solvers
+  static bool isClosedEnumerableType( TypeNode tn );
 
 //miscellaneous
 public: