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.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 141b0c46c..26997e084 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -74,5 +74,7 @@ int main(int argc, char* argv[])
       main::pExecutor->printStatistics(solver->getDriverOptions().err());
     }
   }
+  // Make sure that the command executor is destroyed before the node manager.
+  main::pExecutor.reset();
   exit(1);
 }