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/theory_engine.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 CombinationEngine::CombinationEngine(TheoryEngine& te,
  27                                      const std::vector<Theory*>& paraTheories,
  28                                      ProofNodeManager* pnm)
  29     : d_te(te),
  30       d_logicInfo(te.getLogicInfo()),
  31       d_paraTheories(paraTheories),
  32       d_eemanager(nullptr),
  33       d_mmanager(nullptr),
  34       d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
  35                    : nullptr)
  36 {
  37 }
  38
  39 CombinationEngine::~CombinationEngine() {}
  40
  41 void CombinationEngine::finishInit()
  42 {
  43   // create the equality engine, model manager, and shared solver
  44   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
  45   {
  46     // make the distributed equality engine manager
  47     d_eemanager.reset(new EqEngineManagerDistributed(d_te));
  48     // make the distributed model manager
  49     d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
  50   }
  51   else
  52   {
  53     Unhandled() << "CombinationEngine::finishInit: equality engine mode "
  54                 << options::eeMode() << " not supported";
  55   }
  56
  57   Assert(d_eemanager != nullptr);
  58
  59   // initialize equality engines in all theories, including quantifiers engine
  60   // and the (provided) shared solver
  61   d_eemanager->initializeTheories();
  62
  63   Assert(d_mmanager != nullptr);
  64   // initialize the model manager, based on the notify object of this class
  65   eq::EqualityEngineNotify* meen = getModelEqualityEngineNotify();
  66   d_mmanager->finishInit(meen);
  67 }
  68
  69 const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const
  70 {
  71   return d_eemanager->getEeTheoryInfo(tid);
  72 }
  73
  74 eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine()
  75 {
  76   return d_eemanager->getCoreEqualityEngine();
  77 }
  78
  79 void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
  80
  81 void CombinationEngine::postProcessModel(bool incomplete)
  82 {
  83   // should have a consistent core equality engine
  84   eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine();
  85   if (mee != nullptr)
  86   {
  87     AlwaysAssert(mee->consistent());
  88   }
  89   // postprocess with the model
  90   d_mmanager->postProcessModel(incomplete);
  91 }
  92
  93 theory::TheoryModel* CombinationEngine::getModel()
  94 {
  95   return d_mmanager->getModel();
  96 }
  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