Make theory rewriters non-static (#3547)

[cvc5.git] / src / theory / bv / theory_bv_rewriter.h

diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 0ce3fa3035c2f2140fca5b200da1b8c3a0b2937c..8c8b7846c51e7f63d5838640f07b5f43fae3c2af 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file theory_bv_rewriter.h
  ** \verbatim
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Morgan Deters, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -19,11 +17,11 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
-#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
-#include "theory/rewriter.h"
-#include "util/stats.h"
+#include "theory/theory_rewriter.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -32,27 +30,40 @@ namespace bv {
 struct AllRewriteRules;
 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
-class TheoryBVRewriter {
-  // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
-  // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer; 
-
-#warning "TODO: Double check thread safety and make sure the fix compiles on mac."
-  static RewriteFunction d_rewriteTable[kind::LAST_KIND];
-
+class TheoryBVRewriter : public TheoryRewriter
+{
+ public:
+  /**
+   * Temporary hack for devision-by-zero until we refactor theory code from
+   * smt engine.
+   *
+   * @param node
+   *
+   * @return
+   */
+  static Node eliminateBVSDiv(TNode node);
+
+  TheoryBVRewriter();
+
+  RewriteResponse postRewrite(TNode node) override;
+  RewriteResponse preRewrite(TNode node) override;
+
+ private:
   static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
   static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); 
-
-  static void initializeRewrites();
   
- static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSltBv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUle(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSle(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUge(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSge(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteITEBv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteNot(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false);
@@ -68,6 +79,8 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false);
@@ -80,25 +93,19 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
 
-public:
+  static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
 
-  static RewriteResponse postRewrite(TNode node);
+  void initializeRewrites();
 
-  static RewriteResponse preRewrite(TNode node);
-
-  static inline Node rewriteEquality(TNode node) {
-    Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl;
-    return postRewrite(node).node;
-  }
-
-  static void init();
-  static void shutdown();
-  
-};/* class TheoryBVRewriter */
+  RewriteFunction d_rewriteTable[kind::LAST_KIND];
+}; /* class TheoryBVRewriter */
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */