src/theory/ee_manager_distributed.h

   1 /*********************                                                        */
   2 /*! \file ee_manager_distributed.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 Management of a distributed approach for equality engines over
  13  ** all theories.
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
  19 #define CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
  20
  21 #include <map>
  22 #include <memory>
  23
  24 #include "theory/ee_manager.h"
  25 #include "theory/uf/equality_engine.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 /**
  31  * The (distributed) equality engine manager. This encapsulates an architecture
  32  * in which all theories maintain their own copy of an equality engine.
  33  *
  34  * This class is not responsible for actually initializing equality engines in
  35  * theories (since this class does not have access to the internals of Theory).
  36  * Instead, it is only responsible for the construction of the equality
  37  * engine objects themselves. TheoryEngine is responsible for querying this
  38  * class during finishInit() to determine the equality engines to pass to each
  39  * theories based on getEeTheoryInfo.
  40  *
  41  * This class is also responsible for setting up the master equality engine,
  42  * which is used as a special communication channel to quantifiers engine (e.g.
  43  * for ensuring quantifiers E-matching is aware of terms from all theories).
  44  */
  45 class EqEngineManagerDistributed : public EqEngineManager
  46 {
  47  public:
  48   EqEngineManagerDistributed(TheoryEngine& te, SharedSolver& shs);
  49   ~EqEngineManagerDistributed();
  50   /**
  51    * Initialize theories. This method allocates unique equality engines
  52    * per theories and connects them to a master equality engine.
  53    */
  54   void initializeTheories() override;
  55   /** Notify model */
  56   void notifyModel(bool incomplete) override;
  57
  58  private:
  59   /** notify class for master equality engine */
  60   class MasterNotifyClass : public theory::eq::EqualityEngineNotify
  61   {
  62    public:
  63     MasterNotifyClass(QuantifiersEngine* qe) : d_quantEngine(qe) {}
  64     /**
  65      * Called when a new equivalence class is created in the master equality
  66      * engine.
  67      */
  68     void eqNotifyNewClass(TNode t) override;
  69
  70     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
  71     {
  72       return true;
  73     }
  74     bool eqNotifyTriggerTermEquality(TheoryId tag,
  75                                      TNode t1,
  76                                      TNode t2,
  77                                      bool value) override
  78     {
  79       return true;
  80     }
  81     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
  82     void eqNotifyMerge(TNode t1, TNode t2) override {}
  83     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
  84
  85    private:
  86     /** Pointer to quantifiers engine */
  87     QuantifiersEngine* d_quantEngine;
  88   };
  89   /** The master equality engine notify class */
  90   std::unique_ptr<MasterNotifyClass> d_masterEENotify;
  91   /** The master equality engine. */
  92   std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngine;
  93   /** The equality engine of the shared solver / shared terms database. */
  94   std::unique_ptr<eq::EqualityEngine> d_stbEqualityEngine;
  95 };
  96
  97 }  // namespace theory
  98 }  // namespace CVC4
  99
 100 #endif /* CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H */