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 EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te)
  24     : d_te(te), d_masterEENotify(nullptr)
  25 {
  26 }
  27
  28 EqEngineManagerDistributed::~EqEngineManagerDistributed()
  29 {
  30   // pop the model context which we pushed on initialization
  31   d_modelEeContext.pop();
  32 }
  33
  34 void EqEngineManagerDistributed::initializeTheories()
  35 {
  36   context::Context* c = d_te.getSatContext();
  37
  38   // allocate equality engines per theory
  39   for (TheoryId theoryId = theory::THEORY_FIRST;
  40        theoryId != theory::THEORY_LAST;
  41        ++theoryId)
  42   {
  43     Theory* t = d_te.theoryOf(theoryId);
  44     if (t == nullptr)
  45     {
  46       // theory not active, skip
  47       continue;
  48     }
  49     // always allocate an object in d_einfo here
  50     EeTheoryInfo& eet = d_einfo[theoryId];
  51     EeSetupInfo esi;
  52     if (!t->needsEqualityEngine(esi))
  53     {
  54       // theory said it doesn't need an equality engine, skip
  55       continue;
  56     }
  57     // allocate the equality engine
  58     eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
  59     // the theory uses the equality engine
  60     eet.d_usedEe = eet.d_allocEe.get();
  61   }
  62
  63   const LogicInfo& logicInfo = d_te.getLogicInfo();
  64   if (logicInfo.isQuantified())
  65   {
  66     // construct the master equality engine
  67     Assert(d_masterEqualityEngine == nullptr);
  68     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
  69     Assert(qe != nullptr);
  70     d_masterEENotify.reset(new MasterNotifyClass(qe));
  71     d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
  72                                                         d_te.getSatContext(),
  73                                                         "theory::master",
  74                                                         false));
  75
  76     for (TheoryId theoryId = theory::THEORY_FIRST;
  77          theoryId != theory::THEORY_LAST;
  78          ++theoryId)
  79     {
  80       Theory* t = d_te.theoryOf(theoryId);
  81       if (t == nullptr)
  82       {
  83         // theory not active, skip
  84         continue;
  85       }
  86       EeTheoryInfo& eet = d_einfo[theoryId];
  87       // Get the allocated equality engine, and connect it to the master
  88       // equality engine.
  89       eq::EqualityEngine* eeAlloc = eet.d_allocEe.get();
  90       if (eeAlloc != nullptr)
  91       {
  92         // set the master equality engine of the theory's equality engine
  93         eeAlloc->setMasterEqualityEngine(d_masterEqualityEngine.get());
  94       }
  95     }
  96   }
  97 }
  98
  99 void EqEngineManagerDistributed::initializeModel(
 100     TheoryModel* m, eq::EqualityEngineNotify* notify)
 101 {
 102   Assert(m != nullptr);
 103   // initialize the model equality engine
 104   EeSetupInfo esim;
 105   if (m->needsEqualityEngine(esim))
 106   {
 107     // use the provided notification object
 108     esim.d_notify = notify;
 109     d_modelEqualityEngine.reset(
 110         allocateEqualityEngine(esim, &d_modelEeContext));
 111     m->setEqualityEngine(d_modelEqualityEngine.get());
 112   }
 113   else
 114   {
 115     AlwaysAssert(false) << "Expected model to use equality engine";
 116   }
 117   m->finishInit();
 118   // We push a context during initialization since the model is cleared during
 119   // collectModelInfo using pop/push.
 120   d_modelEeContext.push();
 121 }
 122
 123 void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
 124 {
 125   // adds t to the quantifiers term database
 126   d_quantEngine->eqNotifyNewClass(t);
 127 }
 128
 129 context::Context* EqEngineManagerDistributed::getModelEqualityEngineContext()
 130 {
 131   return &d_modelEeContext;
 132 }
 133
 134 eq::EqualityEngine* EqEngineManagerDistributed::getModelEqualityEngine()
 135 {
 136   return d_modelEqualityEngine.get();
 137 }
 138
 139 eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine()
 140 {
 141   return d_masterEqualityEngine.get();
 142 }
 143
 144 eq::EqualityEngine* EqEngineManagerDistributed::allocateEqualityEngine(
 145     EeSetupInfo& esi, context::Context* c)
 146 {
 147   if (esi.d_notify != nullptr)
 148   {
 149     return new eq::EqualityEngine(
 150         *esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers);
 151   }
 152   // the theory doesn't care about explicit notifications
 153   return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers);
 154 }
 155
 156 }  // namespace theory
 157 }  // namespace CVC4