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