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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
/********************* */
/*! \file static_fact_manager.cpp
** \verbatim
** Original author: Clark Barrett
** Major contributors: none
** Minor contributors (to current version): Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Path-compressing, backtrackable union-find using an undo
** stack. Refactored from the UF union-find.
**
** Path-compressing, backtrackable union-find using an undo stack
** rather than storing items in a CDMap<>.
**/
#include <iostream>
#include "theory/arrays/static_fact_manager.h"
#include "util/cvc4_assert.h"
#include "expr/node.h"
using namespace std;
namespace CVC4 {
namespace theory {
namespace arrays {
bool StaticFactManager::areEq(TNode a, TNode b) {
return (find(a) == find(b));
}
bool StaticFactManager::areDiseq(TNode a, TNode b) {
Node af = find(a);
Node bf = find(b);
Node left, right;
unsigned i;
for (i = 0; i < d_diseq.size(); ++i) {
left = find(d_diseq[i][0]);
right = find(d_diseq[i][1]);
if ((left == af && right == bf) ||
(left == bf && right == af)) {
return true;
}
}
return false;
}
void StaticFactManager::addDiseq(TNode eq) {
Assert(eq.getKind() == kind::EQUAL);
d_diseq.push_back(eq);
}
void StaticFactManager::addEq(TNode eq) {
Assert(eq.getKind() == kind::EQUAL);
Node a = find(eq[0]);
Node b = find(eq[1]);
if( a == b) {
return;
}
/*
* take care of the congruence closure part
*/
// make "a" the one with shorter diseqList
// CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
// CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
// if(deq_ia != d_disequalities.end()) {
// if(deq_ib == d_disequalities.end() ||
// (*deq_ia).second->size() > (*deq_ib).second->size()) {
// TNode tmp = a;
// a = b;
// b = tmp;
// }
// }
// a = find(a);
// b = find(b);
// b becomes the canon of a
setCanon(a, b);
// deq_ia = d_disequalities.find(a);
// map<TNode, TNode> alreadyDiseqs;
// if(deq_ia != d_disequalities.end()) {
// /*
// * Collecting the disequalities of b, no need to check for conflicts
// * since the representative of b does not change and we check all the things
// * in a's class when we look at the diseq list of find(a)
// */
// CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
// if(deq_ib != d_disequalities.end()) {
// CTNodeListAlloc* deq = (*deq_ib).second;
// for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) {
// TNode deqn = *j;
// TNode s = deqn[0];
// TNode t = deqn[1];
// TNode sp = find(s);
// TNode tp = find(t);
// Assert(sp == b || tp == b);
// if(sp == b) {
// alreadyDiseqs[tp] = deqn;
// } else {
// alreadyDiseqs[sp] = deqn;
// }
// }
// }
// /*
// * Looking for conflicts in the a disequality list. Note
// * that at this point a and b are already merged. Also has
// * the side effect that it adds them to the list of b (which
// * became the canonical representative)
// */
// CTNodeListAlloc* deqa = (*deq_ia).second;
// for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) {
// TNode deqn = (*i);
// Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF);
// TNode s = deqn[0];
// TNode t = deqn[1];
// TNode sp = find(s);
// TNode tp = find(t);
// if(find(s) == find(t)) {
// d_conflict = deqn;
// return;
// }
// Assert( sp == b || tp == b);
// // make sure not to add duplicates
// if(sp == b) {
// if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
// appendToDiseqList(b, deqn);
// alreadyDiseqs[tp] = deqn;
// }
// } else {
// if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
// appendToDiseqList(b, deqn);
// alreadyDiseqs[sp] = deqn;
// }
// }
// }
// }
// // TODO: check for equality propagations
// // a and b are find(a) and find(b) here
// checkPropagations(a,b);
// if(a.getType().isArray()) {
// checkRowLemmas(a,b);
// checkRowLemmas(b,a);
// // note the change in order, merge info adds the list of
// // the 2nd argument to the first
// d_infoMap.mergeInfo(b, a);
// }
}
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
|
