More flexible design for model manager distributed (#4976)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 20 Sep 2020 15:59:36 +0000 (10:59 -0500)
committerGitHub <noreply@github.com>
Sun, 20 Sep 2020 15:59:36 +0000 (10:59 -0500)
commit63e7c6bb6d9c99a5282241be8b32a04ea67dfb8d
tree8841b287b35143ff7470811ae164f74c71bc2cad
parent5f04a78336d648b02bc5cfdaaf734b6b350ee805
More flexible design for model manager distributed (#4976)

This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture.

This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine.

This PR is not intended to make any behavior changes to the current architecture.
src/theory/combination_engine.cpp
src/theory/ee_manager.cpp
src/theory/ee_manager.h
src/theory/ee_manager_distributed.cpp
src/theory/ee_manager_distributed.h
src/theory/model_manager.cpp
src/theory/model_manager.h
src/theory/model_manager_distributed.cpp
src/theory/model_manager_distributed.h
src/theory/theory_model.cpp
src/theory/theory_model.h