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 eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine()
  81 {
  82   return d_eemanager->getCoreEqualityEngine();
  83 }
  84
  85 void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
  86
  87 void CombinationEngine::postProcessModel(bool incomplete)
  88 {
  89   // should have a consistent core equality engine
  90   eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine();
  91   if (mee != nullptr)
  92   {
  93     AlwaysAssert(mee->consistent());
  94   }
  95   // postprocess with the model
  96   d_mmanager->postProcessModel(incomplete);
  97 }
  98
  99 theory::TheoryModel* CombinationEngine::getModel()
 100 {
 101   return d_mmanager->getModel();
 102 }
 103
 104 SharedSolver* CombinationEngine::getSharedSolver()
 105 {
 106   return d_sharedSolver.get();
 107 }
 108 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
 109
 110 eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
 111 {
 112   // by default, no notifications from model's equality engine
 113   return nullptr;
 114 }
 115
 116 void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
 117 {
 118   d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
 119 }
 120
 121 void CombinationEngine::resetRound()
 122 {
 123   // compute the relevant terms?
 124 }
 125
 126 }  // namespace theory
 127 }  // namespace CVC4