src/theory/uf/equality_engine_notify.h

   1 /*********************                                                        */
   2 /*! \file equality_engine_notify.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
   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 The virtual class for notifications from the equality engine.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
  18 #define CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
  19
  20 #include "expr/node.h"
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace eq {
  25
  26 /**
  27  * Interface for equality engine notifications. All the notifications
  28  * are safe as TNodes, but not necessarily for negations.
  29  */
  30 class EqualityEngineNotify
  31 {
  32  public:
  33   virtual ~EqualityEngineNotify(){};
  34
  35   /**
  36    * Notifies about a trigger predicate that became true or false. Notice that
  37    * predicate can be an equality.
  38    *
  39    * @param predicate the trigger predicate that became true or false
  40    * @param value the value of the predicate
  41    */
  42   virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0;
  43
  44   /**
  45    * Notifies about the merge of two trigger terms.
  46    *
  47    * @param tag the theory that both triggers were tagged with
  48    * @param t1 a term marked as trigger
  49    * @param t2 a term marked as trigger
  50    * @param value true if equal, false if dis-equal
  51    */
  52   virtual bool eqNotifyTriggerTermEquality(TheoryId tag,
  53                                            TNode t1,
  54                                            TNode t2,
  55                                            bool value) = 0;
  56
  57   /**
  58    * Notifies about the merge of two constant terms. After this, all work is
  59    * suspended and all you can do is ask for explanations.
  60    *
  61    * @param t1 a constant term
  62    * @param t2 a constant term
  63    */
  64   virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
  65
  66   /**
  67    * Notifies about the creation of a new equality class.
  68    *
  69    * @param t the term forming the new class
  70    */
  71   virtual void eqNotifyNewClass(TNode t) = 0;
  72
  73   /**
  74    * Notifies about the merge of two classes (just after the merge).
  75    *
  76    * @param t1 a term
  77    * @param t2 a term
  78    */
  79   virtual void eqNotifyMerge(TNode t1, TNode t2) = 0;
  80
  81   /**
  82    * Notifies about the disequality of two terms.
  83    *
  84    * @param t1 a term
  85    * @param t2 a term
  86    * @param reason the reason
  87    */
  88   virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0;
  89
  90 }; /* class EqualityEngineNotify */
  91
  92 /**
  93  * Implementation of the notification interface that ignores all the
  94  * notifications.
  95  */
  96 class EqualityEngineNotifyNone : public EqualityEngineNotify
  97 {
  98  public:
  99   bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
 100   {
 101     return true;
 102   }
 103   bool eqNotifyTriggerTermEquality(TheoryId tag,
 104                                    TNode t1,
 105                                    TNode t2,
 106                                    bool value) override
 107   {
 108     return true;
 109   }
 110   void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
 111   void eqNotifyNewClass(TNode t) override {}
 112   void eqNotifyMerge(TNode t1, TNode t2) override {}
 113   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 114 }; /* class EqualityEngineNotifyNone */
 115
 116 }  // Namespace eq
 117 }  // Namespace theory
 118 }  // Namespace CVC4
 119
 120 #endif