diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-13 11:34:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-13 11:34:04 -0500 |
| commit | e6f55a60a3a65c55c04cb8bd88d47d6207677a29 (patch) | |
| tree | 5f7e2a32e38c03146d1739e8394a78c1baf30196 /src/CMakeLists.txt | |
| parent | 2fc0fea69f6350db55d217e710efcc08ac56b4db (diff) | |
Add the distributed equality engine manager (#4867)
This is the first step towards making the approach for theory combination in CVC4 configurable.
This PR introduces the "distributed equality engine manager", which encapsulates the current policy that TheoryEngine uses regarding equality engines: each Theory creates a separate copy of an equality engine. The eventual plan is that the official equality engine of Theory is not necessarily unique to the theory, if equality engines are shared. A variant of this class could implement that policy.
This PR does not impact the code, it simply adds the definition of the class. A forthcoming PR will integrate this class into TheoryEngine, which will use dynamic allocation for equality engine objects.
FYI @barrettcw
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 67692f5c0..77c363317 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -478,6 +478,9 @@ libcvc4_add_sources( theory/decision_strategy.h theory/eager_proof_generator.cpp theory/eager_proof_generator.h + theory/ee_manager_distributed.cpp + theory/ee_manager_distributed.h + theory/ee_setup_info.h theory/engine_output_channel.cpp theory/engine_output_channel.h theory/evaluator.cpp |