1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
/********************* */
/*! \file equality_engine_notify.h
** \verbatim
** Top contributors (to current version):
** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The virtual class for notifications from the equality engine.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
#define CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
#include "expr/node.h"
namespace CVC4 {
namespace theory {
namespace eq {
/**
* Interface for equality engine notifications. All the notifications
* are safe as TNodes, but not necessarily for negations.
*/
class EqualityEngineNotify
{
public:
virtual ~EqualityEngineNotify(){};
/**
* Notifies about a trigger equality that became true or false.
*
* @param equality the equality that became true or false
* @param value the value of the equality
*/
virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0;
/**
* Notifies about a trigger predicate that became true or false.
*
* @param predicate the trigger predicate that became true or false
* @param value the value of the predicate
*/
virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0;
/**
* Notifies about the merge of two trigger terms.
*
* @param tag the theory that both triggers were tagged with
* @param t1 a term marked as trigger
* @param t2 a term marked as trigger
* @param value true if equal, false if dis-equal
*/
virtual bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value) = 0;
/**
* Notifies about the merge of two constant terms. After this, all work is
* suspended and all you can do is ask for explanations.
*
* @param t1 a constant term
* @param t2 a constant term
*/
virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
/**
* Notifies about the creation of a new equality class.
*
* @param t the term forming the new class
*/
virtual void eqNotifyNewClass(TNode t) = 0;
/**
* Notifies about the merge of two classes (just before the merge).
*
* @param t1 a term
* @param t2 a term
*/
virtual void eqNotifyPreMerge(TNode t1, TNode t2) = 0;
/**
* Notifies about the merge of two classes (just after the merge).
*
* @param t1 a term
* @param t2 a term
*/
virtual void eqNotifyPostMerge(TNode t1, TNode t2) = 0;
/**
* Notifies about the disequality of two terms.
*
* @param t1 a term
* @param t2 a term
* @param reason the reason
*/
virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0;
}; /* class EqualityEngineNotify */
/**
* Implementation of the notification interface that ignores all the
* notifications.
*/
class EqualityEngineNotifyNone : public EqualityEngineNotify
{
public:
bool eqNotifyTriggerEquality(TNode equality, bool value) override
{
return true;
}
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
return true;
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value) override
{
return true;
}
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
void eqNotifyNewClass(TNode t) override {}
void eqNotifyPreMerge(TNode t1, TNode t2) override {}
void eqNotifyPostMerge(TNode t1, TNode t2) override {}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
}; /* class EqualityEngineNotifyNone */
} // Namespace eq
} // Namespace theory
} // Namespace CVC4
#endif
|
