From 8e0fce94790249ff7aff84ff4500bb96e2ebb9e9 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Nov 2016 13:20:49 -0500
Subject: Working memory leak free version, changes interface to pointers.

---
 src/compat/cvc3_compat.cpp         |  9 +++---
 src/expr/datatype.cpp              |  4 +++
 src/expr/datatype.h                |  9 ++++--
 src/expr/datatype.i                | 14 +++++++++
 src/expr/expr.i                    |  2 +-
 src/expr/expr_manager.i            |  2 +-
 src/expr/expr_manager_template.cpp | 64 ++++++++++++++++++++++----------------
 src/expr/expr_manager_template.h   | 12 +++----
 src/expr/node_manager.cpp          | 28 ++++++++++++-----
 src/expr/node_manager.h            |  7 ++++-
 src/expr/type.cpp                  |  2 +-
 src/expr/type_node.h               |  4 ++-
 src/parser/cvc/Cvc.g               | 14 +++++----
 src/parser/parser.cpp              |  8 ++---
 src/parser/parser.h                |  3 +-
 src/parser/smt2/Smt2.g             | 29 +++++++++--------
 src/parser/smt2/smt2.cpp           | 60 +++++++++++++++++------------------
 src/parser/smt2/smt2.h             | 18 +++++------
 src/printer/cvc/cvc_printer.cpp    | 18 ++++++-----
 src/printer/smt2/smt2_printer.cpp  |  5 ++-
 src/smt/boolean_terms.cpp          | 20 ++++++------
 src/smt/smt_engine.cpp             |  3 ++
 src/theory/datatypes/kinds         |  6 ++--
 23 files changed, 201 insertions(+), 140 deletions(-)

(limited to 'src')

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 8c9992164..0482c99ee 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1384,11 +1384,11 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
   CompatCheckArgument(names.size() == types.size(), types,
                       "Expected names and types vectors to be of equal "
                       "length.");
-  vector<CVC4::Datatype> dv;
+  vector<CVC4::Datatype*> dv;
 
   // Set up the datatype specifications.
   for(unsigned i = 0; i < names.size(); ++i) {
-    CVC4::Datatype dt(names[i], false);
+    CVC4::Datatype* dt = new CVC4::Datatype(names[i], false);
     CompatCheckArgument(constructors[i].size() == selectors[i].size(),
                         "Expected sub-vectors in constructors and selectors "
                         "vectors to match in size.");
@@ -1409,13 +1409,14 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
           ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k]));
         }
       }
-      dt.addConstructor(ctor);
+      dt->addConstructor(ctor);
     }
     dv.push_back(dt);
   }
 
   // Make the datatypes.
-  vector<CVC4::DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dv);
+  vector<CVC4::DatatypeType> dtts; 
+  d_em->mkMutualDatatypeTypes(dv, dtts);
 
   // Post-process to register the names of everything with this validity checker.
   // This is necessary for the compatibility layer because cons/sel operations are
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index a7039110f..26ab2f2da 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -52,6 +52,7 @@ typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAtt
 typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
 
 Datatype::~Datatype(){
+  Trace("ajr-temp") << "delete datatype " << getName() << " " << this << std::endl;
   delete d_record;
 }
 
@@ -1109,5 +1110,8 @@ DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgume
 
 }
 
+std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
+  return out << "index_" << dic.getIndex();
+}
 
 }/* CVC4 namespace */
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 06735262d..f81d2358d 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -28,7 +28,8 @@
 namespace CVC4 {
   // messy; Expr needs Datatype (because it's the payload of a
   // CONSTANT-kinded expression), and Datatype needs Expr.
-  class CVC4_PUBLIC Datatype;
+  //class CVC4_PUBLIC Datatype;
+  class CVC4_PUBLIC DatatypeIndexConstant;
 }/* CVC4 namespace */
 
 #include "base/exception.h"
@@ -792,9 +793,11 @@ private:
   const unsigned d_index;
 };/* class DatatypeIndexConstant */
 
+std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) CVC4_PUBLIC;
+
 struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
-  inline size_t operator()(const DatatypeIndexConstant& uc) const {
-    return IntegerHashFunction()(uc.getIndex());
+  inline size_t operator()(const DatatypeIndexConstant& dic) const {
+    return IntegerHashFunction()(dic.getIndex());
   }
 };/* struct DatatypeIndexConstantHashFunction */
 
diff --git a/src/expr/datatype.i b/src/expr/datatype.i
index a7456df38..a903e0241 100644
--- a/src/expr/datatype.i
+++ b/src/expr/datatype.i
@@ -75,6 +75,20 @@
 %feature("valuewrapper") CVC4::DatatypeUnresolvedType;
 %feature("valuewrapper") CVC4::DatatypeConstructor;
 
+
+%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const;
+%ignore CVC4::DatatypeIndexConstant::operator!=(const DatatypeIndexConstant&) const;
+
+%rename(less) CVC4::DatatypeIndexConstant::operator<(const DatatypeIndexConstant&) const;
+%rename(lessEqual) CVC4::DatatypeIndexConstant::operator<=(const DatatypeIndexConstant&) const;
+%rename(greater) CVC4::DatatypeIndexConstant::operator>(const DatatypeIndexConstant&) const;
+%rename(greaterEqual) CVC4::DatatypeIndexConstant::operator>=(const DatatypeIndexConstant&) const;
+
+%rename(apply) CVC4::DatatypeIndexConstantFunction::operator()(const DatatypeIndexConstant&) const;
+
+%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es);
+
+
 #ifdef SWIGJAVA
 
 // Instead of Datatype::begin() and end(), create an
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 354cacdc0..49cb24321 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -150,7 +150,7 @@ namespace CVC4 {
 %template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>;
 %template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>;
 %template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>;
-%template(getConstDatatype) CVC4::Expr::getConst<CVC4::Datatype>;
+%template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>;
 %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>;
 %template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>;
 %template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 11c1e284d..f8bb55523 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -65,7 +65,7 @@
 //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6d8497a60..525f8ead3 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -645,46 +645,52 @@ SetType ExprManager::mkSetType(Type elementType) const {
   return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
 }
 
-DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+DatatypeType ExprManager::mkDatatypeType(Datatype*& datatype) {
   // Not worth a special implementation; this doesn't need to be fast
   // code anyway.
-  vector<Datatype> datatypes;
+  vector<Datatype*> datatypes;
   datatypes.push_back(datatype);
-  vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
+  std::vector<DatatypeType> result;
+  mkMutualDatatypeTypes(datatypes, result);
   Assert(result.size() == 1);
   return result.front();
 }
 
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
-  return mkMutualDatatypeTypes(datatypes, set<Type>());
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) {
+  std::set<Type> unresolvedTypes;
+  return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts);
 }
 
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
-                                   const std::set<Type>& unresolvedTypes) {
+void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) {
   NodeManagerScope nms(d_nodeManager);
   std::map<std::string, DatatypeType> nameResolutions;
-  std::vector<DatatypeType> dtts;
 
+  Trace("ajr-temp") << "Build datatypes..." << std::endl;
+  //std::vector< Datatype* > dt_copies;
+  //for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
+  //  dt_copies.push_back( new Datatype( **i ) );
+  //}
+  
+  
   // First do some sanity checks, set up the final Type to be used for
   // each datatype, and set up the "named resolutions" used to handle
   // simple self- and mutual-recursion, for example in the definition
   // "nat = succ(pred:nat) | zero", a named resolution can handle the
   // pred selector.
-  for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
-        i_end = datatypes.end();
-      i != i_end;
-      ++i) {
+  for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
     TypeNode* typeNode;
-    if( (*i).getNumParameters() == 0 ) {
-      typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+    if( (*i)->getNumParameters() == 0 ) {
+      unsigned index = d_nodeManager->registerDatatype( *i );
+      typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)));
+      //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
     } else {
-      TypeNode cons = d_nodeManager->mkTypeConst(*i);
+      unsigned index = d_nodeManager->registerDatatype( *i );
+      TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index));
+      //TypeNode cons = d_nodeManager->mkTypeConst(*i);
       std::vector< TypeNode > params;
       params.push_back( cons );
-      for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
-        params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
+      for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) {
+        params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) );
       }
 
       typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
@@ -692,15 +698,19 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     Type type(d_nodeManager, typeNode);
     DatatypeType dtt(type);
     PrettyCheckArgument(
-        nameResolutions.find((*i).getName()) == nameResolutions.end(),
+        nameResolutions.find((*i)->getName()) == nameResolutions.end(),
         datatypes,
         "cannot construct two datatypes at the same time "
         "with the same name `%s'",
-        (*i).getName().c_str());
-    nameResolutions.insert(std::make_pair((*i).getName(), dtt));
+        (*i)->getName().c_str());
+    nameResolutions.insert(std::make_pair((*i)->getName(), dtt));
     dtts.push_back(dtt);
+    //d_keep_dtt.push_back(dtt);
+    //d_keep_dt.push_back(*i);
+    //Assert( dtt.getDatatype()==(*i) );
   }
 
+  Trace("ajr-temp") << "Set up map..." << std::endl;
   // Second, set up the type substitution map for complex type
   // resolution (e.g. if "list" is the type we're defining, and it has
   // a selector of type "ARRAY INT OF list", this can't be taken care
@@ -714,10 +724,7 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
   std::vector< DatatypeType > paramReplacements;
   std::vector<Type> placeholders;// to hold the "unresolved placeholders"
   std::vector<Type> replacements;// to hold our final, resolved types
-  for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
-        i_end = unresolvedTypes.end();
-      i != i_end;
-      ++i) {
+  for(std::set<Type>::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) {
     std::string name;
     if( (*i).isSort() ) {
       name = SortType(*i).getName();
@@ -746,12 +753,14 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     }
   }
 
+  Trace("ajr-temp") << "Resolve..." << std::endl;
   // Lastly, perform the final resolutions and checks.
   for(std::vector<DatatypeType>::iterator i = dtts.begin(),
         i_end = dtts.end();
       i != i_end;
       ++i) {
     const Datatype& dt = (*i).getDatatype();
+    Trace("ajr-temp") << "Resolve " << dt.getName() << std::endl;
     if(!dt.isResolved()) {
       const_cast<Datatype&>(dt).resolve(this, nameResolutions,
                                         placeholders, replacements,
@@ -763,11 +772,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     checkResolvedDatatype(*i);
   }
 
+  Trace("ajr-temp") << "Notify..." << std::endl;
   for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
     (*i)->nmNotifyNewDatatypes(dtts);
   }
 
-  return dtts;
+  Trace("ajr-temp") << "Finish..." << std::endl;
 }
 
 void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 95b9c60bf..3f29396a3 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -87,6 +87,9 @@ private:
   ExprManager(const ExprManager&) CVC4_UNDEFINED;
   ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
 
+  std::vector<DatatypeType> d_keep_dtt;
+  std::vector<Datatype> d_keep_dt;
+
 public:
 
   /**
@@ -371,14 +374,13 @@ public:
   SetType mkSetType(Type elementType) const;
 
   /** Make a type representing the given datatype. */
-  DatatypeType mkDatatypeType(const Datatype& datatype);
+  DatatypeType mkDatatypeType(Datatype*& datatype);
 
   /**
    * Make a set of types representing the given datatypes, which may be
    * mutually recursive.
    */
-  std::vector<DatatypeType>
-  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+  void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts);
 
   /**
    * Make a set of types representing the given datatypes, which may
@@ -409,9 +411,7 @@ public:
    * then no complicated Type needs to be created, and the above,
    * simpler form of mkMutualDatatypeTypes() is enough.
    */
-  std::vector<DatatypeType>
-  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
-                        const std::set<Type>& unresolvedTypes);
+  void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts);
 
   /**
    * Make a type representing a constructor with the given parameterization.
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index af4f89da1..af0b1a2d0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -172,9 +172,11 @@ NodeManager::~NodeManager() {
   
   d_unique_vars.clear();
 
-  //d_tupleAndRecordTypes.clear();
+  TypeNode dummy;
   d_tt_cache.d_children.clear();
+  d_tt_cache.d_data = dummy;
   d_rt_cache.d_children.clear();
+  d_rt_cache.d_data = dummy;
 
   for( std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(),	datatype_end = d_ownedDatatypes.end(); 
        datatype_iter != datatype_end; ++datatype_iter) {
@@ -217,6 +219,18 @@ NodeManager::~NodeManager() {
   d_options = NULL;
 }
 
+unsigned NodeManager::registerDatatype(Datatype* dt) {
+  Trace("ajr-temp") << "Register datatype : " << dt->getName() << " " << dt << std::endl;
+  unsigned sz = d_ownedDatatypes.size();
+  d_ownedDatatypes.push_back( dt );
+  return sz;
+}
+
+const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{
+  Assert( index<d_ownedDatatypes.size() );
+  return *d_ownedDatatypes[index];
+}
+
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
   Assert(!d_attrManager->inGarbageCollection());
@@ -475,15 +489,15 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
 TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
   if( index==types.size() ){
     if( d_data.isNull() ){
-      Datatype dt("__cvc4_tuple");
-      dt.setTuple();
+      Datatype* dt = new Datatype("__cvc4_tuple");
+      dt->setTuple();
       DatatypeConstructor c("__cvc4_tuple_ctor");
       for (unsigned i = 0; i < types.size(); ++ i) {
         std::stringstream ss;
         ss << "__cvc4_tuple_stor_" << i;
         c.addArg(ss.str().c_str(), types[i].toType());
       }
-      dt.addConstructor(c);
+      dt->addConstructor(c);
       d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
@@ -497,13 +511,13 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
   if( index==rec.getNumFields() ){
     if( d_data.isNull() ){
       const Record::FieldVector& fields = rec.getFields();
-      Datatype dt("__cvc4_record");
-      dt.setRecord();
+      Datatype* dt = new Datatype("__cvc4_record");
+      dt->setRecord();
       DatatypeConstructor c("__cvc4_record_ctor");
       for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
         c.addArg((*i).first, (*i).second);
       }
-      dt.addConstructor(c);
+      dt->addConstructor(c);
       d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
       Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
     }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index aa78c9627..9342a02c4 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -84,7 +84,7 @@ class NodeManager {
   friend Expr ExprManager::mkVar(Type, uint32_t flags);
 
   // friend so it can access NodeManager's d_listeners and notify clients
-  friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
+  friend void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>&, std::set<Type>&, std::vector<DatatypeType>&);
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
@@ -380,6 +380,11 @@ public:
     Assert(elt != d_listeners.end(), "listener not subscribed");
     d_listeners.erase(elt);
   }
+  
+  /** register datatype */
+  unsigned registerDatatype(Datatype* dt);
+  /** get datatype for index */
+  const Datatype & getDatatypeForIndex( unsigned index ) const;
 
   /** Get a Kind from an operator expression */
   static inline Kind operatorToKind(TNode n);
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 18157016f..11a45db79 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -608,7 +608,7 @@ std::vector<Type> DatatypeType::getParamTypes() const {
 
 DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
   NodeManagerScope nms(d_nodeManager);
-  TypeNode cons = d_nodeManager->mkTypeConst( getDatatype() );
+  TypeNode cons = d_nodeManager->mkTypeConst( (*d_typeNode)[0].getConst<DatatypeIndexConstant>() );
   vector<TypeNode> paramsNodes;
   paramsNodes.push_back( cons );
   for(vector<Type>::const_iterator i = params.begin(),
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0cada0df2..9fffbdeb2 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1023,7 +1023,9 @@ inline bool TypeNode::isBitVector(unsigned size) const {
 /** Get the datatype specification from a datatype type */
 inline const Datatype& TypeNode::getDatatype() const {
   Assert(isDatatype());
-  return getConst<Datatype>();
+  //return getConst<Datatype>();
+  DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
+  return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
 }
 
 /** Get the exponent size of this floating-point type */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index e6d7f9d86..7ca6beb60 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -708,7 +708,7 @@ mainCommand[CVC4::Command*& cmd]
   SExpr sexpr;
   std::string id;
   Type t;
-  std::vector<CVC4::Datatype> dts;
+  std::vector<CVC4::Datatype*> dts;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
   std::string s;
 }
@@ -769,7 +769,9 @@ mainCommand[CVC4::Command*& cmd]
     ( COMMA datatypeDef[dts] )*
     END_TOK
     { PARSER_STATE->popScope();
-      cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+      std::vector<DatatypeType> dtts;
+      PARSER_STATE->mkMutualDatatypeTypes(dts, dtts);
+      cmd = new DatatypeDeclarationCommand(dtts); }
 
   | CONTEXT_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
@@ -2173,7 +2175,7 @@ iteElseTerm[CVC4::Expr& f]
 /**
  * Parses a datatype definition
  */
-datatypeDef[std::vector<CVC4::Datatype>& datatypes]
+datatypeDef[std::vector<CVC4::Datatype*>& datatypes]
 @init {
   std::string id, id2;
   Type t;
@@ -2193,7 +2195,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
         params.push_back( t ); }
       )* RBRACKET
     )?
-    { datatypes.push_back(Datatype(id, params, false));
+    { datatypes.push_back(new Datatype(id, params, false));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
@@ -2207,7 +2209,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 /**
  * Parses a constructor defintion for type
  */
-constructorDef[CVC4::Datatype& type]
+constructorDef[CVC4::Datatype*& type]
 @init {
   std::string id;
   CVC4::DatatypeConstructor* ctor = NULL;
@@ -2225,7 +2227,7 @@ constructorDef[CVC4::Datatype& type]
       RPAREN
     )?
     { // make the constructor
-      type.addConstructor(*ctor);
+      type->addConstructor(*ctor);
       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
       delete ctor;
     }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 712494805..e46c13140 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -303,12 +303,10 @@ bool Parser::isUnresolvedType(const std::string& name) {
   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 }
 
-std::vector<DatatypeType>
-Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+void Parser::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& types) {
 
   try {
-    std::vector<DatatypeType> types =
-      d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+    d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved, types);
 
     assert(datatypes.size() == types.size());
 
@@ -373,8 +371,6 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
         throw ParserException(dt.getName() + " is not well-founded");
       }
     }
-    
-    return types;
   } catch(IllegalArgumentException& ie) {
     throw ParserException(ie.getMessage());
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 54f25ae74..52f8dcb86 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -501,8 +501,7 @@ public:
   /**
    * Create sorts of mutually-recursive datatypes.
    */
-  std::vector<DatatypeType>
-  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+  void mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts);
 
   /**
    * Add an operator to the current legal set.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f88b30212..0fbd454b4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -512,7 +512,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   SExpr sexpr;
   CommandSequence* seq;
   std::vector< std::vector< CVC4::SygusGTerm > > sgts;
-  std::vector< CVC4::Datatype > datatypes;
+  std::vector< CVC4::Datatype* > datatypes;
   std::vector< std::vector<Expr> > ops;
   std::vector< std::vector< std::string > > cnames;
   std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
@@ -621,14 +621,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         //swap index if necessary
         Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl;
         for( unsigned i=0; i<datatypes.size(); i++ ){
-          Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl;
+          Debug("parser-sygus") << "..." << datatypes[i]->getName() << " has builtin sort " << sorts[i] << std::endl;
         }
         for( unsigned i=0; i<datatypes.size(); i++ ){
-          Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl;
+          Debug("parser-sygus") << "...make " << datatypes[i]->getName() << " with builtin sort " << sorts[i] << std::endl;
           if( sorts[i].isNull() ){
             PARSER_STATE->parseError(std::string("Internal error : could not infer builtin sort for nested gterm."));
           }
-          datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false );
+          datatypes[i]->setSygus( sorts[i], terms[0], allow_const[i], false );
           PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin );
         }
         PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops );
@@ -637,10 +637,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       PARSER_STATE->popScope();
       Debug("parser-sygus") << "--- Make " << datatypes.size() << " mutual datatypes..." << std::endl;
       for( unsigned i=0; i<datatypes.size(); i++ ){
-        Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName() << std::endl;
+        Debug("parser-sygus") << "  " << i << " : " << datatypes[i]->getName() << std::endl;
       }
       seq = new CommandSequence();
-      std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+      std::vector<DatatypeType> datatypeTypes; 
+      PARSER_STATE->mkMutualDatatypeTypes(datatypes, datatypeTypes);
       seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
       std::map<DatatypeType, Expr> evals;
       if( sorts[0]!=range ){
@@ -1168,7 +1169,7 @@ smt25Command[CVC4::Command*& cmd]
 
 extendedCommand[CVC4::Command*& cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<CVC4::Datatype*> dts;
   Expr e, e2;
   Type t;
   std::string name;
@@ -1324,7 +1325,8 @@ extendedCommand[CVC4::Command*& cmd]
 
 datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<CVC4::Datatype*> dts;
+  std::vector<CVC4::DatatypeType> dtts;
   std::string name;
   std::vector<Type> sorts;
 }
@@ -1338,7 +1340,8 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
   RPAREN_TOK
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
-    cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+    PARSER_STATE->mkMutualDatatypeTypes(dts, dtts);
+    cmd = new DatatypeDeclarationCommand(dtts); }
   ;
 
 rewriterulesCommand[CVC4::Command*& cmd]
@@ -2472,7 +2475,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals]
 /**
  * Parses a datatype definition
  */
-datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params]
+datatypeDef[bool isCo, std::vector<CVC4::Datatype*>& datatypes, std::vector< CVC4::Type >& params]
 @init {
   std::string id;
 }
@@ -2490,7 +2493,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4
         params.push_back( t ); }
       )* ']'
     )?*/ //AJR: this isn't necessary if we use z3's style
-    { datatypes.push_back(Datatype(id,params,isCo));
+    { datatypes.push_back(new Datatype(id,params,isCo));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
@@ -2503,7 +2506,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4
 /**
  * Parses a constructor defintion for type
  */
-constructorDef[CVC4::Datatype& type]
+constructorDef[CVC4::Datatype*& type]
 @init {
   std::string id;
   CVC4::DatatypeConstructor* ctor = NULL;
@@ -2517,7 +2520,7 @@ constructorDef[CVC4::Datatype& type]
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
-      type.addConstructor(*ctor);
+      type->addConstructor(*ctor);
       Debug("parser-idt") << "constructor: " << id.c_str() << std::endl;
       delete ctor;
     }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8db344f92..dd48ceca7 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -563,7 +563,7 @@ void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::m
   }
 }
 
-void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
+void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector< CVC4::Datatype* >& datatypes,
                                   std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
 
   //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
@@ -594,7 +594,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
     std::stringstream ss;
     ss << fun << "_" << types[i];
     std::string dname = ss.str();
-    datatypes.push_back(Datatype(dname));
+    datatypes.push_back(new Datatype(dname));
     ops.push_back(std::vector<Expr>());
     //make unresolved type
     Type unres_t = mkUnresolvedType(dname);
@@ -683,7 +683,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       }
     }
     Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-    datatypes[i].setSygus( types[i], bvl, true, true );
+    datatypes[i]->setSygus( types[i], bvl, true, true );
     mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
     sorts.push_back( types[i] );
     //set start index if applicable
@@ -694,12 +694,12 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
 
   //make Boolean type
   Type btype = getExprManager()->booleanType();
-  datatypes.push_back(Datatype(dbname));
+  datatypes.push_back(new Datatype(dbname));
   ops.push_back(std::vector<Expr>());
   std::vector<std::string> cnames;
   std::vector<std::vector<CVC4::Type> > cargs;
   std::vector<std::string> unresolved_gterm_sym;
-  Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
+  Debug("parser-sygus") << "Make grammar for " << btype << " " << *(datatypes.back()) << std::endl;
   //add variables
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
     if( sygus_vars[i].getType().isBoolean() ){
@@ -776,8 +776,8 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   if( range==btype ){
     startIndex = sorts.size();
   }
-  Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-  datatypes.back().setSygus( btype, bvl, true, true );
+  Debug("parser-sygus") << "...make datatype " << *(datatypes.back()) << std::endl;
+  datatypes.back()->setSygus( btype, bvl, true, true );
   mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
   sorts.push_back( btype );
 
@@ -804,7 +804,7 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o
 //  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
 void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
-                              std::vector< CVC4::Datatype >& datatypes,
+                              std::vector< CVC4::Datatype* >& datatypes,
                               std::vector< CVC4::Type>& sorts,
                               std::vector< std::vector<CVC4::Expr> >& ops,
                               std::vector< std::vector<std::string> >& cnames,
@@ -848,7 +848,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
     cargs[index].push_back( std::vector< CVC4::Type >() );
     for( unsigned i=0; i<sgt.d_children.size(); i++ ){
       std::stringstream ss;
-      ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
+      ss << datatypes[index]->getName() << "_" << ops[index].size() << "_arg_" << i;
       std::string sub_dname = ss.str();
       //add datatype for child
       Type null_type;
@@ -921,7 +921,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
 }
 
 bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
-                                  std::vector< CVC4::Datatype >& datatypes,
+                                  std::vector< CVC4::Datatype* >& datatypes,
                                   std::vector< CVC4::Type>& sorts,
                                   std::vector< std::vector<CVC4::Expr> >& ops,
                                   std::vector< std::vector<std::string> >& cnames,
@@ -929,7 +929,7 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
                                   std::vector< bool >& allow_const,
                                   std::vector< std::vector< std::string > >& unresolved_gterm_sym ){
   sorts.push_back(t);
-  datatypes.push_back(Datatype(dname));
+  datatypes.push_back(new Datatype(dname));
   ops.push_back(std::vector<Expr>());
   cnames.push_back(std::vector<std::string>());
   cargs.push_back(std::vector<std::vector<CVC4::Type> >());
@@ -938,7 +938,7 @@ bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname,
   return true;
 }
 
-bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
+bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype* >& datatypes,
                                  std::vector< CVC4::Type>& sorts,
                                  std::vector< std::vector<CVC4::Expr> >& ops,
                                  std::vector< std::vector<std::string> >& cnames,
@@ -955,7 +955,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
   return true;
 }
 
-Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
+Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype* >& datatypes,
                                     std::vector< CVC4::Type>& sorts,
                                     std::vector< std::vector<CVC4::Expr> >& ops,
                                     std::vector< std::vector<std::string> >& cnames,
@@ -1024,7 +1024,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
     sygus_to_builtin[t] = curr_t;
   }else{
     Debug("parser-sygus") << "simple argument " << t << std::endl;
-    Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl;
+    Debug("parser-sygus") << "...removing " << datatypes.back()->getName() << std::endl;
     //otherwise, datatype was unecessary
     //pop argument datatype definition
     popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
@@ -1034,7 +1034,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
 
 void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
                                        int index,
-                                       std::vector< CVC4::Datatype >& datatypes,
+                                       std::vector< CVC4::Datatype* >& datatypes,
                                        std::vector< CVC4::Type>& sorts,
                                        std::vector< std::vector<CVC4::Expr> >& ops,
                                        std::vector< std::vector<std::string> >& cnames,
@@ -1045,7 +1045,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
   std::vector< CVC4::Expr > let_define_args;
   Expr let_body;
   int dindex = cargs[index].size()-1;
-  Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
+  Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index]->getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
     Debug("parser-sygus") << "  " << i << " : " << cargs[index][dindex][i] << std::endl;
     if( i+1==cargs[index][dindex].size() ){
@@ -1054,7 +1054,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
         let_body = it->second;
       }else{
         std::stringstream ss;
-        ss << datatypes[index].getName() << "_body";
+        ss << datatypes[index]->getName() << "_body";
         let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]);
         d_sygus_bound_var_type[let_body] = cargs[index][dindex][i];
       }
@@ -1094,7 +1094,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
 
   Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
   std::stringstream ss;
-  ss << datatypes[index].getName() << "_let";
+  ss << datatypes[index]->getName() << "_let";
   Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
   d_sygus_defined_funs.push_back( let_func );
   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
@@ -1130,11 +1130,11 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr
 }
 
 void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
-                               std::vector< CVC4::Datatype >& datatypes,
+                               std::vector< CVC4::Datatype* >& datatypes,
                                std::vector< CVC4::Type>& sorts,
                                std::vector< std::vector<CVC4::Expr> >& ops ) {
   if( startIndex>0 ){
-    CVC4::Datatype tmp_dt = datatypes[0];
+    CVC4::Datatype* tmp_dt = datatypes[0];
     Type tmp_sort = sorts[0];
     std::vector< Expr > tmp_ops;
     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
@@ -1218,11 +1218,11 @@ void Smt2::defineSygusFuns() {
   }
 }
 
-void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
+void Smt2::mkSygusDatatype( CVC4::Datatype* dt, std::vector<CVC4::Expr>& ops,
                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
                             std::vector<std::string>& unresolved_gterm_sym,
                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
-  Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
+  Debug("parser-sygus") << "Making sygus datatype " << dt->getName() << std::endl;
   Debug("parser-sygus") << "  add constructors..." << std::endl;
   for( int i=0; i<(int)cnames.size(); i++ ){
     bool is_dup = false;
@@ -1260,7 +1260,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       for( unsigned j=0; j<cargs[i].size(); j++ ){
         Type bt = sygus_to_builtin[cargs[i][j]];
         std::stringstream ss;
-        ss << dt.getName() << "_x_" << i << "_" << j;
+        ss << dt->getName() << "_x_" << i << "_" << j;
         Expr v = mkBoundVar(ss.str(), bt);
         let_args.push_back( v );
         fsorts.push_back( bt );
@@ -1280,7 +1280,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
       Debug("parser-sygus") << ": function type is " << ft << std::endl;
       std::stringstream ss;
-      ss << dt.getName() << "_df_" << i;
+      ss << dt->getName() << "_df_" << i;
       //replace operator and name
       ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
       cnames[i] = ss.str();
@@ -1309,7 +1309,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         if( std::find( types.begin(), types.end(), t )==types.end() ){
           types.push_back( t );
           //identity element
-          Type bt = dt.getSygusType();
+          Type bt = dt->getSygusType();
           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
           std::stringstream ss;
           ss << t << "_x_id";
@@ -1338,19 +1338,19 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
 
 }
 
-void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
+void Smt2::addSygusDatatypeConstructor( CVC4::Datatype* dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
                                         CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) {
-  Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl;
+  Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt->getName() << std::endl;
   if( !let_body.isNull() ){
     Debug("parser-sygus") << "    let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl;
     //TODO : remove arguments not occurring in body
     //if this is a self identity function, ignore
     if( let_args.size()==0 && let_args[0]==let_body ){
-      Debug("parser-sygus") << "    identity function " << cargs[0] << " to " << dt.getName() << std::endl;
+      Debug("parser-sygus") << "    identity function " << cargs[0] << " to " << dt->getName() << std::endl;
       //TODO
     }
   }
-  std::string name = dt.getName() + "_" + cname;
+  std::string name = dt->getName() + "_" + cname;
   std::string testerId("is-");
   testerId.append(name);
   checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
@@ -1363,7 +1363,7 @@ void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::
     sname << name << "_" << j;
     c.addArg(sname.str(), cargs[j]);
   }
-  dt.addConstructor(c);
+  dt->addConstructor(c);
 }
 
 
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index b99e142ba..ac4be9bee 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -173,13 +173,13 @@ public:
 
   Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false);
 
-  void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
+  void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector< CVC4::Datatype* >& datatypes,
                               std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex );
 
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
 
   void processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
-                          std::vector< CVC4::Datatype >& datatypes,
+                          std::vector< CVC4::Datatype* >& datatypes,
                           std::vector< CVC4::Type>& sorts,
                           std::vector< std::vector<CVC4::Expr> >& ops,
                           std::vector< std::vector<std::string> >& cnames,
@@ -191,7 +191,7 @@ public:
                           CVC4::Type& ret, bool isNested = false );
 
   static bool pushSygusDatatypeDef( Type t, std::string& dname,
-                                    std::vector< CVC4::Datatype >& datatypes,
+                                    std::vector< CVC4::Datatype* >& datatypes,
                                     std::vector< CVC4::Type>& sorts,
                                     std::vector< std::vector<CVC4::Expr> >& ops,
                                     std::vector< std::vector<std::string> >& cnames,
@@ -199,7 +199,7 @@ public:
                                     std::vector< bool >& allow_const,
                                     std::vector< std::vector< std::string > >& unresolved_gterm_sym );
 
-  static bool popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
+  static bool popSygusDatatypeDef( std::vector< CVC4::Datatype* >& datatypes,
                                    std::vector< CVC4::Type>& sorts,
                                    std::vector< std::vector<CVC4::Expr> >& ops,
                                    std::vector< std::vector<std::string> >& cnames,
@@ -208,7 +208,7 @@ public:
                                    std::vector< std::vector< std::string > >& unresolved_gterm_sym );
 
   void setSygusStartIndex( std::string& fun, int startIndex,
-                           std::vector< CVC4::Datatype >& datatypes,
+                           std::vector< CVC4::Datatype* >& datatypes,
                            std::vector< CVC4::Type>& sorts,
                            std::vector< std::vector<CVC4::Expr> >& ops );
 
@@ -218,7 +218,7 @@ public:
 
   void defineSygusFuns();
 
-  void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
+  void mkSygusDatatype( CVC4::Datatype* dt, std::vector<CVC4::Expr>& ops,
                         std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
                         std::vector<std::string>& unresolved_gterm_sym,
                         std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
@@ -314,10 +314,10 @@ private:
 
   void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
 
-  void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
+  void addSygusDatatypeConstructor( CVC4::Datatype* dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
                                     CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
 
-  Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
+  Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype* >& datatypes,
                                 std::vector< CVC4::Type>& sorts,
                                 std::vector< std::vector<CVC4::Expr> >& ops,
                                 std::vector< std::vector<std::string> >& cnames,
@@ -328,7 +328,7 @@ private:
                                 std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret );
 
   void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index,
-                                   std::vector< CVC4::Datatype >& datatypes,
+                                   std::vector< CVC4::Datatype* >& datatypes,
                                    std::vector< CVC4::Type>& sorts,
                                    std::vector< std::vector<CVC4::Expr> >& ops,
                                    std::vector< std::vector<std::string> >& cnames,
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 550f87081..11cf7dd11 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -163,7 +163,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     case kind::DATATYPE_TYPE: {
-      const Datatype& dt = n.getConst<Datatype>();
+      const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
       if( dt.isTuple() ){
         out << '[';
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
@@ -333,15 +333,17 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     // DATATYPES
-    case kind::PARAMETRIC_DATATYPE:
-      out << n[0].getConst<Datatype>().getName() << '[';
-      for(unsigned i = 1; i < n.getNumChildren(); ++i) {
-        if(i > 1) {
-          out << ',';
+    case kind::PARAMETRIC_DATATYPE: {
+        const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() ));
+        out << dt.getName() << '[';
+        for(unsigned i = 1; i < n.getNumChildren(); ++i) {
+          if(i > 1) {
+            out << ',';
+          }
+          out << n[i];
         }
-        out << n[i];
+        out << ']';
       }
-      out << ']';
       return;
       break;
     case kind::APPLY_TYPE_ASCRIPTION: {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7b7d569b7..be550474c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -284,7 +284,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
 
     case kind::DATATYPE_TYPE:
-      out << maybeQuoteSymbol(n.getConst<Datatype>().getName());
+      {
+        const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
+        out << maybeQuoteSymbol(dt.getName());
+      }
       break;
 
     case kind::UNINTERPRETED_CONSTANT: {
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 51ae0fd11..e9b51c47b 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -60,10 +60,10 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
     d_ffDt = d_ff;
     d_ttDt = d_tt;
   } else {
-    Datatype spec("BooleanTerm");
+    Datatype* spec = new Datatype("BooleanTerm");
     // don't change the order; false is assumed to come first by the model postprocessor
-    spec.addConstructor(DatatypeConstructor("BT_False"));
-    spec.addConstructor(DatatypeConstructor("BT_True"));
+    spec->addConstructor(DatatypeConstructor("BT_False"));
+    spec->addConstructor(DatatypeConstructor("BT_True"));
     const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype();
     d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor()));
     d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor()));
@@ -255,13 +255,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
           mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters());
           unresolvedTypes.insert(mySelfType);
         }
-        vector<Datatype> newDtVector;
+        vector<Datatype*> newDtVector;
         if(dt.isParametric()) {
-          newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false));
+          newDtVector.push_back(new Datatype(dt.getName() + "'", dt.getParameters(), false));
         } else {
-          newDtVector.push_back(Datatype(dt.getName() + "'", false));
+          newDtVector.push_back(new Datatype(dt.getName() + "'", false));
         }
-        Datatype& newDt = newDtVector.front();
+        Datatype * newDt = newDtVector.front();
         Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
         for(c = dt.begin(); c != dt.end(); ++c) {
           DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
@@ -286,10 +286,10 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
               }
             }
           }
-          newDt.addConstructor(ctor);
+          newDt->addConstructor(ctor);
         }
-        vector<DatatypeType> newDttVector =
-          NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
+        vector<DatatypeType> newDttVector;
+        NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes, newDttVector);
         DatatypeType& newDtt = newDttVector.front();
         const Datatype& newD = newDtt.getDatatype();
         for(c = dt.begin(); c != dt.end(); ++c) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e3a0533af..1e5ac84b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -784,8 +784,11 @@ public:
   }
 
   void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) {
+    Trace("ajr-temp") << "Notify " << dtts.size() << " datatypes." << std::endl;
     DatatypeDeclarationCommand c(dtts);
+    Trace("ajr-temp") << "dump command" << std::endl;
     d_smt.addToModelCommandAndDump(c);
+    Trace("ajr-temp") << "Finish" << std::endl;
   }
 
   void nmNotifyNewVar(TNode n, uint32_t flags) {
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 28a6a52d9..42399d61f 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -39,10 +39,10 @@ parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; para
 parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term"
 
 constant DATATYPE_TYPE \
-    ::CVC4::Datatype \
-    "::CVC4::DatatypeHashFunction" \
+    ::CVC4::DatatypeIndexConstant \
+    "::CVC4::DatatypeIndexConstantHashFunction" \
     "expr/datatype.h" \
-    "a datatype type"
+    "a datatype type index"
 cardinality DATATYPE_TYPE \
     "%TYPE%.getDatatype().getCardinality()" \
     "expr/datatype.h"
-- 
cgit v1.2.3