blob: 5a89a493906be2cfc941d6c8df11a3c26d902d9f (
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
|
/********************* */
/** ecdata.cpp
** 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.
**
**
**/
#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),
find(this),
rep(n),
watchListSize(0),
first(NULL),
last(NULL)
{}
bool ECData::isClassRep(){
return this == this->find;
}
void ECData::addPredecessor(TNode n, Context* context){
Assert(isClassRep());
makeCurrent();
Link * newPred = new (context->getCMM()) Link(context, n, first);
first = newPred;
if(last == NULL){
last = newPred;
}
++watchListSize;
}
ContextObj* ECData::save(ContextMemoryManager* pCMM) {
return new(pCMM) ECData(*this);
}
void ECData::restore(ContextObj* pContextObj) {
*this = *((ECData*)pContextObj);
}
Node ECData::getRep(){
return rep;
}
unsigned ECData::getWatchListSize(){
return watchListSize;
}
void ECData::setFind(ECData * ec){
makeCurrent();
find = ec;
}
ECData * ECData::getFind(){
return find;
}
Link* ECData::getFirst(){
return first;
}
void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){
Assert(nslave != nmaster);
Assert(nslave->getFind() == nmaster );
nmaster->makeCurrent();
nmaster->watchListSize += nslave->watchListSize;
if(nmaster->first == NULL){
nmaster->first = nslave->first;
nmaster->last = nslave->last;
}else if(nslave->first != NULL){
Link * currLast = nmaster->last;
currLast->next = nslave->first;
nmaster->last = nslave->last;
}
}
|