src/theory/bv/theory_bv_rewrite_rules.h

   1 #pragma once
   2
   3 #include "cvc4_private.h"
   4 #include "theory/theory.h"
   5 #include "context/context.h"
   6
   7 namespace CVC4 {
   8 namespace theory {
   9 namespace bv {
  10
  11 struct CoreRewriteRules {
  12
  13   struct EmptyRule {
  14     static inline Node apply(Node node) { return node; }
  15     static inline bool applies(Node node) { return false; }
  16   };
  17
  18   struct ConcatFlatten {
  19     static Node apply(Node node);
  20     static bool applies(Node node);
  21   };
  22
  23   struct ConcatExtractMerge {
  24     static Node apply(Node node);
  25     static bool applies(Node node);
  26   };
  27
  28   struct ConcatConstantMerge {
  29     static Node apply(Node node);
  30     static bool applies(Node node);
  31   };
  32
  33   struct ExtractExtract {
  34     static Node apply(Node node);
  35     static bool applies(Node node);
  36   };
  37
  38   struct ExtractWhole {
  39     static Node apply(Node node);
  40     static bool applies(Node node);
  41   };
  42
  43   struct ExtractConcat {
  44     static Node apply(Node node);
  45     static bool applies(Node node);
  46   };
  47
  48   struct ExtractConstant {
  49     static Node apply(Node node);
  50     static bool applies(Node node);
  51   };
  52
  53   struct FailEq {
  54     static Node apply(Node node);
  55     static bool applies(Node node);
  56   };
  57
  58   struct SimplifyEq {
  59     static Node apply(Node node);
  60     static bool applies(Node node);
  61   };
  62
  63 };
  64
  65 template<Kind kind, typename Rule>
  66 struct ApplyRuleToChildren {
  67
  68   static Node apply(Node node) {
  69     if (node.getKind() != kind) {
  70       if (Rule::applies(node)) return Rule::apply(node);
  71       else return node;
  72     }
  73     NodeBuilder<> result(kind);
  74     for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) {
  75       if (Rule::applies(node[i])) result << Rule::apply(node[i]);
  76       else result << node[i];
  77     }
  78     return result;
  79   }
  80
  81   static bool applies(Node node) {
  82     if (node.getKind() == kind) return true;
  83     return Rule::applies(node);
  84   }
  85
  86 };
  87
  88
  89 template <
  90   typename R1,
  91   typename R2,
  92   typename R3 = CoreRewriteRules::EmptyRule,
  93   typename R4 = CoreRewriteRules::EmptyRule,
  94   typename R5 = CoreRewriteRules::EmptyRule,
  95   typename R6 = CoreRewriteRules::EmptyRule,
  96   typename R7 = CoreRewriteRules::EmptyRule
  97   >
  98 struct LinearRewriteStrategy {
  99   static Node apply(Node node) {
 100     Node current = node;
 101     if (R1::applies(current)) current = R1::apply(current);
 102     if (R2::applies(current)) current = R2::apply(current);
 103     if (R3::applies(current)) current = R3::apply(current);
 104     if (R4::applies(current)) current = R4::apply(current);
 105     if (R5::applies(current)) current = R5::apply(current);
 106     if (R6::applies(current)) current = R6::apply(current);
 107     if (R7::applies(current)) current = R7::apply(current);
 108     return current;
 109   }
 110 };
 111
 112 } // End namespace bv
 113 } // End namespace theory
 114 } // End namespace CVC4