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
141
142
143
144
145
146
147
148
149
|
/********************* */
/*! \file congruence_closure.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief The congruence closure module
**
** The congruence closure module.
**/
#include "cvc4_private.h"
#ifndef __CVC4__UTIL__CONGRUENCE_CLOSURE_H
#define __CVC4__UTIL__CONGRUENCE_CLOSURE_H
#include <list>
#include <algorithm>
#include <utility>
#include <ext/hash_map>
#include "expr/node_manager.h"
#include "expr/node.h"
#include "context/cdmap.h"
namespace CVC4 {
/**
* Congruence closure module for CVC4.
*
* This is a service class for theories. One uses a CongruenceClosure
* by adding a number of relevant terms with addTerm() and equalities
* with addEquality(). It then gets notified (through OutputChannel,
* below), of new equalities.
*
* OutputChannel is a template argument (it's probably a thin layer,
* and we want to avoid a virtual call hierarchy in this case, and
* enable aggressive inlining). It need only implement one method,
* merge():
*
* class MyOutputChannel {
* public:
* void merge(TNode a, TNode b) {
* // CongruenceClosure is notifying us that "a" is now the EC
* // representative for "b" in this context. After a pop, "a"
* // will be its own representative again. Note that "a" and
* // "b" might never have been added with addTerm(). However,
* // something in their equivalence class was (for which a
* // previous merge() would have notified you of their EC
* // representative, which is now "a" or "b").
* //
* // This call is made immediately after the merge is done, and
* // while other pending merges may be on the queue. In particular,
* // any exception thrown from this function will immediately
* // exit the CongruenceClosure call. A subsequent call to
* // doPendingMerges() is necessary to continue merging;
* // doPendingMerges() is automatically done at the very beginning
* // of every call, including find() and areCongruent(), to ensure
* // consistency. However, if the context pops, the pending merges
* // up to that level are cleared.
* }
* };
*/
template <class OutputChannel>
class CongruenceClosure {
/** The output channel */
OutputChannel* d_out;
public:
/** Construct a congruence closure module instance */
CongruenceClosure(context::Context* ctxt, OutputChannel* out)
throw(AssertionException);
/**
* Add a term into CC consideration.
*/
void addTerm(TNode trm) throw(AssertionException);
/**
* Add an equality literal eq into CC consideration.
*/
void addEquality(TNode eq) throw(AssertionException);
/**
* Inquire whether two expressions are congruent.
*/
bool areCongruent(TNode a, TNode b) throw(AssertionException);
/**
* Find the EC representative for a term t
*/
TNode find(TNode t) throw(AssertionException);
/**
* Request an explanation for why a and b are in the same EC.
* Throws a CongruenceClosureException if they aren't in the same
* EC.
*/
Node explain(TNode a, TNode b)
throw(CongruenceClosureException, AssertionException);
/**
* Request an explanation for why the lhs and rhs of this equality
* are in the same EC. Throws a CongruenceClosureException if they
* aren't in the same EC.
*/
Node explain(TNode eq)
throw(CongruenceClosureException, AssertionException);
/**
* Request that any pending merges (canceled with an
* exception thrown from OutputChannel::merge()) be
* performed and the OutputChannel notified.
*/
void doPendingMerges() throw(AssertionException);
private:
/**
* Internal propagation of information.
*/
void propagate();
/**
* Internal lookup mapping.
*/
TNode lookup(TNode a);
/**
* Internal lookup mapping.
*/
void setLookup(TNode a, TNode b);
/**
* Internal normalization.
*/
Node normalize(TNode t);
};
}/* CVC4 namespace */
#endif /* __CVC4__UTIL__CONGRUENCE_CLOSURE_H */
|
