diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-17 16:14:42 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-17 23:14:42 +0000 |
| commit | 4209fb71c97c06833ef320ad9c73590546c16fa2 (patch) | |
| tree | 5155ab68258970de7485b5e3e65d3cd3f79d1078 /AUTHORS | |
| parent | 1704b74ffa93b36a2e08e42ca21aad0991ad4d70 (diff) | |
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.
Diffstat (limited to 'AUTHORS')
0 files changed, 0 insertions, 0 deletions