1 /********************* */
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Morgan Deters, Liana Hadarean
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The Rewriter class
14 ** The Rewriter class.
17 #include "cvc4_private.h"
21 #include "expr/node.h"
22 #include "util/unsafe_interrupt_exception.h"
28 * Theory rewriters signal whether more rewriting is needed (or not)
29 * by using a member of this enumeration. See RewriteResponse, below.
35 };/* enum RewriteStatus */
38 * Instances of this class serve as response codes from
39 * Theory::preRewrite() and Theory::postRewrite(). Instances of
40 * derived classes RewriteComplete(n), RewriteAgain(n), and
41 * FullRewriteNeeded(n) should be used, giving self-documenting
44 struct RewriteResponse
{
45 const RewriteStatus status
;
47 RewriteResponse(RewriteStatus status
, Node node
) :
48 status(status
), node(node
) {}
49 };/* struct RewriteResponse */
51 class RewriterInitializer
;
54 * The main rewriter class. All functionality is static.
58 friend class RewriterInitializer
;
59 static unsigned long d_iterationCount
;
60 /** Returns the appropriate cache for a node */
61 static Node
getPreRewriteCache(theory::TheoryId theoryId
, TNode node
);
63 /** Returns the appropriate cache for a node */
64 static Node
getPostRewriteCache(theory::TheoryId theoryId
, TNode node
);
66 /** Sets the appropriate cache for a node */
67 static void setPreRewriteCache(theory::TheoryId theoryId
,
68 TNode node
, TNode cache
);
70 /** Sets the appropriate cache for a node */
71 static void setPostRewriteCache(theory::TheoryId theoryId
,
72 TNode node
, TNode cache
);
74 // disable construction of rewriters; all functionality is static
76 Rewriter(const Rewriter
&) = delete;
79 * Rewrites the node using the given theory rewriter.
81 static Node
rewriteTo(theory::TheoryId theoryId
, Node node
);
83 /** Calls the pre-rewriter for the given theory */
84 static RewriteResponse
callPreRewrite(theory::TheoryId theoryId
, TNode node
);
86 /** Calls the post-rewriter for the given theory */
87 static RewriteResponse
callPostRewrite(theory::TheoryId theoryId
, TNode node
);
90 * Calls the equality-rewriter for the given theory.
92 static Node
callRewriteEquality(theory::TheoryId theoryId
, TNode equality
);
95 * Should be called before the rewriter gets used for the first time.
100 * Should be called to clean up any state.
102 static void shutdown();
103 static void clearCachesInternal();
107 * Rewrites the node using theoryOf() to determine which rewriter to
110 static Node
rewrite(TNode node
);
113 * Garbage collects the rewrite caches.
115 static void clearCaches();
116 };/* class Rewriter */
118 }/* CVC4::theory namespace */
119 }/* CVC4 namespace */