Partial support for codatatype models.

6 files changed, 90 insertions, 54 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 508106106..44474c18a 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -302,9 +302,6 @@ operator SEXPR 0: "a symbolic expression (any arity)"
 
 operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body"
 
-## for co-datatypes, not yet supported
-# operator MU 2 "mu"
-
 parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
 constant CHAIN_OP \
     ::CVC4::Chain \
@@ -336,7 +333,6 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
-#typerule MU ::CVC4::theory::builtin::MuTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 045f440e6..977a097d0 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -164,27 +164,6 @@ public:
   }
 };/* class LambdaTypeRule */
 
-/* For co-datatypes, not yet supported--
-**
-class MuTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    if( n[0].getType(check) != nodeManager->boundVarListType() ) {
-      std::stringstream ss;
-      ss << "expected a bound var list for MU expression, got `"
-         << n[0].getType().toString() << "'";
-      throw TypeCheckingExceptionPrivate(n, ss.str());
-    }
-    std::vector<TypeNode> argTypes;
-    for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) {
-      argTypes.push_back((*i).getType());
-    }
-    TypeNode rangeType = n[1].getType(check);
-    return nodeManager->mkFunctionType(argTypes, rangeType);
-  }
-};
-**/
-
 class ChainTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index d8b42111c..faaf78fe4 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -89,6 +89,12 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType
 # constructor applications are constant if they are applied only to constants
 construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 
+## for co-datatypes
+operator MU 2 "a mu operator, first argument is a bound variable, second argument is body"
+typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
+# mu applications are constant expressions
+construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
+
 operator TUPLE_TYPE 0: "tuple type"
 cardinality TUPLE_TYPE \
     "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d3f0dac9b..145cd32dd 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1321,32 +1321,44 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
     if( dt.isCodatatype() ){
       std::map< Node, Node > vmap;
-      Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap );
-      Trace("dt-cmi-cod") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << std::endl;
+      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 );
     }
   }
 }
 
 
-Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ){
+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 );
   if( itv!=vmap.end() ){
+    if( std::find( fv.begin(), fv.end(), itv->second )==fv.end() ){
+      fv.push_back( itv->second );
+    }
     return itv->second;
   }else if( DatatypesRewriter::isTermDatatype( n ) ){
-    Node nv = NodeManager::currentNM()->mkBoundVar( n.getType() );
+    std::stringstream ss;
+    ss << "$x" << vmap.size();
+    Node nv = NodeManager::currentNM()->mkBoundVar( ss.str().c_str(), n.getType() );
     vmap[n] = nv;
-    Trace("dt-cmi-cod-debug") << "    map " << n << " -> " << nv << std::endl;
+    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 );
+      Node rv = getCodatatypesValue( r, eqc_cons, eqc_mu, vmap, fv );
       children.push_back( rv );
     }
     vmap.erase( n );
-    return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+    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 );
+    }
+    return v;
   }else{
     return n;
   }
@@ -1464,7 +1476,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
 
 void TheoryDatatypes::checkCycles() {
   Debug("datatypes-cycle-check") << "Check cycles" << std::endl;
-  std::vector< Node > cod_eqc;
+  std::vector< Node > cdt_eqc;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
@@ -1495,30 +1507,30 @@ void TheoryDatatypes::checkCycles() {
         }
       }else{
         //indexing
-        cod_eqc.push_back( eqc );
+        cdt_eqc.push_back( eqc );
       }
     }
     ++eqcs_i;
   }
   //process codatatypes
-  if( cod_eqc.size()>1 && options::cdtBisimilar() ){
-    Trace("dt-cod-debug") << "Process " << cod_eqc.size() << " co-datatypes" << std::endl;
+  if( cdt_eqc.size()>1 && options::cdtBisimilar() ){
+    Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl;
     std::vector< std::vector< Node > > part_out;
     std::vector< TNode > exp;
     std::map< Node, Node > cn;
     std::map< Node, std::map< Node, int > > dni;
-    for( unsigned i=0; i<cod_eqc.size(); i++ ){
-      cn[cod_eqc[i]] = cod_eqc[i];
+    for( unsigned i=0; i<cdt_eqc.size(); i++ ){
+      cn[cdt_eqc[i]] = cdt_eqc[i];
     }
-    separateBisimilar( cod_eqc, part_out, exp, cn, dni, 0, false );
-    Trace("dt-cod-debug") << "Done separate bisimilar." << std::endl;
+    separateBisimilar( cdt_eqc, part_out, exp, cn, dni, 0, false );
+    Trace("dt-cdt-debug") << "Done separate bisimilar." << std::endl;
     if( !part_out.empty() ){
-      Trace("dt-cod-debug") << "Process partition size " << part_out.size() << std::endl;
+      Trace("dt-cdt-debug") << "Process partition size " << part_out.size() << std::endl;
       for( unsigned i=0; i<part_out.size(); i++ ){
         std::vector< Node > part;
         part.push_back( part_out[i][0] );
         for( unsigned j=1; j<part_out[i].size(); j++ ){
-          Trace("dt-cod") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl;
+          Trace("dt-cdt") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl;
           part.push_back( part_out[i][j] );
           std::vector< std::vector< Node > > tpart_out;
           exp.clear();
@@ -1530,16 +1542,16 @@ void TheoryDatatypes::checkCycles() {
           Assert( tpart_out.size()==1 && tpart_out[0].size()==2 );
           part.pop_back();
           //merge based on explanation
-          Trace("dt-cod") << "  exp is : ";
+          Trace("dt-cdt") << "  exp is : ";
           for( unsigned k=0; k<exp.size(); k++ ){
-            Trace("dt-cod") << exp[k] << " ";
+            Trace("dt-cdt") << exp[k] << " ";
           }
-          Trace("dt-cod") << std::endl;
+          Trace("dt-cdt") << std::endl;
           Node eq = part_out[i][0].eqNode( part_out[i][j] );
           Node eqExp = mkAnd( exp );
           d_pending.push_back( eq );
           d_pending_exp[ eq ] = eqExp;
-          Trace("datatypes-infer") << "DtInfer : cod-bisimilar : " << eq << " by " << eqExp << std::endl;
+          Trace("datatypes-infer") << "DtInfer : cdt-bisimilar : " << eq << " by " << eqExp << std::endl;
           d_infer.push_back( eq );
           d_infer_exp.push_back( eqExp );
         }
@@ -1554,9 +1566,9 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
                                          std::map< Node, Node >& cn,
                                          std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){
   if( !mkExp ){
-    Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl;
+    Trace("dt-cdt-debug") << "Separate bisimilar : " << std::endl;
     for( unsigned i=0; i<part.size(); i++ ){
-      Trace("dt-cod-debug") << "   " << part[i] << ", current = " << cn[part[i]] << std::endl;
+      Trace("dt-cdt-debug") << "   " << part[i] << ", current = " << cn[part[i]] << std::endl;
     }
   }
   Assert( part.size()>1 );
@@ -1570,7 +1582,7 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
     std::map< Node, int >::iterator it_rec = dni[part[j]].find( c );
     if( it_rec!=dni[part[j]].end() ){
       //looped
-      if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
+      if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
       new_part_rec[ it_rec->second ].push_back( part[j] );
     }else{
       if( DatatypesRewriter::isTermDatatype( c ) ){
@@ -1582,14 +1594,14 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
             explainEquality( c, ncons, true, exp );
           }
           new_part[cc].push_back( part[j] );
-          if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is datatype " << ncons << "." << std::endl; }
+          if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is datatype " << ncons << "." << std::endl; }
         }else{
           new_part_c[c].push_back( part[j] );
-          if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is unspecified datatype." << std::endl; }
+          if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is unspecified datatype." << std::endl; }
         }
       }else{
         //add equivalences
-        if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is term " << c << "." << std::endl; }
+        if( !mkExp ){ Trace("dt-cdt-debug") << "  - " << part[j] << " is term " << c << "." << std::endl; }
         new_part_c[c].push_back( part[j] );
       }
     }
@@ -1631,7 +1643,7 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
       //for each child of constructor
       unsigned cindex = 0;
       while( cindex<nChildren && !split_new_part.empty() ){
-        if( !mkExp ){ Trace("dt-cod-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; }
+        if( !mkExp ){ Trace("dt-cdt-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; }
         std::vector< std::vector< Node > > next_split_new_part;
         for( unsigned j=0; j<split_new_part.size(); j++ ){
           //set current node
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 3592dbe30..74d10e754 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -256,7 +256,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 );
+  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 );
   /** collect terms */
   void collectTerms( Node n );
   /** get instantiate cons */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index ddad913fe..8ce8ee7df 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -209,6 +209,49 @@ struct DatatypeAscriptionTypeRule {
   }
 };/* struct DatatypeAscriptionTypeRule */
 
+/* For co-datatypes */
+class DatatypeMuTypeRule {
+private:
+  //a Mu-expression is constant iff its body is composed of constructors applied to constant expr and bound variables only
+  inline static bool computeIsConstNode(TNode n, std::vector< TNode >& fv ){
+    if( n.getKind()==kind::MU ){
+      fv.push_back( n[0] );
+      bool ret = computeIsConstNode( n[1], fv );
+      fv.pop_back();
+      return ret;
+    }else if( n.isConst() || std::find( fv.begin(), fv.end(), n )!=fv.end() ){
+      return true;
+    }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( !computeIsConstNode( n[i], fv ) ){
+          return false;
+        }
+      }
+      return true; 
+    }else{
+      return false;
+    }
+  }
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    if( n[0].getKind()!=kind::BOUND_VARIABLE  ) {
+      std::stringstream ss;
+      ss << "expected a bound var for MU expression, got `"
+         << n[0] << "'";
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+    return n[1].getType(check);
+  }
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
+    throw(AssertionException) {
+    Assert(n.getKind() == kind::MU);
+    NodeManagerScope nms(nodeManager);
+    std::vector< TNode > fv;
+    return computeIsConstNode( n, fv );
+  }
+};
+
+
 struct ConstructorProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
     // Constructors aren't exactly functions, they're like