src/theory/bv/theory_bv_rewriter.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_rewriter.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Andres Noetzli, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 #ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
  21 #define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
  22
  23 #include "theory/theory_rewriter.h"
  24 #include "util/statistics_registry.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace bv {
  29
  30 struct AllRewriteRules;
  31 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
  32
  33 class TheoryBVRewriter : public TheoryRewriter
  34 {
  35  public:
  36   /**
  37    * Temporary hack for devision-by-zero until we refactor theory code from
  38    * smt engine.
  39    *
  40    * @param node
  41    *
  42    * @return
  43    */
  44   static Node eliminateBVSDiv(TNode node);
  45
  46   TheoryBVRewriter();
  47
  48   RewriteResponse postRewrite(TNode node) override;
  49   RewriteResponse preRewrite(TNode node) override;
  50
  51  private:
  52   static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
  53   static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
  54
  55   static RewriteResponse RewriteBitOf(TNode node, bool prerewrite = false);
  56   static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
  57   static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
  58   static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false);
  59   static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false);
  60   static RewriteResponse RewriteSltBv(TNode node, bool prerewrite = false);
  61   static RewriteResponse RewriteUle(TNode node, bool prerewrite = false);
  62   static RewriteResponse RewriteSle(TNode node, bool prerewrite = false);
  63   static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false);
  64   static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false);
  65   static RewriteResponse RewriteUge(TNode node, bool prerewrite = false);
  66   static RewriteResponse RewriteSge(TNode node, bool prerewrite = false);
  67   static RewriteResponse RewriteITEBv(TNode node, bool prerewrite = false);
  68   static RewriteResponse RewriteNot(TNode node, bool prerewrite = false);
  69   static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false);
  70   static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false);
  71   static RewriteResponse RewriteOr(TNode node, bool prerewrite = false);
  72   static RewriteResponse RewriteXnor(TNode node, bool prerewrite = false);
  73   static RewriteResponse RewriteXor(TNode node, bool prerewrite = false);
  74   static RewriteResponse RewriteNand(TNode node, bool prerewrite = false);
  75   static RewriteResponse RewriteNor(TNode node, bool prerewrite = false);
  76   static RewriteResponse RewriteComp(TNode node, bool prerewrite = false);
  77   static RewriteResponse RewriteMult(TNode node, bool prerewrite = false);
  78   static RewriteResponse RewritePlus(TNode node, bool prerewrite = false);
  79   static RewriteResponse RewriteSub(TNode node, bool prerewrite = false);
  80   static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
  81   static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
  82   static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false);
  83   static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false);
  84   static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false);
  85   static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false);
  86   static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false);
  87   static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false);
  88   static RewriteResponse RewriteShl(TNode node, bool prerewrite = false);
  89   static RewriteResponse RewriteLshr(TNode node, bool prerewrite = false);
  90   static RewriteResponse RewriteAshr(TNode node, bool prerewrite = false);
  91   static RewriteResponse RewriteExtract(TNode node, bool prerewrite = false);
  92   static RewriteResponse RewriteRepeat(TNode node, bool prerewrite = false);
  93   static RewriteResponse RewriteZeroExtend(TNode node, bool prerewrite = false);
  94   static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
  95   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
  96   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
  97   static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
  98   static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
  99
 100   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
 101   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
 102
 103   void initializeRewrites();
 104
 105   RewriteFunction d_rewriteTable[kind::LAST_KIND];
 106 }; /* class TheoryBVRewriter */
 107
 108 }/* CVC4::theory::bv namespace */
 109 }/* CVC4::theory namespace */
 110 }/* CVC4 namespace */
 111
 112 #endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */