src/theory/theory_eq_notify.h

   1 /*********************                                                        */
   2 /*! \file theory_eq_notify.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Tim King
   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 theory equality notify utility.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__THEORY_EQ_NOTIFY_H
  18 #define CVC4__THEORY__THEORY_EQ_NOTIFY_H
  19
  20 #include "expr/node.h"
  21 #include "theory/theory_inference_manager.h"
  22 #include "theory/uf/equality_engine_notify.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 /**
  28  * The default class for equality engine callbacks for a theory. This forwards
  29  * calls for trigger predicates, trigger term equalities and conflicts due to
  30  * constant merges to the provided theory inference manager.
  31  */
  32 class TheoryEqNotifyClass : public eq::EqualityEngineNotify
  33 {
  34  public:
  35   TheoryEqNotifyClass(TheoryInferenceManager& im) : d_im(im) {}
  36   ~TheoryEqNotifyClass() {}
  37
  38   bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
  39   {
  40     if (value)
  41     {
  42       return d_im.propagateLit(predicate);
  43     }
  44     return d_im.propagateLit(predicate.notNode());
  45   }
  46   bool eqNotifyTriggerTermEquality(TheoryId tag,
  47                                    TNode t1,
  48                                    TNode t2,
  49                                    bool value) override
  50   {
  51     if (value)
  52     {
  53       return d_im.propagateLit(t1.eqNode(t2));
  54     }
  55     return d_im.propagateLit(t1.eqNode(t2).notNode());
  56   }
  57   void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
  58   {
  59     d_im.conflictEqConstantMerge(t1, t2);
  60   }
  61   void eqNotifyNewClass(TNode t) override
  62   {
  63     // do nothing
  64   }
  65   void eqNotifyMerge(TNode t1, TNode t2) override
  66   {
  67     // do nothing
  68   }
  69   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
  70   {
  71     // do nothing
  72   }
  73
  74  protected:
  75   /** Reference to the theory inference manager */
  76   TheoryInferenceManager& d_im;
  77 };
  78
  79 }  // namespace theory
  80 }  // namespace CVC4
  81
  82 #endif