Introduce quantifiers inference manager (#5821)

[cvc5.git] / src / theory / combination_engine.cpp

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 7ff2848dfb275d9a0b2ce7a06cf98566010efef7..5e242659f238c350073e99dff8fc721b66f0888d 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -18,6 +18,7 @@
 #include "theory/care_graph.h"
 #include "theory/ee_manager_distributed.h"
 #include "theory/model_manager_distributed.h"
+#include "theory/shared_solver_distributed.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
@@ -27,10 +28,12 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
                                      const std::vector<Theory*>& paraTheories,
                                      ProofNodeManager* pnm)
     : d_te(te),
+      d_pnm(pnm),
       d_logicInfo(te.getLogicInfo()),
       d_paraTheories(paraTheories),
       d_eemanager(nullptr),
       d_mmanager(nullptr),
+      d_sharedSolver(nullptr),
       d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
                    : nullptr)
 {
@@ -43,8 +46,11 @@ void CombinationEngine::finishInit()
   // create the equality engine, model manager, and shared solver
   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
   {
+    // use the distributed shared solver
+    d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
     // make the distributed equality engine manager
-    d_eemanager.reset(new EqEngineManagerDistributed(d_te));
+    d_eemanager.reset(
+        new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
     // make the distributed model manager
     d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
   }
@@ -95,6 +101,10 @@ theory::TheoryModel* CombinationEngine::getModel()
   return d_mmanager->getModel();
 }
 
+SharedSolver* CombinationEngine::getSharedSolver()
+{
+  return d_sharedSolver.get();
+}
 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
 
 eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()