diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-26 10:07:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-26 10:07:42 -0500 |
commit | 1fe9c2efe36b126c70097b0f83db5654e0abcabe (patch) | |
tree | 46323cb7c712618a974092bced6f66dd07be3862 /src/theory/theory_engine.h | |
parent | 6ad02b5e0599149e0bd1548855aec8ac890f5a87 (diff) |
Connect the shared solver to theory engine (#5103)
This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.
It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.
This PR has no intended behavior changes.
FYI @barrettcw
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7639afdbf..cfca03515 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -154,14 +154,10 @@ class TheoryEngine { /** The proof generator */ std::shared_ptr<TheoryEngineProofGenerator> d_tepg; //--------------------------------- end new proofs - - /** - * The database of shared terms. - */ - SharedTermsDatabase d_sharedTerms; - /** The combination manager we are using */ std::unique_ptr<theory::CombinationEngine> d_tc; + /** The shared solver of the above combination engine. */ + theory::SharedSolver* d_sharedSolver; /** * The quantifiers engine */ @@ -176,9 +172,6 @@ class TheoryEngine { /** Default visitor for pre-registration */ PreRegisterVisitor d_preRegistrationVisitor; - /** Visitor for collecting shared terms */ - SharedTermsVisitor d_sharedTermsVisitor; - /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; |