diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-21 18:51:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-21 18:51:37 -0500 |
| commit | 45fd2390beab04e560508d83c99492490c2d8d57 (patch) | |
| tree | 7b8d743c3f002a4cc0810d37da7224bc791d60a3 /src/theory/theory_model.h | |
| parent | 9ea213066b989a8154b1ebd40ebea3bc7e18c42d (diff) | |
Dynamic allocation of model equality engine (#4911)
This makes the equality engine manager responsible for initializing the equality engine of the model.
It also moves the base equality engine manager class to its own file.
Notice the code in TheoryEngine will undergo significant cleaning in forthcoming PRs when the "ModelManagerDistributed" is added. This PR adds temporary calls there to preserve the current behavior.
Diffstat (limited to 'src/theory/theory_model.h')
| -rw-r--r-- | src/theory/theory_model.h | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 2d6bdd2af..f465cec88 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -81,6 +81,17 @@ class TheoryModel : public Model public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); ~TheoryModel() override; + //---------------------------- initialization + /** Called to set the equality engine. */ + void setEqualityEngine(eq::EqualityEngine* ee); + /** + * Returns true if we need an equality engine, this has the same contract + * as Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi); + /** Finish init */ + void finishInit(); + //---------------------------- end initialization /** reset the model */ virtual void reset(); @@ -348,15 +359,14 @@ public: std::vector< Node > getFunctionsToAssign(); //---------------------------- end function values protected: + /** Unique name of this model */ + std::string d_name; /** substitution map for this model */ SubstitutionMap d_substitutions; /** whether we have tried to build this model in the current context */ bool d_modelBuilt; /** whether this model has been built successfully */ bool d_modelBuiltSuccess; - /** special local context for our equalityEngine so we can clear it - * independently of search context */ - context::Context* d_eeContext; /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine* d_equalityEngine; /** approximations (see recordApproximation) */ |