Updates not related to creation for eliminating Expr-level datatype (#4838)

This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.

This required updating a unit test from Expr -> Node.

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 9ec3ac5fd0360500ea0e0330ff0afae41ea13b80..f8712e20e6987bd5bc94699ea6596b644fa8193e 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -304,6 +304,7 @@ void Datatype::setRecord() {
   PrettyCheckArgument(
       !isResolved(), this, "cannot set record to a finalized Datatype");
   d_isRecord = true;
+  d_internal->setRecord();
 }
 
 Cardinality Datatype::getCardinality(Type t) const

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 85e07866bc97494c7b35f31f19802b981b22d3ec..c64814ed6b250bfbea13f11ecf48607ee5522b43 100644 (file)
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -66,7 +66,7 @@ void DTypeConstructor::addArgSelf(std::string selectorName)
 {
   Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
   std::shared_ptr<DTypeSelector> a =
-      std::make_shared<DTypeSelector>(selectorName, Node::null());
+      std::make_shared<DTypeSelector>(selectorName + '\0', Node::null());
   addArg(a);
 }
 

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 68d3904d37dfc40f1573b096ef0d28138efa3440..1da60eb05521dbe0cd73da3e83c487354d9aeed1 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -26,6 +26,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/context.h"
+#include "expr/dtype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/type.h"
@@ -212,11 +213,10 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
           Trace("parser-overloading")
               << "Parametric overloaded datatype selector " << name << " "
               << tna << std::endl;
-          DatatypeType tnd = static_cast<DatatypeType>(argTypes[i]);
-          const Datatype& dt = tnd.getDatatype();
+          const DType& dt = TypeNode::fromType(argTypes[i]).getDType();
           // tng is the "generalized" version of the instantiated parametric
           // type tna
-          Type tng = dt.getDatatypeType();
+          Type tng = dt.getTypeNode().toType();
           itc = tat->d_children.find(tng);
           if (itc != tat->d_children.end())
           {

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 7696d9d7a2c3559a62e0663cd05ec08a06f169c7..8232ef339f347f5ae42ed64f867b77aeb7007ece 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -331,8 +331,7 @@ bool Type::isTuple() const {
 /** Is this a record type? */
 bool Type::isRecord() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getKind() == kind::DATATYPE_TYPE
-         && DatatypeType(*this).getDatatype().isRecord();
+  return d_typeNode->isRecord();
 }
 
 /** Is this a symbolic expression type? */
@@ -586,7 +585,8 @@ std::vector<Type> ConstructorType::getArgTypes() const {
   return args;
 }
 
-const Datatype& DatatypeType::getDatatype() const {
+const Datatype& DatatypeType::getDatatype() const
+{
   NodeManagerScope nms(d_nodeManager);
   Assert(isDatatype());
   if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
@@ -602,10 +602,6 @@ bool DatatypeType::isParametric() const {
   return d_typeNode->isParametricDatatype();
 }
 
-Expr DatatypeType::getConstructor(std::string name) const {
-  return getDatatype().getConstructor(name);
-}
-
 bool DatatypeType::isInstantiated() const {
   return d_typeNode->isInstantiatedDatatype();
 }
@@ -662,14 +658,6 @@ std::vector<Type> DatatypeType::getTupleTypes() const {
   return vect;
 }
 
-/** Get the description of the record type */
-const Record& DatatypeType::getRecord() const {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isRecord());
-  const Datatype& dt = getDatatype();
-  return *(dt.getRecord());
-}
-
 DatatypeType SelectorType::getDomain() const {
   return DatatypeType(makeType((*d_typeNode)[0]));
 }

diff --git a/src/expr/type.h b/src/expr/type.h
index 61cb7eabfb8464204d6d0c21f13fb56b641e170f..0067ba7e7ab2a841857d0fc413376ded3b36edba 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -621,13 +621,6 @@ class CVC4_PUBLIC DatatypeType : public Type {
 
   /** Is this datatype parametric? */
   bool isParametric() const;
-
-  /**
-   * Get the constructor operator associated to the given constructor
-   * name in this datatype.
-   */
-  Expr getConstructor(std::string name) const;
-
   /**
    * Has this datatype been fully instantiated ?
    *
@@ -654,9 +647,6 @@ class CVC4_PUBLIC DatatypeType : public Type {
   /** Get the constituent types of a tuple type */
   std::vector<Type> getTupleTypes() const;
 
-  /** Get the description of the record type */
-  const Record& getRecord() const;
-
 };/* class DatatypeType */
 
 /** Class encapsulating the constructor type. */

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index c97a24d6da40195cad5f6bc7642743128e8bcb25..7e38fac3dc91a3e7d95582e6f53b122588a56d36 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -396,12 +396,16 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
-
-/** Is this a tuple type? */
-bool TypeNode::isTuple() const {
+bool TypeNode::isTuple() const
+{
   return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple());
 }
 
+bool TypeNode::isRecord() const
+{
+  return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord());
+}
+
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
   const DType& dt = getDType();

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0d0c17edf4e5522e4adbbd8b58555b63a36863fc..b836e5069e324f0e3e91b7b817ecbd32cbd2f830 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -599,6 +599,9 @@ public:
   /** Is this a tuple type? */
   bool isTuple() const;
 
+  /** Is this a record type? */
+  bool isRecord() const;
+
   /** Get the length of a tuple type */
   size_t getTupleLength() const;
 

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 7d1f66d65e758053bb47da5bc8617d36356066f5..53abf2e3dc9e9a376273905fc0dbc106ff4465dd 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -18,6 +18,7 @@
 
 #include "preprocessing/passes/unconstrained_simplifier.h"
 
+#include "expr/dtype.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
@@ -262,8 +263,8 @@ void UnconstrainedSimplifier::processUnconstrained()
           if (parent[0].getType().isDatatype())
           {
             TypeNode tn = parent[0].getType();
-            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            if (dt.isRecursiveSingleton(tn.toType()))
+            const DType& dt = tn.getDType();
+            if (dt.isRecursiveSingleton(tn))
             {
               // domain size may be 1
               break;

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 9ec522141f30eb1f1e4fd0ff65a7fbedc5911f36..2435924560005f6d25b21af3d02ad7a045a775c9 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -214,23 +214,26 @@ void CvcPrinter::toStream(
       const Datatype& dt =
           NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
               n.getConst<DatatypeIndexConstant>().getIndex());
+
       if( dt.isTuple() ){
         out << '[';
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
           if (i > 0) {
             out << ", ";
           }
-          Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
+          Type t = dt[0][i].getRangeType();
           out << t;
         }
         out << ']';
-      }else if( dt.isRecord() ){
+      }
+      else if (dt.isRecord())
+      {
         out << "[# ";
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
           if (i > 0) {
             out << ", ";
           }
-          Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
+          Type t = dt[0][i].getRangeType();
           out << dt[0][i].getSelector() << ":" << t;
         }
         out << " #]";
@@ -414,18 +417,17 @@ void CvcPrinter::toStream(
         }
         else if (t.toType().isRecord())
         {
-          const Record& rec = static_cast<DatatypeType>(t.toType()).getRecord();
+          const DType& dt = t.getDType();
+          const DTypeConstructor& recCons = dt[0];
           out << "(# ";
-          TNode::iterator i = n.begin();
-          bool first = true;
-          const Record::FieldVector& fields = rec.getFields();
-          for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
-            if(!first) {
+          for (size_t i = 0, nargs = recCons.getNumArgs(); i < nargs; i++)
+          {
+            if (i != 0)
+            {
               out << ", ";
             }
-            out << (*j).first << " := ";
-            toStream(out, *i, depth, types, false);
-            first = false;
+            out << recCons[i].getName() << " := ";
+            toStream(out, n[i], depth, types, false);
           }
           out << " #)";
           return;
@@ -450,18 +452,17 @@ void CvcPrinter::toStream(
         {
           toStream(op, opn, depth, types, false);
         }
-        else if (t.isTuple()
-                 || DatatypeType(t.toType()).isRecord())
+        else if (t.isTuple() || t.isRecord())
         {
           toStream(out, n[0], depth, types, true);
           out << '.';
-          const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
+          const DType& dt = t.getDType();
           if (t.isTuple())
           {
             int sindex;
             if (n.getKind() == kind::APPLY_SELECTOR)
             {
-              sindex = Datatype::indexOf(opn.toExpr());
+              sindex = DType::indexOf(opn.toExpr());
             }
             else
             {
@@ -483,9 +484,9 @@ void CvcPrinter::toStream(
     case kind::APPLY_TESTER: {
       Assert(!n.getType().isTuple() && !n.getType().toType().isRecord());
       op << "is_";
-      unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
-      const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-      toStream(op, Node::fromExpr(dt[cindex].getConstructor()), depth, types, false);
+      unsigned cindex = DType::indexOf(n.getOperator());
+      const DType& dt = DType::datatypeOf(n.getOperator());
+      toStream(op, dt[cindex].getConstructor(), depth, types, false);
     }
       break;
     case kind::CONSTRUCTOR_TYPE:
@@ -1515,7 +1516,7 @@ static void toStream(std::ostream& out,
 {
   const vector<Type>& datatypes = c->getDatatypes();
   Assert(!datatypes.empty() && datatypes[0].isDatatype());
-  const Datatype& dt0 = DatatypeType(datatypes[0]).getDatatype();
+  const DType& dt0 = TypeNode::fromType(datatypes[0]).getDType();
   //do not print tuple/datatype internal declarations
   if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord()))
   {
@@ -1526,7 +1527,7 @@ static void toStream(std::ostream& out,
       if(! firstDatatype) {
         out << ',' << endl;
       }
-      const Datatype& dt = DatatypeType(t).getDatatype();
+      const DType& dt = TypeNode::fromType(t).getDType();
       out << "  " << dt.getName();
       if(dt.isParametric()) {
         out << '[';
@@ -1539,31 +1540,28 @@ static void toStream(std::ostream& out,
         out << ']';
       }
       out << " = ";
-      bool firstConstructor = true;
-      for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
-        if(! firstConstructor) {
+      for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+      {
+        const DTypeConstructor& cons = dt[j];
+        if (j != 0)
+        {
           out << " | ";
         }
-        firstConstructor = false;
-        const DatatypeConstructor& cons = *j;
         out << cons.getName();
         if (cons.getNumArgs() > 0)
         {
           out << '(';
-          bool firstSelector = true;
-          for (DatatypeConstructor::const_iterator k = cons.begin();
-               k != cons.end();
-               ++k)
+          for (size_t k = 0, nargs = cons.getNumArgs(); k < nargs; k++)
           {
-            if(! firstSelector) {
+            if (k != 0)
+            {
               out << ", ";
             }
-            firstSelector = false;
-            const DatatypeConstructorArg& selector = *k;
-            Type tr = SelectorType(selector.getType()).getRangeType();
+            const DTypeSelector& selector = cons[k];
+            TypeNode tr = selector.getRangeType();
             if (tr.isDatatype())
             {
-              const Datatype& sdt = DatatypeType(tr).getDatatype();
+              const DType& sdt = tr.getDType();
               out << selector.getName() << ": " << sdt.getName();
             }
             else

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7560b2ce4dc2af529c616a844612011e8bad214e..b92490ae26df3305b16e6dc4bc1809b0e149085e 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -793,7 +793,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::APPLY_CONSTRUCTOR:
   {
     typeChildren = true;
-    const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+    const DType& dt = DType::datatypeOf(n.getOperator());
     if (dt.isTuple())
     {
       stillNeedToPrintParams = false;
@@ -898,16 +898,24 @@ void Smt2Printer::toStream(std::ostream& out,
     if(toDepth != 0) {
       if (n.getKind() == kind::APPLY_TESTER)
       {
-        unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
-        const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+        unsigned cindex = DType::indexOf(n.getOperator().toExpr());
+        const DType& dt = DType::datatypeOf(n.getOperator().toExpr());
         if (isVariant_2_6(d_variant))
         {
           out << "(_ is ";
-          toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
+          toStream(out,
+                   dt[cindex].getConstructor(),
+                   toDepth < 0 ? toDepth : toDepth - 1,
+                   types,
+                   TypeNode::null());
           out << ")";
         }else{
           out << "is-";
-          toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
+          toStream(out,
+                   dt[cindex].getConstructor(),
+                   toDepth < 0 ? toDepth : toDepth - 1,
+                   types,
+                   TypeNode::null());
         }
       }else{
         toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
@@ -963,14 +971,14 @@ void Smt2Printer::toStream(std::ostream& out,
       TypeNode opt = n.getOperator().getType();
       if (n.getKind() == kind::APPLY_CONSTRUCTOR)
       {
-        Type tn = n.getType().toType();
+        TypeNode tn = n.getType();
         // may be parametric, in which case the constructor type must be
         // specialized
-        const Datatype& dt = static_cast<DatatypeType>(tn).getDatatype();
+        const DType& dt = tn.getDType();
         if (dt.isParametric())
         {
-          unsigned ci = Datatype::indexOf(n.getOperator().toExpr());
-          opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn));
+          unsigned ci = DType::indexOf(n.getOperator().toExpr());
+          opt = dt[ci].getSpecializedConstructorType(tn);
         }
       }
       Assert(opt.getNumChildren() == n.getNumChildren() + 1);
@@ -1845,16 +1853,20 @@ static void toStream(std::ostream& out, const GetOptionCommand* c)
   out << "(get-option :" << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const Datatype & d) {
-  for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end();
-      ctor != ctor_end; ++ctor){
-    if( ctor!=d.begin() ) out << " ";
-    out << "(" << CVC4::quoteSymbol(ctor->getName());
-
-    for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end();
-        arg != arg_end; ++arg){
-      out << " (" << arg->getSelector() << " "
-          << static_cast<SelectorType>(arg->getType()).getRangeType() << ")";
+static void toStream(std::ostream& out, const DType& dt)
+{
+  for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+  {
+    const DTypeConstructor& cons = dt[i];
+    if (i != 0)
+    {
+      out << " ";
+    }
+    out << "(" << CVC4::quoteSymbol(cons.getName());
+    for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
+    {
+      const DTypeSelector& arg = cons[j];
+      out << " (" << arg.getSelector() << " " << arg.getRangeType() << ")";
     }
     out << ")";
   }
@@ -1867,8 +1879,7 @@ static void toStream(std::ostream& out,
   const std::vector<Type>& datatypes = c->getDatatypes();
   Assert(!datatypes.empty());
   Assert(datatypes[0].isDatatype());
-  DatatypeType dt0 = DatatypeType(datatypes[0]);
-  const Datatype& d0 = dt0.getDatatype();
+  const DType& d0 = TypeNode::fromType(datatypes[0]).getDType();
   if (d0.isTuple())
   {
     // not necessary to print tuples
@@ -1887,7 +1898,7 @@ static void toStream(std::ostream& out,
     for (const Type& t : datatypes)
     {
       Assert(t.isDatatype());
-      const Datatype& d = DatatypeType(t).getDatatype();
+      const DType& d = TypeNode::fromType(t).getDType();
       out << "(" << CVC4::quoteSymbol(d.getName());
       out << " " << d.getNumParameters() << ")";
     }
@@ -1895,7 +1906,7 @@ static void toStream(std::ostream& out,
     for (const Type& t : datatypes)
     {
       Assert(t.isDatatype());
-      const Datatype& d = DatatypeType(t).getDatatype();
+      const DType& d = TypeNode::fromType(t).getDType();
       if (d.isParametric())
       {
         out << "(par (";
@@ -1927,7 +1938,7 @@ static void toStream(std::ostream& out,
     for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++)
     {
       Assert(datatypes[j].isDatatype());
-      const Datatype& dj = DatatypeType(datatypes[j]).getDatatype();
+      const DType& dj = TypeNode::fromType(datatypes[j]).getDType();
       if (dj.getNumParameters() != nparam)
       {
         success = false;
@@ -1967,7 +1978,7 @@ static void toStream(std::ostream& out,
     for (const Type& t : datatypes)
     {
       Assert(t.isDatatype());
-      const Datatype& dt = DatatypeType(t).getDatatype();
+      const DType& dt = TypeNode::fromType(t).getDType();
       out << "(" << CVC4::quoteSymbol(dt.getName()) << " ";
       toStream(out, dt);
       out << ")";
@@ -2011,13 +2022,13 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
 static void toStreamSygusGrammar(std::ostream& out, const Type& t)
 {
   if (!t.isNull() && t.isDatatype()
-      && static_cast<DatatypeType>(t).getDatatype().isSygus())
+      && TypeNode::fromType(t).getDType().isSygus())
   {
     std::stringstream types_predecl, types_list;
-    std::set<Type> grammarTypes;
-    std::list<Type> typesToPrint;
-    grammarTypes.insert(t);
-    typesToPrint.push_back(t);
+    std::set<TypeNode> grammarTypes;
+    std::list<TypeNode> typesToPrint;
+    grammarTypes.insert(TypeNode::fromType(t));
+    typesToPrint.push_back(TypeNode::fromType(t));
     NodeManager* nm = NodeManager::currentNM();
     // for each datatype in grammar
     //   name
@@ -2025,28 +2036,28 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t)
     //   constructors in order
     do
     {
-      Type curr = typesToPrint.front();
+      TypeNode curr = typesToPrint.front();
       typesToPrint.pop_front();
-      Assert(curr.isDatatype()
-             && static_cast<DatatypeType>(curr).getDatatype().isSygus());
-      const Datatype& dt = static_cast<DatatypeType>(curr).getDatatype();
+      Assert(curr.isDatatype() && curr.getDType().isSygus());
+      const DType& dt = curr.getDType();
       types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " (";
       types_predecl << '(' << dt.getName() << ' ' << dt.getSygusType() << ") ";
       if (dt.getSygusAllowConst())
       {
         types_list << "(Constant " << dt.getSygusType() << ") ";
       }
-      for (const DatatypeConstructor& cons : dt)
+      for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
       {
+        const DTypeConstructor& cons = dt[i];
         // make a sygus term
         std::vector<Node> cchildren;
-        cchildren.push_back(Node::fromExpr(cons.getConstructor()));
-        for (const DatatypeConstructorArg& i : cons)
+        cchildren.push_back(cons.getConstructor());
+        for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
         {
-          Type argType = i.getRangeType();
+          TypeNode argType = cons[j].getRangeType();
           std::stringstream ss;
           ss << argType;
-          Node bv = nm->mkBoundVar(ss.str(), TypeNode::fromType(argType));
+          Node bv = nm->mkBoundVar(ss.str(), argType);
           cchildren.push_back(bv);
           // if fresh type, store it for later processing
           if (grammarTypes.insert(argType).second)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 585c2819de46c545f7d10dceb9bc78202cef4e79..c2d1a971eeef1037be1f0d8e74de3c957b8a5eed 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1335,10 +1335,9 @@ void SmtEngine::declareSynthFun(const std::string& id,
     setUserAttribute("sygus-synth-fun-var-list", func, attr_val_bvl, "");
   }
   // whether sygus type encodes syntax restrictions
-  if (sygusType.isDatatype()
-      && static_cast<DatatypeType>(sygusType).getDatatype().isSygus())
+  TypeNode stn = TypeNode::fromType(sygusType);
+  if (sygusType.isDatatype() && stn.getDType().isSygus())
   {
-    TypeNode stn = TypeNode::fromType(sygusType);
     Node sym = d_nodeManager->mkBoundVar("sfproxy", stn);
     std::vector<Expr> attr_value;
     attr_value.push_back(sym.toExpr());

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9b8badc5eb880f963225a1d8ca0a93d278747597..17a43bc04f18a849f73e4083a96f1c5b4acc54cb 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -18,7 +18,6 @@
 #include <map>
 
 #include "base/check.h"
-#include "expr/datatype.h"
 #include "expr/dtype.h"
 #include "expr/kind.h"
 #include "options/datatypes_options.h"
@@ -654,10 +653,11 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
       }
       else
       {
-        Assert(tn.toType().isRecord());
-        const Record& record = DatatypeType(tn.toType()).getRecord();
-        size = record.getNumFields();
-        updateIndex = record.getIndex(
+        Assert(tn.isRecord());
+        const DTypeConstructor& recCons = dt[0];
+        size = recCons.getNumArgs();
+        // get the index for the name
+        updateIndex = recCons.getSelectorIndexForName(
             n.getOperator().getConst<RecordUpdate>().getField());
       }
       Debug("tuprec") << "expr is " << n << std::endl;

diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index ac27acfb5b52b2041be562f323f12bc525a28190..6d92668be308e979b35e667f7072b0feeafe93c6 100644 (file)
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::Datatype
+ ** \brief Black box testing of CVC4::DType
  **
- ** Black box testing of CVC4::Datatype.
+ ** Black box testing of CVC4::DType.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -19,7 +19,7 @@
 #include <sstream>
 
 #include "api/cvc4cpp.h"
-#include "expr/datatype.h"
+#include "expr/dtype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
@@ -33,8 +33,8 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void setUp() override
   {
     d_slv = new api::Solver();
-    d_em = d_slv->getExprManager();
-    d_scope = new ExprManagerScope(*d_em);
+    d_nm = d_slv->getNodeManager();
+    d_scope = new NodeManagerScope(d_nm);
     Debug.on("datatypes");
     Debug.on("groundterms");
   }
@@ -46,12 +46,16 @@ class DatatypeBlack : public CxxTest::TestSuite {
   }
 
   void testEnumeration() {
-    Datatype colors(d_em, "colors");
+    DType colors("colors");
 
-    DatatypeConstructor yellow("yellow");
-    DatatypeConstructor blue("blue");
-    DatatypeConstructor green("green");
-    DatatypeConstructor red("red");
+    std::shared_ptr<DTypeConstructor> yellow =
+        std::make_shared<DTypeConstructor>("yellow");
+    std::shared_ptr<DTypeConstructor> blue =
+        std::make_shared<DTypeConstructor>("blue");
+    std::shared_ptr<DTypeConstructor> green =
+        std::make_shared<DTypeConstructor>("green");
+    std::shared_ptr<DTypeConstructor> red =
+        std::make_shared<DTypeConstructor>("red");
 
     colors.addConstructor(yellow);
     colors.addConstructor(blue);
@@ -59,159 +63,171 @@ class DatatypeBlack : public CxxTest::TestSuite {
     colors.addConstructor(red);
 
     Debug("datatypes") << colors << std::endl;
-    DatatypeType colorsType = d_em->mkDatatypeType(colors);
+    TypeNode colorsType = d_nm->mkDatatypeType(colors);
     Debug("datatypes") << colorsType << std::endl;
 
-    Expr ctor = colorsType.getDatatype()[1].getConstructor();
-    Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
+    Node ctor = colorsType.getDType()[1].getConstructor();
+    Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
     Debug("datatypes") << apply << std::endl;
 
-    const Datatype& colorsDT = colorsType.getDatatype();
-    TS_ASSERT(colorsDT.getConstructor("blue") == ctor);
-    TS_ASSERT(colorsDT["blue"].getConstructor() == ctor);
-    TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"),
-                     IllegalArgumentException&);
-    TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException&);
-
-    TS_ASSERT(! colorsType.getDatatype().isParametric());
-    TS_ASSERT(colorsType.getDatatype().isFinite());
-    TS_ASSERT(colorsType.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL);
+    TS_ASSERT(!colorsType.getDType().isParametric());
+    TS_ASSERT(colorsType.getDType().isFinite());
+    TS_ASSERT(colorsType.getDType().getCardinality().compare(4)
+              == Cardinality::EQUAL);
     TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL);
-    TS_ASSERT(colorsType.getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl
+    TS_ASSERT(colorsType.getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << colorsType.getDType().getName()
+                         << endl
                          << "  is " << colorsType.mkGroundTerm() << endl;
     TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType);
   }
 
   void testNat() {
-    Datatype nat(d_em, "nat");
+    DType nat("nat");
 
-    DatatypeConstructor succ("succ");
-    succ.addArg("pred", DatatypeSelfType());
+    std::shared_ptr<DTypeConstructor> succ =
+        std::make_shared<DTypeConstructor>("succ");
+    succ->addArgSelf("pred");
     nat.addConstructor(succ);
 
-    DatatypeConstructor zero("zero");
+    std::shared_ptr<DTypeConstructor> zero =
+        std::make_shared<DTypeConstructor>("zero");
     nat.addConstructor(zero);
 
     Debug("datatypes") << nat << std::endl;
-    DatatypeType natType = d_em->mkDatatypeType(nat);
+    TypeNode natType = d_nm->mkDatatypeType(nat);
     Debug("datatypes") << natType << std::endl;
 
-    Expr ctor = natType.getDatatype()[1].getConstructor();
-    Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor);
+    Node ctor = natType.getDType()[1].getConstructor();
+    Node apply = d_nm->mkNode(kind::APPLY_CONSTRUCTOR, ctor);
     Debug("datatypes") << apply << std::endl;
 
-    TS_ASSERT(! natType.getDatatype().isParametric());
-    TS_ASSERT(! natType.getDatatype().isFinite());
-    TS_ASSERT(natType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(natType.getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl
+    TS_ASSERT(!natType.getDType().isParametric());
+    TS_ASSERT(!natType.getDType().isFinite());
+    TS_ASSERT(natType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+              == Cardinality::EQUAL);
+    TS_ASSERT(natType.getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << natType.getDType().getName()
+                         << endl
                          << "  is " << natType.mkGroundTerm() << endl;
     TS_ASSERT(natType.mkGroundTerm().getType() == natType);
   }
 
   void testTree() {
-    Datatype tree(d_em, "tree");
-    Type integerType = d_em->integerType();
+    DType tree("tree");
+    TypeNode integerType = d_nm->integerType();
 
-    DatatypeConstructor node("node");
-    node.addArg("left", DatatypeSelfType());
-    node.addArg("right", DatatypeSelfType());
+    std::shared_ptr<DTypeConstructor> node =
+        std::make_shared<DTypeConstructor>("node");
+    node->addArgSelf("left");
+    node->addArgSelf("right");
     tree.addConstructor(node);
 
-    DatatypeConstructor leaf("leaf");
-    leaf.addArg("leaf", integerType);
+    std::shared_ptr<DTypeConstructor> leaf =
+        std::make_shared<DTypeConstructor>("leaf");
+    leaf->addArg("leaf", integerType);
     tree.addConstructor(leaf);
 
     Debug("datatypes") << tree << std::endl;
-    DatatypeType treeType = d_em->mkDatatypeType(tree);
+    TypeNode treeType = d_nm->mkDatatypeType(tree);
     Debug("datatypes") << treeType << std::endl;
 
-    Expr ctor = treeType.getDatatype()[1].getConstructor();
-    TS_ASSERT(treeType.getConstructor("leaf") == ctor);
-    TS_ASSERT(treeType.getConstructor("leaf") == ctor);
-    TS_ASSERT_THROWS(treeType.getConstructor("leff"),
-                     IllegalArgumentException&);
-
-    TS_ASSERT(! treeType.getDatatype().isParametric());
-    TS_ASSERT(! treeType.getDatatype().isFinite());
-    TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(treeType.getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl
+    TS_ASSERT(!treeType.getDType().isParametric());
+    TS_ASSERT(!treeType.getDType().isFinite());
+    TS_ASSERT(
+        treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(treeType.getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << treeType.getDType().getName()
+                         << endl
                          << "  is " << treeType.mkGroundTerm() << endl;
     TS_ASSERT(treeType.mkGroundTerm().getType() == treeType);
   }
 
   void testListInt() {
-    Datatype list(d_em, "list");
-    Type integerType = d_em->integerType();
+    DType list("list");
+    TypeNode integerType = d_nm->integerType();
 
-    DatatypeConstructor cons("cons");
-    cons.addArg("car", integerType);
-    cons.addArg("cdr", DatatypeSelfType());
+    std::shared_ptr<DTypeConstructor> cons =
+        std::make_shared<DTypeConstructor>("cons");
+    cons->addArg("car", integerType);
+    cons->addArgSelf("cdr");
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil");
+    std::shared_ptr<DTypeConstructor> nil =
+        std::make_shared<DTypeConstructor>("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
-    DatatypeType listType = d_em->mkDatatypeType(list);
+    TypeNode listType = d_nm->mkDatatypeType(list);
     Debug("datatypes") << listType << std::endl;
 
-    TS_ASSERT(! listType.getDatatype().isParametric());
-    TS_ASSERT(! listType.getDatatype().isFinite());
-    TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(listType.getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
+    TS_ASSERT(!listType.getDType().isParametric());
+    TS_ASSERT(!listType.getDType().isFinite());
+    TS_ASSERT(
+        listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(listType.getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << listType.getDType().getName()
+                         << endl
                          << "  is " << listType.mkGroundTerm() << endl;
     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
   }
 
   void testListReal() {
-    Datatype list(d_em, "list");
-    Type realType = d_em->realType();
+    DType list("list");
+    TypeNode realType = d_nm->realType();
 
-    DatatypeConstructor cons("cons");
-    cons.addArg("car", realType);
-    cons.addArg("cdr", DatatypeSelfType());
+    std::shared_ptr<DTypeConstructor> cons =
+        std::make_shared<DTypeConstructor>("cons");
+    cons->addArg("car", realType);
+    cons->addArgSelf("cdr");
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil");
+    std::shared_ptr<DTypeConstructor> nil =
+        std::make_shared<DTypeConstructor>("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
-    DatatypeType listType = d_em->mkDatatypeType(list);
+    TypeNode listType = d_nm->mkDatatypeType(list);
     Debug("datatypes") << listType << std::endl;
 
-    TS_ASSERT(! listType.getDatatype().isParametric());
-    TS_ASSERT(! listType.getDatatype().isFinite());
-    TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL);
-    TS_ASSERT(listType.getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
+    TS_ASSERT(!listType.getDType().isParametric());
+    TS_ASSERT(!listType.getDType().isFinite());
+    TS_ASSERT(listType.getDType().getCardinality().compare(Cardinality::REALS)
+              == Cardinality::EQUAL);
+    TS_ASSERT(listType.getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << listType.getDType().getName()
+                         << endl
                          << "  is " << listType.mkGroundTerm() << endl;
     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
   }
 
   void testListBoolean() {
-    Datatype list(d_em, "list");
-    Type booleanType = d_em->booleanType();
+    DType list("list");
+    TypeNode booleanType = d_nm->booleanType();
 
-    DatatypeConstructor cons("cons");
-    cons.addArg("car", booleanType);
-    cons.addArg("cdr", DatatypeSelfType());
+    std::shared_ptr<DTypeConstructor> cons =
+        std::make_shared<DTypeConstructor>("cons");
+    cons->addArg("car", booleanType);
+    cons->addArgSelf("cdr");
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil");
+    std::shared_ptr<DTypeConstructor> nil =
+        std::make_shared<DTypeConstructor>("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
-    DatatypeType listType = d_em->mkDatatypeType(list);
+    TypeNode listType = d_nm->mkDatatypeType(list);
     Debug("datatypes") << listType << std::endl;
 
-    TS_ASSERT(! listType.getDatatype().isFinite());
-    TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(listType.getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl
+    TS_ASSERT(!listType.getDType().isFinite());
+    TS_ASSERT(
+        listType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(listType.getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << listType.getDType().getName()
+                         << endl
                          << "  is " << listType.mkGroundTerm() << endl;
     TS_ASSERT(listType.mkGroundTerm().getType() == listType);
   }
@@ -225,156 +241,192 @@ class DatatypeBlack : public CxxTest::TestSuite {
      *     list = cons(car: tree, cdr: list) | nil
      *   END;
      */
-    Datatype tree(d_em, "tree");
-    DatatypeConstructor node("node");
-    node.addArg("left", DatatypeSelfType());
-    node.addArg("right", DatatypeSelfType());
+    std::set<TypeNode> unresolvedTypes;
+    TypeNode unresList =
+        d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER);
+    unresolvedTypes.insert(unresList);
+    TypeNode unresTree =
+        d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER);
+    unresolvedTypes.insert(unresTree);
+
+    DType tree("tree");
+    std::shared_ptr<DTypeConstructor> node =
+        std::make_shared<DTypeConstructor>("node");
+    node->addArgSelf("left");
+    node->addArgSelf("right");
     tree.addConstructor(node);
 
-    DatatypeConstructor leaf("leaf");
-    leaf.addArg("leaf", DatatypeUnresolvedType("list"));
+    std::shared_ptr<DTypeConstructor> leaf =
+        std::make_shared<DTypeConstructor>("leaf");
+    leaf->addArg("leaf", unresList);
     tree.addConstructor(leaf);
 
     Debug("datatypes") << tree << std::endl;
 
-    Datatype list(d_em, "list");
-    DatatypeConstructor cons("cons");
-    cons.addArg("car", DatatypeUnresolvedType("tree"));
-    cons.addArg("cdr", DatatypeSelfType());
+    DType list("list");
+    std::shared_ptr<DTypeConstructor> cons =
+        std::make_shared<DTypeConstructor>("cons");
+    cons->addArg("car", unresTree);
+    cons->addArgSelf("cdr");
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil");
+    std::shared_ptr<DTypeConstructor> nil =
+        std::make_shared<DTypeConstructor>("nil");
     list.addConstructor(nil);
 
     Debug("datatypes") << list << std::endl;
 
     TS_ASSERT(! tree.isResolved());
-    TS_ASSERT(! node.isResolved());
-    TS_ASSERT(! leaf.isResolved());
     TS_ASSERT(! list.isResolved());
-    TS_ASSERT(! cons.isResolved());
-    TS_ASSERT(! nil.isResolved());
 
-    vector<Datatype> dts;
+    vector<DType> dts;
     dts.push_back(tree);
     dts.push_back(list);
-    vector<DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dts);
+    vector<TypeNode> dtts = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes);
 
-    TS_ASSERT(dtts[0].getDatatype().isResolved());
-    TS_ASSERT(dtts[1].getDatatype().isResolved());
+    TS_ASSERT(dtts[0].getDType().isResolved());
+    TS_ASSERT(dtts[1].getDType().isResolved());
 
-    TS_ASSERT(! dtts[0].getDatatype().isFinite());
-    TS_ASSERT(dtts[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(dtts[0].getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl
+    TS_ASSERT(!dtts[0].getDType().isFinite());
+    TS_ASSERT(dtts[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
+              == Cardinality::EQUAL);
+    TS_ASSERT(dtts[0].getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts[0].getDType().getName()
+                         << endl
                          << "  is " << dtts[0].mkGroundTerm() << endl;
     TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]);
 
-    TS_ASSERT(! dtts[1].getDatatype().isFinite());
-    TS_ASSERT(dtts[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(dtts[1].getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl
+    TS_ASSERT(!dtts[1].getDType().isFinite());
+    TS_ASSERT(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
+              == Cardinality::EQUAL);
+    TS_ASSERT(dtts[1].getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts[1].getDType().getName()
+                         << endl
                          << "  is " << dtts[1].mkGroundTerm() << endl;
     TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]);
   }
   void testMutualListTrees2()
   {
-    Datatype tree(d_em, "tree");
-    DatatypeConstructor node("node");
-    node.addArg("left", DatatypeSelfType());
-    node.addArg("right", DatatypeSelfType());
+    std::set<TypeNode> unresolvedTypes;
+    TypeNode unresList =
+        d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER);
+    unresolvedTypes.insert(unresList);
+    TypeNode unresTree =
+        d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER);
+    unresolvedTypes.insert(unresTree);
+
+    DType tree("tree");
+    std::shared_ptr<DTypeConstructor> node =
+        std::make_shared<DTypeConstructor>("node");
+    node->addArgSelf("left");
+    node->addArgSelf("right");
     tree.addConstructor(node);
 
-    DatatypeConstructor leaf("leaf");
-    leaf.addArg("leaf", DatatypeUnresolvedType("list"));
+    std::shared_ptr<DTypeConstructor> leaf =
+        std::make_shared<DTypeConstructor>("leaf");
+    leaf->addArg("leaf", unresList);
     tree.addConstructor(leaf);
 
-    Datatype list(d_em, "list");
-    DatatypeConstructor cons("cons");
-    cons.addArg("car", DatatypeUnresolvedType("tree"));
-    cons.addArg("cdr", DatatypeSelfType());
+    DType list("list");
+    std::shared_ptr<DTypeConstructor> cons =
+        std::make_shared<DTypeConstructor>("cons");
+    cons->addArg("car", unresTree);
+    cons->addArgSelf("cdr");
     list.addConstructor(cons);
 
-    DatatypeConstructor nil("nil");
+    std::shared_ptr<DTypeConstructor> nil =
+        std::make_shared<DTypeConstructor>("nil");
     list.addConstructor(nil);
 
     // add another constructor to list datatype resulting in an
     // "otherNil-list"
-    DatatypeConstructor otherNil("otherNil");
+    std::shared_ptr<DTypeConstructor> otherNil =
+        std::make_shared<DTypeConstructor>("otherNil");
     list.addConstructor(otherNil);
 
-    vector<Datatype> dts;
+    vector<DType> dts;
     dts.push_back(tree);
     dts.push_back(list);
     // remake the types
-    vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts);
-
-    TS_ASSERT(! dtts2[0].getDatatype().isFinite());
-    TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(dtts2[0].getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl
+    vector<TypeNode> dtts2 = d_nm->mkMutualDatatypeTypes(dts, unresolvedTypes);
+
+    TS_ASSERT(!dtts2[0].getDType().isFinite());
+    TS_ASSERT(
+        dtts2[0].getDType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(dtts2[0].getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName()
+                         << endl
                          << "  is " << dtts2[0].mkGroundTerm() << endl;
     TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
 
-    TS_ASSERT(! dtts2[1].getDatatype().isParametric());
-    TS_ASSERT(! dtts2[1].getDatatype().isFinite());
-    TS_ASSERT(dtts2[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(dtts2[1].getDatatype().isWellFounded());
-    Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl
+    TS_ASSERT(!dtts2[1].getDType().isParametric());
+    TS_ASSERT(!dtts2[1].getDType().isFinite());
+    TS_ASSERT(
+        dtts2[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(dtts2[1].getDType().isWellFounded());
+    Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName()
+                         << endl
                          << "  is " << dtts2[1].mkGroundTerm() << endl;
     TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
   }
 
   void testNotSoWellFounded() {
-    Datatype tree(d_em, "tree");
+    DType tree("tree");
 
-    DatatypeConstructor node("node");
-    node.addArg("left", DatatypeSelfType());
-    node.addArg("right", DatatypeSelfType());
+    std::shared_ptr<DTypeConstructor> node =
+        std::make_shared<DTypeConstructor>("node");
+    node->addArgSelf("left");
+    node->addArgSelf("right");
     tree.addConstructor(node);
 
     Debug("datatypes") << tree << std::endl;
-    DatatypeType treeType = d_em->mkDatatypeType(tree);
+    TypeNode treeType = d_nm->mkDatatypeType(tree);
     Debug("datatypes") << treeType << std::endl;
 
-    TS_ASSERT(! treeType.getDatatype().isParametric());
-    TS_ASSERT(! treeType.getDatatype().isFinite());
-    TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
-    TS_ASSERT(! treeType.getDatatype().isWellFounded());
-    TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() );
-    TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) );
+    TS_ASSERT(!treeType.getDType().isParametric());
+    TS_ASSERT(!treeType.getDType().isFinite());
+    TS_ASSERT(
+        treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(!treeType.getDType().isWellFounded());
+    TS_ASSERT(treeType.mkGroundTerm().isNull());
+    TS_ASSERT(treeType.getDType().mkGroundTerm(treeType).isNull());
   }
 
-  void testParametricDatatype() {
-    vector<Type> v;
-    Type t1, t2;
-    v.push_back(t1 = d_em->mkSort("T1"));
-    v.push_back(t2 = d_em->mkSort("T2"));
-    Datatype pair(d_em, "pair", v);
-
-    DatatypeConstructor mkpair("mk-pair");
-    mkpair.addArg("first", t1);
-    mkpair.addArg("second", t2);
+  void testParametricDType()
+  {
+    vector<TypeNode> v;
+    TypeNode t1, t2;
+    v.push_back(t1 = d_nm->mkSort("T1"));
+    v.push_back(t2 = d_nm->mkSort("T2"));
+    DType pair("pair", v);
+
+    std::shared_ptr<DTypeConstructor> mkpair =
+        std::make_shared<DTypeConstructor>("mk-pair");
+    mkpair->addArg("first", t1);
+    mkpair->addArg("second", t2);
     pair.addConstructor(mkpair);
-    DatatypeType pairType = d_em->mkDatatypeType(pair);
+    TypeNode pairType = d_nm->mkDatatypeType(pair);
 
-    TS_ASSERT(pairType.getDatatype().isParametric());
+    TS_ASSERT(pairType.getDType().isParametric());
     v.clear();
-    v.push_back(d_em->integerType());
-    v.push_back(d_em->integerType());
-    DatatypeType pairIntInt = pairType.getDatatype().getDatatypeType(v);
+    v.push_back(d_nm->integerType());
+    v.push_back(d_nm->integerType());
+    TypeNode pairIntInt = pairType.getDType().getTypeNode(v);
     v.clear();
-    v.push_back(d_em->realType());
-    v.push_back(d_em->realType());
-    DatatypeType pairRealReal = pairType.getDatatype().getDatatypeType(v);
+    v.push_back(d_nm->realType());
+    v.push_back(d_nm->realType());
+    TypeNode pairRealReal = pairType.getDType().getTypeNode(v);
     v.clear();
-    v.push_back(d_em->realType());
-    v.push_back(d_em->integerType());
-    DatatypeType pairRealInt = pairType.getDatatype().getDatatypeType(v);
+    v.push_back(d_nm->realType());
+    v.push_back(d_nm->integerType());
+    TypeNode pairRealInt = pairType.getDType().getTypeNode(v);
     v.clear();
-    v.push_back(d_em->integerType());
-    v.push_back(d_em->realType());
-    DatatypeType pairIntReal = pairType.getDatatype().getDatatypeType(v);
+    v.push_back(d_nm->integerType());
+    v.push_back(d_nm->realType());
+    TypeNode pairIntReal = pairType.getDType().getTypeNode(v);
 
     TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
     TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
@@ -417,26 +469,34 @@ class DatatypeBlack : public CxxTest::TestSuite {
     TS_ASSERT(!pairRealInt.isSubtypeOf(pairIntInt));
     TS_ASSERT(pairIntInt.isSubtypeOf(pairIntInt));
 
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealReal)).toType(), pairRealReal);
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealReal)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealReal)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealReal)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairRealInt)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairRealInt)).isNull());
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairRealInt)).toType(), pairRealInt);
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairRealInt)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntReal)).isNull());
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntReal)).toType(), pairIntReal);
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntReal)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntReal)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealReal), TypeNode::fromType(pairIntInt)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntReal), TypeNode::fromType(pairIntInt)).isNull());
-    TS_ASSERT(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairRealInt), TypeNode::fromType(pairIntInt)).isNull());
-    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt);
+    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealReal, pairRealReal),
+                     pairRealReal);
+    TS_ASSERT(
+        TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull());
+    TS_ASSERT(
+        TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull());
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull());
+    TS_ASSERT(
+        TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull());
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull());
+    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt),
+                     pairRealInt);
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull());
+    TS_ASSERT(
+        TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull());
+    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal),
+                     pairIntReal);
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull());
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull());
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull());
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull());
+    TS_ASSERT(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull());
+    TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt),
+                     pairIntInt);
   }
 
  private:
   api::Solver* d_slv;
-  ExprManager* d_em;
-  ExprManagerScope* d_scope;
-};/* class DatatypeBlack */
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+}; /* class DTypeBlack */