blob: 822f3a95bf125e1b6b820e2717196f8800bd6c33 (
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
|
/********************* */
/*! \file ecdata.cpp
** \verbatim
** Original author: taking
** Major contributors: mdeters
** 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 Implementation of equivalence class data for UF theory.
**
** Implementation of equivalence class data for UF theory. This is a
** context-dependent object.
**/
#include "theory/uf/ecdata.h"
using namespace CVC4;
using namespace context;
using namespace theory;
using namespace uf;
ECData::ECData(Context * context, TNode n) :
ContextObj(context),
d_find(this),
d_rep(n),
d_watchListSize(0),
d_first(NULL),
d_last(NULL) {
}
bool ECData::isClassRep() {
return this == this->d_find;
}
void ECData::addPredecessor(TNode n) {
Assert(isClassRep());
makeCurrent();
Link * newPred = new(getCMM()) Link(getContext(), n, d_first);
d_first = newPred;
if(d_last == NULL) {
d_last = newPred;
}
++d_watchListSize;
}
ContextObj* ECData::save(ContextMemoryManager* pCMM) {
return new(pCMM) ECData(*this);
}
void ECData::restore(ContextObj* pContextObj) {
ECData* data = (ECData*)pContextObj;
d_find = data->d_find;
d_first = data->d_first;
d_last = data->d_last;
d_rep = data->d_rep;
d_watchListSize = data->d_watchListSize;
}
Node ECData::getRep() {
return d_rep;
}
unsigned ECData::getWatchListSize() {
return d_watchListSize;
}
void ECData::setFind(ECData * ec) {
makeCurrent();
d_find = ec;
}
ECData* ECData::getFind() {
return d_find;
}
Link* ECData::getFirst() {
return d_first;
}
void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) {
Assert(nslave != nmaster);
Assert(nslave->getFind() == nmaster);
nmaster->makeCurrent();
nmaster->d_watchListSize += nslave->d_watchListSize;
if(nmaster->d_first == NULL) {
nmaster->d_first = nslave->d_first;
nmaster->d_last = nslave->d_last;
} else if(nslave->d_first != NULL) {
Link* currLast = nmaster->d_last;
currLast->d_next = nslave->d_first;
nmaster->d_last = nslave->d_last;
}
}
|