Add the distributed equality engine manager (#4867)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Aug 2020 16:34:04 +0000 (11:34 -0500)
committerGitHub <noreply@github.com>
Thu, 13 Aug 2020 16:34:04 +0000 (11:34 -0500)
commite6f55a60a3a65c55c04cb8bd88d47d6207677a29
tree5f7e2a32e38c03146d1739e8394a78c1baf30196
parent2fc0fea69f6350db55d217e710efcc08ac56b4db
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
src/CMakeLists.txt
src/theory/ee_manager_distributed.cpp [new file with mode: 0644]
src/theory/ee_manager_distributed.h [new file with mode: 0644]
src/theory/ee_setup_info.h [new file with mode: 0644]
src/theory/theory.cpp
src/theory/theory.h