diff options
Diffstat (limited to 'src/theory/arith/arith_rewriter.h')
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 74 |
1 files changed, 49 insertions, 25 deletions
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index f7ef8c0c7..e161bd8d6 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -17,10 +17,13 @@ ** \todo document this file **/ -#include "theory/arith/arith_constants.h" #include "theory/theory.h" +#include "theory/arith/arith_constants.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" +#include "theory/rewriter.h" + #ifndef __CVC4__THEORY__ARITH__REWRITER_H #define __CVC4__THEORY__ARITH__REWRITER_H @@ -28,46 +31,67 @@ namespace CVC4 { namespace theory { namespace arith { -class ArithRewriter{ +class ArithRewriter { + private: - ArithConstants* d_constants; - Node makeSubtractionNode(TNode l, TNode r); - Node makeUnaryMinusNode(TNode n); + static arith::ArithConstants* s_constants; + + static Node makeSubtractionNode(TNode l, TNode r); + static Node makeUnaryMinusNode(TNode n); - RewriteResponse preRewriteTerm(TNode t); - RewriteResponse postRewriteTerm(TNode t); + static RewriteResponse preRewriteTerm(TNode t); + static RewriteResponse postRewriteTerm(TNode t); - RewriteResponse rewriteVariable(TNode t); - RewriteResponse rewriteConstant(TNode t); - RewriteResponse rewriteMinus(TNode t, bool pre); - RewriteResponse rewriteUMinus(TNode t, bool pre); - RewriteResponse rewriteDivByConstant(TNode t, bool pre); + static RewriteResponse rewriteVariable(TNode t); + static RewriteResponse rewriteConstant(TNode t); + static RewriteResponse rewriteMinus(TNode t, bool pre); + static RewriteResponse rewriteUMinus(TNode t, bool pre); + static RewriteResponse rewriteDivByConstant(TNode t, bool pre); - RewriteResponse preRewritePlus(TNode t); - RewriteResponse postRewritePlus(TNode t); + static RewriteResponse preRewritePlus(TNode t); + static RewriteResponse postRewritePlus(TNode t); - RewriteResponse preRewriteMult(TNode t); - RewriteResponse postRewriteMult(TNode t); + static RewriteResponse preRewriteMult(TNode t); + static RewriteResponse postRewriteMult(TNode t); - RewriteResponse preRewriteAtom(TNode t); - RewriteResponse postRewriteAtom(TNode t); - RewriteResponse postRewriteAtomConstantRHS(TNode t); + static RewriteResponse preRewriteAtom(TNode t); + static RewriteResponse postRewriteAtom(TNode t); + static RewriteResponse postRewriteAtomConstantRHS(TNode t); public: - ArithRewriter(ArithConstants* ac) : d_constants(ac) {} - RewriteResponse preRewrite(TNode n); - RewriteResponse postRewrite(TNode n); + static RewriteResponse preRewrite(TNode n); + static RewriteResponse postRewrite(TNode n); + + static void init() { + if (s_constants == NULL) { + s_constants = new arith::ArithConstants(NodeManager::currentNM()); + } + } + + static void shutdown() { + if (s_constants != NULL) { + delete s_constants; + s_constants = NULL; + } + } private: - bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); } - bool isTerm(TNode n) const { return !isAtom(n); } + + static inline bool isAtom(TNode n) { + return arith::isRelationOperator(n.getKind()); + } + + static inline bool isTerm(TNode n) { + return !isAtom(n); + } + }; -}; /* namesapce arith */ +}; /* namesapce rewrite */ }; /* namespace theory */ }; /* namespace CVC4 */ |