src/theory/ee_manager.cpp

   1 /*********************                                                        */
   2 /*! \file ee_manager.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 Utilities for management of equality engines.
  13  **/
  14
  15 #include "theory/ee_manager.h"
  16
  17 #include "theory/theory_model.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21
  22 EqEngineManager::EqEngineManager(TheoryEngine& te, SharedSolver& shs)
  23     : d_te(te), d_sharedSolver(shs)
  24 {
  25 }
  26
  27 const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const
  28 {
  29   std::map<TheoryId, EeTheoryInfo>::const_iterator it = d_einfo.find(tid);
  30   if (it != d_einfo.end())
  31   {
  32     return &it->second;
  33   }
  34   return nullptr;
  35 }
  36
  37 eq::EqualityEngine* EqEngineManager::allocateEqualityEngine(EeSetupInfo& esi,
  38                                                             context::Context* c)
  39 {
  40   if (esi.d_notify != nullptr)
  41   {
  42     return new eq::EqualityEngine(
  43         *esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers);
  44   }
  45   // the theory doesn't care about explicit notifications
  46   return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers);
  47 }
  48
  49 }  // namespace theory
  50 }  // namespace CVC4