blob: 34b6719d7e22b1757c73a7a6376afed182a2c68f (
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
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
150
151
152
153
|
/********************* */
/** theory_uf.h
** Original author: taking
** 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.
**
**
**/
#ifndef __CVC4__THEORY__THEORY_UF_H
#define __CVC4__THEORY__THEORY_UF_H
#include "expr/node.h"
#include "expr/attribute.h"
#include "theory/theory.h"
#include "context/context.h"
#include "theory/uf/ecdata.h"
namespace CVC4 {
namespace theory {
namespace uf {
class TheoryUF : public TheoryImpl<TheoryUF> {
private:
//TODO document
context::CDList<Node> d_assertions;
/**
* List of pending equivalence class merges.
*
* Tricky part:
* Must keep a hard link because new equality terms are created and appended
* to this list.
*/
context::CDList<Node> d_pending;
/** Index of the next pending equality to merge. */
context::CDO<unsigned> d_currentPendingIdx;
/** List of all disequalities this theory has seen. */
context::CDList<Node> d_disequality;
/**
* List of all of the terms that are registered in the current context.
* When registerTerm is called on a term we want to guarentee that there
* is a hard link to the term for the duration of the context in which
* register term is called.
* This invariant is enough for us to use soft links where we want is the
* current implementation as well as making ECAttr() not context dependent.
* Soft links used both in ECData, and Link.
*/
context::CDList<Node> d_registered;
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TheoryUF(context::Context* c, OutputChannel& out);
/** Destructor for the TheoryUF object. */
~TheoryUF();
//TODO Tim: I am going to delay documenting these functions while Morgan
//has pending changes to the contracts
void registerTerm(TNode n);
void preRegisterTerm(TNode n);
void check(Effort level);
void propagate(Effort level) {}
void explain(TNode n, Effort level) {}
private:
/**
* Checks whether 2 nodes are already in the same equivalence class tree.
* This should only be used internally, and it should only be done when
* the only thing done with the equivalence classes is an equality check.
*
* @returns true iff ccFind(x) == ccFind(y);
*/
bool sameCongruenceClass(TNode x, TNode y);
/**
* Checks whether Node x and Node y are currently congruent
* using the equivalence class data structures.
* @returns true iff
* |x| = n = |y| and
* x.getOperator() == y.getOperator() and
* forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
*/
bool equiv(TNode x, TNode y);
/**
* Merges 2 equivalence classes, checks wether any predecessors need to
* be set equal to complete congruence closure.
* The class with the smaller class size will be merged.
* @pre ecX->isClassRep()
* @pre ecY->isClassRep()
*/
void ccUnion(ECData* ecX, ECData* ecY);
/**
* Returns the representative of the equivalence class.
* May modify the find pointers associated with equivalence classes.
*/
ECData* ccFind(ECData* x);
/** Performs Congruence Closure to reflect the new additions to d_pending. */
void merge();
/** Constructs a conflict from an inconsistent disequality. */
Node constructConflict(TNode diseq);
};
/**
* Cleanup function for ECData. This will be used for called whenever
* a ECAttr is being destructed.
*/
struct ECCleanupFcn{
static void cleanup(ECData* & ec){
ec->deleteSelf();
}
};
/** Unique name to use for constructing ECAttr. */
struct EquivClass;
/**
* ECAttr is the attribute that maps a node to an equivalence class.
*/
typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
} /* CVC4::theory::uf namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__THEORY__THEORY_UF_H */
|
