Minor refactoring and optimizing.

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 99245ef690e9d0fe3e3a74b88edbe54f25c32b89..e884248e75a3c9d5dcf423c9fdcb8065c0f44cab 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -248,6 +248,58 @@ public:
     }
     return false;
   }
+  /** get instantiate cons */
+  static Node getInstCons( Node n, const Datatype& dt, int index, bool mkVar = false ) {
+    Type tspec;
+    if( dt.isParametric() ){
+      tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
+    }
+    std::vector< Node > children;
+    children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
+    for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
+      Node nc = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n );
+      if( mkVar ){
+        TypeNode tn = nc.getType();
+        if( dt.isParametric() ){
+          tn = TypeNode::fromType( tspec )[i];
+        }
+        nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" );
+      }
+      children.push_back( nc );
+    }
+    Node n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+    //add type ascription for ambiguous constructor types
+    if(!n_ic.getType().isComparableTo(n.getType())) {
+      Assert( dt.isParametric() );
+      Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
+      Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
+      Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
+      Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl;
+      children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                                                     NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] );
+      n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+      Assert( n_ic.getType()==n.getType() );
+    }
+    Assert( isInstCons( n_ic, dt, index ) );
+    //n_ic = Rewriter::rewrite( n_ic );
+    return n_ic;
+  }
+  static bool isInstCons( Node n, const Datatype& dt, int index ){
+    if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
+      const DatatypeConstructor& c = dt[index];
+      if( n.getOperator()==Node::fromExpr( c.getConstructor() ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          if( n[i].getKind()!=kind::APPLY_SELECTOR_TOTAL ||
+              n[i].getOperator()!=Node::fromExpr( c[i].getSelector() ) ){
+            return false;
+          }
+        }
+        return true;
+      }
+    }
+    return false;
+  }
+
   /** is this term a datatype */
   static bool isTermDatatype( Node n ){
     TypeNode tn = n.getType();

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 4858d99dbf7e4c993b4a60b8d3c82736fc616231..8afcbb1de0995d7b276e939283d17c0a250edcf4 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1173,51 +1173,23 @@ void TheoryDatatypes::processNewTerm( Node n ){
 }
 
 Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){
-  //if( !d_inst_map[n][index].isNull() ){
-  //  return d_inst_map[n][index];
-  //}else{
+  std::map< int, Node >::iterator it = d_inst_map[n].find( index );
+  if( it!=d_inst_map[n].end() ){
+    return it->second;
+  }else{
     //add constructor to equivalence class
-    Type tspec;
-    if( dt.isParametric() ){
-      tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
-    }
-    std::vector< Node > children;
-    children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
-    for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
-      Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n );
-      if( mkVar ){
-        TypeNode tn = nc.getType();
-        if( dt.isParametric() ){
-          tn = TypeNode::fromType( tspec )[i];
-        }
-        nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created during model gen" );
-      }
-      children.push_back( nc );
-      if( isActive ){
-        processNewTerm( nc );
-      }
-    }
-    Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+    Node n_ic = DatatypesRewriter::getInstCons( n, dt, index, mkVar );
     if( isActive ){
+      for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){
+        processNewTerm( n_ic[i] );
+      }
       collectTerms( n_ic );
     }
-    //add type ascription for ambiguous constructor types
-    if(!n_ic.getType().isComparableTo(n.getType())) {
-      Assert( dt.isParametric() );
-      Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
-      Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
-      Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
-      Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl;
-      children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                     NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] );
-      n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-      Assert( n_ic.getType()==n.getType() );
-    }
     n_ic = Rewriter::rewrite( n_ic );
     Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
-    //d_inst_map[n][index] = n_ic;
+    d_inst_map[n][index] = n_ic;
     return n_ic;
-  //}
+  }
 }
 
 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
@@ -1238,7 +1210,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment()
     //instantiate this equivalence class
     eqc->d_inst = true;
-    Node tt_cons = getInstantiateCons( tt, dt, index );
+    Node tt_cons = getInstantiateCons( tt, dt, index, false, true );
     Node eq;
     if( tt!=tt_cons ){
       eq = tt.eqNode( tt_cons );

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index eb8d792cf94745612cf7c26bbefbe19b30681ed3..307e90e9160e1806dbb09da1f20a71d559446cb9 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -247,7 +247,7 @@ private:
   /** collect terms */
   void collectTerms( Node n );
   /** get instantiate cons */
-  Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true );
+  Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive );
   /** process new term that was created internally */
   void processNewTerm( Node n );
   /** check instantiate */