Add the shared solver (#4982)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 18 Sep 2020 17:52:16 +0000 (12:52 -0500)
committerGitHub <noreply@github.com>
Fri, 18 Sep 2020 17:52:16 +0000 (12:52 -0500)
commit30678fb782e88412469db4decd2cb42919f4ea02
tree505b7d4ec705e74d036d3b498f8ab2b4092c9fae
parentf92c4476e335322c1eeaa9e15ff5e1fda06181fe
Add the shared solver (#4982)

This PR adds the definition for the "shared solver", it does not connect it to TheoryEngine/CombinationEngine yet. This is an object that behaves like a "glue" theory solver and has a special role in TheoryEngine.

In the current architecture, the "SharedTermsDatabase" is the "shared solver", although in the central architecture, the shared solver will be required to behave differently. This PR adds the abstract definition of shared solver, where notice SharedSolverDistributed is a thin layer on top of SharedTermsDatabase.

In a followup PR, CombinationEngine will maintain a shared solver and ~5 blocks of code in TheoryEngine will be callbacks to the SharedSolver. Also, eventually the code for SharedTermsDatabase should be split: the parts involving equality reason/propagation/explanation should be migrated into SharedSolverDistributed, and the parts related to registration will remain in SharedTermsDatabase (to also be used in the planned SharedSolverCentral).

FYI @barrettcw
src/CMakeLists.txt
src/theory/shared_solver.cpp [new file with mode: 0644]
src/theory/shared_solver.h [new file with mode: 0644]
src/theory/shared_solver_distributed.cpp [new file with mode: 0644]
src/theory/shared_solver_distributed.h [new file with mode: 0644]
src/theory/shared_terms_database.cpp
src/theory/shared_terms_database.h
src/theory/theory_engine.h