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.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.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 725a932a2..31b44aa70 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -75,8 +75,6 @@ void TheoryModel::finishInit() } void TheoryModel::reset(){ - d_modelBuilt = false; - d_modelBuiltSuccess = false; d_modelCache.clear(); d_comment_str.clear(); d_sep_heap = Node::null(); |