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/ee_manager_distributed.h | |
| 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/ee_manager_distributed.h')
| -rw-r--r-- | src/theory/ee_manager_distributed.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 693466867..dd4608c9a 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -59,7 +59,8 @@ class EqEngineManagerDistributed : public EqEngineManager * Initialize model. This method allocates a new equality engine for the * model. */ - void initializeModel(TheoryModel* m) override; + void initializeModel(TheoryModel* m, + eq::EqualityEngineNotify* notify) override; /** * Get the model equality engine context. This is a dummy context that is * used for clearing the contents of the model's equality engine via |