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