1 /********************* */
4 ** Original author: dejan
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief The Rewriter class
16 ** The Rewriter class.
19 #include "cvc4_private.h"
23 #include "expr/node.h"
24 #include "expr/attribute.h"
30 * Theory rewriters signal whether more rewriting is needed (or not)
31 * by using a member of this enumeration. See RewriteResponse, below.
37 };/* enum RewriteStatus */
40 * Instances of this class serve as response codes from
41 * Theory::preRewrite() and Theory::postRewrite(). Instances of
42 * derived classes RewriteComplete(n), RewriteAgain(n), and
43 * FullRewriteNeeded(n) should be used, giving self-documenting
46 struct RewriteResponse
{
47 const RewriteStatus status
;
49 RewriteResponse(RewriteStatus status
, Node node
) :
50 status(status
), node(node
) {}
51 };/* struct RewriteResponse */
54 * The main rewriter class. All functionality is static.
58 /** Returns the appropriate cache for a node */
59 static Node
getPreRewriteCache(theory::TheoryId theoryId
, TNode node
);
61 /** Returns the appropriate cache for a node */
62 static Node
getPostRewriteCache(theory::TheoryId theoryId
, TNode node
);
64 /** Sets the appropriate cache for a node */
65 static void setPreRewriteCache(theory::TheoryId theoryId
,
66 TNode node
, TNode cache
);
68 /** Sets the appropriate cache for a node */
69 static void setPostRewriteCache(theory::TheoryId theoryId
,
70 TNode node
, TNode cache
);
72 // disable construction of rewriters; all functionality is static
73 Rewriter() CVC4_UNUSED
;
74 Rewriter(const Rewriter
&) CVC4_UNUSED
;
77 * Rewrites the node using the given theory rewriter.
79 static Node
rewriteTo(theory::TheoryId theoryId
, Node node
);
81 /** Calls the pre-rewriter for the given theory */
82 static RewriteResponse
callPreRewrite(theory::TheoryId theoryId
, TNode node
);
84 /** Calls the post-rewriter for the given theory */
85 static RewriteResponse
callPostRewrite(theory::TheoryId theoryId
, TNode node
);
88 * Calls the equality-rewruter for the given theory.
90 static Node
callRewriteEquality(theory::TheoryId theoryId
, TNode equality
);
96 * Rewrites the node using theoryOf() to determine which rewriter to
99 static Node
rewrite(Node node
);
102 * Rewrite an equality between two terms that are already in normal form, so
103 * that the equality is in theory-normal form.
105 static Node
rewriteEquality(theory::TheoryId theoryId
, TNode node
);
108 * Should be called before the rewriter gets used for the first time.
113 * Should be called to clean up any state.
115 static void shutdown();
116 };/* class Rewriter */
118 }/* CVC4::theory namespace */
119 }/* CVC4 namespace */