blob: c8303a24559d1257da74af09132f0b9e6a6f8455 (
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
|
/********************* */
/** ecdata.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.
**
** Context dependent equivalence class datastructure for nodes.
** Currently keeps a context dependent watch list.
**/
#ifndef __CVC4__THEORY__UF__ECDATA_H
#define __CVC4__THEORY__UF__ECDATA_H
#include "expr/node.h"
#include "context/context.h"
#include "context/context_mm.h"
namespace CVC4 {
namespace theory {
struct Link {
context::CDO< Link* > next;
//TODO soft reference
Node data;
Link(context::Context* context, Node n, Link * l = NULL):
next(context, l), data(n)
{}
static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
return pCMM->newData(size);
}
};
class ECData : public context::ContextObj {
private:
ECData * find;
Node rep;
unsigned watchListSize;
Link * first;
Link * last;
context::ContextObj* save(context::ContextMemoryManager* pCMM);
void restore(context::ContextObj* pContextObj);
public:
/**
* Returns true if this ECData object is the current representative of
* the equivalence class.
*/
bool isClassRep();
/**
* Adds a node to the watch list of the equivalence class.
* Requires a context to do memory management.
* @param n the node to be added.
* @pre isClassRep() == true
*/
void addPredecessor(Node n, context::Context* context);
/**
* Creates a EQ with the representative n
* @param context the context to associate with this ecdata.
* This is required as ECData is context dependent
* @param n the node that corresponds to this ECData
*/
ECData(context::Context* context, const Node & n);
static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
static ECData * ccFind(ECData * fp);
/**
* Returns the representative of this ECData.
*/
Node getRep();
/**
* Returns the size of the equivalence class.
*/
unsigned getWatchListSize();
/**
* Returns a pointer the first member of the watch list.
*/
Link* getFirst();
/**
* Returns the find pointer of the ECData.
* If isClassRep(), then getFind() == this
*/
ECData* getFind();
/**
* @pre isClassRep() == true
* @pre ec->isClassRep() == true
* @post isClassRep() == false
* @post ec->isClassRep() == true
*/
void setFind(ECData * ec);
private:
/**
* @pre isClassRep() == true
*/
void setWatchListSize(unsigned newSize);
/**
* @pre isClassRep() == true
*/
void setFirst(Link * nfirst);
Link* getLast();
/**
* @pre isClassRep() == true
*/
void setLast(Link * nlast);
}; /* class ECData */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__UF__ECDATA_H */
|
