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, Morgan Deters, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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/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   static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
  81   static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
  82
  83   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
  84   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
  85
  86 public:
  87
  88   static RewriteResponse postRewrite(TNode node);
  89
  90   static RewriteResponse preRewrite(TNode node);
  91
  92   static void init();
  93   static void shutdown();
  94   /**
  95    * Temporary hack for devision-by-zero until we refactor theory code from
  96    * smt engine.
  97    *
  98    * @param node
  99    *
 100    * @return
 101    */
 102   static Node eliminateBVSDiv(TNode node);
 103 };/* class TheoryBVRewriter */
 104
 105 }/* CVC4::theory::bv namespace */
 106 }/* CVC4::theory namespace */
 107 }/* CVC4 namespace */
 108
 109 #endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */