Remove NodeBuilder constructors with implicit NodeManager (cvc5#11392)

This change introduces some calls to `NodeManager::currentNM()`, which will be removed in a follow-up PR.
ajreynol · Dec 9, 2024 · 2a1d74a · 2a1d74a
1 parent 9c1ecb0
commit 2a1d74a
Show file tree

Hide file tree

Showing 68 changed files with 201 additions and 226 deletions.
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
@@ -5640,7 +5640,7 @@ Term TermManager::mkTermHelper(const Op& op, const std::vector<Term>& children)
   const internal::Kind int_kind = extToIntKind(op.d_kind);
   std::vector<internal::Node> echildren = Term::termVectorToNodes(children);
 
-  internal::NodeBuilder nb(int_kind);
+  internal::NodeBuilder nb(d_nm, int_kind);
   nb << *op.d_node;
   nb.append(echildren);
   internal::Node res = nb.constructNode();
@@ -6640,7 +6640,7 @@ Term TermManager::mkTuple(const std::vector<Term>& terms)
   }
   internal::TypeNode tn = d_nm->mkTupleType(typeNodes);
   const internal::DType& dt = tn.getDType();
-  internal::NodeBuilder nb(extToIntKind(Kind::APPLY_CONSTRUCTOR));
+  internal::NodeBuilder nb(d_nm, extToIntKind(Kind::APPLY_CONSTRUCTOR));
   nb << dt[0].getConstructor();
   nb.append(args);
   internal::Node res = nb.constructNode();
@@ -6659,7 +6659,7 @@ Term TermManager::mkNullableSome(const Term& term)
   internal::TypeNode typeNode = arg.getType();
   internal::TypeNode tn = d_nm->mkNullableType(typeNode);
   const internal::DType& dt = tn.getDType();
-  internal::NodeBuilder nb(extToIntKind(Kind::APPLY_CONSTRUCTOR));
+  internal::NodeBuilder nb(d_nm, extToIntKind(Kind::APPLY_CONSTRUCTOR));
   nb << dt[1].getConstructor();
   nb.append(arg);
   internal::Node res = nb.constructNode();
@@ -6677,7 +6677,7 @@ Term TermManager::mkNullableNull(const Sort& sort)
   //////// all checks before this line
   internal::TypeNode tn = sort.getTypeNode();
   const internal::DType& dt = tn.getDType();
-  internal::NodeBuilder nb(extToIntKind(Kind::APPLY_CONSTRUCTOR));
+  internal::NodeBuilder nb(d_nm, extToIntKind(Kind::APPLY_CONSTRUCTOR));
   nb << dt[0].getConstructor();
   internal::Node res = nb.constructNode();
   (void)res.getType(true); /* kick off type checking */

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
@@ -694,7 +694,7 @@ TypeNode DTypeConstructor::doParametricSubstitution(
       }
     }
   }
-  NodeBuilder nb(range.getKind());
+  NodeBuilder nb(NodeManager::currentNM(), range.getKind());
   for (size_t i = 0, csize = children.size(); i < csize; ++i)
   {
     nb << children[i];

diff --git a/src/expr/node.h b/src/expr/node.h
@@ -1315,7 +1315,7 @@ Node NodeTemplate<ref_count>::substitute(
   }
 
   // otherwise compute
-  NodeBuilder nb(getKind());
+  NodeBuilder nb(NodeManager::currentNM(), getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
     if(getOperator() == node) {
@@ -1385,7 +1385,7 @@ Node NodeTemplate<ref_count>::substitute(
     cache[*this] = *this;
     return *this;
   } else {
-    NodeBuilder nb(getKind());
+    NodeBuilder nb(NodeManager::currentNM(), getKind());
     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
       // push the operator
       nb << getOperator().substitute(nodesBegin, nodesEnd,
@@ -1449,7 +1449,7 @@ Node NodeTemplate<ref_count>::substitute(
     cache[*this] = *this;
     return *this;
   } else {
-    NodeBuilder nb(getKind());
+    NodeBuilder nb(NodeManager::currentNM(), getKind());
     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
       // push the operator
       nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache);

diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
@@ -19,33 +19,6 @@
 
 namespace cvc5::internal {
 
-NodeBuilder::NodeBuilder()
-    : d_nv(&d_inlineNv),
-      d_nm(NodeManager::currentNM()),
-      d_nvMaxChildren(default_nchild_thresh)
-{
-  d_inlineNv.d_id = 0;
-  d_inlineNv.d_rc = 0;
-  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(Kind::UNDEFINED_KIND);
-  d_inlineNv.d_nm = d_nm;
-  d_inlineNv.d_nchildren = 0;
-}
-
-NodeBuilder::NodeBuilder(Kind k)
-    : d_nv(&d_inlineNv),
-      d_nm(NodeManager::currentNM()),
-      d_nvMaxChildren(default_nchild_thresh)
-{
-  Assert(k != Kind::NULL_EXPR && k != Kind::UNDEFINED_KIND)
-      << "illegal Node-building kind";
-
-  d_inlineNv.d_id = 1;  // have a kind already
-  d_inlineNv.d_rc = 0;
-  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
-  d_inlineNv.d_nm = d_nm;
-  d_inlineNv.d_nchildren = 0;
-}
-
 NodeBuilder::NodeBuilder(NodeManager* nm)
     : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
 {

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
@@ -161,8 +161,6 @@ class NodeBuilder {
   constexpr static size_t default_nchild_thresh = 10;
 
  public:
-  NodeBuilder();
-  NodeBuilder(Kind k);
   NodeBuilder(NodeManager* nm);
   NodeBuilder(NodeManager* nm, Kind k);
   NodeBuilder(const NodeBuilder& nb);

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
@@ -211,7 +211,7 @@ TypeNode NodeConverter::convertType(TypeNode tn)
         TypeNode ret = cur;
         // reconstruct using a node builder, which seems to be required for
         // type nodes.
-        NodeBuilder nb(ret.getKind());
+        NodeBuilder nb(d_nm, ret.getKind());
         // there are no parameterized types
         Assert (ret.getMetaKind() != kind::metakind::PARAMETERIZED);
         for (TypeNode::const_iterator j = ret.begin(), iend = ret.end();

diff --git a/src/expr/sygus_grammar.cpp b/src/expr/sygus_grammar.cpp
@@ -203,7 +203,7 @@ Node purifySygusGNode(const Node& n,
   if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     // it's an indexed operator so we should provide the op
-    internal::NodeBuilder nb(n.getKind());
+    internal::NodeBuilder nb(NodeManager::currentNM(), n.getKind());
     nb << n.getOperator();
     nb.append(pchildren);
     nret = nb.constructNode();

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
@@ -57,7 +57,7 @@ TypeNode TypeNode::substitute(
   }
 
   // otherwise compute
-  NodeBuilder nb(getKind());
+  NodeBuilder nb(NodeManager::currentNM(), getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
     nb << TypeNode(d_nv->d_children[0]);
@@ -399,7 +399,7 @@ TypeNode TypeNode::unifyInternal(const TypeNode& t, bool isLub) const
     // different arities
     return TypeNode::null();
   }
-  NodeBuilder nb(k);
+  NodeBuilder nb(NodeManager::currentNM(), k);
   for (size_t i = 0; i < nchild; i++)
   {
     TypeNode c = (*this)[i];

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
@@ -847,7 +847,7 @@ TypeNode TypeNode::substitute(
     cache[*this] = *this;
     return *this;
   } else {
-    NodeBuilder nb(getKind());
+    NodeBuilder nb(NodeManager::currentNM(), getKind());
     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
       // push the operator
       nb << TypeNode(d_nv->d_children[0]);

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
@@ -366,7 +366,7 @@ void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
 {
   Kind k = n.getKind();
   NodeManager* nm = nodeManager();
-  NodeBuilder builder(new_kind);
+  NodeBuilder builder(nm, new_kind);
 
   Trace("bool-to-bv") << "BoolToBV::rebuildNode with " << n
                       << " and new_kind = " << kindToString(new_kind)

diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
@@ -223,7 +223,7 @@ Node BVToBool::convertBvTerm(TNode node)
     default: Unhandled();
   }
 
-  NodeBuilder builder(new_kind);
+  NodeBuilder builder(nm, new_kind);
   for (unsigned i = 0; i < node.getNumChildren(); ++i)
   {
     builder << convertBvTerm(node[i]);
@@ -257,7 +257,7 @@ Node BVToBool::liftNode(TNode current)
     }
     else
     {
-      NodeBuilder builder(current.getKind());
+      NodeBuilder builder(nodeManager(), current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         builder << current.getOperator();

diff --git a/src/preprocessing/passes/ff_bitsum.cpp b/src/preprocessing/passes/ff_bitsum.cpp
@@ -85,7 +85,7 @@ PreprocessingPassResult FfBitsum::applyInternal(
       else
       {
         Kind oldKind = current.getKind();
-        NodeBuilder builder(oldKind);
+        NodeBuilder builder(nm, oldKind);
         if (current.getMetaKind() == kind::MetaKind::PARAMETERIZED)
         {
           builder << current.getOperator();

diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -121,7 +121,7 @@ Node ForeignTheoryRewriter::reconstructNode(Node originalNode,
   }
   // re-build the node with the same kind and new children
   Kind k = originalNode.getKind();
-  NodeBuilder builder(k);
+  NodeBuilder builder(originalNode.getNodeManager(), k);
   // special case for parameterized nodes
   if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
   {

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
@@ -85,7 +85,7 @@ Node intToBVMakeBinary(NodeManager* nm, TNode n, NodeMap& cache)
     }
     else
     {
-      NodeBuilder builder(current.getKind());
+      NodeBuilder builder(nm, current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << current.getOperator();
       }
@@ -217,7 +217,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
            << " to a bit-vector operator. Remove option `--solve-int-as-bv`.";
         throw LogicException(ss.str());
       }
-      NodeBuilder builder(newKind);
+      NodeBuilder builder(nm, newKind);
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << current.getOperator();
       }

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
@@ -100,7 +100,7 @@ size_t MipLibTrick::removeFromConjunction(
         || (sub.getKind() == Kind::AND
             && (subremovals = removeFromConjunction(sub, toRemove)) > 0))
     {
-      NodeBuilder b(Kind::AND);
+      NodeBuilder b(nodeManager(), Kind::AND);
       b.append(n.begin(), j);
       if (subremovals > 0)
       {
@@ -559,7 +559,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           Node sum;
           if (pos.getKind() == Kind::AND)
           {
-            NodeBuilder sumb(Kind::ADD);
+            NodeBuilder sumb(nodeManager(), Kind::ADD);
             for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
             {
               sumb << nm->mkNode(

diff --git a/src/preprocessing/util/boolean_simplification.h b/src/preprocessing/util/boolean_simplification.h
@@ -84,7 +84,7 @@ class BooleanSimplification
       return buffer[0];
     }
 
-    NodeBuilder nb(Kind::AND);
+    NodeBuilder nb(andNode.getNodeManager(), Kind::AND);
     nb.append(buffer);
     return nb;
   }
@@ -111,7 +111,7 @@ class BooleanSimplification
       return buffer[0];
     }
 
-    NodeBuilder nb(Kind::OR);
+    NodeBuilder nb(orNode.getNodeManager(), Kind::OR);
     nb.append(buffer);
     return nb;
   }
@@ -131,7 +131,8 @@ class BooleanSimplification
     TNode right = implication[1];
 
     Node notLeft = negate(left);
-    Node clause = NodeBuilder(Kind::OR) << notLeft << right;
+    Node clause = NodeBuilder(implication.getNodeManager(), Kind::OR)
+                  << notLeft << right;
 
     return simplifyClause(clause);
   }

diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
@@ -395,7 +395,7 @@ Node ITECompressor::compressBooleanITEs(Node toCompress)
     }
   }
 
-  NodeBuilder nb(Kind::AND);
+  NodeBuilder nb(nodeManager(), Kind::AND);
   Node curr = toCompress;
   while (curr.getKind() == Kind::ITE
          && (curr[1] == d_false || curr[2] == d_false)
@@ -459,7 +459,7 @@ Node ITECompressor::compressTerm(Node toCompress)
     }
   }
 
-  NodeBuilder nb(toCompress.getKind());
+  NodeBuilder nb(nodeManager(), toCompress.getKind());
 
   if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
@@ -496,7 +496,7 @@ Node ITECompressor::compressBoolean(Node toCompress)
   else
   {
     bool ta = ite::isTheoryAtom(toCompress);
-    NodeBuilder nb(toCompress.getKind());
+    NodeBuilder nb(nodeManager(), toCompress.getKind());
     if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
     {
       nb << (toCompress.getOperator());
@@ -885,7 +885,7 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
     return d_replaceOverCache[p];
   }
 
-  NodeBuilder builder(n.getKind());
+  NodeBuilder builder(nodeManager(), n.getKind());
   if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << n.getOperator();
@@ -1184,7 +1184,7 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
   }
   else
   {
-    NodeBuilder nb(Kind::OR);
+    NodeBuilder nb(nodeManager(), Kind::OR);
     NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
     for (; it != end; ++it)
     {
@@ -1309,7 +1309,7 @@ Node ITESimplifier::simpConstants(TNode simpContext,
 
   if (iteNode.getKind() == Kind::ITE)
   {
-    NodeBuilder builder(Kind::ITE);
+    NodeBuilder builder(nodeManager(), Kind::ITE);
     builder << iteNode[0];
     unsigned i = 1;
     for (; i < iteNode.getNumChildren(); ++i)
@@ -1402,7 +1402,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
     return simpVar;
   }
 
-  NodeBuilder builder(c.getKind());
+  NodeBuilder builder(nodeManager(), c.getKind());
   if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << c.getOperator();
@@ -1553,7 +1553,7 @@ Node ITESimplifier::simpITE(TNode assertion)
     if (stackHead.d_children_added)
     {
       // Children have been processed, so substitute
-      NodeBuilder builder(current.getKind());
+      NodeBuilder builder(nodeManager(), current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         builder << current.getOperator();
@@ -1700,7 +1700,7 @@ Node ITECareSimplifier::substitute(TNode e,
     return e;
   }
 
-  NodeBuilder builder(e.getKind());
+  NodeBuilder builder(e.getNodeManager(), e.getKind());
   if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << e.getOperator();

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
@@ -107,7 +107,7 @@ Node ExpandDefs::expandDefinitions(TNode n,
       if (node.getNumChildren() > 0)
       {
         // cout << "cons : " << node << std::endl;
-        NodeBuilder nb(node.getKind());
+        NodeBuilder nb(nodeManager(), node.getKind());
         if (node.getMetaKind() == metakind::PARAMETERIZED)
         {
           Trace("expand") << "op   : " << node.getOperator() << std::endl;

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
@@ -38,7 +38,7 @@ namespace theory {
 namespace arith {
 
 Node ArithIteUtils::applyReduceVariablesInItes(Node n){
-  NodeBuilder nb(n.getKind());
+  NodeBuilder nb(nodeManager(), n.getKind());
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
     nb << (n.getOperator());
   }
@@ -277,7 +277,7 @@ Node ArithIteUtils::reduceConstantIteByGCD(Node n){
   }
 
   if(n.getNumChildren() > 0){
-    NodeBuilder nb(n.getKind());
+    NodeBuilder nb(nodeManager(), n.getKind());
     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       nb << (n.getOperator());
     }

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
@@ -1387,7 +1387,7 @@ Node ArithRewriter::expandPowConst(NodeManager* nm, const Node& t)
         }
         else
         {
-          NodeBuilder nb(Kind::MULT);
+          NodeBuilder nb(nm, Kind::MULT);
           for (unsigned i = 0; i < num; ++i)
           {
             nb << base;

diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
@@ -358,7 +358,7 @@ Node eliminateInt2Bv(TNode node)
   {
     return v[0];
   }
-  NodeBuilder result(Kind::BITVECTOR_CONCAT);
+  NodeBuilder result(NodeManager::currentNM(), Kind::BITVECTOR_CONCAT);
   result.append(v.rbegin(), v.rend());
   return Node(result);
 }