Models for codatatypes. Fixes bug 662.

6 files changed, 118 insertions, 75 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8bdf38ca3..d872ab42c 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -757,7 +757,7 @@ void TheoryArrays::computeCareGraph()
 
       // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
       // Also, insert this read in the list at the proper index
-      
+
       if (!x_shared.isConst()) {
         x_shared = d_valuation.getModelValue(x_shared);
       }
@@ -1032,7 +1032,7 @@ void TheoryArrays::check(Effort e) {
   if (done() && !fullEffort(e)) {
     return;
   }
-  
+
   getOutputChannel().spendResource(options::theoryCheckStep());
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index f33c380d7..c342e488a 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -58,6 +58,13 @@ public:
           return RewriteResponse(REWRITE_DONE, inr);
         }
       }
+      if( in.isConst() ){
+        Node inn = normalizeConstant( in );
+        if( inn!=in ){
+          Trace("datatypes-rewrite-debug") << "Normalized constant " << in << " -> " << inn << std::endl;
+          return RewriteResponse(REWRITE_DONE, inn);
+        }
+      }
     }
 
     if(in.getKind() == kind::APPLY_TESTER) {
@@ -585,23 +592,27 @@ public:
   }
   //normalize constant : apply to top-level codatatype constants
   static Node normalizeConstant( Node n ){
-    Assert( n.getType().isDatatype() );
-    const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
-    if( dt.isCodatatype() ){
-      return normalizeCodatatypeConstant( n );
-    }else{
-      std::vector< Node > children;
-      bool childrenChanged = false;
-      for( unsigned i = 0; i<n.getNumChildren(); i++ ){
-        Node nc = normalizeConstant( n[i] );
-        children.push_back( nc );
-        childrenChanged = childrenChanged || nc!=n[i];
-      }
-      if( childrenChanged ){
-        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+    if( n.getType().isDatatype() ){
+      Assert( n.getType().isDatatype() );
+      const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+      if( dt.isCodatatype() ){
+        return normalizeCodatatypeConstant( n );
       }else{
-        return n;
+        std::vector< Node > children;
+        bool childrenChanged = false;
+        for( unsigned i = 0; i<n.getNumChildren(); i++ ){
+          Node nc = normalizeConstant( n[i] );
+          children.push_back( nc );
+          childrenChanged = childrenChanged || nc!=n[i];
+        }
+        if( childrenChanged ){
+          return NodeManager::currentNM()->mkNode( n.getKind(), children );
+        }else{
+          return n;
+        }
       }
+    }else{
+      return n;
     }
   }
 };/* class DatatypesRewriter */
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e0a4dc7d8..72717f974 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1277,26 +1277,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
         Node c = ei->d_constructor.get();
         cons.push_back( c );
         eqc_cons[ eqc ] = c;
-        Trace("dt-cmi") << "Datatypes : assert representative " << c << " for " << eqc << std::endl;
-        m->assertRepresentative( c );
       }else{
         //if eqc contains a symbol known to datatypes (a selector), then we must assign
-#if 0
-        bool shouldConsider = false;
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-        while( !eqc_i.isFinished() ){
-          Node n = *eqc_i;
-          Trace("dt-cmi-debug") << n << " has kind " << n.getKind() << ", isVar = " << n.isVar() << std::endl;
-          if( n.isVar() || n.getKind()==APPLY_SELECTOR_TOTAL ){
-            shouldConsider = true;
-            break;
-          }
-          ++eqc_i;
-        }
-#else
         //should assign constructors to EQC if they have a selector or a tester
         bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
-#endif
         if( shouldConsider ){
           nodes.push_back( eqc );
         }
@@ -1398,68 +1382,56 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
       Trace("dt-cmi") << "Assign : " << neqc << std::endl;
       m->assertEquality( eqc, neqc, true );
       eqc_cons[ eqc ] = neqc;
-      Trace("dt-cmi") << "Datatypes : assert representative " << neqc << " for " << eqc << std::endl;
-      m->assertRepresentative( neqc );
     }
-    //m->assertRepresentative( neqc );
     if( addCons ){
       cons.push_back( neqc );
     }
     ++index;
   }
 
-  //assign MU for each codatatype eqc
-  std::map< Node, Node > eqc_mu;
   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() ){
       //until models are implemented for codatatypes
-      throw Exception("Models for codatatypes are not supported in this version.");
-      /*
-      std::map< Node, Node > vmap;
-      std::vector< Node > fv;
-      Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap, fv );
-      Trace("dt-cmi-cdt") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
-      //m->assertEquality( eqc, v, true );
-      */
+      //throw Exception("Models for codatatypes are not supported in this version.");
+      //must proactive expand to avoid looping behavior in model builder
+      std::map< Node, int > vmap;
+      Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 );
+      Trace("dt-cmi") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
+      m->assertEquality( eqc, v, true );
+      m->assertRepresentative( v );
+    }else{
+      Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl;
+      m->assertRepresentative( it->second );
     }
   }
 }
 
 
-Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv ){
-  std::map< Node, Node >::iterator itv = vmap.find( n );
+Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){
+  std::map< Node, int >::iterator itv = vmap.find( n );
   if( itv!=vmap.end() ){
-    if( std::find( fv.begin(), fv.end(), itv->second )==fv.end() ){
-      fv.push_back( itv->second );
-    }
-    return itv->second;
+    int debruijn = depth - 1 - itv->second;
+    return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
   }else if( DatatypesRewriter::isTermDatatype( n ) ){
-    std::stringstream ss;
-    ss << "$x" << vmap.size();
-    Node nv = NodeManager::currentNM()->mkBoundVar( ss.str().c_str(), n.getType() );
-    vmap[n] = nv;
-    Trace("dt-cmi-cdt-debug") << "    map " << n << " -> " << nv << std::endl;
     Node nc = eqc_cons[n];
-    Assert( nc.getKind()==APPLY_CONSTRUCTOR );
-    std::vector< Node > children;
-    children.push_back( nc.getOperator() );
-    for( unsigned i=0; i<nc.getNumChildren(); i++ ){
-      Node r = getRepresentative( nc[i] );
-      Node rv = getCodatatypesValue( r, eqc_cons, eqc_mu, vmap, fv );
-      children.push_back( rv );
-    }
-    vmap.erase( n );
-    Node v = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-    //add mu if we found a circular reference
-    if( std::find( fv.begin(), fv.end(), nv )!=fv.end() ){
-      v = NodeManager::currentNM()->mkNode( MU, nv, v );
+    if( !nc.isNull() ){
+      vmap[n] = depth;
+      Trace("dt-cmi-cdt-debug") << "    map " << n << " -> " << depth << std::endl;
+      Assert( nc.getKind()==APPLY_CONSTRUCTOR );
+      std::vector< Node > children;
+      children.push_back( nc.getOperator() );
+      for( unsigned i=0; i<nc.getNumChildren(); i++ ){
+        Node r = getRepresentative( nc[i] );
+        Node rv = getCodatatypesValue( r, eqc_cons, vmap, depth+1 );
+        children.push_back( rv );
+      }
+      vmap.erase( n );
+      return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
     }
-    return v;
-  }else{
-    return n;
   }
+  return n;
 }
 
 Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index ab40f07db..a221153a3 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -266,7 +266,7 @@ private:
                           std::map< Node, Node >& cn,
                           std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp );
   /** build model */
-  Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap, std::vector< Node >& fv );
+  Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth );
   /** get singleton lemma */
   Node getSingletonLemma( TypeNode tn, bool pol );
   /** collect terms */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index cf0fbcbfe..5766a26c1 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -489,6 +489,46 @@ void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node
   }
 }
 
+bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
+  Trace("model-builder-cdt") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl;
+  for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i ) {
+    Assert(assertedReps.find(*i) != assertedReps.end());
+    Node rep = assertedReps[*i];
+    Trace("model-builder-cdt") << "  Rep : " << rep << std::endl;
+    //check matching val to rep with eqc as a free variable
+    Node eqc_m;
+    if( isCdtValueMatch( val, rep, eqc, eqc_m ) ){
+      Trace("model-builder-cdt") << "  ...matches with " << eqc << " -> " << eqc_m << std::endl;
+      Trace("model-builder-cdt") << "*** " << val << " is excluded datatype for " << eqc << std::endl;
+      return true;
+    }
+  }
+  return false;
+}
+
+bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ) {
+  if( r==v ){
+    return true;
+  }else if( r==eqc ){
+    if( eqc_m.isNull() ){
+      //only if an uninterpreted constant?
+      eqc_m = v;
+      return true;
+    }else{
+      return v==eqc_m;
+    }
+  }else if( v.getKind()==kind::APPLY_CONSTRUCTOR && r.getKind()==kind::APPLY_CONSTRUCTOR ){
+    if( v.getOperator()==r.getOperator() ){
+      for( unsigned i=0; i<v.getNumChildren(); i++ ){
+        if( !isCdtValueMatch( v[i], r[i], eqc, eqc_m ) ){
+          return false;
+        }
+      }
+      return true;
+    }
+  }
+  return false;
+}
 
 void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 {
@@ -699,6 +739,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       if(t.isTuple() || t.isRecord()) {
         t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
       }
+      bool isCorecursive = false;
+      if( t.isDatatype() ){
+        const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
+        isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
+      }
+      set<Node>* repSet = typeRepSet.getSet(t);
       TypeNode tb = t.getBaseType();
       if (!assignOne) {
         set<Node>* repSet = typeRepSet.getSet(tb);
@@ -731,7 +777,18 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
           Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
           Node n;
           if (t.getCardinality().isInfinite()) {
-            n = typeConstSet.nextTypeEnum(t, true);
+            bool success;
+            do{
+              n = typeConstSet.nextTypeEnum(t, true);
+              success = true;
+              if( isCorecursive ){
+                if (repSet != NULL && !repSet->empty()) {
+                  // in the case of codatatypes, check if it is in the set of values that we cannot assign
+                  // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015
+                  success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 );
+                }
+              }
+            }while( !success );
           }
           else {
             TypeEnumerator te(t);
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index a161f02f4..092b5e8c7 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -262,6 +262,9 @@ protected:
   bool isAssignable(TNode n);
   void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
   void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
+  /** is v an excluded codatatype value */
+  bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
+  bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
 public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder(){}