GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewrite_rules.h Lines: 74 250 29.6 %
Date: 2021-03-22 Branches: 5021 21496 23.4 %

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