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