src/theory/combination_engine.cpp

   1 /*********************                                                        */
   2 /*! \file combination_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Management of a care graph based approach for theory combination.
  13  **/
  14
  15 #include "theory/combination_engine.h"
  16
  17 #include "expr/node_visitor.h"
  18 #include "theory/care_graph.h"
  19 #include "theory/ee_manager_distributed.h"
  20 #include "theory/model_manager_distributed.h"
  21 #include "theory/shared_solver_distributed.h"
  22 #include "theory/theory_engine.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 CombinationEngine::CombinationEngine(TheoryEngine& te,
  28                                      const std::vector<Theory*>& paraTheories,
  29                                      ProofNodeManager* pnm)
  30     : d_te(te),
  31       d_pnm(pnm),
  32       d_logicInfo(te.getLogicInfo()),
  33       d_paraTheories(paraTheories),
  34       d_eemanager(nullptr),
  35       d_mmanager(nullptr),
  36       d_sharedSolver(nullptr),
  37       d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
  38                    : nullptr)
  39 {
  40 }
  41
  42 CombinationEngine::~CombinationEngine() {}
  43
  44 void CombinationEngine::finishInit()
  45 {
  46   // create the equality engine, model manager, and shared solver
  47   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
  48   {
  49     // use the distributed shared solver
  50     d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
  51     // make the distributed equality engine manager
  52     d_eemanager.reset(
  53         new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
  54     // make the distributed model manager
  55     d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
  56   }
  57   else
  58   {
  59     Unhandled() << "CombinationEngine::finishInit: equality engine mode "
  60                 << options::eeMode() << " not supported";
  61   }
  62
  63   Assert(d_eemanager != nullptr);
  64
  65   // initialize equality engines in all theories, including quantifiers engine
  66   // and the (provided) shared solver
  67   d_eemanager->initializeTheories();
  68
  69   Assert(d_mmanager != nullptr);
  70   // initialize the model manager, based on the notify object of this class
  71   eq::EqualityEngineNotify* meen = getModelEqualityEngineNotify();
  72   d_mmanager->finishInit(meen);
  73 }
  74
  75 const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const
  76 {
  77   return d_eemanager->getEeTheoryInfo(tid);
  78 }
  79
  80 void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
  81
  82 void CombinationEngine::postProcessModel(bool incomplete)
  83 {
  84   d_eemanager->notifyModel(incomplete);
  85   // postprocess with the model
  86   d_mmanager->postProcessModel(incomplete);
  87 }
  88
  89 theory::TheoryModel* CombinationEngine::getModel()
  90 {
  91   return d_mmanager->getModel();
  92 }
  93
  94 SharedSolver* CombinationEngine::getSharedSolver()
  95 {
  96   return d_sharedSolver.get();
  97 }
  98 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
  99
 100 eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
 101 {
 102   // by default, no notifications from model's equality engine
 103   return nullptr;
 104 }
 105
 106 void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
 107 {
 108   d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
 109 }
 110
 111 void CombinationEngine::resetRound()
 112 {
 113   // compute the relevant terms?
 114 }
 115
 116 }  // namespace theory
 117 }  // namespace CVC4