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/quantifiers | |
| 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/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 5d5e23c75..56eac761e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -19,7 +19,7 @@ #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H -#include "theory/rewriter.h" +#include "theory/theory_rewriter.h" namespace CVC4 { namespace theory { @@ -27,8 +27,9 @@ namespace quantifiers { struct QAttributes; -class QuantifiersRewriter { -public: +class QuantifiersRewriter : public TheoryRewriter +{ + public: static bool isLiteral( Node n ); //-------------------------------------variable elimination utilities /** is variable elimination @@ -194,10 +195,9 @@ private: }; static Node computeOperation( Node f, int computeOption, QAttributes& qa ); public: - static RewriteResponse preRewrite(TNode in); - static RewriteResponse postRewrite(TNode in); - static inline void init() {} - static inline void shutdown() {} + RewriteResponse preRewrite(TNode in) override; + RewriteResponse postRewrite(TNode in) override; + private: /** options */ static bool doOperation( Node f, int computeOption, QAttributes& qa ); @@ -223,7 +223,7 @@ public: static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false ); -};/* class QuantifiersRewriter */ +}; /* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ |