1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Dejan Jovanovic, Aina Niemetz |
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 <sstream> |
24 |
|
|
25 |
|
#include "context/context.h" |
26 |
|
#include "printer/printer.h" |
27 |
|
#include "smt/dump.h" |
28 |
|
#include "smt/smt_engine.h" |
29 |
|
#include "smt/smt_engine_scope.h" |
30 |
|
#include "theory/bv/theory_bv_utils.h" |
31 |
|
#include "theory/theory.h" |
32 |
|
#include "util/statistics_stats.h" |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace theory { |
36 |
|
namespace bv { |
37 |
|
|
38 |
|
enum RewriteRuleId |
39 |
|
{ |
40 |
|
|
41 |
|
/// core normalization rules |
42 |
|
EmptyRule, |
43 |
|
ConcatFlatten, |
44 |
|
ConcatExtractMerge, |
45 |
|
ConcatConstantMerge, |
46 |
|
ExtractExtract, |
47 |
|
ExtractWhole, |
48 |
|
ExtractConcat, |
49 |
|
ExtractConstant, |
50 |
|
FailEq, |
51 |
|
SimplifyEq, |
52 |
|
ReflexivityEq, |
53 |
|
|
54 |
|
/// operator elimination rules |
55 |
|
UgtEliminate, |
56 |
|
UgeEliminate, |
57 |
|
SgeEliminate, |
58 |
|
SgtEliminate, |
59 |
|
RedorEliminate, |
60 |
|
RedandEliminate, |
61 |
|
SubEliminate, |
62 |
|
SltEliminate, |
63 |
|
SleEliminate, |
64 |
|
UleEliminate, |
65 |
|
CompEliminate, |
66 |
|
RepeatEliminate, |
67 |
|
RotateLeftEliminate, |
68 |
|
RotateRightEliminate, |
69 |
|
NandEliminate, |
70 |
|
NorEliminate, |
71 |
|
XnorEliminate, |
72 |
|
SdivEliminate, |
73 |
|
SdivEliminateFewerBitwiseOps, |
74 |
|
UdivEliminate, |
75 |
|
SmodEliminate, |
76 |
|
SmodEliminateFewerBitwiseOps, |
77 |
|
SremEliminate, |
78 |
|
SremEliminateFewerBitwiseOps, |
79 |
|
ZeroExtendEliminate, |
80 |
|
SignExtendEliminate, |
81 |
|
BVToNatEliminate, |
82 |
|
IntToBVEliminate, |
83 |
|
|
84 |
|
/// ground term evaluation |
85 |
|
EvalEquals, |
86 |
|
EvalConcat, |
87 |
|
EvalAnd, |
88 |
|
EvalOr, |
89 |
|
EvalXor, |
90 |
|
EvalNot, |
91 |
|
EvalMult, |
92 |
|
EvalAdd, |
93 |
|
EvalUdiv, |
94 |
|
EvalUrem, |
95 |
|
EvalShl, |
96 |
|
EvalLshr, |
97 |
|
EvalAshr, |
98 |
|
EvalUlt, |
99 |
|
EvalUltBv, |
100 |
|
EvalUle, |
101 |
|
EvalExtract, |
102 |
|
EvalSignExtend, |
103 |
|
EvalRotateLeft, |
104 |
|
EvalRotateRight, |
105 |
|
EvalNeg, |
106 |
|
EvalSlt, |
107 |
|
EvalSltBv, |
108 |
|
EvalSle, |
109 |
|
EvalITEBv, |
110 |
|
EvalComp, |
111 |
|
EvalEagerAtom, |
112 |
|
|
113 |
|
/// simplification rules |
114 |
|
/// all of these rules decrease formula size |
115 |
|
BvIteConstCond, |
116 |
|
BvIteEqualChildren, |
117 |
|
BvIteConstChildren, |
118 |
|
BvIteEqualCond, |
119 |
|
BvIteMergeThenIf, |
120 |
|
BvIteMergeElseIf, |
121 |
|
BvIteMergeThenElse, |
122 |
|
BvIteMergeElseElse, |
123 |
|
BvComp, |
124 |
|
ShlByConst, |
125 |
|
LshrByConst, |
126 |
|
AshrByConst, |
127 |
|
BitwiseIdemp, |
128 |
|
AndZero, |
129 |
|
AndOne, |
130 |
|
AndOrXorConcatPullUp, |
131 |
|
NegEliminate, |
132 |
|
OrEliminate, |
133 |
|
XorEliminate, |
134 |
|
OrZero, |
135 |
|
OrOne, |
136 |
|
XorDuplicate, |
137 |
|
XorOne, |
138 |
|
XorZero, |
139 |
|
BitwiseNotAnd, |
140 |
|
BitwiseNotOr, |
141 |
|
XorNot, |
142 |
|
NotIdemp, |
143 |
|
LtSelf, |
144 |
|
LteSelf, |
145 |
|
UltZero, |
146 |
|
UltSelf, |
147 |
|
UleZero, |
148 |
|
UleSelf, |
149 |
|
ZeroUle, |
150 |
|
UleMax, |
151 |
|
NotUlt, |
152 |
|
NotUle, |
153 |
|
MultPow2, |
154 |
|
MultSlice, |
155 |
|
ExtractMultLeadingBit, |
156 |
|
NegIdemp, |
157 |
|
UdivPow2, |
158 |
|
UdivZero, |
159 |
|
UdivOne, |
160 |
|
UremPow2, |
161 |
|
UremOne, |
162 |
|
UremSelf, |
163 |
|
ShiftZero, |
164 |
|
UgtUrem, |
165 |
|
|
166 |
|
UltOne, |
167 |
|
SltZero, |
168 |
|
ZeroUlt, |
169 |
|
MergeSignExtend, |
170 |
|
SignExtendEqConst, |
171 |
|
ZeroExtendEqConst, |
172 |
|
SignExtendUltConst, |
173 |
|
ZeroExtendUltConst, |
174 |
|
|
175 |
|
/// normalization rules |
176 |
|
ExtractBitwise, |
177 |
|
ExtractNot, |
178 |
|
ExtractArith, |
179 |
|
ExtractArith2, |
180 |
|
ExtractSignExtend, |
181 |
|
DoubleNeg, |
182 |
|
NegMult, |
183 |
|
NegSub, |
184 |
|
NegAdd, |
185 |
|
NotConcat, |
186 |
|
NotAnd, // not sure why this would help (not done) |
187 |
|
NotOr, // not sure why this would help (not done) |
188 |
|
NotXor, // not sure why this would help (not done) |
189 |
|
FlattenAssocCommut, |
190 |
|
FlattenAssocCommutNoDuplicates, |
191 |
|
AddCombineLikeTerms, |
192 |
|
MultSimplify, |
193 |
|
MultDistribConst, |
194 |
|
MultDistrib, |
195 |
|
SolveEq, |
196 |
|
BitwiseEq, |
197 |
|
AndSimplify, |
198 |
|
OrSimplify, |
199 |
|
XorSimplify, |
200 |
|
BitwiseSlicing, |
201 |
|
NormalizeEqAddNeg, |
202 |
|
// rules to simplify bitblasting |
203 |
|
BBAddNeg, |
204 |
|
UltAddOne, |
205 |
|
ConcatToMult, |
206 |
|
IsPowerOfTwo, |
207 |
|
MultSltMult, |
208 |
|
BitOfConst, |
209 |
|
}; |
210 |
|
|
211 |
|
inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { |
212 |
|
switch (ruleId) { |
213 |
|
case EmptyRule: out << "EmptyRule"; return out; |
214 |
|
case ConcatFlatten: out << "ConcatFlatten"; return out; |
215 |
|
case ConcatExtractMerge: out << "ConcatExtractMerge"; return out; |
216 |
|
case ConcatConstantMerge: out << "ConcatConstantMerge"; return out; |
217 |
|
case AndOrXorConcatPullUp:out << "AndOrXorConcatPullUp";return out; |
218 |
|
case NegEliminate: out << "NegEliminate"; return out; |
219 |
|
case OrEliminate: out << "OrEliminate"; return out; |
220 |
|
case XorEliminate: out << "XorEliminate"; return out; |
221 |
|
case ExtractExtract: out << "ExtractExtract"; return out; |
222 |
|
case ExtractWhole: out << "ExtractWhole"; return out; |
223 |
|
case ExtractConcat: out << "ExtractConcat"; return out; |
224 |
|
case ExtractConstant: out << "ExtractConstant"; return out; |
225 |
|
case FailEq: out << "FailEq"; return out; |
226 |
|
case SimplifyEq: out << "SimplifyEq"; return out; |
227 |
|
case ReflexivityEq: out << "ReflexivityEq"; return out; |
228 |
|
case UgtEliminate: out << "UgtEliminate"; return out; |
229 |
|
case SgtEliminate: out << "SgtEliminate"; return out; |
230 |
|
case UgeEliminate: out << "UgeEliminate"; return out; |
231 |
|
case SgeEliminate: out << "SgeEliminate"; return out; |
232 |
|
case RedorEliminate: out << "RedorEliminate"; return out; |
233 |
|
case RedandEliminate: out << "RedandEliminate"; return out; |
234 |
|
case RepeatEliminate: out << "RepeatEliminate"; return out; |
235 |
|
case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; |
236 |
|
case RotateRightEliminate:out << "RotateRightEliminate";return out; |
237 |
|
case BVToNatEliminate: out << "BVToNatEliminate"; return out; |
238 |
|
case IntToBVEliminate: out << "IntToBVEliminate"; return out; |
239 |
|
case NandEliminate: out << "NandEliminate"; return out; |
240 |
|
case NorEliminate : out << "NorEliminate"; return out; |
241 |
|
case SdivEliminate : out << "SdivEliminate"; return out; |
242 |
|
case SdivEliminateFewerBitwiseOps: |
243 |
|
out << "SdivEliminateFewerBitwiseOps"; |
244 |
|
return out; |
245 |
|
case SremEliminate : out << "SremEliminate"; return out; |
246 |
|
case SremEliminateFewerBitwiseOps: |
247 |
|
out << "SremEliminateFewerBitwiseOps"; |
248 |
|
return out; |
249 |
|
case SmodEliminate : out << "SmodEliminate"; return out; |
250 |
|
case SmodEliminateFewerBitwiseOps: |
251 |
|
out << "SmodEliminateFewerBitwiseOps"; |
252 |
|
return out; |
253 |
|
case ZeroExtendEliminate :out << "ZeroExtendEliminate"; return out; |
254 |
|
case EvalEquals : out << "EvalEquals"; return out; |
255 |
|
case EvalConcat : out << "EvalConcat"; return out; |
256 |
|
case EvalAnd : out << "EvalAnd"; return out; |
257 |
|
case EvalOr : out << "EvalOr"; return out; |
258 |
|
case EvalXor : out << "EvalXor"; return out; |
259 |
|
case EvalNot : out << "EvalNot"; return out; |
260 |
|
case EvalMult : out << "EvalMult"; return out; |
261 |
|
case EvalAdd: out << "EvalAdd"; return out; |
262 |
|
case EvalUdiv : out << "EvalUdiv"; return out; |
263 |
|
case EvalUrem : out << "EvalUrem"; return out; |
264 |
|
case EvalShl : out << "EvalShl"; return out; |
265 |
|
case EvalLshr : out << "EvalLshr"; return out; |
266 |
|
case EvalAshr : out << "EvalAshr"; return out; |
267 |
|
case EvalUlt : out << "EvalUlt"; return out; |
268 |
|
case EvalUle : out << "EvalUle"; return out; |
269 |
|
case EvalSlt : out << "EvalSlt"; return out; |
270 |
|
case EvalSle : out << "EvalSle"; return out; |
271 |
|
case EvalSltBv: out << "EvalSltBv"; return out; |
272 |
|
case EvalITEBv: out << "EvalITEBv"; return out; |
273 |
|
case EvalComp: out << "EvalComp"; return out; |
274 |
|
case EvalEagerAtom: out << "EvalEagerAtom"; return out; |
275 |
|
case EvalExtract : out << "EvalExtract"; return out; |
276 |
|
case EvalSignExtend : out << "EvalSignExtend"; return out; |
277 |
|
case EvalRotateLeft : out << "EvalRotateLeft"; return out; |
278 |
|
case EvalRotateRight : out << "EvalRotateRight"; return out; |
279 |
|
case EvalNeg : out << "EvalNeg"; return out; |
280 |
|
case BvIteConstCond : out << "BvIteConstCond"; return out; |
281 |
|
case BvIteEqualChildren : out << "BvIteEqualChildren"; return out; |
282 |
|
case BvIteConstChildren : out << "BvIteConstChildren"; return out; |
283 |
|
case BvIteEqualCond : out << "BvIteEqualCond"; return out; |
284 |
|
case BvIteMergeThenIf : out << "BvIteMergeThenIf"; return out; |
285 |
|
case BvIteMergeElseIf : out << "BvIteMergeElseIf"; return out; |
286 |
|
case BvIteMergeThenElse : out << "BvIteMergeThenElse"; return out; |
287 |
|
case BvIteMergeElseElse : out << "BvIteMergeElseElse"; return out; |
288 |
|
case BvComp : out << "BvComp"; return out; |
289 |
|
case ShlByConst : out << "ShlByConst"; return out; |
290 |
|
case LshrByConst : out << "LshrByConst"; return out; |
291 |
|
case AshrByConst : out << "AshrByConst"; return out; |
292 |
|
case ExtractBitwise : out << "ExtractBitwise"; return out; |
293 |
|
case ExtractNot : out << "ExtractNot"; return out; |
294 |
|
case ExtractArith : out << "ExtractArith"; return out; |
295 |
|
case ExtractArith2 : out << "ExtractArith2"; return out; |
296 |
|
case DoubleNeg : out << "DoubleNeg"; return out; |
297 |
|
case NotConcat : out << "NotConcat"; return out; |
298 |
|
case NotAnd : out << "NotAnd"; return out; |
299 |
|
case NotOr : out << "NotOr"; return out; |
300 |
|
case NotXor : out << "NotXor"; return out; |
301 |
|
case BitwiseIdemp : out << "BitwiseIdemp"; return out; |
302 |
|
case XorDuplicate : out << "XorDuplicate"; return out; |
303 |
|
case BitwiseNotAnd : out << "BitwiseNotAnd"; return out; |
304 |
|
case BitwiseNotOr : out << "BitwiseNotOr"; return out; |
305 |
|
case XorNot : out << "XorNot"; return out; |
306 |
|
case LtSelf : out << "LtSelf"; return out; |
307 |
|
case LteSelf : out << "LteSelf"; return out; |
308 |
|
case UltZero : out << "UltZero"; return out; |
309 |
|
case UleZero : out << "UleZero"; return out; |
310 |
|
case ZeroUle : out << "ZeroUle"; return out; |
311 |
|
case NotUlt : out << "NotUlt"; return out; |
312 |
|
case NotUle : out << "NotUle"; return out; |
313 |
|
case UleMax : out << "UleMax"; return out; |
314 |
|
case SltEliminate : out << "SltEliminate"; return out; |
315 |
|
case SleEliminate : out << "SleEliminate"; return out; |
316 |
|
case AndZero : out << "AndZero"; return out; |
317 |
|
case AndOne : out << "AndOne"; return out; |
318 |
|
case OrZero : out << "OrZero"; return out; |
319 |
|
case OrOne : out << "OrOne"; return out; |
320 |
|
case XorOne : out << "XorOne"; return out; |
321 |
|
case XorZero : out << "XorZero"; return out; |
322 |
|
case MultPow2 : out << "MultPow2"; return out; |
323 |
|
case MultSlice : out << "MultSlice"; return out; |
324 |
|
case ExtractMultLeadingBit : out << "ExtractMultLeadingBit"; return out; |
325 |
|
case NegIdemp : out << "NegIdemp"; return out; |
326 |
|
case UdivPow2 : out << "UdivPow2"; return out; |
327 |
|
case UdivZero: |
328 |
|
out << "UdivZero"; |
329 |
|
return out; |
330 |
|
case UdivOne : out << "UdivOne"; return out; |
331 |
|
case UremPow2 : out << "UremPow2"; return out; |
332 |
|
case UremOne : out << "UremOne"; return out; |
333 |
|
case UremSelf : out << "UremSelf"; return out; |
334 |
|
case ShiftZero : out << "ShiftZero"; return out; |
335 |
|
case UgtUrem: out << "UgtUrem"; return out; |
336 |
|
case SubEliminate : out << "SubEliminate"; return out; |
337 |
|
case CompEliminate : out << "CompEliminate"; return out; |
338 |
|
case XnorEliminate : out << "XnorEliminate"; return out; |
339 |
|
case SignExtendEliminate : out << "SignExtendEliminate"; return out; |
340 |
|
case NotIdemp : out << "NotIdemp"; return out; |
341 |
|
case UleSelf: out << "UleSelf"; return out; |
342 |
|
case FlattenAssocCommut: out << "FlattenAssocCommut"; return out; |
343 |
|
case FlattenAssocCommutNoDuplicates: |
344 |
|
out << "FlattenAssocCommutNoDuplicates"; |
345 |
|
return out; |
346 |
|
case AddCombineLikeTerms: out << "AddCombineLikeTerms"; return out; |
347 |
|
case MultSimplify: out << "MultSimplify"; return out; |
348 |
|
case MultDistribConst: out << "MultDistribConst"; return out; |
349 |
|
case SolveEq : out << "SolveEq"; return out; |
350 |
|
case BitwiseEq : out << "BitwiseEq"; return out; |
351 |
|
case NegMult : out << "NegMult"; return out; |
352 |
|
case NegSub : out << "NegSub"; return out; |
353 |
|
case AndSimplify : out << "AndSimplify"; return out; |
354 |
|
case OrSimplify : out << "OrSimplify"; return out; |
355 |
|
case XorSimplify : out << "XorSimplify"; return out; |
356 |
|
case NegAdd: out << "NegAdd"; return out; |
357 |
|
case BBAddNeg: out << "BBAddNeg"; return out; |
358 |
|
case UltOne : out << "UltOne"; return out; |
359 |
|
case SltZero : out << "SltZero"; return out; |
360 |
|
case ZeroUlt : out << "ZeroUlt"; return out; |
361 |
|
case MergeSignExtend : out << "MergeSignExtend"; return out; |
362 |
|
case SignExtendEqConst: out << "SignExtendEqConst"; return out; |
363 |
|
case ZeroExtendEqConst: out << "ZeroExtendEqConst"; return out; |
364 |
|
case SignExtendUltConst: out << "SignExtendUltConst"; return out; |
365 |
|
case ZeroExtendUltConst: out << "ZeroExtendUltConst"; return out; |
366 |
|
|
367 |
|
case UleEliminate : out << "UleEliminate"; return out; |
368 |
|
case BitwiseSlicing : out << "BitwiseSlicing"; return out; |
369 |
|
case ExtractSignExtend : out << "ExtractSignExtend"; return out; |
370 |
|
case MultDistrib: out << "MultDistrib"; return out; |
371 |
|
case UltAddOne: out << "UltAddOne"; return out; |
372 |
|
case ConcatToMult: out << "ConcatToMult"; return out; |
373 |
|
case IsPowerOfTwo: out << "IsPowerOfTwo"; return out; |
374 |
|
case MultSltMult: out << "MultSltMult"; return out; |
375 |
|
case NormalizeEqAddNeg: out << "NormalizeEqAddNeg"; return out; |
376 |
|
case BitOfConst: out << "BitOfConst"; return out; |
377 |
|
default: |
378 |
|
Unreachable(); |
379 |
|
} |
380 |
|
}; |
381 |
|
|
382 |
|
template <RewriteRuleId rule> |
383 |
|
class RewriteRule { |
384 |
|
|
385 |
|
// class RuleStatistics { |
386 |
|
|
387 |
|
// /** The name of the rule prefixed with the prefix */ |
388 |
|
// static std::string getStatName(const char* prefix) { |
389 |
|
// std::stringstream statName; |
390 |
|
// statName << prefix << rule; |
391 |
|
// return statName.str(); |
392 |
|
// } |
393 |
|
|
394 |
|
// public: |
395 |
|
|
396 |
|
// /** Number of applications of this rule */ |
397 |
|
// IntStat d_ruleApplications; |
398 |
|
|
399 |
|
// /** Constructor */ |
400 |
|
// RuleStatistics() |
401 |
|
// : d_ruleApplications(getStatName("theory::bv::RewriteRules::count"), 0) { |
402 |
|
// currentStatisticsRegistry()->registerStat(&d_ruleApplications); |
403 |
|
// } |
404 |
|
|
405 |
|
// /** Destructor */ |
406 |
|
// ~RuleStatistics() { |
407 |
|
// StatisticsRegistry::unregisterStat(&d_ruleApplications); |
408 |
|
// } |
409 |
|
// }; |
410 |
|
|
411 |
|
// /* Statistics about the rule */ |
412 |
|
// // NOTE: Cannot have static fields like this, or else you can't have |
413 |
|
// // two SmtEngines in the process (the second-to-be-destroyed will |
414 |
|
// // have a dangling pointer and segfault). If this statistic is needed, |
415 |
|
// // fix the rewriter by making it an instance per-SmtEngine (instead of |
416 |
|
// // static). |
417 |
|
// static RuleStatistics* s_statistics; |
418 |
|
|
419 |
|
/** Actually apply the rewrite rule */ |
420 |
|
static inline Node apply(TNode node) { |
421 |
|
Unreachable(); |
422 |
|
SuppressWrongNoReturnWarning; |
423 |
|
} |
424 |
|
|
425 |
|
public: |
426 |
|
|
427 |
|
RewriteRule() { |
428 |
|
|
429 |
|
// if (s_statistics == NULL) { |
430 |
|
// s_statistics = new RuleStatistics(); |
431 |
|
// } |
432 |
|
|
433 |
|
} |
434 |
|
|
435 |
|
~RewriteRule() { |
436 |
|
|
437 |
|
// delete s_statistics; |
438 |
|
// s_statistics = NULL; |
439 |
|
|
440 |
|
} |
441 |
|
|
442 |
|
static inline bool applies(TNode node) |
443 |
|
{ |
444 |
|
Unreachable(); |
445 |
|
SuppressWrongNoReturnWarning; |
446 |
|
} |
447 |
|
|
448 |
|
template<bool checkApplies> |
449 |
2273022 |
static inline Node run(TNode node) { |
450 |
492048 |
if (!checkApplies || applies(node)) { |
451 |
1789349 |
Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl; |
452 |
1789349 |
Assert(checkApplies || applies(node)); |
453 |
|
//++ s_statistics->d_ruleApplications; |
454 |
3578698 |
Node result = apply(node); |
455 |
1789349 |
if (result != node) { |
456 |
767705 |
if(Dump.isOn("bv-rewrites")) { |
457 |
|
std::ostringstream os; |
458 |
|
os << "RewriteRule <"<<rule<<">; expect unsat"; |
459 |
|
|
460 |
|
Node condition = node.eqNode(result).notNode(); |
461 |
|
|
462 |
|
const Printer& printer = |
463 |
|
smt::currentSmtEngine()->getOutputManager().getPrinter(); |
464 |
|
std::ostream& out = |
465 |
|
smt::currentSmtEngine()->getOutputManager().getDumpOut(); |
466 |
|
|
467 |
|
printer.toStreamCmdComment(out, os.str()); |
468 |
|
printer.toStreamCmdCheckSat(out, condition); |
469 |
|
} |
470 |
|
} |
471 |
1789349 |
Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl; |
472 |
1789349 |
return result; |
473 |
|
} else { |
474 |
483673 |
return node; |
475 |
|
} |
476 |
|
} |
477 |
|
}; |
478 |
|
|
479 |
|
|
480 |
|
// template<RewriteRuleId rule> |
481 |
|
// typename RewriteRule<rule>::RuleStatistics* RewriteRule<rule>::s_statistics = NULL; |
482 |
|
|
483 |
|
|
484 |
|
/** Have to list all the rewrite rules to get the statistics out */ |
485 |
|
struct AllRewriteRules { |
486 |
|
RewriteRule<EmptyRule> rule00; |
487 |
|
RewriteRule<ConcatFlatten> rule01; |
488 |
|
RewriteRule<ConcatExtractMerge> rule02; |
489 |
|
RewriteRule<ConcatConstantMerge> rule03; |
490 |
|
RewriteRule<ExtractExtract> rule04; |
491 |
|
RewriteRule<ExtractWhole> rule05; |
492 |
|
RewriteRule<ExtractConcat> rule06; |
493 |
|
RewriteRule<ExtractConstant> rule07; |
494 |
|
RewriteRule<FailEq> rule08; |
495 |
|
RewriteRule<SimplifyEq> rule09; |
496 |
|
RewriteRule<ReflexivityEq> rule10; |
497 |
|
RewriteRule<UgtEliminate> rule11; |
498 |
|
RewriteRule<SgtEliminate> rule12; |
499 |
|
RewriteRule<UgeEliminate> rule13; |
500 |
|
RewriteRule<SgeEliminate> rule14; |
501 |
|
RewriteRule<NegMult> rule15; |
502 |
|
RewriteRule<NegSub> rule16; |
503 |
|
RewriteRule<RepeatEliminate> rule17; |
504 |
|
RewriteRule<RotateLeftEliminate> rule18; |
505 |
|
RewriteRule<RotateRightEliminate> rule19; |
506 |
|
RewriteRule<NandEliminate> rule20; |
507 |
|
RewriteRule<NorEliminate> rule21; |
508 |
|
RewriteRule<SdivEliminate> rule22; |
509 |
|
RewriteRule<SremEliminate> rule23; |
510 |
|
RewriteRule<SmodEliminate> rule24; |
511 |
|
RewriteRule<EvalConcat> rule25; |
512 |
|
RewriteRule<EvalAnd> rule26; |
513 |
|
RewriteRule<EvalOr> rule27; |
514 |
|
RewriteRule<EvalXor> rule28; |
515 |
|
RewriteRule<EvalNot> rule29; |
516 |
|
RewriteRule<EvalSlt> rule30; |
517 |
|
RewriteRule<EvalMult> rule31; |
518 |
|
RewriteRule<EvalAdd> rule32; |
519 |
|
RewriteRule<XorSimplify> rule33; |
520 |
|
RewriteRule<EvalUdiv> rule34; |
521 |
|
RewriteRule<EvalUrem> rule35; |
522 |
|
RewriteRule<EvalShl> rule36; |
523 |
|
RewriteRule<EvalLshr> rule37; |
524 |
|
RewriteRule<EvalAshr> rule38; |
525 |
|
RewriteRule<EvalUlt> rule39; |
526 |
|
RewriteRule<EvalUle> rule40; |
527 |
|
RewriteRule<EvalSle> rule41; |
528 |
|
RewriteRule<EvalExtract> rule43; |
529 |
|
RewriteRule<EvalSignExtend> rule44; |
530 |
|
RewriteRule<EvalRotateLeft> rule45; |
531 |
|
RewriteRule<EvalRotateRight> rule46; |
532 |
|
RewriteRule<EvalEquals> rule47; |
533 |
|
RewriteRule<EvalNeg> rule48; |
534 |
|
RewriteRule<ShlByConst> rule50; |
535 |
|
RewriteRule<LshrByConst> rule51; |
536 |
|
RewriteRule<AshrByConst> rule52; |
537 |
|
RewriteRule<ExtractBitwise> rule53; |
538 |
|
RewriteRule<ExtractNot> rule54; |
539 |
|
RewriteRule<ExtractArith> rule55; |
540 |
|
RewriteRule<DoubleNeg> rule56; |
541 |
|
RewriteRule<NotConcat> rule57; |
542 |
|
RewriteRule<NotAnd> rule58; |
543 |
|
RewriteRule<NotOr> rule59; |
544 |
|
RewriteRule<NotXor> rule60; |
545 |
|
RewriteRule<BitwiseIdemp> rule61; |
546 |
|
RewriteRule<XorDuplicate> rule62; |
547 |
|
RewriteRule<BitwiseNotAnd> rule63; |
548 |
|
RewriteRule<BitwiseNotOr> rule64; |
549 |
|
RewriteRule<XorNot> rule65; |
550 |
|
RewriteRule<LtSelf> rule66; |
551 |
|
RewriteRule<LtSelf> rule67; |
552 |
|
RewriteRule<UltZero> rule68; |
553 |
|
RewriteRule<UleZero> rule69; |
554 |
|
RewriteRule<ZeroUle> rule70; |
555 |
|
RewriteRule<NotUlt> rule71; |
556 |
|
RewriteRule<NotUle> rule72; |
557 |
|
RewriteRule<ZeroExtendEliminate> rule73; |
558 |
|
RewriteRule<UleMax> rule74; |
559 |
|
RewriteRule<LteSelf> rule75; |
560 |
|
RewriteRule<SltEliminate> rule76; |
561 |
|
RewriteRule<SleEliminate> rule77; |
562 |
|
RewriteRule<AndZero> rule78; |
563 |
|
RewriteRule<AndOne> rule79; |
564 |
|
RewriteRule<OrZero> rule80; |
565 |
|
RewriteRule<OrOne> rule81; |
566 |
|
RewriteRule<SubEliminate> rule82; |
567 |
|
RewriteRule<XorOne> rule83; |
568 |
|
RewriteRule<XorZero> rule84; |
569 |
|
RewriteRule<MultSlice> rule85; |
570 |
|
RewriteRule<FlattenAssocCommutNoDuplicates> rule86; |
571 |
|
RewriteRule<MultPow2> rule87; |
572 |
|
RewriteRule<ExtractMultLeadingBit> rule88; |
573 |
|
RewriteRule<NegIdemp> rule91; |
574 |
|
RewriteRule<UdivPow2> rule92; |
575 |
|
RewriteRule<UdivZero> rule93; |
576 |
|
RewriteRule<UdivOne> rule94; |
577 |
|
RewriteRule<UremPow2> rule95; |
578 |
|
RewriteRule<UremOne> rule96; |
579 |
|
RewriteRule<UremSelf> rule97; |
580 |
|
RewriteRule<ShiftZero> rule98; |
581 |
|
RewriteRule<CompEliminate> rule99; |
582 |
|
RewriteRule<XnorEliminate> rule100; |
583 |
|
RewriteRule<SignExtendEliminate> rule101; |
584 |
|
RewriteRule<NotIdemp> rule102; |
585 |
|
RewriteRule<UleSelf> rule103; |
586 |
|
RewriteRule<FlattenAssocCommut> rule104; |
587 |
|
RewriteRule<AddCombineLikeTerms> rule105; |
588 |
|
RewriteRule<MultSimplify> rule106; |
589 |
|
RewriteRule<MultDistribConst> rule107; |
590 |
|
RewriteRule<AndSimplify> rule108; |
591 |
|
RewriteRule<OrSimplify> rule109; |
592 |
|
RewriteRule<NegAdd> rule110; |
593 |
|
RewriteRule<BBAddNeg> rule111; |
594 |
|
RewriteRule<SolveEq> rule112; |
595 |
|
RewriteRule<BitwiseEq> rule113; |
596 |
|
RewriteRule<UltOne> rule114; |
597 |
|
RewriteRule<SltZero> rule115; |
598 |
|
RewriteRule<BVToNatEliminate> rule116; |
599 |
|
RewriteRule<IntToBVEliminate> rule117; |
600 |
|
RewriteRule<MultDistrib> rule118; |
601 |
|
RewriteRule<UltAddOne> rule119; |
602 |
|
RewriteRule<ConcatToMult> rule120; |
603 |
|
RewriteRule<IsPowerOfTwo> rule121; |
604 |
|
RewriteRule<RedorEliminate> rule122; |
605 |
|
RewriteRule<RedandEliminate> rule123; |
606 |
|
RewriteRule<SignExtendEqConst> rule124; |
607 |
|
RewriteRule<ZeroExtendEqConst> rule125; |
608 |
|
RewriteRule<SignExtendUltConst> rule126; |
609 |
|
RewriteRule<ZeroExtendUltConst> rule127; |
610 |
|
RewriteRule<MultSltMult> rule128; |
611 |
|
RewriteRule<NormalizeEqAddNeg> rule129; |
612 |
|
RewriteRule<BvComp> rule130; |
613 |
|
RewriteRule<BvIteConstCond> rule131; |
614 |
|
RewriteRule<BvIteEqualChildren> rule132; |
615 |
|
RewriteRule<BvIteConstChildren> rule133; |
616 |
|
RewriteRule<BvIteEqualCond> rule134; |
617 |
|
RewriteRule<BvIteMergeThenIf> rule135; |
618 |
|
RewriteRule<BvIteMergeElseIf> rule136; |
619 |
|
RewriteRule<BvIteMergeThenElse> rule137; |
620 |
|
RewriteRule<BvIteMergeElseElse> rule138; |
621 |
|
RewriteRule<AndOrXorConcatPullUp> rule139; |
622 |
|
RewriteRule<NegEliminate> rule140; |
623 |
|
RewriteRule<OrEliminate> rule141; |
624 |
|
RewriteRule<XorEliminate> rule142; |
625 |
|
RewriteRule<SdivEliminate> rule143; |
626 |
|
RewriteRule<SremEliminate> rule144; |
627 |
|
RewriteRule<SmodEliminate> rule145; |
628 |
|
RewriteRule<UgtUrem> rule146; |
629 |
|
}; |
630 |
|
|
631 |
|
template<> inline |
632 |
54861665 |
bool RewriteRule<EmptyRule>::applies(TNode node) { |
633 |
54861665 |
return false; |
634 |
|
} |
635 |
|
|
636 |
|
template<> inline |
637 |
|
Node RewriteRule<EmptyRule>::apply(TNode node) { |
638 |
|
Debug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n"; |
639 |
|
Unreachable(); |
640 |
|
return node; |
641 |
|
} |
642 |
|
|
643 |
|
template<Kind kind, RewriteRuleId rule> |
644 |
|
struct ApplyRuleToChildren { |
645 |
|
|
646 |
157954 |
static Node apply(TNode node) { |
647 |
157954 |
if (node.getKind() != kind) { |
648 |
13 |
return RewriteRule<rule>::template run<true>(node); |
649 |
|
} |
650 |
315882 |
NodeBuilder result(kind); |
651 |
649788 |
for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) { |
652 |
491847 |
result << RewriteRule<rule>::template run<true>(node[i]); |
653 |
|
} |
654 |
157941 |
return result; |
655 |
|
} |
656 |
|
|
657 |
185864 |
static bool applies(TNode node) { |
658 |
185864 |
if (node.getKind() == kind) return true; |
659 |
27923 |
return RewriteRule<rule>::applies(node); |
660 |
|
} |
661 |
|
|
662 |
|
template <bool checkApplies> |
663 |
157954 |
static Node run(TNode node) { |
664 |
|
if (!checkApplies || applies(node)) { |
665 |
157954 |
return apply(node); |
666 |
|
} else { |
667 |
|
return node; |
668 |
|
} |
669 |
|
} |
670 |
|
}; |
671 |
|
|
672 |
|
template < |
673 |
|
typename R1, |
674 |
|
typename R2 = RewriteRule<EmptyRule>, |
675 |
|
typename R3 = RewriteRule<EmptyRule>, |
676 |
|
typename R4 = RewriteRule<EmptyRule>, |
677 |
|
typename R5 = RewriteRule<EmptyRule>, |
678 |
|
typename R6 = RewriteRule<EmptyRule>, |
679 |
|
typename R7 = RewriteRule<EmptyRule>, |
680 |
|
typename R8 = RewriteRule<EmptyRule>, |
681 |
|
typename R9 = RewriteRule<EmptyRule>, |
682 |
|
typename R10 = RewriteRule<EmptyRule>, |
683 |
|
typename R11 = RewriteRule<EmptyRule>, |
684 |
|
typename R12 = RewriteRule<EmptyRule>, |
685 |
|
typename R13 = RewriteRule<EmptyRule>, |
686 |
|
typename R14 = RewriteRule<EmptyRule>, |
687 |
|
typename R15 = RewriteRule<EmptyRule>, |
688 |
|
typename R16 = RewriteRule<EmptyRule>, |
689 |
|
typename R17 = RewriteRule<EmptyRule>, |
690 |
|
typename R18 = RewriteRule<EmptyRule>, |
691 |
|
typename R19 = RewriteRule<EmptyRule>, |
692 |
|
typename R20 = RewriteRule<EmptyRule> |
693 |
|
> |
694 |
|
struct LinearRewriteStrategy { |
695 |
3113884 |
static Node apply(TNode node) { |
696 |
3113884 |
Node current = node; |
697 |
3113884 |
if (R1::applies(current)) current = R1::template run<false>(current); |
698 |
3113884 |
if (R2::applies(current)) current = R2::template run<false>(current); |
699 |
3113884 |
if (R3::applies(current)) current = R3::template run<false>(current); |
700 |
3113884 |
if (R4::applies(current)) current = R4::template run<false>(current); |
701 |
3113884 |
if (R5::applies(current)) current = R5::template run<false>(current); |
702 |
3113884 |
if (R6::applies(current)) current = R6::template run<false>(current); |
703 |
3113884 |
if (R7::applies(current)) current = R7::template run<false>(current); |
704 |
3113884 |
if (R8::applies(current)) current = R8::template run<false>(current); |
705 |
3113884 |
if (R9::applies(current)) current = R9::template run<false>(current); |
706 |
3113884 |
if (R10::applies(current)) current = R10::template run<false>(current); |
707 |
3113884 |
if (R11::applies(current)) current = R11::template run<false>(current); |
708 |
3113884 |
if (R12::applies(current)) current = R12::template run<false>(current); |
709 |
3113884 |
if (R13::applies(current)) current = R13::template run<false>(current); |
710 |
3113884 |
if (R14::applies(current)) current = R14::template run<false>(current); |
711 |
3113884 |
if (R15::applies(current)) current = R15::template run<false>(current); |
712 |
3113884 |
if (R16::applies(current)) current = R16::template run<false>(current); |
713 |
3113884 |
if (R17::applies(current)) current = R17::template run<false>(current); |
714 |
3113884 |
if (R18::applies(current)) current = R18::template run<false>(current); |
715 |
3113884 |
if (R19::applies(current)) current = R19::template run<false>(current); |
716 |
3113884 |
if (R20::applies(current)) current = R20::template run<false>(current); |
717 |
3113884 |
return current; |
718 |
|
} |
719 |
|
}; |
720 |
|
|
721 |
|
template < |
722 |
|
typename R1, |
723 |
|
typename R2 = RewriteRule<EmptyRule>, |
724 |
|
typename R3 = RewriteRule<EmptyRule>, |
725 |
|
typename R4 = RewriteRule<EmptyRule>, |
726 |
|
typename R5 = RewriteRule<EmptyRule>, |
727 |
|
typename R6 = RewriteRule<EmptyRule>, |
728 |
|
typename R7 = RewriteRule<EmptyRule>, |
729 |
|
typename R8 = RewriteRule<EmptyRule>, |
730 |
|
typename R9 = RewriteRule<EmptyRule>, |
731 |
|
typename R10 = RewriteRule<EmptyRule>, |
732 |
|
typename R11 = RewriteRule<EmptyRule>, |
733 |
|
typename R12 = RewriteRule<EmptyRule>, |
734 |
|
typename R13 = RewriteRule<EmptyRule>, |
735 |
|
typename R14 = RewriteRule<EmptyRule>, |
736 |
|
typename R15 = RewriteRule<EmptyRule>, |
737 |
|
typename R16 = RewriteRule<EmptyRule>, |
738 |
|
typename R17 = RewriteRule<EmptyRule>, |
739 |
|
typename R18 = RewriteRule<EmptyRule>, |
740 |
|
typename R19 = RewriteRule<EmptyRule>, |
741 |
|
typename R20 = RewriteRule<EmptyRule> |
742 |
|
> |
743 |
|
struct FixpointRewriteStrategy { |
744 |
1962 |
static Node apply(TNode node) { |
745 |
3924 |
Node previous = node; |
746 |
1962 |
Node current = node; |
747 |
81 |
do { |
748 |
2043 |
previous = current; |
749 |
2043 |
if (R1::applies(current)) current = R1::template run<false>(current); |
750 |
2043 |
if (R2::applies(current)) current = R2::template run<false>(current); |
751 |
2043 |
if (R3::applies(current)) current = R3::template run<false>(current); |
752 |
2043 |
if (R4::applies(current)) current = R4::template run<false>(current); |
753 |
2043 |
if (R5::applies(current)) current = R5::template run<false>(current); |
754 |
2043 |
if (R6::applies(current)) current = R6::template run<false>(current); |
755 |
2043 |
if (R7::applies(current)) current = R7::template run<false>(current); |
756 |
2043 |
if (R8::applies(current)) current = R8::template run<false>(current); |
757 |
2043 |
if (R9::applies(current)) current = R9::template run<false>(current); |
758 |
2043 |
if (R10::applies(current)) current = R10::template run<false>(current); |
759 |
2043 |
if (R11::applies(current)) current = R11::template run<false>(current); |
760 |
2043 |
if (R12::applies(current)) current = R12::template run<false>(current); |
761 |
2043 |
if (R13::applies(current)) current = R13::template run<false>(current); |
762 |
2043 |
if (R14::applies(current)) current = R14::template run<false>(current); |
763 |
2043 |
if (R15::applies(current)) current = R15::template run<false>(current); |
764 |
2043 |
if (R16::applies(current)) current = R16::template run<false>(current); |
765 |
2043 |
if (R17::applies(current)) current = R17::template run<false>(current); |
766 |
2043 |
if (R18::applies(current)) current = R18::template run<false>(current); |
767 |
2043 |
if (R19::applies(current)) current = R19::template run<false>(current); |
768 |
2043 |
if (R20::applies(current)) current = R20::template run<false>(current); |
769 |
2043 |
} while (previous != current); |
770 |
|
|
771 |
3924 |
return current; |
772 |
|
} |
773 |
|
}; |
774 |
|
|
775 |
|
|
776 |
|
} // End namespace bv |
777 |
|
} // End namespace theory |
778 |
|
} // End namespace cvc5 |