diff options
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep_rewriter.h | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h index f4639efa3..0d1de3463 100644 --- a/src/theory/sep/theory_sep_rewriter.h +++ b/src/theory/sep/theory_sep_rewriter.h @@ -20,30 +20,32 @@ #ifndef CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H #define CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H -#include "theory/rewriter.h" +#include "theory/theory_rewriter.h" #include "theory/type_enumerator.h" namespace CVC4 { namespace theory { namespace sep { - -class TheorySepRewriter { -private: - static void getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ); - static void getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ); - static bool isSpatial( Node n, std::map< Node, bool >& visited ); -public: - - static RewriteResponse postRewrite(TNode node); - static inline RewriteResponse preRewrite(TNode node) { +class TheorySepRewriter : public TheoryRewriter +{ + public: + RewriteResponse postRewrite(TNode node) override; + RewriteResponse preRewrite(TNode node) override + { Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); } - static inline void init() {} - static inline void shutdown() {} -};/* class TheorySepRewriter */ + private: + static void getStarChildren(Node n, + std::vector<Node>& s_children, + std::vector<Node>& ns_children); + static void getAndChildren(Node n, + std::vector<Node>& s_children, + std::vector<Node>& ns_children); + static bool isSpatial(Node n, std::map<Node, bool>& visited); +}; /* class TheorySepRewriter */ }/* CVC4::theory::sep namespace */ }/* CVC4::theory namespace */ |