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 42bccb534fe0c868bc7e6eb4f79a37d5b0f5bfaa..8c8b7846c51e7f63d5838640f07b5f43fae3c2af 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_bv_rewriter.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Liana Hadarean
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** 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 ]]
  **
@@ -17,10 +17,10 @@
 
 #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 "theory/theory_rewriter.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -30,24 +30,40 @@ namespace bv {
 struct AllRewriteRules;
 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
-class TheoryBVRewriter {
+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);
 
-  static RewriteFunction d_rewriteTable[kind::LAST_KIND];
+  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 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);
@@ -77,31 +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);
 
   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
 
-public:
+  void initializeRewrites();
 
-  static RewriteResponse postRewrite(TNode node);
-
-  static RewriteResponse preRewrite(TNode node);
-  
-  static void init();
-  static void shutdown();
-  /** 
-   * Temporary hack for devision-by-zero until we refactor theory code from
-   * smt engine. 
-   * 
-   * @param node 
-   * 
-   * @return 
-   */
-  static Node eliminateBVSDiv(TNode node); 
-};/* 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 */