diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-25 07:10:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-25 07:10:38 -0500 |
| commit | 16578fca1c50d2ca9fce45c9c262db7ff6e2fd92 (patch) | |
| tree | dc827a563e52198b1519c746718b2a976e0c4d16 /src/theory/theory_engine.cpp | |
| parent | 5aeb8b78c4a26b274dbfecc882c0e0bb836cb398 (diff) | |
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.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cf29039ff..647a40999 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -167,7 +167,8 @@ void TheoryEngine::finishInit() { } // Initialize the model - d_eeDistributed->initializeModel(d_curr_model); + // !!!! temporary, will be part of combination engine initialization + d_eeDistributed->initializeModel(d_curr_model, nullptr); // set the core equality engine on quantifiers engine if (d_logicInfo.isQuantified()) |