diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-30 10:06:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-30 10:06:58 -0500 |
| commit | 7127be18692e2fd32bd2dfce53e50c105ed8a25d (patch) | |
| tree | 0ac218e0effcebf81629c4d90508a7d8bb4f3182 /src/theory/ee_manager_distributed.h | |
| parent | 0cf0dc3b3661e668f8c03113faad5078d91cea98 (diff) | |
Dynamic allocation of equality engine for shared solver (#5152)
This updates shared solver to have dynamic allocation of equality engine, analogous to theory solvers.
Diffstat (limited to 'src/theory/ee_manager_distributed.h')
| -rw-r--r-- | src/theory/ee_manager_distributed.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 90beb0d3b..c7c1e7f4c 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -89,6 +89,8 @@ class EqEngineManagerDistributed : public EqEngineManager std::unique_ptr<MasterNotifyClass> d_masterEENotify; /** The master equality engine. */ std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngine; + /** The equality engine of the shared solver / shared terms database. */ + std::unique_ptr<eq::EqualityEngine> d_stbEqualityEngine; }; } // namespace theory |