diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 11:19:10 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-09 11:19:10 -0800 |
commit | b6ce0f23ce0aaa0552767e8067fe58dbceee11cb (patch) | |
tree | 0783321580ed511c7ecfa3f59363dadcee15acde /src/theory/builtin | |
parent | d06b46efade674023236da228601806daf06f1af (diff) |
Make theory rewriters non-static (#3547)
This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
singletons in general. Note that the `Rewriter` class is still a
singleton, which will be changed in a future commit.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 3 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 21 |
2 files changed, 10 insertions, 14 deletions
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index d483bf994..d9fe2fecc 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -15,11 +15,12 @@ ** \todo document this file **/ -#include "expr/attribute.h" #include "theory/builtin/theory_builtin_rewriter.h" +#include "expr/attribute.h" #include "expr/chain.h" #include "expr/node_algorithm.h" +#include "theory/rewriter.h" using namespace std; diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 5f703fa00..05b1b643c 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -20,15 +20,15 @@ #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H -#include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_rewriter.h" namespace CVC4 { namespace theory { namespace builtin { -class TheoryBuiltinRewriter { - +class TheoryBuiltinRewriter : public TheoryRewriter +{ static Node blastDistinct(TNode node); static Node blastChain(TNode node); @@ -45,17 +45,12 @@ public: } } - static RewriteResponse postRewrite(TNode node); - - static inline RewriteResponse preRewrite(TNode node) { - return doRewrite(node); - } + RewriteResponse postRewrite(TNode node) override; - static inline void init() {} - static inline void shutdown() {} + RewriteResponse preRewrite(TNode node) override { return doRewrite(node); } -// conversions between lambdas and arrays -private: + // conversions between lambdas and arrays + private: /** recursive helper for getLambdaForArrayRepresentation */ static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, std::unordered_map< TNode, Node, TNodeHashFunction >& visited ); @@ -124,7 +119,7 @@ private: * to n, this method returns null. */ static Node getArrayRepresentationForLambda(TNode n); -};/* class TheoryBuiltinRewriter */ +}; /* class TheoryBuiltinRewriter */ }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ |