Use a single `NodeManager` per thread (#7204)

This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.

One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.

10 files changed, 32 insertions, 47 deletions

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 0001b3723..0e8bb62db 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -69,7 +69,7 @@ class TestNodeBlackNode : public TestNode
     Options opts;
     opts.base.outputLanguage = Language::LANG_AST;
     opts.base.outputLanguageWasSetByUser = true;
-    d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
+    d_smt.reset(new SmtEngine(d_nodeManager, &opts));
   }
 
   std::unique_ptr<SmtEngine> d_smt;
@@ -653,7 +653,7 @@ TEST_F(TestNodeBlackNode, dagifier)
 TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
   std::vector<Node> children;
   for (Node child : add)
@@ -667,7 +667,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
 TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
   std::vector<TNode> children;
   for (TNode child : add)
@@ -681,7 +681,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
 TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
   TNode add_tnode = add_node;
   std::vector<Node> children;
@@ -696,7 +696,7 @@ TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
 TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
   TNode add_tnode = add_node;
   std::vector<TNode> children;
@@ -801,8 +801,8 @@ TNode level1(NodeManager* nm) { return level0(nm); }
 TEST_F(TestNodeBlackNode, node_tnode_usage)
 {
   Node n;
-  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
-  ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
+  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager));
+  ASSERT_DEATH(n = level1(d_nodeManager), "d_nv->d_rc > 0");
 }
 
 }  // namespace test
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index fc8b6fb7b..05ccfc90c 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -62,14 +62,14 @@ TEST_F(TestNodeBlackNodeBuilder, ctors)
   ASSERT_EQ(spec.getKind(), d_specKind);
   ASSERT_EQ(spec.getNumChildren(), 0u);
 
-  NodeBuilder from_nm(d_nodeManager.get());
+  NodeBuilder from_nm(d_nodeManager);
   ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(from_nm.getNumChildren(),
                "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
-  NodeBuilder from_nm_kind(d_nodeManager.get(), d_specKind);
+  NodeBuilder from_nm_kind(d_nodeManager, d_specKind);
   ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
   ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
 
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index d8db32a4b..d3d05040f 100644
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -36,7 +36,7 @@ class TestNodeWhiteTypeNode : public TestNode
   void SetUp() override
   {
     TestNode::SetUp();
-    d_smt.reset(new SmtEngine(d_nodeManager.get()));
+    d_smt.reset(new SmtEngine(d_nodeManager));
   }
   std::unique_ptr<SmtEngine> d_smt;
 };
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 68758f766..329c565ea 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -2053,16 +2053,16 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
           bv::utils::mkExtract(
               d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0)));
 
-  NodeBuilder nbx(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbx(d_nodeManager, kind::BITVECTOR_MULT);
   nbx << d_x << d_one << x;
   Node x_mul_one_mul_xx = nbx.constructNode();
-  NodeBuilder nby(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nby(d_nodeManager, kind::BITVECTOR_MULT);
   nby << d_y << y << d_one;
   Node y_mul_yy_mul_one = nby.constructNode();
-  NodeBuilder nbz(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbz(d_nodeManager, kind::BITVECTOR_MULT);
   nbz << d_three << d_z << z;
   Node three_mul_z_mul_zz = nbz.constructNode();
-  NodeBuilder nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbz2(d_nodeManager, kind::BITVECTOR_MULT);
   nbz2 << d_z << d_nine << z;
   Node z_mul_nine_mul_zz = nbz2.constructNode();
 
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index bc5bfe8f1..46bea5e19 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -150,7 +150,6 @@ class TestPropWhiteCnfStream : public TestSmt
 
 TEST_F(TestPropWhiteCnfStream, and)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
@@ -161,7 +160,6 @@ TEST_F(TestPropWhiteCnfStream, and)
 
 TEST_F(TestPropWhiteCnfStream, complex_expr)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
@@ -184,21 +182,18 @@ TEST_F(TestPropWhiteCnfStream, complex_expr)
 
 TEST_F(TestPropWhiteCnfStream, true)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
   ASSERT_TRUE(d_satSolver->addClauseCalled());
 }
 
 TEST_F(TestPropWhiteCnfStream, false)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
   ASSERT_TRUE(d_satSolver->addClauseCalled());
 }
 
 TEST_F(TestPropWhiteCnfStream, iff)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
@@ -208,7 +203,6 @@ TEST_F(TestPropWhiteCnfStream, iff)
 
 TEST_F(TestPropWhiteCnfStream, implies)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
@@ -218,7 +212,6 @@ TEST_F(TestPropWhiteCnfStream, implies)
 
 TEST_F(TestPropWhiteCnfStream, not )
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
       d_nodeManager->mkNode(kind::NOT, a), false, false);
@@ -227,7 +220,6 @@ TEST_F(TestPropWhiteCnfStream, not )
 
 TEST_F(TestPropWhiteCnfStream, or)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
@@ -238,7 +230,6 @@ TEST_F(TestPropWhiteCnfStream, or)
 
 TEST_F(TestPropWhiteCnfStream, var)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(a, false, false);
@@ -250,7 +241,6 @@ TEST_F(TestPropWhiteCnfStream, var)
 
 TEST_F(TestPropWhiteCnfStream, xor)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
@@ -260,7 +250,6 @@ TEST_F(TestPropWhiteCnfStream, xor)
 
 TEST_F(TestPropWhiteCnfStream, ensure_literal)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
diff --git a/test/unit/test_env.h b/test/unit/test_env.h
index a0c7c68c3..b3f60a98a 100644
--- a/test/unit/test_env.h
+++ b/test/unit/test_env.h
@@ -33,13 +33,12 @@ class TestEnv : public TestInternal
   void SetUp() override
   {
     d_options.reset(new Options());
-    d_nodeManager.reset(new NodeManager());
-    d_env.reset(new Env(d_nodeManager.get(), d_options.get()));
+    d_nodeManager = NodeManager::currentNM();
+    d_env.reset(new Env(d_nodeManager, d_options.get()));
   }
 
-
   std::unique_ptr<Options> d_options;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   std::unique_ptr<Env> d_env;
 };
 
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 4250bb7da..a6a85b1b1 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -30,17 +30,16 @@ class TestNode : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager());
+    d_nodeManager = NodeManager::currentNM();
+    d_nodeManager->init();
     d_skolemManager = d_nodeManager->getSkolemManager();
-    d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
     d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
     d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType()));
     d_realTypeNode.reset(new TypeNode(d_nodeManager->realType()));
   }
 
-  std::unique_ptr<NodeManagerScope> d_scope;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   SkolemManager* d_skolemManager;
   std::unique_ptr<TypeNode> d_boolTypeNode;
   std::unique_ptr<TypeNode> d_bvTypeNode;
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 1cc6b0507..92701d60c 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -44,15 +44,14 @@ class TestSmt : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager());
+    d_nodeManager = NodeManager::currentNM();
+    d_nodeManager->init();
     d_skolemManager = d_nodeManager->getSkolemManager();
-    d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
-    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
+    d_smtEngine.reset(new SmtEngine(d_nodeManager));
     d_smtEngine->finishInit();
   }
 
-  std::unique_ptr<NodeManagerScope> d_nmScope;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   SkolemManager* d_skolemManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
@@ -62,14 +61,13 @@ class TestSmtNoFinishInit : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager());
+    d_nodeManager = NodeManager::currentNM();
+    d_nodeManager->init();
     d_skolemManager = d_nodeManager->getSkolemManager();
-    d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
-    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
+    d_smtEngine.reset(new SmtEngine(d_nodeManager));
   }
 
-  std::unique_ptr<NodeManagerScope> d_nmScope;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   SkolemManager* d_skolemManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp
index 3d5f7a8c5..0a2bcb532 100644
--- a/test/unit/theory/theory_arith_cad_white.cpp
+++ b/test/unit/theory/theory_arith_cad_white.cpp
@@ -51,7 +51,7 @@ class TestTheoryWhiteArithCAD : public TestSmt
     d_realType.reset(new TypeNode(d_nodeManager->realType()));
     d_intType.reset(new TypeNode(d_nodeManager->integerType()));
     Trace.on("cad-check");
-    nodeManager = d_nodeManager.get();
+    nodeManager = d_nodeManager;
   }
 
   Node dummy(int i) const { return d_nodeManager->mkConst(Rational(i)); }
diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
index eace59c96..682ae5bb2 100644
--- a/test/unit/theory/theory_bags_type_rules_white.cpp
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -88,9 +88,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
                                        d_nodeManager->mkConst(Rational(1)));
 
   // only positive multiplicity are constants
-  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative));
-  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero));
-  ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive));
+  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative));
+  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero));
+  ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive));
 }
 
 TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)