1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Dejan Jovanovic, Liana Hadarean, Clark Barrett |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#pragma once |
22 |
|
|
23 |
|
#include "theory/bv/theory_bv_rewrite_rules.h" |
24 |
|
#include "theory/bv/theory_bv_utils.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace bv { |
29 |
|
|
30 |
|
/* -------------------------------------------------------------------------- */ |
31 |
|
|
32 |
|
template<> inline |
33 |
335222 |
bool RewriteRule<ConcatFlatten>::applies(TNode node) { |
34 |
335222 |
return (node.getKind() == kind::BITVECTOR_CONCAT); |
35 |
|
} |
36 |
|
|
37 |
|
template<> inline |
38 |
167611 |
Node RewriteRule<ConcatFlatten>::apply(TNode node) { |
39 |
167611 |
Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl; |
40 |
335222 |
NodeBuilder result(kind::BITVECTOR_CONCAT); |
41 |
335222 |
std::vector<Node> processing_stack; |
42 |
167611 |
processing_stack.push_back(node); |
43 |
1615277 |
while (!processing_stack.empty()) { |
44 |
1447666 |
Node current = processing_stack.back(); |
45 |
723833 |
processing_stack.pop_back(); |
46 |
723833 |
if (current.getKind() == kind::BITVECTOR_CONCAT) { |
47 |
730392 |
for (int i = current.getNumChildren() - 1; i >= 0; i--) |
48 |
556222 |
processing_stack.push_back(current[i]); |
49 |
|
} else { |
50 |
549663 |
result << current; |
51 |
|
} |
52 |
|
} |
53 |
167611 |
Node resultNode = result; |
54 |
167611 |
Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl; |
55 |
335222 |
return resultNode; |
56 |
|
} |
57 |
|
|
58 |
|
/* -------------------------------------------------------------------------- */ |
59 |
|
|
60 |
|
template<> inline |
61 |
335222 |
bool RewriteRule<ConcatExtractMerge>::applies(TNode node) { |
62 |
335222 |
return (node.getKind() == kind::BITVECTOR_CONCAT); |
63 |
|
} |
64 |
|
|
65 |
|
template<> inline |
66 |
167611 |
Node RewriteRule<ConcatExtractMerge>::apply(TNode node) { |
67 |
|
|
68 |
167611 |
Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl; |
69 |
|
|
70 |
335222 |
std::vector<Node> mergedExtracts; |
71 |
|
|
72 |
335222 |
Node current = node[0]; |
73 |
167611 |
bool mergeStarted = false; |
74 |
167611 |
unsigned currentHigh = 0; |
75 |
167611 |
unsigned currentLow = 0; |
76 |
|
|
77 |
549663 |
for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) { |
78 |
|
// The next candidate for merging |
79 |
453152 |
Node next = node[i]; |
80 |
|
// If the current is not an extract we just go to the next |
81 |
693004 |
if (current.getKind() != kind::BITVECTOR_EXTRACT) { |
82 |
310952 |
mergedExtracts.push_back(current); |
83 |
310952 |
current = next; |
84 |
310952 |
continue; |
85 |
|
} |
86 |
|
// If it is an extract and the first one, get the extract parameters |
87 |
71100 |
else if (!mergeStarted) { |
88 |
71067 |
currentHigh = utils::getExtractHigh(current); |
89 |
71067 |
currentLow = utils::getExtractLow(current); |
90 |
|
} |
91 |
|
|
92 |
|
// If the next one can be merged, try to merge |
93 |
71100 |
bool merged = false; |
94 |
71100 |
if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) { |
95 |
|
// x[i : j] @ x[j - 1 : k] -> c x[i : k] |
96 |
24939 |
unsigned nextHigh = utils::getExtractHigh(next); |
97 |
24939 |
unsigned nextLow = utils::getExtractLow(next); |
98 |
24939 |
if(nextHigh + 1 == currentLow) { |
99 |
96 |
currentLow = nextLow; |
100 |
96 |
mergeStarted = true; |
101 |
96 |
merged = true; |
102 |
|
} |
103 |
|
} |
104 |
|
// If we haven't merged anything, add the previous merge and continue with the next |
105 |
71100 |
if (!merged) { |
106 |
71004 |
if (!mergeStarted) mergedExtracts.push_back(current); |
107 |
9 |
else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow)); |
108 |
71004 |
current = next; |
109 |
71004 |
mergeStarted = false; |
110 |
|
} |
111 |
|
} |
112 |
|
|
113 |
|
// Add the last child |
114 |
167611 |
if (!mergeStarted) mergedExtracts.push_back(current); |
115 |
63 |
else mergedExtracts.push_back(utils::mkExtract(current[0], currentHigh, currentLow)); |
116 |
|
|
117 |
|
// Return the result |
118 |
335222 |
return utils::mkConcat(mergedExtracts); |
119 |
|
} |
120 |
|
|
121 |
|
/* -------------------------------------------------------------------------- */ |
122 |
|
|
123 |
|
template<> inline |
124 |
335185 |
bool RewriteRule<ConcatConstantMerge>::applies(TNode node) { |
125 |
335185 |
return node.getKind() == kind::BITVECTOR_CONCAT; |
126 |
|
} |
127 |
|
|
128 |
|
template<> inline |
129 |
167574 |
Node RewriteRule<ConcatConstantMerge>::apply(TNode node) { |
130 |
|
|
131 |
167574 |
Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl; |
132 |
|
|
133 |
335148 |
std::vector<Node> mergedConstants; |
134 |
681633 |
for (unsigned i = 0, end = node.getNumChildren(); i < end;) { |
135 |
514059 |
if (node[i].getKind() != kind::CONST_BITVECTOR) { |
136 |
|
// If not a constant, just add it |
137 |
373782 |
mergedConstants.push_back(node[i]); |
138 |
373782 |
++i; |
139 |
|
} else { |
140 |
|
// Find the longest sequence of constants |
141 |
140277 |
unsigned j = i + 1; |
142 |
211219 |
while (j < end) { |
143 |
116648 |
if (node[j].getKind() != kind::CONST_BITVECTOR) { |
144 |
81177 |
break; |
145 |
|
} else { |
146 |
35471 |
++ j; |
147 |
|
} |
148 |
|
} |
149 |
|
// Append all the constants |
150 |
280554 |
BitVector current = node[i].getConst<BitVector>(); |
151 |
175748 |
for (unsigned k = i + 1; k < j; ++ k) { |
152 |
35471 |
current = current.concat(node[k].getConst<BitVector>()); |
153 |
|
} |
154 |
|
// Add the new merged constant |
155 |
140277 |
mergedConstants.push_back(utils::mkConst(current)); |
156 |
140277 |
i = j; |
157 |
|
} |
158 |
|
} |
159 |
|
|
160 |
167574 |
Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl; |
161 |
|
|
162 |
335148 |
return utils::mkConcat(mergedConstants); |
163 |
|
} |
164 |
|
|
165 |
|
/* -------------------------------------------------------------------------- */ |
166 |
|
|
167 |
|
template<> inline |
168 |
659040 |
bool RewriteRule<ExtractWhole>::applies(TNode node) { |
169 |
659040 |
if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; |
170 |
199522 |
unsigned length = utils::getSize(node[0]); |
171 |
199522 |
unsigned extractHigh = utils::getExtractHigh(node); |
172 |
199522 |
if (extractHigh != length - 1) return false; |
173 |
87366 |
unsigned extractLow = utils::getExtractLow(node); |
174 |
87366 |
if (extractLow != 0) return false; |
175 |
19757 |
return true; |
176 |
|
} |
177 |
|
|
178 |
|
template<> inline |
179 |
15116 |
Node RewriteRule<ExtractWhole>::apply(TNode node) { |
180 |
15116 |
Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl; |
181 |
15116 |
return node[0]; |
182 |
|
} |
183 |
|
|
184 |
|
/* -------------------------------------------------------------------------- */ |
185 |
|
|
186 |
|
template<> inline |
187 |
183475 |
bool RewriteRule<ExtractConstant>::applies(TNode node) { |
188 |
183475 |
if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; |
189 |
183475 |
if (node[0].getKind() != kind::CONST_BITVECTOR) return false; |
190 |
86344 |
return true; |
191 |
|
} |
192 |
|
|
193 |
|
template<> inline |
194 |
43172 |
Node RewriteRule<ExtractConstant>::apply(TNode node) { |
195 |
43172 |
Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl; |
196 |
86344 |
Node child = node[0]; |
197 |
86344 |
BitVector childValue = child.getConst<BitVector>(); |
198 |
86344 |
return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node))); |
199 |
|
} |
200 |
|
|
201 |
|
/* -------------------------------------------------------------------------- */ |
202 |
|
|
203 |
|
template<> inline |
204 |
162898 |
bool RewriteRule<ExtractConcat>::applies(TNode node) { |
205 |
|
//Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl; |
206 |
162898 |
if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; |
207 |
162898 |
if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false; |
208 |
20404 |
return true; |
209 |
|
} |
210 |
|
|
211 |
|
template<> inline |
212 |
10202 |
Node RewriteRule<ExtractConcat>::apply(TNode node) { |
213 |
10202 |
Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl; |
214 |
10202 |
int extract_high = utils::getExtractHigh(node); |
215 |
10202 |
int extract_low = utils::getExtractLow(node); |
216 |
|
|
217 |
20404 |
std::vector<Node> resultChildren; |
218 |
|
|
219 |
20404 |
Node concat = node[0]; |
220 |
33433 |
for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) { |
221 |
46462 |
Node concatChild = concat[i]; |
222 |
23231 |
int concatChildSize = utils::getSize(concatChild); |
223 |
23231 |
if (extract_low < concatChildSize) { |
224 |
19852 |
int extract_start = extract_low < 0 ? 0 : extract_low; |
225 |
19852 |
int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1; |
226 |
19852 |
resultChildren.push_back(utils::mkExtract(concatChild, extract_end, extract_start)); |
227 |
|
} |
228 |
23231 |
extract_low -= concatChildSize; |
229 |
23231 |
extract_high -= concatChildSize; |
230 |
|
} |
231 |
|
|
232 |
10202 |
std::reverse(resultChildren.begin(), resultChildren.end()); |
233 |
|
|
234 |
20404 |
return utils::mkConcat(resultChildren); |
235 |
|
} |
236 |
|
|
237 |
|
/* -------------------------------------------------------------------------- */ |
238 |
|
|
239 |
|
template<> inline |
240 |
142380 |
bool RewriteRule<ExtractExtract>::applies(TNode node) { |
241 |
142380 |
if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; |
242 |
99208 |
if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false; |
243 |
4154 |
return true; |
244 |
|
} |
245 |
|
|
246 |
|
template<> inline |
247 |
2077 |
Node RewriteRule<ExtractExtract>::apply(TNode node) { |
248 |
2077 |
Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl; |
249 |
|
|
250 |
|
// x[i:j][k:l] ~> x[k+j:l+j] |
251 |
4154 |
Node child = node[0]; |
252 |
2077 |
unsigned k = utils::getExtractHigh(node); |
253 |
2077 |
unsigned l = utils::getExtractLow(node); |
254 |
2077 |
unsigned j = utils::getExtractLow(child); |
255 |
|
|
256 |
2077 |
Node result = utils::mkExtract(child[0], k + j, l + j); |
257 |
4154 |
return result; |
258 |
|
} |
259 |
|
|
260 |
|
/* -------------------------------------------------------------------------- */ |
261 |
|
|
262 |
|
template<> inline |
263 |
464247 |
bool RewriteRule<FailEq>::applies(TNode node) { |
264 |
|
//Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl; |
265 |
464247 |
if (node.getKind() != kind::EQUAL) return false; |
266 |
464247 |
if (node[0].getKind() != kind::CONST_BITVECTOR) return false; |
267 |
103881 |
if (node[1].getKind() != kind::CONST_BITVECTOR) return false; |
268 |
85959 |
return node[0] != node[1]; |
269 |
|
} |
270 |
|
|
271 |
|
template<> inline |
272 |
41325 |
Node RewriteRule<FailEq>::apply(TNode node) { |
273 |
41325 |
return utils::mkFalse(); |
274 |
|
} |
275 |
|
|
276 |
|
/* -------------------------------------------------------------------------- */ |
277 |
|
|
278 |
|
template<> inline |
279 |
430987 |
bool RewriteRule<SimplifyEq>::applies(TNode node) { |
280 |
430987 |
if (node.getKind() != kind::EQUAL) return false; |
281 |
389662 |
return node[0] == node[1]; |
282 |
|
} |
283 |
|
|
284 |
|
template<> inline |
285 |
8065 |
Node RewriteRule<SimplifyEq>::apply(TNode node) { |
286 |
8065 |
Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl; |
287 |
8065 |
return utils::mkTrue(); |
288 |
|
} |
289 |
|
|
290 |
|
/* -------------------------------------------------------------------------- */ |
291 |
|
|
292 |
|
template<> inline |
293 |
463695 |
bool RewriteRule<ReflexivityEq>::applies(TNode node) { |
294 |
463695 |
return (node.getKind() == kind::EQUAL && node[0] < node[1]); |
295 |
|
} |
296 |
|
|
297 |
|
template<> inline |
298 |
40773 |
Node RewriteRule<ReflexivityEq>::apply(TNode node) { |
299 |
40773 |
Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl; |
300 |
40773 |
Node res = node[1].eqNode(node[0]); |
301 |
40773 |
return res; |
302 |
|
} |
303 |
|
|
304 |
|
} |
305 |
|
} |
306 |
|
} // namespace cvc5 |