src/theory/ee_manager_distributed.cpp

   1 /*********************                                                        */
   2 /*! \file ee_manager_distributed.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 distributed approach for equality sharing.
  13  **/
  14
  15 #include "theory/ee_manager_distributed.h"
  16
  17 #include "theory/quantifiers_engine.h"
  18 #include "theory/shared_solver.h"
  19 #include "theory/theory_engine.h"
  20
  21 namespace CVC4 {
  22 namespace theory {
  23
  24 EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te,
  25                                                        SharedSolver& shs)
  26     : EqEngineManager(te, shs), d_masterEENotify(nullptr)
  27 {
  28 }
  29
  30 EqEngineManagerDistributed::~EqEngineManagerDistributed()
  31 {
  32 }
  33
  34 void EqEngineManagerDistributed::initializeTheories()
  35 {
  36   context::Context* c = d_te.getSatContext();
  37   // initialize the shared solver
  38   EeSetupInfo esis;
  39   if (d_sharedSolver.needsEqualityEngine(esis))
  40   {
  41     // allocate an equality engine for the shared terms database
  42     d_stbEqualityEngine.reset(allocateEqualityEngine(esis, c));
  43     d_sharedSolver.setEqualityEngine(d_stbEqualityEngine.get());
  44   }
  45   else
  46   {
  47     Unhandled() << "Expected shared solver to use equality engine";
  48   }
  49
  50   const LogicInfo& logicInfo = d_te.getLogicInfo();
  51   if (logicInfo.isQuantified())
  52   {
  53     // construct the master equality engine
  54     Assert(d_masterEqualityEngine == nullptr);
  55     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
  56     Assert(qe != nullptr);
  57     d_masterEENotify.reset(new MasterNotifyClass(qe));
  58     d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
  59                                                         d_te.getSatContext(),
  60                                                         "theory::master",
  61                                                         false));
  62   }
  63   // allocate equality engines per theory
  64   for (TheoryId theoryId = theory::THEORY_FIRST;
  65        theoryId != theory::THEORY_LAST;
  66        ++theoryId)
  67   {
  68     Theory* t = d_te.theoryOf(theoryId);
  69     if (t == nullptr)
  70     {
  71       // theory not active, skip
  72       continue;
  73     }
  74     // always allocate an object in d_einfo here
  75     EeTheoryInfo& eet = d_einfo[theoryId];
  76     EeSetupInfo esi;
  77     if (!t->needsEqualityEngine(esi))
  78     {
  79       // the theory said it doesn't need an equality engine, skip
  80       continue;
  81     }
  82     if (esi.d_useMaster)
  83     {
  84       // the theory said it wants to use the master equality engine
  85       eet.d_usedEe = d_masterEqualityEngine.get();
  86       continue;
  87     }
  88     // allocate the equality engine
  89     eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
  90     // the theory uses the equality engine
  91     eet.d_usedEe = eet.d_allocEe.get();
  92     // if there is a master equality engine
  93     if (d_masterEqualityEngine != nullptr)
  94     {
  95       // set the master equality engine of the theory's equality engine
  96       eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine.get());
  97     }
  98   }
  99 }
 100
 101 void EqEngineManagerDistributed::notifyModel(bool incomplete)
 102 {
 103   // should have a consistent master equality engine
 104   if (d_masterEqualityEngine.get() != nullptr)
 105   {
 106     AlwaysAssert(d_masterEqualityEngine->consistent());
 107   }
 108 }
 109
 110 void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
 111 {
 112   // adds t to the quantifiers term database
 113   d_quantEngine->eqNotifyNewClass(t);
 114 }
 115
 116 }  // namespace theory
 117 }  // namespace CVC4