Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)

[cvc5.git] / src / theory / booleans / theory_bool_rewriter.h

diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index b7512ad09f4fe52bcc073339a1284f220099c828..322d3a96a13784ffca5c9b437ef6f93c3497f0e4 100644 (file)
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -2,10 +2,10 @@
 /*! \file theory_bool_rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Tim King
+ **   Andres Noetzli, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 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
  **
@@ -17,29 +17,25 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
-#define __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
+#define CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
 
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 
 namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-class TheoryBoolRewriter {
+class TheoryBoolRewriter : public TheoryRewriter
+{
+ public:
+  RewriteResponse preRewrite(TNode node) override;
+  RewriteResponse postRewrite(TNode node) override;
 
-public:
-
-  static RewriteResponse preRewrite(TNode node);
-  static RewriteResponse postRewrite(TNode node);
-
-  static void init() {}
-  static void shutdown() {}
-
-};/* class TheoryBoolRewriter */
+}; /* class TheoryBoolRewriter */
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
+#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */