diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-25 20:18:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-25 20:18:52 -0500 |
commit | a407bd70c09724dc20af3241775abedd3a73ec67 (patch) | |
tree | f130f92cb1ede63516a00197f069bb8720e2abde /src/theory/theory_model_builder.cpp | |
parent | 34eac85599875517732d53a5cc1acd3ab60479d1 (diff) |
Connect combination engine to theory engine (#4940)
This connects the implementation of CombinationEngine into TheoryEngine. By default, the combination engine of theory engine is CombinationCareGraph.
This PR also consolidates and simplifies how models are built, note that:
The TheoryModel object no longer tracks whether it is built, instead that is the job of ModelManager,
The TheoryModelBuilder object is no longer responsible for calling TheoryEngine's collect model info method.
Quantifiers engine uses a simpler interface for ensuring that TheoryEngine's model is built.
This PR also makes some minor simplifications to TheoryEngine from the centralEe branch.
Note that no significant behavior changes are intended in this PR.
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 25 |
1 files changed, 1 insertions, 24 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index c82486bdd..31ba60be1 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -372,32 +372,11 @@ void TheoryEngineModelBuilder::addToTypeList( } } -bool TheoryEngineModelBuilder::buildModel(Model* m) +bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) { Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl; - TheoryModel* tm = (TheoryModel*)m; eq::EqualityEngine* ee = tm->d_equalityEngine; - // buildModel should only be called once per check - Assert(!tm->isBuilt()); - - // Reset model - tm->reset(); - - // mark as built - tm->d_modelBuilt = true; - tm->d_modelBuiltSuccess = false; - - // Collect model info from the theories - Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." - << std::endl; - if (!d_te->collectModelInfo(tm)) - { - Trace("model-builder") - << "TheoryEngineModelBuilder: fail collect model info" << std::endl; - return false; - } - Trace("model-builder") << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl; // model-builder specific initialization @@ -943,7 +922,6 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) return false; } Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl; - tm->d_modelBuiltSuccess = true; return true; } void TheoryEngineModelBuilder::computeAssignableInfo( @@ -1124,7 +1102,6 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m) void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) { #ifdef CVC4_ASSERTIONS - Assert(tm->isBuilt()); if (tm->hasApproximations()) { // models with approximations may fail the assertions below |