Remove dependency of `TypeNode` on `Node` (#7690)

This is further work towards breaking cyclic dependencies in the `expr`
folder.

23 files changed, 179 insertions, 158 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index a6a7c04e9..9a89dfbe6 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -105,6 +105,7 @@ libcvc5_add_sources(GENERATED
   metakind.h
   node_manager.cpp
   type_checker.cpp
+  type_properties.cpp
   type_properties.h
 )
 
@@ -147,6 +148,16 @@ add_custom_command(
 )
 
 add_custom_command(
+  OUTPUT type_properties.cpp
+  COMMAND
+    ${mkkind_script}
+    ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.cpp
+    ${KINDS_FILES}
+    > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.cpp
+  DEPENDS mkkind type_properties_template.cpp type_properties.h ${KINDS_FILES}
+)
+
+add_custom_command(
   OUTPUT metakind.h
   COMMAND
     ${mkmetakind_script}
@@ -194,5 +205,6 @@ add_custom_target(gen-expr
     metakind.h
     node_manager.cpp
     type_checker.cpp
+    type_properties.cpp
     type_properties.h
 )
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index a5719a7ff..5b2503454 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -278,7 +278,8 @@ void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll)
     if (!hasConstant)
     {
       // add an arbitrary one
-      Node op = st.mkGroundTerm();
+      NodeManager* nm = NodeManager::currentNM();
+      Node op = nm->mkGroundTerm(st);
       // use same naming convention as SygusDatatype
       std::stringstream ss;
       ss << getName() << "_" << getNumConstructors() << "_" << op;
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index f23cfa4f9..6ba3970c9 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -410,7 +410,7 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t,
     else
     {
       // call mkGroundValue or mkGroundTerm based on isValue
-      arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
+      arg = isValue ? nm->mkGroundValue(selType) : nm->mkGroundTerm(selType);
     }
     if (arg.isNull())
     {
diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
index b72aa99f6..3b165ded8 100644
--- a/src/expr/node_converter.cpp
+++ b/src/expr/node_converter.cpp
@@ -199,7 +199,7 @@ TypeNode NodeConverter::convertType(TypeNode tn)
         if (ret.getMetaKind() == kind::metakind::PARAMETERIZED)
         {
           // push the operator
-          nb << ret.getOperator();
+          nb << NodeManager::operatorFromType(ret);
         }
         for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();
              j != iend;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5b74b04e1..6435c488a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -73,6 +73,18 @@ class NodeManager
    */
   static bool isNAryKind(Kind k);
 
+  /**
+   * Returns a node representing the operator of this `TypeNode`.
+   * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) have an
+   * operator. "Little-p parameterized" types (like Array), are OPERATORs, not
+   * PARAMETERIZEDs.
+   */
+  static Node operatorFromType(const TypeNode& tn)
+  {
+    Assert(tn.getMetaKind() == kind::metakind::PARAMETERIZED);
+    return Node(tn.d_nv->getOperator());
+  }
+
  private:
   /**
    * Instead of creating an instance using the constructor,
@@ -448,6 +460,24 @@ class NodeManager
 
   Node mkBoundVar(const TypeNode& type);
 
+  /**
+   * Construct and return a ground term of a given type. If the type is not
+   * well founded, this function throws an exception.
+   *
+   * @param tn The type
+   * @return a ground term of the type
+   */
+  Node mkGroundTerm(const TypeNode& tn);
+
+  /**
+   * Construct and return a ground value of a given type. If the type is not
+   * well founded, this function throws an exception.
+   *
+   * @param tn The type
+   * @return a ground value of the type
+   */
+  Node mkGroundValue(const TypeNode& tn);
+
   /** get the canonical bound variable list for function type tn */
   Node getBoundVarListForFunctionType( TypeNode tn );
 
diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 06f5bcfb6..a3e267d95 100644
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -29,8 +29,10 @@
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
+#include "expr/type_properties.h"
 #include "theory/bags/bag_make_op.h"
 #include "theory/sets/singleton_op.h"
+#include "theory/type_enumerator.h"
 #include "util/abstract_value.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
@@ -1216,6 +1218,17 @@ NodeClass NodeManager::mkConstInternal(Kind k, const T& val)
   return NodeClass(nv);
 }
 
+Node NodeManager::mkGroundTerm(const TypeNode& tn)
+{
+  return kind::mkGroundTerm(tn);
+}
+
+Node NodeManager::mkGroundValue(const TypeNode& tn)
+{
+  theory::TypeEnumerator te(tn);
+  return *te;
+}
+
 bool NodeManager::safeToReclaimZombies() const
 {
   // FIXME multithreading
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index e94d4733e..8358facac 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -264,16 +264,6 @@ bool TypeNode::isWellFounded() const {
   return kind::isWellFounded(*this);
 }
 
-Node TypeNode::mkGroundTerm() const {
-  return kind::mkGroundTerm(*this);
-}
-
-Node TypeNode::mkGroundValue() const
-{
-  theory::TypeEnumerator te(*this);
-  return *te;
-}
-
 bool TypeNode::isStringLike() const { return isString() || isSequence(); }
 
 // !!! Note that this will change to isReal() || isInteger() when subtyping is
@@ -560,47 +550,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   }
 }
 
-Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
-  TypeNode ntn = n.getType();
-  Assert(ntn.isComparableTo(tn));
-  if( !ntn.isSubtypeOf( tn ) ){
-    if( tn.isInteger() ){
-      if( tn.isSubtypeOf( ntn ) ){
-        return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
-      }
-    }else if( tn.isDatatype() && ntn.isDatatype() ){
-      if( tn.isTuple() && ntn.isTuple() ){
-        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 = 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{
-              conds.push_back( etc );
-            }
-          }
-          if( conds.empty() ){
-            return nm->mkConst(true);
-          }else if( conds.size()==1 ){
-            return conds[0];
-          }else{
-            return nm->mkNode(kind::AND, conds);
-          }
-        }
-      }
-    }
-    return Node::null();
-  }else{
-    return NodeManager::currentNM()->mkConst( true );
-  }
-}
-
 /** Is this a sort kind */
 bool TypeNode::isSort() const {
   return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
@@ -698,6 +647,17 @@ uint32_t TypeNode::getBitVectorSize() const
   return getConst<BitVectorSize>();
 }
 
+TypeNode TypeNode::getRangeType() const
+{
+  if (isTester())
+  {
+    return NodeManager::currentNM()->booleanType();
+  }
+  Assert(isFunction() || isConstructor() || isSelector())
+      << "Cannot get range type of " << *this;
+  return (*this)[getNumChildren() - 1];
+}
+
 }  // namespace cvc5
 
 namespace std {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 33d698163..9882c7fc5 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -218,16 +218,6 @@ private:
   }
 
   /**
-   * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these)
-   * have an operator.  "Little-p parameterized" types (like Array),
-   * are OPERATORs, not PARAMETERIZEDs.
-   */
-  inline Node getOperator() const {
-    Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
-    return Node(d_nv->getOperator());
-  }
-
-  /**
    * Returns the unique id of this node
    *
    * @return the id
@@ -443,22 +433,6 @@ private:
   bool isWellFounded() const;
 
   /**
-   * Construct and return a ground term of this type.  If the type is
-   * not well founded, this function throws an exception.
-   *
-   * @return a ground term of the type
-   */
-  Node mkGroundTerm() const;
-
-  /**
-   * Construct and return a ground value of this type.  If the type is
-   * not well founded, this function throws an exception.
-   *
-   * @return a ground value of the type
-   */
-  Node mkGroundValue() const;
-
-  /**
    * Is this type a subtype of the given type?
    */
   bool isSubtypeOf(TypeNode t) const;
@@ -699,10 +673,6 @@ private:
   static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
   static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1);
 
-  /** get ensure type condition
-   *  Return value is a condition that implies that n has type tn.
-  */
-  static Node getEnsureTypeCondition( Node n, TypeNode tn );
 private:
   static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
 
@@ -975,15 +945,6 @@ inline bool TypeNode::isPredicateLike() const {
   return isFunctionLike() && getRangeType().isBoolean();
 }
 
-inline TypeNode TypeNode::getRangeType() const {
-  if(isTester()) {
-    return NodeManager::currentNM()->booleanType();
-  }
-  Assert(isFunction() || isConstructor() || isSelector())
-      << "Cannot get range type of " << *this;
-  return (*this)[getNumChildren() - 1];
-}
-
 /** Is this a floating-point type of with <code>exp</code> exponent bits
     and <code>sig</code> significand bits */
 inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
diff --git a/src/expr/type_properties_template.cpp b/src/expr/type_properties_template.cpp
new file mode 100644
index 000000000..1ad2572d7
--- /dev/null
+++ b/src/expr/type_properties_template.cpp
@@ -0,0 +1,51 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Template for the Type properties source file.
+ */
+
+#include "expr/type_properties.h"
+
+namespace cvc5 {
+namespace kind {
+
+Node mkGroundTerm(TypeConstant tc)
+{
+  switch (tc)
+  {
+    // clang-format off
+${type_constant_groundterms}
+      // clang-format on
+    default:
+      InternalError() << "No ground term known for type constant: " << tc;
+  }
+}
+
+Node mkGroundTerm(TypeNode typeNode)
+{
+  AssertArgument(!typeNode.isNull(), typeNode);
+  switch (Kind k = typeNode.getKind())
+  {
+    case TYPE_CONSTANT:
+      return mkGroundTerm(typeNode.getConst<TypeConstant>());
+      // clang-format off
+${type_groundterms}
+      // clang-format on
+    default:
+      InternalError() << "A theory kinds file did not provide a ground term "
+                      << "or ground term computer for type:\n"
+                      << typeNode << "\nof kind " << k;
+  }
+}
+
+}  // namespace kind
+}  // namespace cvc5
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 40ead9a5e..3ce3391dc 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -97,34 +97,8 @@ ${type_wellfoundednesses}
   }
 }/* isWellFounded(TypeNode) */
 
-inline Node mkGroundTerm(TypeConstant tc)
-{
-  switch (tc)
-  {
-    // clang-format off
-${type_constant_groundterms}
-      // clang-format on
-    default:
-      InternalError() << "No ground term known for type constant: " << tc;
-  }
-} /* mkGroundTerm(TypeConstant) */
-
-inline Node mkGroundTerm(TypeNode typeNode)
-{
-  AssertArgument(!typeNode.isNull(), typeNode);
-  switch (Kind k = typeNode.getKind())
-  {
-    case TYPE_CONSTANT:
-      return mkGroundTerm(typeNode.getConst<TypeConstant>());
-      // clang-format off
-${type_groundterms}
-      // clang-format on
-    default:
-      InternalError() << "A theory kinds file did not provide a ground term "
-                      << "or ground term computer for type:\n"
-                      << typeNode << "\nof kind " << k;
-  }
-} /* mkGroundTerm(TypeNode) */
+Node mkGroundTerm(TypeConstant tc);
+Node mkGroundTerm(TypeNode typeNode);
 
 }  // namespace kind
 }  // namespace cvc5
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index a389c6efb..7ba98000a 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -251,8 +251,9 @@ bool ArraysProperties::isWellFounded(TypeNode type)
 Node ArraysProperties::mkGroundTerm(TypeNode type)
 {
   Assert(type.getKind() == kind::ARRAY_TYPE);
+  NodeManager* nm = NodeManager::currentNM();
   TypeNode elemType = type.getArrayConstituentType();
-  Node elem = elemType.mkGroundTerm();
+  Node elem = nm->mkGroundTerm(elemType);
   if (elem.isConst())
   {
     return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 4cda9f728..903a08bb4 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -441,7 +441,8 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
     else if (k == kind::APPLY_SELECTOR_TOTAL)
     {
       // evaluates to the first ground value of type tn.
-      Node gt = tn.mkGroundValue();
+      NodeManager* nm = NodeManager::currentNM();
+      Node gt = nm->mkGroundValue(tn);
       Assert(!gt.isNull());
       if (tn.isDatatype() && !tn.isInstantiatedDatatype())
       {
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index cfeb72b5c..69153ef00 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -93,7 +93,7 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id,
     const DTypeConstructor& dtc = dt[constructorIndex];
     int selectorIndex = dtc.getSelectorIndexInternal(selector);
     Node r =
-        selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
+        selectorIndex < 0 ? nm->mkGroundTerm(t.getType()) : t[0][selectorIndex];
     return t.eqNode(r);
   }
   else if (id == PfRule::DT_SPLIT)
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index b19eb53af..a9f0c3198 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1007,10 +1007,11 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
       // uninterpreted sorts and arrays, where the solver does not fully
       // handle values of the sort. The call to mkGroundTerm does not introduce
       // values for these sorts.
-      rrs = r.getType().mkGroundTerm();
+      NodeManager* nm = NodeManager::currentNM();
+      rrs = nm->mkGroundTerm(r.getType());
       Trace("datatypes-wrong-sel")
           << "Bad apply " << r << " term = " << rrs
-          << ", value = " << r.getType().mkGroundValue() << std::endl;
+          << ", value = " << nm->mkGroundValue(r.getType()) << std::endl;
     }
     else
     {
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 5a5d97064..5f129f3fc 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -150,6 +150,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
         if (r.asSatisfiabilityResult().isSat() == Result::SAT)
         {
           Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
+          NodeManager* nm = NodeManager::currentNM();
           is_unique_term = true;
           std::vector<Node> vars;
           d_sampler->getVariables(vars);
@@ -166,7 +167,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol,
               if (itf == d_fv_to_skolem.end())
               {
                 // not in conjecture, can use arbitrary value
-                val = v.getType().mkGroundTerm();
+                val = nm->mkGroundTerm(v.getType());
               }
               else
               {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index a05b64249..438afbe82 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -437,7 +437,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   else if (type.isArray() || type.isSet())
   {
     // generate constant array over the first element of the constituent type
-    Node c = type.mkGroundTerm();
+    Node c = nm->mkGroundTerm(type);
     // note that c should never contain an uninterpreted constant
     Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c));
     ops.push_back(c);
@@ -1065,8 +1065,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     {
       // if there are not constructors yet by this point, which can happen,
       // e.g. for unimplemented types that have no variables in the argument
-      // list of the function-to-synthesize, create a fresh ground term 
-      sdts[i].addConstructor(types[i].mkGroundTerm(), "", {});
+      // list of the function-to-synthesize, create a fresh ground term
+      sdts[i].addConstructor(nm->mkGroundTerm(types[i]), "", {});
     }
 
     // always add ITE
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index 6167f7474..bd71de283 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -442,9 +442,10 @@ Node SygusReconstruct::mkGround(Node n) const
   std::unordered_map<TNode, TNode> subs;
 
   // generate a ground value for each one of those variables
+  NodeManager* nm = NodeManager::currentNM();
   for (const TNode& var : vars)
   {
-    subs.emplace(var, var.getType().mkGroundValue());
+    subs.emplace(var, nm->mkGroundValue(var.getType()));
   }
 
   // substitute the variables with ground values
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 6b023075b..d1f29d207 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -609,7 +609,8 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
         {
           if (sol_templ_children[j].isNull())
           {
-            sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
+            sol_templ_children[j] =
+                nm->mkGroundTerm(cop_to_sks[cop][j].getType());
           }
         }
         sol_templ_children.insert(sol_templ_children.begin(), cop);
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index d22bde370..3e4a69dc9 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -116,9 +116,10 @@ Result checkWithSubsolver(Node query,
     if (r.asSatisfiabilityResult().isSat() == Result::SAT)
     {
       // default model
+      NodeManager* nm = NodeManager::currentNM();
       for (const Node& v : vars)
       {
-        modelVals.push_back(v.getType().mkGroundTerm());
+        modelVals.push_back(nm->mkGroundTerm(v.getType()));
       }
     }
     return r;
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 69cd790e8..1d82f9abd 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1757,7 +1757,8 @@ Node SequencesRewriter::rewriteSeqNth(Node node)
     if (node.getKind() == SEQ_NTH_TOTAL)
     {
       // return arbitrary term
-      Node ret = s.getType().getSequenceElementType().mkGroundValue();
+      NodeManager* nm = NodeManager::currentNM();
+      Node ret = nm->mkGroundValue(s.getType().getSequenceElementType());
       return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB);
     }
     else
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index a91a185a0..079683116 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -124,7 +124,8 @@ std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
   {
     // This is called when t is a sort that does not occur in this model.
     // Sorts are always interpreted as non-empty, thus we add a single element.
-    elements.push_back(tn.mkGroundTerm());
+    NodeManager* nm = NodeManager::currentNM();
+    elements.push_back(nm->mkGroundTerm(tn));
     return elements;
   }
   return *type_refs;
diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp
index a05c76d4c..2c0dcd763 100644
--- a/src/theory/uf/theory_uf_type_rules.cpp
+++ b/src/theory/uf/theory_uf_type_rules.cpp
@@ -264,7 +264,7 @@ Node FunctionProperties::mkGroundTerm(TypeNode type)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node bvl = nm->getBoundVarListForFunctionType(type);
-  Node ret = type.getRangeType().mkGroundTerm();
+  Node ret = nm->mkGroundTerm(type.getRangeType());
   return nm->mkNode(kind::LAMBDA, bvl, ret);
 }
 
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index 15dde0cc2..336190b8e 100644
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -71,8 +71,9 @@ TEST_F(TestUtilBlackDatatype, enumeration)
   ASSERT_TRUE(colorsType.getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << colorsType.getDType().getName()
                        << std::endl
-                       << "  is " << colorsType.mkGroundTerm() << std::endl;
-  ASSERT_EQ(colorsType.mkGroundTerm().getType(), colorsType);
+                       << "  is " << d_nodeManager->mkGroundTerm(colorsType)
+                       << std::endl;
+  ASSERT_EQ(d_nodeManager->mkGroundTerm(colorsType).getType(), colorsType);
 }
 
 TEST_F(TestUtilBlackDatatype, nat)
@@ -103,8 +104,9 @@ TEST_F(TestUtilBlackDatatype, nat)
   ASSERT_TRUE(natType.getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << natType.getDType().getName()
                        << std::endl
-                       << "  is " << natType.mkGroundTerm() << std::endl;
-  ASSERT_TRUE(natType.mkGroundTerm().getType() == natType);
+                       << "  is " << d_nodeManager->mkGroundTerm(natType)
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(natType).getType() == natType);
 }
 
 TEST_F(TestUtilBlackDatatype, tree)
@@ -135,8 +137,9 @@ TEST_F(TestUtilBlackDatatype, tree)
   ASSERT_TRUE(treeType.getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << treeType.getDType().getName()
                        << std::endl
-                       << "  is " << treeType.mkGroundTerm() << std::endl;
-  ASSERT_TRUE(treeType.mkGroundTerm().getType() == treeType);
+                       << "  is " << d_nodeManager->mkGroundTerm(treeType)
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(treeType).getType() == treeType);
 }
 
 TEST_F(TestUtilBlackDatatype, list_int)
@@ -166,8 +169,9 @@ TEST_F(TestUtilBlackDatatype, list_int)
   ASSERT_TRUE(listType.getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << listType.getDType().getName()
                        << std::endl
-                       << "  is " << listType.mkGroundTerm() << std::endl;
-  ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+                       << "  is " << d_nodeManager->mkGroundTerm(listType)
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType);
 }
 
 TEST_F(TestUtilBlackDatatype, list_real)
@@ -196,8 +200,9 @@ TEST_F(TestUtilBlackDatatype, list_real)
   ASSERT_TRUE(listType.getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << listType.getDType().getName()
                        << std::endl
-                       << "  is " << listType.mkGroundTerm() << std::endl;
-  ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+                       << "  is " << d_nodeManager->mkGroundTerm(listType)
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType);
 }
 
 TEST_F(TestUtilBlackDatatype, list_boolean)
@@ -226,8 +231,9 @@ TEST_F(TestUtilBlackDatatype, list_boolean)
   ASSERT_TRUE(listType.getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << listType.getDType().getName()
                        << std::endl
-                       << "  is " << listType.mkGroundTerm() << std::endl;
-  ASSERT_TRUE(listType.mkGroundTerm().getType() == listType);
+                       << "  is " << d_nodeManager->mkGroundTerm(listType)
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType);
 }
 
 TEST_F(TestUtilBlackDatatype, listIntUpdate)
@@ -248,7 +254,7 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate)
   TypeNode listType = d_nodeManager->mkDatatypeType(list);
   const DType& ldt = listType.getDType();
   Node updater = ldt[0][0].getUpdater();
-  Node gt = listType.mkGroundTerm();
+  Node gt = d_nodeManager->mkGroundTerm(listType);
   Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
   Node truen = d_nodeManager->mkConst(true);
   // construct an update term
@@ -322,8 +328,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees1)
   ASSERT_TRUE(dtts[0].getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << dtts[0].getDType().getName()
                        << std::endl
-                       << "  is " << dtts[0].mkGroundTerm() << std::endl;
-  ASSERT_TRUE(dtts[0].mkGroundTerm().getType() == dtts[0]);
+                       << "  is " << d_nodeManager->mkGroundTerm(dtts[0])
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts[0]).getType() == dtts[0]);
 
   ASSERT_FALSE(dtts[1].getDType().isFinite());
   ASSERT_TRUE(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS)
@@ -331,8 +338,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees1)
   ASSERT_TRUE(dtts[1].getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << dtts[1].getDType().getName()
                        << std::endl
-                       << "  is " << dtts[1].mkGroundTerm() << std::endl;
-  ASSERT_TRUE(dtts[1].mkGroundTerm().getType() == dtts[1]);
+                       << "  is " << d_nodeManager->mkGroundTerm(dtts[1])
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts[1]).getType() == dtts[1]);
 }
 
 TEST_F(TestUtilBlackDatatype, mutual_list_trees2)
@@ -388,8 +396,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees2)
   ASSERT_TRUE(dtts2[0].getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName()
                        << std::endl
-                       << "  is " << dtts2[0].mkGroundTerm() << std::endl;
-  ASSERT_TRUE(dtts2[0].mkGroundTerm().getType() == dtts2[0]);
+                       << "  is " << d_nodeManager->mkGroundTerm(dtts2[0])
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts2[0]).getType() == dtts2[0]);
 
   ASSERT_FALSE(dtts2[1].getDType().isParametric());
   ASSERT_FALSE(dtts2[1].getDType().isFinite());
@@ -399,8 +408,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees2)
   ASSERT_TRUE(dtts2[1].getDType().isWellFounded());
   Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName()
                        << std::endl
-                       << "  is " << dtts2[1].mkGroundTerm() << std::endl;
-  ASSERT_TRUE(dtts2[1].mkGroundTerm().getType() == dtts2[1]);
+                       << "  is " << d_nodeManager->mkGroundTerm(dtts2[1])
+                       << std::endl;
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts2[1]).getType() == dtts2[1]);
 }
 
 TEST_F(TestUtilBlackDatatype, not_so_well_founded)
@@ -423,7 +433,7 @@ TEST_F(TestUtilBlackDatatype, not_so_well_founded)
       treeType.getDType().getCardinality().compare(Cardinality::INTEGERS)
       == Cardinality::EQUAL);
   ASSERT_FALSE(treeType.getDType().isWellFounded());
-  ASSERT_TRUE(treeType.mkGroundTerm().isNull());
+  ASSERT_TRUE(d_nodeManager->mkGroundTerm(treeType).isNull());
   ASSERT_TRUE(treeType.getDType().mkGroundTerm(treeType).isNull());
 }