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