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/theory_engine.h"
  19
  20 namespace CVC4 {
  21 namespace theory {
  22
  23 const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const
  24 {
  25   std::map<TheoryId, EeTheoryInfo>::const_iterator it = d_einfo.find(tid);
  26   if (it != d_einfo.end())
  27   {
  28     return &it->second;
  29   }
  30   return nullptr;
  31 }
  32
  33 EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te)
  34     : d_te(te), d_masterEENotify(nullptr)
  35 {
  36 }
  37
  38 EqEngineManagerDistributed::~EqEngineManagerDistributed() {}
  39
  40 void EqEngineManagerDistributed::finishInit()
  41 {
  42   context::Context* c = d_te.getSatContext();
  43   // allocate equality engines per theory
  44   for (TheoryId theoryId = theory::THEORY_FIRST;
  45        theoryId != theory::THEORY_LAST;
  46        ++theoryId)
  47   {
  48     Theory* t = d_te.theoryOf(theoryId);
  49     if (t == nullptr)
  50     {
  51       // theory not active, skip
  52       continue;
  53     }
  54     // always allocate an object in d_einfo here
  55     EeTheoryInfo& eet = d_einfo[theoryId];
  56     EeSetupInfo esi;
  57     if (!t->needsEqualityEngine(esi))
  58     {
  59       // theory said it doesn't need an equality engine, skip
  60       continue;
  61     }
  62     // allocate the equality engine
  63     eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
  64     eet.d_usedEe = eet.d_allocEe.get();
  65   }
  66
  67   const LogicInfo& logicInfo = d_te.getLogicInfo();
  68   if (logicInfo.isQuantified())
  69   {
  70     // construct the master equality engine
  71     Assert(d_masterEqualityEngine == nullptr);
  72     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
  73     Assert(qe != nullptr);
  74     d_masterEENotify.reset(new MasterNotifyClass(qe));
  75     d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
  76                                                         d_te.getSatContext(),
  77                                                         "theory::master",
  78                                                         false));
  79
  80     for (TheoryId theoryId = theory::THEORY_FIRST;
  81          theoryId != theory::THEORY_LAST;
  82          ++theoryId)
  83     {
  84       Theory* t = d_te.theoryOf(theoryId);
  85       if (t == nullptr)
  86       {
  87         // theory not active, skip
  88         continue;
  89       }
  90       EeTheoryInfo& eet = d_einfo[theoryId];
  91       // Get the allocated equality engine, and connect it to the master
  92       // equality engine.
  93       eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
  94       if (eeAlloc != nullptr)
  95       {
  96         // set the master equality engine of the theory's equality engine
  97         eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
  98       }
  99     }
 100   }
 101 }
 102
 103 void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
 104 {
 105   // adds t to the quantifiers term database
 106   d_quantEngine->eqNotifyNewClass(t);
 107 }
 108
 109 eq::EqualityEngine* EqEngineManagerDistributed::getMasterEqualityEngine()
 110 {
 111   return d_masterEqualityEngine.get();
 112 }
 113
 114 eq::EqualityEngine* EqEngineManagerDistributed::allocateEqualityEngine(
 115     EeSetupInfo& esi, context::Context* c)
 116 {
 117   if (esi.d_notify != nullptr)
 118   {
 119     return new eq::EqualityEngine(
 120         *esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers);
 121   }
 122   // the theory doesn't care about explicit notifications
 123   return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers);
 124 }
 125
 126 }  // namespace theory
 127 }  // namespace CVC4