Add node manager to node converter (cvc5#10545)

Towards eliminating NodeManager::currentNM. A followup PR will eliminate this call within these utilities.
HanielB · Apr 2, 2024 · ee588d4 · ee588d4
1 parent b9b4e1b
commit ee588d4
Show file tree

Hide file tree

Showing 34 changed files with 81 additions and 40 deletions.
diff --git a/src/expr/annotation_elim_node_converter.cpp b/src/expr/annotation_elim_node_converter.cpp
@@ -19,7 +19,10 @@ using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
 
-AnnotationElimNodeConverter::AnnotationElimNodeConverter() {}
+AnnotationElimNodeConverter::AnnotationElimNodeConverter(NodeManager* nm)
+    : NodeConverter(nm)
+{
+}
 
 Node AnnotationElimNodeConverter::postConvert(Node n)
 {

diff --git a/src/expr/annotation_elim_node_converter.h b/src/expr/annotation_elim_node_converter.h
@@ -30,7 +30,7 @@ namespace cvc5::internal {
 class AnnotationElimNodeConverter : public NodeConverter
 {
  public:
-  AnnotationElimNodeConverter();
+  AnnotationElimNodeConverter(NodeManager* nm);
   ~AnnotationElimNodeConverter() {}
   /** convert node n as described above during post-order traversal */
   Node postConvert(Node n) override;

diff --git a/src/expr/elim_shadow_converter.cpp b/src/expr/elim_shadow_converter.cpp
@@ -34,14 +34,16 @@ struct QElimShadowAttributeId
 };
 using QElimShadowAttribute = expr::Attribute<QElimShadowAttributeId, Node>;
 
-ElimShadowNodeConverter::ElimShadowNodeConverter(const Node& q) : d_closure(q)
+ElimShadowNodeConverter::ElimShadowNodeConverter(NodeManager* nm, const Node& q)
+    : NodeConverter(nm), d_closure(q)
 {
   Assert(q.isClosure());
   d_vars.insert(d_vars.end(), q[0].begin(), q[0].end());
 }
 
 ElimShadowNodeConverter::ElimShadowNodeConverter(
-    const Node& n, const std::unordered_set<Node>& vars)
+    NodeManager* nm, const Node& n, const std::unordered_set<Node>& vars)
+    : NodeConverter(nm)
 {
   d_closure = n;
   d_vars.insert(d_vars.end(), vars.begin(), vars.end());
@@ -85,7 +87,8 @@ Node ElimShadowNodeConverter::getElimShadowVar(const Node& q,
 Node ElimShadowNodeConverter::eliminateShadow(const Node& q)
 {
   Assert(q.isClosure());
-  ElimShadowNodeConverter esnc(q);
+  NodeManager* nm = NodeManager::currentNM();
+  ElimShadowNodeConverter esnc(nm, q);
   // eliminate shadowing in all children
   std::vector<Node> children;
   children.push_back(q[0]);

diff --git a/src/expr/elim_shadow_converter.h b/src/expr/elim_shadow_converter.h
@@ -41,12 +41,14 @@ class ElimShadowNodeConverter : public NodeConverter
   /**
    * Eliminate shadowing of the top-most variables in closure q.
    */
-  ElimShadowNodeConverter(const Node& q);
+  ElimShadowNodeConverter(NodeManager* nm, const Node& q);
   /**
    * Eliminate shadowing of variables vars. Node n is a term used as a unique
    * identifier for which the introduced bound variables are indexed on.
    */
-  ElimShadowNodeConverter(const Node& n, const std::unordered_set<Node>& vars);
+  ElimShadowNodeConverter(NodeManager* nm,
+                          const Node& n,
+                          const std::unordered_set<Node>& vars);
   ~ElimShadowNodeConverter() {}
   /**
    * Convert node n as described above during post-order traversal. This

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
@@ -21,7 +21,10 @@ using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
 
-NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {}
+NodeConverter::NodeConverter(NodeManager* nm, bool forceIdem)
+    : d_nm(nm), d_forceIdem(forceIdem)
+{
+}
 
 Node NodeConverter::convert(Node n, bool preserveTypes)
 {
@@ -30,7 +33,6 @@ Node NodeConverter::convert(Node n, bool preserveTypes)
     return n;
   }
   Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<Node, Node>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
@@ -116,7 +118,7 @@ Node NodeConverter::convert(Node n, bool preserveTypes)
         {
           if (childChanged)
           {
-            ret = nm->mkNode(ret.getKind(), children);
+            ret = d_nm->mkNode(ret.getKind(), children);
             Trace("nconv-debug2") << "..from children changed " << cur
                                   << " into " << ret << std::endl;
           }

diff --git a/src/expr/node_converter.h b/src/expr/node_converter.h
@@ -41,7 +41,7 @@ class NodeConverter
    * @param forceIdem If true, this assumes that terms returned by postConvert
    * and postConvertType should not be converted again.
    */
-  NodeConverter(bool forceIdem = true);
+  NodeConverter(NodeManager* nm, bool forceIdem = true);
   virtual ~NodeConverter() {}
   /**
    * This converts node n based on the preConvert/postConvert methods that can
@@ -109,6 +109,10 @@ class NodeConverter
    */
   virtual TypeNode postConvertType(TypeNode n);
   //------------------------- end virtual interface
+ protected:
+  /** The underlying node manager */
+  NodeManager* d_nm;
+
  private:
   /** Add to cache */
   void addToCache(TNode cur, TNode ret);

diff --git a/src/expr/subtype_elim_node_converter.cpp b/src/expr/subtype_elim_node_converter.cpp
@@ -21,7 +21,10 @@ using namespace cvc5::internal::kind;
 
 namespace cvc5::internal {
 
-SubtypeElimNodeConverter::SubtypeElimNodeConverter() {}
+SubtypeElimNodeConverter::SubtypeElimNodeConverter(NodeManager* nm)
+    : NodeConverter(nm)
+{
+}
 
 bool SubtypeElimNodeConverter::isRealTypeStrict(TypeNode tn)
 {

diff --git a/src/expr/subtype_elim_node_converter.h b/src/expr/subtype_elim_node_converter.h
@@ -35,7 +35,7 @@ namespace cvc5::internal {
 class SubtypeElimNodeConverter : public NodeConverter
 {
  public:
-  SubtypeElimNodeConverter();
+  SubtypeElimNodeConverter(NodeManager* nm);
   ~SubtypeElimNodeConverter() {}
   /** convert node n as described above during post-order traversal */
   Node postConvert(Node n) override;

diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
@@ -21,6 +21,8 @@
 namespace cvc5::internal {
 namespace proof {
 
+AletheNodeConverter::AletheNodeConverter(NodeManager* nm) : NodeConverter(nm) {}
+
 Node AletheNodeConverter::postConvert(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();

diff --git a/src/proof/alethe/alethe_node_converter.h b/src/proof/alethe/alethe_node_converter.h
@@ -31,8 +31,7 @@ namespace proof {
 class AletheNodeConverter : public NodeConverter
 {
  public:
-  AletheNodeConverter() {}
-  ~AletheNodeConverter() {}
+  AletheNodeConverter(NodeManager* nm);
   /** convert at post-order traversal */
   Node postConvert(Node n) override;
 

diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp
@@ -47,9 +47,12 @@ using namespace cvc5::internal::kind;
 namespace cvc5::internal {
 namespace proof {
 
-AlfNodeConverter::AlfNodeConverter()
+BaseAlfNodeConverter::BaseAlfNodeConverter(NodeManager* nm) : NodeConverter(nm)
+{
+}
+
+AlfNodeConverter::AlfNodeConverter(NodeManager* nm) : BaseAlfNodeConverter(nm)
 {
-  NodeManager* nm = NodeManager::currentNM();
   d_sortType = nm->mkSort("sortType");
 }
 

diff --git a/src/proof/alf/alf_node_converter.h b/src/proof/alf/alf_node_converter.h
@@ -35,6 +35,7 @@ namespace proof {
 class BaseAlfNodeConverter : public NodeConverter
 {
  public:
+  BaseAlfNodeConverter(NodeManager* nm);
   /**
    * Returns the operator of node n.
    * @param n The term whose operator we wish to retrieve.
@@ -59,7 +60,7 @@ class BaseAlfNodeConverter : public NodeConverter
 class AlfNodeConverter : public BaseAlfNodeConverter
 {
  public:
-  AlfNodeConverter();
+  AlfNodeConverter(NodeManager* nm);
   ~AlfNodeConverter() {}
   /** Convert at pre-order traversal */
   Node preConvert(Node n) override;

diff --git a/src/proof/lfsc/lfsc_list_sc_node_converter.cpp b/src/proof/lfsc/lfsc_list_sc_node_converter.cpp
@@ -19,10 +19,11 @@ namespace cvc5::internal {
 namespace proof {
 
 LfscListScNodeConverter::LfscListScNodeConverter(
+    NodeManager* nm,
     LfscNodeConverter& conv,
     const std::unordered_set<Node>& listVars,
     bool isPre)
-    : d_conv(conv), d_listVars(listVars), d_isPre(isPre)
+    : NodeConverter(nm), d_conv(conv), d_listVars(listVars), d_isPre(isPre)
 {
 }
 

diff --git a/src/proof/lfsc/lfsc_list_sc_node_converter.h b/src/proof/lfsc/lfsc_list_sc_node_converter.h
@@ -61,7 +61,8 @@ namespace proof {
 class LfscListScNodeConverter : public NodeConverter
 {
  public:
-  LfscListScNodeConverter(LfscNodeConverter& conv,
+  LfscListScNodeConverter(NodeManager* nm,
+                          LfscNodeConverter& conv,
                           const std::unordered_set<Node>& listVars,
                           bool isPre = false);
   /** convert to internal */

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -46,9 +46,8 @@ using namespace cvc5::internal::kind;
 namespace cvc5::internal {
 namespace proof {
 
-LfscNodeConverter::LfscNodeConverter()
+LfscNodeConverter::LfscNodeConverter(NodeManager* nm) : NodeConverter(nm)
 {
-  NodeManager* nm = NodeManager::currentNM();
   d_arrow = nm->mkSortConstructor("arrow", 2);
 
   d_sortType = nm->mkSort("sortType");

diff --git a/src/proof/lfsc/lfsc_node_converter.h b/src/proof/lfsc/lfsc_node_converter.h
@@ -34,8 +34,7 @@ namespace proof {
 class LfscNodeConverter : public NodeConverter
 {
  public:
-  LfscNodeConverter();
-  ~LfscNodeConverter() {}
+  LfscNodeConverter(NodeManager* nm);
   /** convert at pre-order traversal */
   Node preConvert(Node n) override;
   /** convert at post-order traversal */

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
@@ -1150,7 +1150,7 @@ void LfscPrinter::printDslRule(std::ostream& out,
            << std::endl;
       // body must be converted to incorporate list semantics for substitutions
       // first traversal applies nary_elim to required n-ary applications
-      LfscListScNodeConverter llsncp(d_tproc, listVars, true);
+      LfscListScNodeConverter llsncp(nodeManager(), d_tproc, listVars, true);
       Node tscp;
       if (isConclusion)
       {
@@ -1166,7 +1166,7 @@ void LfscPrinter::printDslRule(std::ostream& out,
       // second traversal converts to LFSC form
       Node t = d_tproc.convert(tscp);
       // third traversal applies nary_concat where list variables are used
-      LfscListScNodeConverter llsnc(d_tproc, listVars, false);
+      LfscListScNodeConverter llsnc(nodeManager(), d_tproc, listVars, false);
       Node tsc = llsnc.convert(t);
       oscs << "  ";
       print(oscs, tsc);

diff --git a/src/proof/proof_rule_checker.cpp b/src/proof/proof_rule_checker.cpp
@@ -74,4 +74,6 @@ Node ProofRuleChecker::mkKindNode(Kind k)
       Rational(static_cast<uint32_t>(k)));
 }
 
+NodeManager* ProofRuleChecker::nodeManager() const { return d_nm; }
+
 }  // namespace cvc5::internal
diff --git a/src/proof/proof_rule_checker.h b/src/proof/proof_rule_checker.h
@@ -83,6 +83,8 @@ class ProofRuleChecker
   virtual Node checkInternal(ProofRule id,
                              const std::vector<Node>& children,
                              const std::vector<Node>& args) = 0;
+  /** Get a pointer to the node manager */
+  NodeManager* nodeManager() const;
   /** The underlying node manager */
   NodeManager* d_nm;
 };

diff --git a/src/proof/subtype_elim_proof_converter.cpp b/src/proof/subtype_elim_proof_converter.cpp
@@ -23,7 +23,7 @@
 namespace cvc5::internal {
 
 SubtypeElimConverterCallback::SubtypeElimConverterCallback(Env& env)
-    : EnvObj(env)
+    : EnvObj(env), d_nconv(nodeManager())
 {
   d_pc = d_env.getProofNodeManager()->getChecker();
 }

diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -36,6 +36,7 @@ RewriteDbProofCons::RewriteDbProofCons(Env& env, RewriteDb* db)
     : EnvObj(env),
       d_notify(*this),
       d_trrc(env),
+      d_rdnc(nodeManager()),
       d_db(db),
       d_eval(nullptr),
       d_currRecLimit(0),

diff --git a/src/rewriter/rewrite_db_term_process.cpp b/src/rewriter/rewrite_db_term_process.cpp
@@ -29,6 +29,11 @@ using namespace cvc5::internal::kind;
 namespace cvc5::internal {
 namespace rewriter {
 
+RewriteDbNodeConverter::RewriteDbNodeConverter(NodeManager* nm)
+    : NodeConverter(nm)
+{
+}
+
 Node RewriteDbNodeConverter::postConvert(Node n)
 {
   Kind k = n.getKind();

diff --git a/src/rewriter/rewrite_db_term_process.h b/src/rewriter/rewrite_db_term_process.h
@@ -45,6 +45,7 @@ namespace rewriter {
 class RewriteDbNodeConverter : public NodeConverter
 {
  public:
+  RewriteDbNodeConverter(NodeManager* nm);
   /**
    * This converts the node n to the internal shape that it should be in
    * for the DSL proof reconstruction algorithm.

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
@@ -261,13 +261,13 @@ void PfManager::printProof(std::ostream& out,
   else if (mode == options::ProofFormatMode::ALF)
   {
     Assert(fp->getRule() == ProofRule::SCOPE);
-    proof::AlfNodeConverter atp;
+    proof::AlfNodeConverter atp(nodeManager());
     proof::AlfPrinter alfp(d_env, atp);
     alfp.print(out, fp);
   }
   else if (mode == options::ProofFormatMode::ALETHE)
   {
-    proof::AletheNodeConverter anc;
+    proof::AletheNodeConverter anc(nodeManager());
     proof::AletheProofPostprocess vpfpp(
         d_env, anc, options().proof.proofAletheResPivots);
     vpfpp.process(fp);
@@ -277,7 +277,7 @@ void PfManager::printProof(std::ostream& out,
   else if (mode == options::ProofFormatMode::LFSC)
   {
     Assert(fp->getRule() == ProofRule::SCOPE);
-    proof::LfscNodeConverter ltp;
+    proof::LfscNodeConverter ltp(nodeManager());
     proof::LfscProofPostprocess lpp(d_env, ltp);
     lpp.process(fp);
     proof::LfscPrinter lp(d_env, ltp, d_rewriteDb.get());

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
@@ -134,7 +134,7 @@ Node QuantElimSolver::getQuantifierElimination(Node q,
       ret = SkolemManager::getOriginalForm(ret);
     }
     // make so that the returned formula does not involve arithmetic subtyping
-    SubtypeElimNodeConverter senc;
+    SubtypeElimNodeConverter senc(nodeManager());
     ret = senc.convert(ret);
     return ret;
   }

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
@@ -538,7 +538,7 @@ void SolverEngine::defineFunction(Node func,
   Node def = formula;
   if (!formals.empty())
   {
-    NodeManager* nm = NodeManager::currentNM();
+    NodeManager* nm = d_env->getNodeManager();
     def = nm->mkNode(
         Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, formals), def);
   }
@@ -1102,7 +1102,7 @@ Node SolverEngine::simplify(const Node& t)
   // now rewrite
   Node ret = d_env->getRewriter()->rewrite(tt);
   // make so that the returned term does not involve arithmetic subtyping
-  SubtypeElimNodeConverter senc;
+  SubtypeElimNodeConverter senc(d_env->getNodeManager());
   ret = senc.convert(ret);
   endCall();
   return ret;

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
@@ -420,7 +420,7 @@ Node BuiltinProofRuleChecker::checkInternal(ProofRule id,
   {
     Assert(children.size() == 1);
     Assert(args.size() == 1);
-    rewriter::RewriteDbNodeConverter rconv;
+    rewriter::RewriteDbNodeConverter rconv(nodeManager());
     Node f = children[0];
     Node g = args[0];
     // equivalent up to conversion via utility

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1369,7 +1369,7 @@ Node CegInstantiator::getModelValue(Node n)
   {
     // Witness terms with identifiers may appear in the model. We require
     // dropping their annotations here.
-    AnnotationElimNodeConverter aenc;
+    AnnotationElimNodeConverter aenc(nodeManager());
     mv = aenc.convert(mv);
   }
   return mv;

diff --git a/src/theory/quantifiers/oracle_checker.cpp b/src/theory/quantifiers/oracle_checker.cpp
@@ -25,6 +25,11 @@ namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
 
+OracleChecker::OracleChecker(Env& env)
+    : EnvObj(env), NodeConverter(env.getNodeManager())
+{
+}
+
 Node OracleChecker::checkConsistent(Node app, Node val)
 {
   Node result = evaluateApp(app);

diff --git a/src/theory/quantifiers/oracle_checker.h b/src/theory/quantifiers/oracle_checker.h
@@ -46,8 +46,7 @@ namespace quantifiers {
 class OracleChecker : protected EnvObj, public NodeConverter
 {
  public:
-  OracleChecker(Env& env) : EnvObj(env) {}
-  ~OracleChecker() {}
+  OracleChecker(Env& env);
 
   /**
    * Check predicted io pair is consistent, generate a lemma if