Add the combination engine (#4939)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 25 Aug 2020 12:10:38 +0000 (07:10 -0500)
committerGitHub <noreply@github.com>
Tue, 25 Aug 2020 12:10:38 +0000 (07:10 -0500)
commit16578fca1c50d2ca9fce45c9c262db7ff6e2fd92
treedc827a563e52198b1519c746718b2a976e0c4d16
parent5aeb8b78c4a26b274dbfecc882c0e0bb836cb398
Add the combination engine (#4939)

This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR.

FYI @barrettcw

The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class.
src/CMakeLists.txt
src/options/theory_options.toml
src/theory/combination_care_graph.cpp [new file with mode: 0644]
src/theory/combination_care_graph.h [new file with mode: 0644]
src/theory/combination_engine.cpp [new file with mode: 0644]
src/theory/combination_engine.h [new file with mode: 0644]
src/theory/ee_manager.h
src/theory/ee_manager_distributed.cpp
src/theory/ee_manager_distributed.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h