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-2017 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 [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/rewriter.h"
20 #include "theory/theory.h"
21 #include "smt/smt_engine_scope.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/rewriter_tables.h"
24 #include "util/resource_manager.h"
31 unsigned long Rewriter::d_iterationCount
= 0;
33 static TheoryId
theoryOf(TNode node
) {
34 return Theory::theoryOf(THEORY_OF_TYPE_BASED
, node
);
37 #ifdef CVC4_ASSERTIONS
38 static CVC4_THREAD_LOCAL
std::unordered_set
<Node
, NodeHashFunction
>* s_rewriteStack
= NULL
;
39 #endif /* CVC4_ASSERTIONS */
41 class RewriterInitializer
{
42 static RewriterInitializer s_rewriterInitializer
;
43 RewriterInitializer() {
46 ~RewriterInitializer() { Rewriter::shutdown(); }
47 };/* class RewriterInitializer */
50 * This causes initialization of the rewriter before first use,
51 * and tear-down at exit time.
53 RewriterInitializer
RewriterInitializer::s_rewriterInitializer
;
56 * TheoryEngine::rewrite() keeps a stack of things that are being pre-
57 * and post-rewritten. Each element of the stack is a
58 * RewriteStackElement.
60 struct RewriteStackElement
{
62 /** The node we're currently rewriting */
66 /** Id of the theory that's currently rewriting this node */
67 unsigned theoryId
: 8;
68 /** Id of the original theory that started the rewrite */
69 unsigned originalTheoryId
: 8;
70 /** Index of the child this node is done rewriting */
71 unsigned nextChild
: 32;
72 /** Builder for this node */
73 NodeBuilder
<> builder
;
76 * Construct a fresh stack element.
78 RewriteStackElement(TNode node
, TheoryId theoryId
) :
82 originalTheoryId(theoryId
),
87 Node
Rewriter::rewrite(TNode node
) {
88 return rewriteTo(theoryOf(node
), node
);
91 Node
Rewriter::rewriteTo(theory::TheoryId theoryId
, Node node
) {
93 #ifdef CVC4_ASSERTIONS
94 bool isEquality
= node
.getKind() == kind::EQUAL
&& (!node
[0].getType().isBoolean());
96 if(s_rewriteStack
== NULL
) {
97 s_rewriteStack
= new std::unordered_set
<Node
, NodeHashFunction
>();
101 Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId
<< "," << node
<< ")"<< std::endl
;
103 // Check if it's been cached already
104 Node cached
= getPostRewriteCache(theoryId
, node
);
105 if (!cached
.isNull()) {
109 // Put the node on the stack in order to start the "recursive" rewrite
110 vector
<RewriteStackElement
> rewriteStack
;
111 rewriteStack
.push_back(RewriteStackElement(node
, theoryId
));
113 ResourceManager
* rm
= NULL
;
114 bool hasSmtEngine
= smt::smtEngineInScope();
116 rm
= NodeManager::currentResourceManager();
118 // Rewrite until the stack is empty
122 d_iterationCount
% ResourceManager::getFrequencyCount() == 0) {
123 rm
->spendResource(options::rewriteStep());
124 d_iterationCount
= 0;
127 // Get the top of the recursion stack
128 RewriteStackElement
& rewriteStackTop
= rewriteStack
.back();
130 Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId
) rewriteStackTop
.theoryId
<< "," << rewriteStackTop
.node
<< std::endl
;
132 // Before rewriting children we need to do a pre-rewrite of the node
133 if (rewriteStackTop
.nextChild
== 0) {
135 // Check if the pre-rewrite has already been done (it's in the cache)
136 Node cached
= Rewriter::getPreRewriteCache((TheoryId
) rewriteStackTop
.theoryId
, rewriteStackTop
.node
);
137 if (cached
.isNull()) {
138 // Rewrite until fix-point is reached
140 // Perform the pre-rewrite
141 RewriteResponse response
= Rewriter::callPreRewrite((TheoryId
) rewriteStackTop
.theoryId
, rewriteStackTop
.node
);
142 // Put the rewritten node to the top of the stack
143 rewriteStackTop
.node
= response
.node
;
144 TheoryId newTheory
= theoryOf(rewriteStackTop
.node
);
145 // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
146 if (newTheory
== (TheoryId
) rewriteStackTop
.theoryId
&& response
.status
== REWRITE_DONE
) {
149 rewriteStackTop
.theoryId
= newTheory
;
152 Rewriter::setPreRewriteCache((TheoryId
) rewriteStackTop
.originalTheoryId
, rewriteStackTop
.original
, rewriteStackTop
.node
);
154 // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
156 // Continue with the cached version
157 rewriteStackTop
.node
= cached
;
158 rewriteStackTop
.theoryId
= theoryOf(cached
);
162 rewriteStackTop
.original
=rewriteStackTop
.node
;
163 // Now it's time to rewrite the children, check if this has already been done
164 Node cached
= Rewriter::getPostRewriteCache((TheoryId
) rewriteStackTop
.theoryId
, rewriteStackTop
.node
);
165 // If not, go through the children
166 if(cached
.isNull()) {
168 // The child we need to rewrite
169 unsigned child
= rewriteStackTop
.nextChild
++;
171 // To build the rewritten expression we set up the builder
173 if (rewriteStackTop
.node
.getNumChildren() > 0) {
174 // The children will add themselves to the builder once they're done
175 rewriteStackTop
.builder
<< rewriteStackTop
.node
.getKind();
176 kind::MetaKind metaKind
= rewriteStackTop
.node
.getMetaKind();
177 if (metaKind
== kind::metakind::PARAMETERIZED
) {
178 rewriteStackTop
.builder
<< rewriteStackTop
.node
.getOperator();
183 // Process the next child
184 if(child
< rewriteStackTop
.node
.getNumChildren()) {
186 Node childNode
= rewriteStackTop
.node
[child
];
187 // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
188 rewriteStack
.push_back(RewriteStackElement(childNode
, theoryOf(childNode
)));
189 // Go on with the rewriting
193 // Incorporate the children if necessary
194 if (rewriteStackTop
.node
.getNumChildren() > 0) {
195 Node rewritten
= rewriteStackTop
.builder
;
196 rewriteStackTop
.node
= rewritten
;
197 rewriteStackTop
.theoryId
= theoryOf(rewriteStackTop
.node
);
200 // Done with all pre-rewriting, so let's do the post rewrite
202 // Do the post-rewrite
203 RewriteResponse response
= Rewriter::callPostRewrite((TheoryId
) rewriteStackTop
.theoryId
, rewriteStackTop
.node
);
204 // We continue with the response we got
205 TheoryId newTheoryId
= theoryOf(response
.node
);
206 if (newTheoryId
!= (TheoryId
) rewriteStackTop
.theoryId
|| response
.status
== REWRITE_AGAIN_FULL
) {
207 // In the post rewrite if we've changed theories, we must do a full rewrite
208 Assert(response
.node
!= rewriteStackTop
.node
);
209 //TODO: this is not thread-safe - should make this assertion dependent on sequential build
210 #ifdef CVC4_ASSERTIONS
211 Assert(s_rewriteStack
->find(response
.node
) == s_rewriteStack
->end());
212 s_rewriteStack
->insert(response
.node
);
214 Node rewritten
= rewriteTo(newTheoryId
, response
.node
);
215 rewriteStackTop
.node
= rewritten
;
216 #ifdef CVC4_ASSERTIONS
217 s_rewriteStack
->erase(response
.node
);
220 } else if (response
.status
== REWRITE_DONE
) {
221 #ifdef CVC4_ASSERTIONS
222 RewriteResponse r2
= Rewriter::callPostRewrite(newTheoryId
, response
.node
);
223 Assert(r2
.node
== response
.node
);
225 rewriteStackTop
.node
= response
.node
;
228 // Check for trivial rewrite loops of size 1 or 2
229 Assert(response
.node
!= rewriteStackTop
.node
);
230 Assert(Rewriter::callPostRewrite((TheoryId
) rewriteStackTop
.theoryId
, response
.node
).node
!= rewriteStackTop
.node
);
231 rewriteStackTop
.node
= response
.node
;
233 // We're done with the post rewrite, so we add to the cache
234 Rewriter::setPostRewriteCache((TheoryId
) rewriteStackTop
.originalTheoryId
, rewriteStackTop
.original
, rewriteStackTop
.node
);
237 // We were already in cache, so just remember it
238 rewriteStackTop
.node
= cached
;
239 rewriteStackTop
.theoryId
= theoryOf(cached
);
242 // If this is the last node, just return
243 if (rewriteStack
.size() == 1) {
244 Assert(!isEquality
|| rewriteStackTop
.node
.getKind() == kind::EQUAL
|| rewriteStackTop
.node
.isConst());
245 return rewriteStackTop
.node
;
248 // We're done with this node, append it to the parent
249 rewriteStack
[rewriteStack
.size() - 2].builder
<< rewriteStackTop
.node
;
250 rewriteStack
.pop_back();
254 }/* Rewriter::rewriteTo() */
256 void Rewriter::clearCaches() {
257 #ifdef CVC4_ASSERTIONS
258 if(s_rewriteStack
!= NULL
) {
259 delete s_rewriteStack
;
260 s_rewriteStack
= NULL
;
263 Rewriter::clearCachesInternal();
266 }/* CVC4::theory namespace */
267 }/* CVC4 namespace */