blob: c32bc28d355eb259567b50c356c6624f62f0153d (
plain)
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
|
/********************* */
/*! \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 equalities with addEquality().
*
* 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.
* }
* };
*/
template <class OutputChannel>
class CongruenceClosure {
/** The output channel */
OutputChannel* d_out;
public:
/** Construct a congruence closure module instance */
CongruenceClosure(context::Context* ctxt, OutputChannel* out);
/**
* Add an equality literal eq into CC consideration. This is the
* only input to the congruence closure module.
*/
void addEquality(TNode eq);
/**
* 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);
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 */
|
