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_logicInfo(te.getLogicInfo()),
  32       d_paraTheories(paraTheories),
  33       d_eemanager(nullptr),
  34       d_mmanager(nullptr),
  35       d_sharedSolver(nullptr),
  36       d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
  37                    : nullptr)
  38 {
  39 }
  40
  41 CombinationEngine::~CombinationEngine() {}
  42
  43 void CombinationEngine::finishInit()
  44 {
  45   // create the equality engine, model manager, and shared solver
  46   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
  47   {
  48     // use the distributed shared solver
  49     d_sharedSolver.reset(new SharedSolverDistributed(d_te));
  50     // make the distributed equality engine manager
  51     d_eemanager.reset(
  52         new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
  53     // make the distributed model manager
  54     d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
  55   }
  56   else
  57   {
  58     Unhandled() << "CombinationEngine::finishInit: equality engine mode "
  59                 << options::eeMode() << " not supported";
  60   }
  61
  62   Assert(d_eemanager != nullptr);
  63
  64   // initialize equality engines in all theories, including quantifiers engine
  65   // and the (provided) shared solver
  66   d_eemanager->initializeTheories();
  67
  68   Assert(d_mmanager != nullptr);
  69   // initialize the model manager, based on the notify object of this class
  70   eq::EqualityEngineNotify* meen = getModelEqualityEngineNotify();
  71   d_mmanager->finishInit(meen);
  72 }
  73
  74 const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const
  75 {
  76   return d_eemanager->getEeTheoryInfo(tid);
  77 }
  78
  79 eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine()
  80 {
  81   return d_eemanager->getCoreEqualityEngine();
  82 }
  83
  84 void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
  85
  86 void CombinationEngine::postProcessModel(bool incomplete)
  87 {
  88   // should have a consistent core equality engine
  89   eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine();
  90   if (mee != nullptr)
  91   {
  92     AlwaysAssert(mee->consistent());
  93   }
  94   // postprocess with the model
  95   d_mmanager->postProcessModel(incomplete);
  96 }
  97
  98 theory::TheoryModel* CombinationEngine::getModel()
  99 {
 100   return d_mmanager->getModel();
 101 }
 102
 103 SharedSolver* CombinationEngine::getSharedSolver()
 104 {
 105   return d_sharedSolver.get();
 106 }
 107 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
 108
 109 eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
 110 {
 111   // by default, no notifications from model's equality engine
 112   return nullptr;
 113 }
 114
 115 void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
 116 {
 117   d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
 118 }
 119
 120 void CombinationEngine::resetRound()
 121 {
 122   // compute the relevant terms?
 123 }
 124
 125 }  // namespace theory
 126 }  // namespace CVC4