GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/equality_engine_notify.h Lines: 7 11 63.6 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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-2021 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
113987
class EqualityEngineNotify
31
{
32
 public:
33
122843
  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
8895
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
4
  void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
111
1629817
  void eqNotifyNewClass(TNode t) override {}
112
883612
  void eqNotifyMerge(TNode t1, TNode t2) override {}
113
639
  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