Connect combination engine to theory engine (#4940)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 26 Aug 2020 01:18:52 +0000 (20:18 -0500)
committerGitHub <noreply@github.com>
Wed, 26 Aug 2020 01:18:52 +0000 (20:18 -0500)
commita407bd70c09724dc20af3241775abedd3a73ec67
treef130f92cb1ede63516a00197f069bb8720e2abde
parent34eac85599875517732d53a5cc1acd3ab60479d1
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.
src/theory/quantifiers_engine.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_model.cpp
src/theory/theory_model.h
src/theory/theory_model_builder.cpp
src/theory/theory_model_builder.h