From 1fe9c2efe36b126c70097b0f83db5654e0abcabe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 26 Sep 2020 10:07:42 -0500 Subject: 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 --- src/theory/theory_engine.h | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'src/theory/theory_engine.h') 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 d_tepg; //--------------------------------- end new proofs - - /** - * The database of shared terms. - */ - SharedTermsDatabase d_sharedTerms; - /** The combination manager we are using */ std::unique_ptr 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; -- cgit v1.2.3