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   }
  65
  66   const LogicInfo& logicInfo = d_te.getLogicInfo();
  67   if (logicInfo.isQuantified())
  68   {
  69     // construct the master equality engine
  70     Assert(d_masterEqualityEngine == nullptr);
  71     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
  72     Assert(qe != nullptr);
  73     d_masterEENotify.reset(new MasterNotifyClass(qe));
  74     d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
  75                                                         d_te.getSatContext(),
  76                                                         "theory::master",
  77                                                         false));
  78
  79     for (TheoryId theoryId = theory::THEORY_FIRST;
  80          theoryId != theory::THEORY_LAST;
  81          ++theoryId)
  82     {
  83       Theory* t = d_te.theoryOf(theoryId);
  84       if (t == nullptr)
  85       {
  86         // theory not active, skip
  87         continue;
  88       }
  89       EeTheoryInfo& eet = d_einfo[theoryId];
  90       // Get the allocated equality engine, and connect it to the master
  91       // equality engine.
  92       eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
  93       if (eeAlloc != nullptr)
  94       {
  95         // set the master equality engine of the theory's equality engine
  96         eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
  97       }
  98     }
  99   }
 100 }
 101
 102 void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
 103 {
 104   // adds t to the quantifiers term database
 105   d_quantEngine->eqNotifyNewClass(t);
 106 }
 107
 108 eq::EqualityEngine* EqEngineManagerDistributed::getMasterEqualityEngine()
 109 {
 110   return d_masterEqualityEngine.get();
 111 }
 112
 113 eq::EqualityEngine* EqEngineManagerDistributed::allocateEqualityEngine(
 114     EeSetupInfo& esi, context::Context* c)
 115 {
 116   if (esi.d_notify != nullptr)
 117   {
 118     return new eq::EqualityEngine(
 119         *esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers);
 120   }
 121   // the theory doesn't care about explicit notifications
 122   return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers);
 123 }
 124
 125 }  // namespace theory
 126 }  // namespace CVC4