src/theory/ee_manager.h

   1 /*********************                                                        */
   2 /*! \file ee_manager.h
   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 "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__EE_MANAGER__H
  18 #define CVC4__THEORY__EE_MANAGER__H
  19
  20 #include <map>
  21 #include <memory>
  22
  23 #include "theory/ee_setup_info.h"
  24 #include "theory/theory.h"
  25 #include "theory/uf/equality_engine.h"
  26
  27 namespace CVC4 {
  28
  29 class TheoryEngine;
  30
  31 namespace theory {
  32
  33 /**
  34  * This is (theory-agnostic) information associated with the management of
  35  * an equality engine for a single theory. This information is maintained
  36  * by the manager class below.
  37  *
  38  * Currently, this simply is the equality engine itself, for memory
  39  * management purposes.
  40  */
  41 struct EeTheoryInfo
  42 {
  43   EeTheoryInfo() : d_usedEe(nullptr) {}
  44   /** Equality engine that is used (if it exists) */
  45   eq::EqualityEngine* d_usedEe;
  46   /** Equality engine allocated specifically for this theory (if it exists) */
  47   std::unique_ptr<eq::EqualityEngine> d_allocEe;
  48 };
  49
  50 /** Virtual base class for equality engine managers */
  51 class EqEngineManager
  52 {
  53  public:
  54   EqEngineManager(TheoryEngine& te);
  55   virtual ~EqEngineManager() {}
  56   /**
  57    * Initialize theories, called during TheoryEngine::finishInit after theory
  58    * objects have been created but prior to their final initialization. This
  59    * sets up equality engines for all theories.
  60    *
  61    * This method is context-independent, and is applied once during
  62    * the lifetime of TheoryEngine (during finishInit).
  63    */
  64   virtual void initializeTheories() = 0;
  65   /**
  66    * Get the equality engine theory information for theory with the given id.
  67    */
  68   const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
  69   /**
  70    * Get the core equality engine, which is the equality engine that the
  71    * quantifiers engine should use. This corresponds to the master equality
  72    * engine if eeMode is distributed, or the central equality engine if eeMode
  73    * is central.
  74    */
  75   virtual eq::EqualityEngine* getCoreEqualityEngine() = 0;
  76
  77   /** Allocate equality engine that is context-dependent on c with info esi */
  78   eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
  79                                              context::Context* c);
  80
  81  protected:
  82   /** Reference to the theory engine */
  83   TheoryEngine& d_te;
  84   /** Information related to the equality engine, per theory. */
  85   std::map<TheoryId, EeTheoryInfo> d_einfo;
  86 };
  87
  88 }  // namespace theory
  89 }  // namespace CVC4
  90
  91 #endif /* CVC4__THEORY__EE_MANAGER__H */