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/strings | |
| 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/strings')
| -rw-r--r-- | src/theory/strings/regexp_elim.cpp | 1 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 17 |
2 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 42d679692..1942938c3 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -16,6 +16,7 @@ #include "theory/strings/regexp_elim.h" #include "options/strings_options.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index b19d49e67..35805e1c2 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -18,19 +18,20 @@ #ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H #define CVC4__THEORY__STRINGS__THEORY_STRINGS_REWRITER_H +#include <climits> #include <utility> #include <vector> -#include "theory/rewriter.h" -#include "theory/type_enumerator.h" #include "expr/attribute.h" -#include <climits> +#include "theory/theory_rewriter.h" +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { namespace strings { -class TheoryStringsRewriter { +class TheoryStringsRewriter : public TheoryRewriter +{ private: /** simple regular expression consume * @@ -155,11 +156,9 @@ class TheoryStringsRewriter { static Node returnRewrite(Node node, Node ret, const char* c); public: - static RewriteResponse postRewrite(TNode node); - static RewriteResponse preRewrite(TNode node); + RewriteResponse postRewrite(TNode node) override; + RewriteResponse preRewrite(TNode node) override; - static inline void init() {} - static inline void shutdown() {} /** get the cardinality of the alphabet used, based on the options */ static unsigned getAlphabetCardinality(); /** rewrite equality @@ -769,7 +768,7 @@ class TheoryStringsRewriter { * and the list of nodes that are compared to the empty string */ static std::pair<bool, std::vector<Node> > collectEmptyEqs(Node x); -};/* class TheoryStringsRewriter */ +}; /* class TheoryStringsRewriter */ }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ |