src/theory/bv/theory_bv_rewriter.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_rewriter.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Morgan Deters, Liana Hadarean
   6  ** Minor contributors (to current version): Tim King
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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/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 {
  34
  35   static RewriteFunction d_rewriteTable[kind::LAST_KIND];
  36
  37   static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
  38   static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
  39
  40   static void initializeRewrites();
  41
  42   static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
  43   static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
  44   static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false);
  45   static RewriteResponse RewriteUle(TNode node, bool prerewrite = false);
  46   static RewriteResponse RewriteSle(TNode node, bool prerewrite = false);
  47   static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false);
  48   static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false);
  49   static RewriteResponse RewriteUge(TNode node, bool prerewrite = false);
  50   static RewriteResponse RewriteSge(TNode node, bool prerewrite = false);
  51   static RewriteResponse RewriteNot(TNode node, bool prerewrite = false);
  52   static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false);
  53   static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false);
  54   static RewriteResponse RewriteOr(TNode node, bool prerewrite = false);
  55   static RewriteResponse RewriteXnor(TNode node, bool prerewrite = false);
  56   static RewriteResponse RewriteXor(TNode node, bool prerewrite = false);
  57   static RewriteResponse RewriteNand(TNode node, bool prerewrite = false);
  58   static RewriteResponse RewriteNor(TNode node, bool prerewrite = false);
  59   static RewriteResponse RewriteComp(TNode node, bool prerewrite = false);
  60   static RewriteResponse RewriteMult(TNode node, bool prerewrite = false);
  61   static RewriteResponse RewritePlus(TNode node, bool prerewrite = false);
  62   static RewriteResponse RewriteSub(TNode node, bool prerewrite = false);
  63   static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
  64   static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
  65   static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false);
  66   static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false);
  67   static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false);
  68   static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false);
  69   static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false);
  70   static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false);
  71   static RewriteResponse RewriteShl(TNode node, bool prerewrite = false);
  72   static RewriteResponse RewriteLshr(TNode node, bool prerewrite = false);
  73   static RewriteResponse RewriteAshr(TNode node, bool prerewrite = false);
  74   static RewriteResponse RewriteExtract(TNode node, bool prerewrite = false);
  75   static RewriteResponse RewriteRepeat(TNode node, bool prerewrite = false);
  76   static RewriteResponse RewriteZeroExtend(TNode node, bool prerewrite = false);
  77   static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
  78   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
  79   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
  80
  81 public:
  82
  83   static RewriteResponse postRewrite(TNode node);
  84
  85   static RewriteResponse preRewrite(TNode node);
  86
  87   static void init();
  88   static void shutdown();
  89   /**
  90    * Temporary hack for devision-by-zero until we refactor theory code from
  91    * smt engine.
  92    *
  93    * @param node
  94    *
  95    * @return
  96    */
  97   static Node eliminateBVSDiv(TNode node);
  98 };/* class TheoryBVRewriter */
  99
 100 }/* CVC4::theory::bv namespace */
 101 }/* CVC4::theory namespace */
 102 }/* CVC4 namespace */
 103
 104 #endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */