Eliminate Expr-level calls in TypeNode (#3562)

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 31f21667aa1042c1e408a208cecc12488180dfee..99fe73c22208a66d53378d4e45e1d09a89beec70 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -98,7 +98,12 @@ bool Type::isFunctionLike() const
 
 Expr Type::mkGroundTerm() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->mkGroundTerm().toExpr();
+  Expr ret = d_typeNode->mkGroundTerm().toExpr();
+  if (ret.isNull())
+  {
+    IllegalArgument(this, "Cannot construct ground term!");
+  }
+  return ret;
 }
 
 Expr Type::mkGroundValue() const
@@ -326,7 +331,8 @@ bool Type::isTuple() const {
 /** Is this a record type? */
 bool Type::isRecord() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isRecord();
+  return d_typeNode->getKind() == kind::DATATYPE_TYPE
+         && DatatypeType(*this).getDatatype().isRecord();
 }
 
 /** Is this a symbolic expression type? */
@@ -566,7 +572,14 @@ std::vector<Type> ConstructorType::getArgTypes() const {
 
 const Datatype& DatatypeType::getDatatype() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getDatatype();
+  Assert(isDatatype());
+  if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
+  {
+    DatatypeIndexConstant dic = d_typeNode->getConst<DatatypeIndexConstant>();
+    return d_nodeManager->getDatatypeForIndex(dic.getIndex());
+  }
+  Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE);
+  return DatatypeType((*d_typeNode)[0].toType()).getDatatype();
 }
 
 bool DatatypeType::isParametric() const {
@@ -636,7 +649,9 @@ std::vector<Type> DatatypeType::getTupleTypes() const {
 /** Get the description of the record type */
 const Record& DatatypeType::getRecord() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getRecord();
+  Assert(isRecord());
+  const Datatype& dt = getDatatype();
+  return *(dt.getRecord());
 }
 
 DatatypeType SelectorType::getDomain() const {

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8cc10b5b20d78ce5a0730e9d207a60c1fb3511b5..abca1e3ed5a5e969786dc6312279b9c091bc1f1b 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -141,9 +141,8 @@ bool TypeNode::isFiniteInternal(bool usortFinite)
     if (isDatatype())
     {
       TypeNode tn = *this;
-      const Datatype& dt = getDatatype();
-      ret = usortFinite ? dt.isInterpretedFinite(tn.toType())
-                        : dt.isFinite(tn.toType());
+      const DType& dt = getDType();
+      ret = usortFinite ? dt.isInterpretedFinite(tn) : dt.isFinite(tn);
     }
     else if (isArray())
     {
@@ -250,12 +249,12 @@ bool TypeNode::isClosedEnumerable()
       setAttribute(IsClosedEnumerableAttr(), ret);
       setAttribute(IsClosedEnumerableComputedAttr(), true);
       TypeNode tn = *this;
-      const Datatype& dt = getDatatype();
+      const DType& dt = getDType();
       for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
       {
         for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
         {
-          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+          TypeNode ctn = dt[i][j].getRangeType();
           if (tn != ctn && !ctn.isClosedEnumerable())
           {
             ret = false;
@@ -351,12 +350,11 @@ TypeNode TypeNode::getBaseType() const {
   if (isSubtypeOf(realt)) {
     return realt;
   } else if (isParametricDatatype()) {
-    vector<Type> v;
+    std::vector<TypeNode> v;
     for(size_t i = 1; i < getNumChildren(); ++i) {
-      v.push_back((*this)[i].getBaseType().toType());
+      v.push_back((*this)[i].getBaseType());
     }
-    TypeNode tn = TypeNode::fromType((*this)[0].getDatatype().getDatatypeType(v));
-    return tn;
+    return (*this)[0].getDType().getTypeNode().instantiateParametricDatatype(v);
   }
   return *this;
 }
@@ -387,39 +385,27 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
 
 /** Is this a tuple type? */
 bool TypeNode::isTuple() const {
-  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() );
-}
-
-/** Is this a record type? */
-bool TypeNode::isRecord() const {
-  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() );
+  return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple());
 }
 
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
-  const Datatype& dt = getDatatype();
+  const DType& dt = getDType();
   Assert(dt.getNumConstructors() == 1);
   return dt[0].getNumArgs();
 }
 
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
-  const Datatype& dt = getDatatype();
+  const DType& dt = getDType();
   Assert(dt.getNumConstructors() == 1);
   vector<TypeNode> types;
   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
-    types.push_back(TypeNode::fromType(dt[0][i].getRangeType()));
+    types.push_back(dt[0][i].getRangeType());
   }
   return types;
 }
 
-const Record& TypeNode::getRecord() const {
-  Assert(isRecord());
-  const Datatype & dt = getDatatype();
-  return *(dt.getRecord());
-  //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
-}
-
 vector<TypeNode> TypeNode::getSExprTypes() const {
   Assert(isSExpr());
   vector<TypeNode> types;
@@ -437,11 +423,12 @@ bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() != kind::PARAMETRIC_DATATYPE) {
     return false;
   }
-  const Datatype& dt = (*this)[0].getDatatype();
+  const DType& dt = (*this)[0].getDType();
   unsigned n = dt.getNumParameters();
   Assert(n < getNumChildren());
   for(unsigned i = 0; i < n; ++i) {
-    if(TypeNode::fromType(dt.getParameter(i)) == (*this)[i + 1]) {
+    if (dt.getParameter(i) == (*this)[i + 1])
+    {
       return false;
     }
   }
@@ -473,9 +460,9 @@ TypeNode TypeNode::instantiateSortConstructor(
 /** Is this an instantiated datatype parameter */
 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
-  const Datatype& dt = (*this)[0].getDatatype();
+  const DType& dt = (*this)[0].getDType();
   AssertArgument(n < dt.getNumParameters(), *this);
-  return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
+  return dt.getParameter(n) != (*this)[n + 1];
 }
 
 TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
@@ -601,13 +588,15 @@ Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
       }
     }else if( tn.isDatatype() && ntn.isDatatype() ){
       if( tn.isTuple() && ntn.isTuple() ){
-        const Datatype& dt1 = tn.getDatatype();
-        const Datatype& dt2 = ntn.getDatatype();
+        const DType& dt1 = tn.getDType();
+        const DType& dt2 = ntn.getDType();
+        NodeManager* nm = NodeManager::currentNM();
         if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
           std::vector< Node > conds;
           for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
-            Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt2[0][i].getSelector() ), n );
-            Node etc = getEnsureTypeCondition( s, TypeNode::fromType( dt1[0][i].getRangeType() ) );
+            Node s = nm->mkNode(
+                kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n);
+            Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType());
             if( etc.isNull() ){
               return Node::null();
             }else{
@@ -615,11 +604,11 @@ Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
             }
           }
           if( conds.empty() ){
-            return NodeManager::currentNM()->mkConst( true );
+            return nm->mkConst(true);
           }else if( conds.size()==1 ){
             return conds[0];
           }else{
-            return NodeManager::currentNM()->mkNode( kind::AND, conds );
+            return nm->mkNode(kind::AND, conds);
           }
         }
       }
@@ -640,6 +629,16 @@ bool TypeNode::isSortConstructor() const {
   return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 }
 
+/** Is this a codatatype type */
+bool TypeNode::isCodatatype() const
+{
+  if (isDatatype())
+  {
+    return getDType().isCodatatype();
+  }
+  return false;
+}
+
 std::string TypeNode::toString() const {
   std::stringstream ss;
   OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index b1c4da026aa0cc541ce847fce8175f4fc6f4eb57..017ffe3ddac4b87508a2803a41beac7e219d26c6 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -597,12 +597,6 @@ public:
   /** Get the constituent types of a tuple type */
   std::vector<TypeNode> getTupleTypes() const;
 
-  /** Is this a record type? */
-  bool isRecord() const;
-
-  /** Get the description of the record type */
-  const Record& getRecord() const;
-
   /** Is this a symbolic expression type? */
   bool isSExpr() const;
 
@@ -659,9 +653,6 @@ public:
   /** Is this a tester type */
   bool isTester() const;
 
-  /** Get the Datatype specification from a datatype type */
-  const Datatype& getDatatype() const;
-
   /** Get the internal Datatype specification from a datatype type */
   const DType& getDType() const;
 
@@ -1027,15 +1018,6 @@ inline bool TypeNode::isParametricDatatype() const {
   return getKind() == kind::PARAMETRIC_DATATYPE;
 }
 
-/** Is this a codatatype type */
-inline bool TypeNode::isCodatatype() const {
-  if( isDatatype() ){
-    return getDatatype().isCodatatype();
-  }else{
-    return false;
-  }
-}
-
 /** Is this a constructor type */
 inline bool TypeNode::isConstructor() const {
   return getKind() == kind::CONSTRUCTOR_TYPE;
@@ -1066,18 +1048,6 @@ inline bool TypeNode::isBitVector(unsigned size) const {
     ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size );
 }
 
-/** Get the datatype specification from a datatype type */
-inline const Datatype& TypeNode::getDatatype() const {
-  Assert(isDatatype());
-  if( getKind() == kind::DATATYPE_TYPE ){
-    DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
-    return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
-  }else{
-    Assert(getKind() == kind::PARAMETRIC_DATATYPE);
-    return (*this)[0].getDatatype();
-  }
-}
-
 /** Get the exponent size of this floating-point type */
 inline unsigned TypeNode::getFloatingPointExponentSize() const {
   Assert(isFloatingPoint());

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 47e64b2e4d2f0f54b4c249f62c6013a04e057b13..f3ca65b79cc01c04e4788d99425f5308f76b8659 100644 (file)
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -417,7 +417,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
                            0);
       Trace("srs-input-debug")
           << "Grammar for subterm " << n << " is: " << std::endl;
-      Trace("srs-input-debug") << subtermTypes[n].getDatatype() << std::endl;
+      Trace("srs-input-debug") << subtermTypes[n].getDType() << std::endl;
     }
     // set that this is a sygus datatype
     sdttl.initializeDatatype(t, sygusVarList, false, false);

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b11ee77a7108989c2f95df02654fc64b794f32a9..22a491af54e7be4e9b7720ba91c3f84707ae26e7 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -373,8 +373,10 @@ void CvcPrinter::toStream(
           if( n.getNumChildren()==1 ){
             out << "TUPLE";
           }
-        }else if( t.isRecord() ){
-          const Record& rec = t.getRecord();
+        }
+        else if (t.toType().isRecord())
+        {
+          const Record& rec = static_cast<DatatypeType>(t.toType()).getRecord();
           out << "(# ";
           TNode::iterator i = n.begin();
           bool first = true;
@@ -389,7 +391,9 @@ void CvcPrinter::toStream(
           }
           out << " #)";
           return;
-        }else{
+        }
+        else
+        {
           toStream(op, n.getOperator(), depth, types, false);
           if (n.getNumChildren() == 0)
           {
@@ -404,7 +408,12 @@ void CvcPrinter::toStream(
     case kind::APPLY_SELECTOR_TOTAL: {
         TypeNode t = n[0].getType();
         Node opn = n.getOperator();
-        if (t.isTuple() || t.isRecord())
+        if (!t.isDatatype())
+        {
+          toStream(op, opn, depth, types, false);
+        }
+        else if (t.isTuple()
+                 || DatatypeType(t.toType()).isRecord())
         {
           toStream(out, n[0], depth, types, true);
           out << '.';
@@ -434,7 +443,7 @@ void CvcPrinter::toStream(
       }
       break;
     case kind::APPLY_TESTER: {
-      Assert(!n.getType().isTuple() && !n.getType().isRecord());
+      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());

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 22d13da0c72231f6a6cd7f0e1ca3f4b90413a074..e3c09b63510f0f8ca0f539329bcc92d6b2f167ed 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -44,11 +44,11 @@ constant DATATYPE_TYPE \
     "expr/datatype.h" \
     "a datatype type index"
 cardinality DATATYPE_TYPE \
-    "%TYPE%.getDatatype().getCardinality(%TYPE%.toType())" \
+    "%TYPE%.getDType().getCardinality(%TYPE%)" \
     "expr/datatype.h"
 well-founded DATATYPE_TYPE \
-    "%TYPE%.getDatatype().isWellFounded()" \
-    "%TYPE%.getDatatype().mkGroundTerm(%TYPE%.toType())" \
+    "%TYPE%.getDType().isWellFounded()" \
+    "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
     "expr/datatype.h"
 
 enumerator DATATYPE_TYPE \
@@ -57,11 +57,11 @@ enumerator DATATYPE_TYPE \
 
 operator PARAMETRIC_DATATYPE 1: "parametric datatype"
 cardinality PARAMETRIC_DATATYPE \
-    "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality(%TYPE%.toType())" \
+    "%TYPE%.getDType().getCardinality(%TYPE%)" \
     "expr/datatype.h"
 well-founded PARAMETRIC_DATATYPE \
-    "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
-    "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
+    "%TYPE%.getDType().isWellFounded()" \
+    "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
     "expr/datatype.h"
 
 enumerator PARAMETRIC_DATATYPE \

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 5e071c85c0ac963d58206cabc6a62d64a8b676fc..cf07bc0c1778c838ab629e39c5099e90274f6427 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -631,8 +631,9 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
       }
       else
       {
-        Assert(t.isRecord());
-        const Record& record = t.getRecord();
+        Assert(t.toType().isRecord());
+        const Record& record =
+            DatatypeType(t.toType()).getRecord();
         size = record.getNumFields();
         updateIndex = record.getIndex(
             n.getOperator().getConst<RecordUpdate>().getField());

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 97e67e7faa12b64560983b7e0c5ee9aba13e4070..e11ac67f135157f0c9f5faa399c1e89c0bc0b7da 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -287,11 +287,13 @@ struct RecordUpdateTypeRule {
     TypeNode recordType = n[0].getType(check);
     TypeNode newValue = n[1].getType(check);
     if (check) {
-      if (!recordType.isRecord()) {
+      if (!recordType.toType().isRecord())
+      {
         throw TypeCheckingExceptionPrivate(
             n, "Record-update expression formed over non-record");
       }
-      const Record& rec = recordType.getRecord();
+      const Record& rec =
+          DatatypeType(recordType.toType()).getRecord();
       if (!rec.contains(ru.getField())) {
         std::stringstream ss;
         ss << "Record-update field `" << ru.getField()

diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index 2fe8a99fef628bced5e5cb1785363bd93c8f52b4..cb9ab1e300fbecd69a38f7b459671e728c101752 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -489,7 +489,7 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args)
     if (it == visited.end())
     {
       TypeNode tn = cur.getType();
-      if (!tn.isDatatype() || !tn.getDatatype().isSygus())
+      if (!tn.isDatatype() || !tn.getDType().isSygus())
       {
         visited[cur] = cur;
       }
@@ -502,7 +502,7 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args)
         {
           svarsInit = true;
           TypeNode tn = cur.getType();
-          Node varList = Node::fromExpr(tn.getDatatype().getSygusVarList());
+          Node varList = tn.getDType().getSygusVarList();
           for (const Node& v : varList)
           {
             svars.push_back(v);

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 4727ab0b021ac04aded2f596024b6bfca66d1cec..8c005bd3ce303846ef67d03734e5395d2e9a9c7c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -49,7 +49,7 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q)
     if (!gv.isNull())
     {
       TypeNode tn = gv.getType();
-      if (tn.isDatatype() && tn.getDatatype().isSygus())
+      if (tn.isDatatype() && tn.getDType().isSygus())
       {
         return true;
       }
@@ -137,9 +137,9 @@ Node CegGrammarConstructor::process(Node q,
     std::stringstream ss;
     ss << sf;
     Node sfvl;
-    if (preGrammarType.isDatatype() && preGrammarType.getDatatype().isSygus())
+    if (preGrammarType.isDatatype() && preGrammarType.getDType().isSygus())
     {
-      sfvl = Node::fromExpr(preGrammarType.getDatatype().getSygusVarList());
+      sfvl = preGrammarType.getDType().getSygusVarList();
       tn = preGrammarType;
     }else{
       sfvl = getSygusVarList(sf);
@@ -260,7 +260,7 @@ Node CegGrammarConstructor::process(Node q,
     }
     tds->registerSygusType(tn);
     Assert(tn.isDatatype());
-    const Datatype& dt = tn.getDatatype();
+    const DType& dt = tn.getDType();
     Assert(dt.isSygus());
     if( !dt.getSygusAllowAll() ){
       d_is_syntax_restricted = true;
@@ -427,13 +427,13 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
       Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
       types.push_back( range );
       if( range.isDatatype() ){
-        const Datatype& dt = range.getDatatype();
+        const DType& dt = range.getDType();
         for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
         {
           for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
                ++j)
           {
-            TypeNode tn = TypeNode::fromType(dt[i][j].getRangeType());
+            TypeNode tn = dt[i][j].getRangeType();
             collectSygusGrammarTypesFor(tn, types);
           }
         }
@@ -817,11 +817,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     else if (types[i].isDatatype())
     {
       Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
-      const Datatype& dt = types[i].getDatatype();
+      const DType& dt = types[i].getDType();
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
         Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
-        Node cop = Node::fromExpr(dt[k].getConstructor());
+        Node cop = dt[k].getConstructor();
         if (dt[k].getNumArgs() == 0)
         {
           // Nullary constructors are interpreted as terms, not operators.
@@ -834,7 +834,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         {
           Trace("sygus-grammar-def")
               << "...for " << dt[k][j].getName() << std::endl;
-          TypeNode crange = TypeNode::fromType(dt[k][j].getRangeType());
+          TypeNode crange = dt[k][j].getRangeType();
           Assert(type_to_unres.find(crange) != type_to_unres.end());
           cargsCons.push_back(type_to_unres[crange]);
           // add to the selector type the selector operator
@@ -842,12 +842,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
           Assert(std::find(types.begin(), types.end(), crange) != types.end());
           unsigned i_selType = std::distance(
               types.begin(), std::find(types.begin(), types.end(), crange));
-          TypeNode arg_type = TypeNode::fromType(dt[k][j].getType());
+          TypeNode arg_type = dt[k][j].getType();
           arg_type = arg_type.getSelectorDomainType();
           Assert(type_to_unres.find(arg_type) != type_to_unres.end());
           std::vector<TypeNode> cargsSel;
           cargsSel.push_back(type_to_unres[arg_type]);
-          Node sel = Node::fromExpr(dt[k][j].getSelector());
+          Node sel = dt[k][j].getSelector();
           sdts[i_selType].addConstructor(sel, dt[k][j].getName(), cargsSel);
         }
         sdts[i].addConstructor(cop, dt[k].getName(), cargsCons);
@@ -1175,14 +1175,16 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     {
       //add for testers
       Trace("sygus-grammar-def") << "...add for testers" << std::endl;
-      const Datatype& dt = types[i].getDatatype();
+      const DType& dt = types[i].getDType();
       std::vector<TypeNode> cargsTester;
       cargsTester.push_back(unres_types[iuse]);
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
-        Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
-        sdtBool.addConstructor(
-            dt[k].getTester(), dt[k].getTesterName(), cargsTester);
+        Trace("sygus-grammar-def")
+            << "...for " << dt[k].getTester() << std::endl;
+        std::stringstream sst;
+        sst << dt[k].getTester();
+        sdtBool.addConstructor(dt[k].getTester(), sst.str(), cargsTester);
       }
     }
   }

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 019abc28a44178063253a8a233c98575fce98ee4..c7c1d820fa3be66dc565deae9d8e31deddda15cf 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -599,7 +599,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
     return tn;
   }
   /* Collect all operators for normalization */
-  const Datatype& dt = tn.getDatatype();
+  const Datatype& dt = DatatypeType(tn.toType()).getDatatype();
   if (!dt.isSygus())
   {
     // datatype but not sygus datatype case