1 /********************* */
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief The Rewriter class
14 ** The Rewriter class.
17 #include "cvc4_private.h"
21 #include "expr/node.h"
22 #include "expr/attribute.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
;
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
75 Rewriter() CVC4_UNDEFINED
;
76 Rewriter(const Rewriter
&) CVC4_UNDEFINED
;
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();
107 * Rewrites the node using theoryOf() to determine which rewriter to
110 static Node
rewrite(TNode node
);
112 };/* class Rewriter */
114 }/* CVC4::theory namespace */
115 }/* CVC4 namespace */