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
|
/********************* */
/*! \file equality_engine_notify.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Dejan Jovanovic
** 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 predicate that became true or false. Notice that
* predicate can be an equality.
*
* @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 after the merge).
*
* @param t1 a term
* @param t2 a term
*/
virtual void eqNotifyMerge(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 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 eqNotifyMerge(TNode t1, TNode t2) override {}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
}; /* class EqualityEngineNotifyNone */
} // Namespace eq
} // Namespace theory
} // Namespace CVC4
#endif
|
