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/rewriter.h | |
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/rewriter.h')
-rw-r--r-- | src/theory/rewriter.h | 99 |
1 files changed, 39 insertions, 60 deletions
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 5a15d15fb..e55ca5d1c 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,100 +19,79 @@ #pragma once #include "expr/node.h" +#include "theory/theory_rewriter.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { namespace theory { -/** - * Theory rewriters signal whether more rewriting is needed (or not) - * by using a member of this enumeration. See RewriteResponse, below. - */ -enum RewriteStatus { - REWRITE_DONE, - REWRITE_AGAIN, - REWRITE_AGAIN_FULL -};/* enum RewriteStatus */ - -/** - * Instances of this class serve as response codes from - * Theory::preRewrite() and Theory::postRewrite(). Instances of - * derived classes RewriteComplete(n), RewriteAgain(n), and - * FullRewriteNeeded(n) should be used, giving self-documenting - * rewrite behavior. - */ -struct RewriteResponse { - const RewriteStatus status; - const Node node; - RewriteResponse(RewriteStatus status, Node node) : - status(status), node(node) {} -};/* struct RewriteResponse */ - class RewriterInitializer; /** - * The main rewriter class. All functionality is static. + * The main rewriter class. */ class Rewriter { + public: + Rewriter(); + + /** + * Rewrites the node using theoryOf() to determine which rewriter to + * use on the node. + */ + static Node rewrite(TNode node); + + /** + * Garbage collects the rewrite caches. + */ + static void clearCaches(); + + private: + /** + * Get the (singleton) instance of the rewriter. + * + * TODO(#3468): Get rid of this singleton + */ + static Rewriter& getInstance(); - friend class RewriterInitializer; - static unsigned long d_iterationCount; /** Returns the appropriate cache for a node */ - static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node); + Node getPreRewriteCache(theory::TheoryId theoryId, TNode node); /** Returns the appropriate cache for a node */ - static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node); + Node getPostRewriteCache(theory::TheoryId theoryId, TNode node); /** Sets the appropriate cache for a node */ - static void setPreRewriteCache(theory::TheoryId theoryId, - TNode node, TNode cache); + void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); /** Sets the appropriate cache for a node */ - static void setPostRewriteCache(theory::TheoryId theoryId, - TNode node, TNode cache); - - // disable construction of rewriters; all functionality is static - Rewriter() = delete; - Rewriter(const Rewriter&) = delete; + void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache); /** * Rewrites the node using the given theory rewriter. */ - static Node rewriteTo(theory::TheoryId theoryId, Node node); + Node rewriteTo(theory::TheoryId theoryId, Node node); /** Calls the pre-rewriter for the given theory */ - static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); + RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); /** Calls the post-rewriter for the given theory */ - static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); + RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); /** * Calls the equality-rewriter for the given theory. */ - static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality); + Node callRewriteEquality(theory::TheoryId theoryId, TNode equality); - /** - * Should be called before the rewriter gets used for the first time. - */ - static void init(); + void clearCachesInternal(); - /** - * Should be called to clean up any state. - */ - static void shutdown(); - static void clearCachesInternal(); -public: + /** Theory rewriters managed by this rewriter instance */ + std::unique_ptr<TheoryRewriter> d_theoryRewriters[theory::THEORY_LAST]; - /** - * Rewrites the node using theoryOf() to determine which rewriter to - * use on the node. - */ - static Node rewrite(TNode node); + unsigned long d_iterationCount = 0; - /** - * Garbage collects the rewrite caches. - */ - static void clearCaches(); +#ifdef CVC4_ASSERTIONS + std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack = + nullptr; +#endif /* CVC4_ASSERTIONS */ };/* class Rewriter */ }/* CVC4::theory namespace */ |