Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The Rewriter class.
11 : : */
12 : :
13 : : #include "theory/rewriter.h"
14 : :
15 : : #include <deque>
16 : :
17 : : #include "options/theory_options.h"
18 : : #include "proof/conv_proof_generator.h"
19 : : #include "theory/builtin/proof_checker.h"
20 : : #include "theory/evaluator.h"
21 : : #include "theory/quantifiers/extended_rewrite.h"
22 : : #include "theory/rewriter_tables.h"
23 : : #include "theory/theory.h"
24 : : #include "util/resource_manager.h"
25 : :
26 : : using namespace std;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : :
31 : : // Note that this function is a simplified version of Theory::theoryOf for
32 : : // (type-based) theoryOfMode. We expand and simplify it here for the sake of
33 : : // efficiency.
34 : 299178221 : static TheoryId theoryOf(TNode node)
35 : : {
36 [ + + ]: 299178221 : if (node.getKind() == Kind::EQUAL)
37 : : {
38 : : // Equality is owned by the theory that owns the domain
39 : 45316393 : return Theory::theoryOf(node[0].getType());
40 : : }
41 : : // Regular nodes are owned by the kind
42 : 253861828 : return kindToTheoryId(node.getKind());
43 : : }
44 : :
45 : : /**
46 : : * TheoryEngine::rewrite() keeps a stack of things that are being pre-
47 : : * and post-rewritten. Each element of the stack is a
48 : : * RewriteStackElement.
49 : : */
50 : : struct RewriteStackElement
51 : : {
52 : : enum State
53 : : {
54 : : PRE_REWRITE,
55 : : REWRITE_CHILDREN,
56 : : POST_REWRITE,
57 : : WAIT_FOR_FULL_REWRITE,
58 : : FINALIZE
59 : : };
60 : :
61 : : /**
62 : : * Construct a fresh stack element.
63 : : */
64 : 63553536 : RewriteStackElement(TNode node, TheoryId theoryId)
65 : 63553536 : : d_node(node),
66 : 63553536 : d_original(node),
67 : 63553536 : d_postRewriteCache(Node::null()),
68 : 63553536 : d_fullRewriteNode(Node::null()),
69 : 63553536 : d_theoryId(theoryId),
70 : 63553536 : d_originalTheoryId(theoryId),
71 : 63553536 : d_state(PRE_REWRITE),
72 : 63553536 : d_nextChild(0),
73 : 63553536 : d_builder(node.getNodeManager())
74 : : {
75 : 63553536 : }
76 : :
77 : 205496513 : TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }
78 : :
79 : 87117402 : TheoryId getOriginalTheoryId()
80 : : {
81 : 87117402 : return static_cast<TheoryId>(d_originalTheoryId);
82 : : }
83 : :
84 : 269662384 : State getState() const { return static_cast<State>(d_state); }
85 : :
86 : 110855612 : void setState(State state) { d_state = state; }
87 : :
88 : : /** The node we're currently rewriting */
89 : : Node d_node;
90 : : /** Original node (either the unrewritten node or the node after prerewriting)
91 : : */
92 : : Node d_original;
93 : : /** Cached post-rewrite result, if one exists for d_original */
94 : : Node d_postRewriteCache;
95 : : /** Node whose full rewrite this stack element is waiting on */
96 : : Node d_fullRewriteNode;
97 : : /** Id of the theory that's currently rewriting this node */
98 : : unsigned d_theoryId : 8;
99 : : /** Id of the original theory that started the rewrite */
100 : : unsigned d_originalTheoryId : 8;
101 : : /** The current processing state for this node */
102 : : unsigned d_state : 8;
103 : : /** Index of the child this node is done rewriting */
104 : : unsigned d_nextChild : 32;
105 : : /** Builder for this node */
106 : : NodeBuilder d_builder;
107 : : };
108 : :
109 : 100533991 : Node Rewriter::rewrite(TNode node)
110 : : {
111 [ + + ]: 100533991 : if (node.getNumChildren() == 0)
112 : : {
113 : : // Nodes with zero children should never change via rewriting. We return
114 : : // eagerly for the sake of efficiency here.
115 : 8993984 : return node;
116 : : }
117 : 91540007 : return rewriteTo(theoryOf(node), node);
118 : : }
119 : :
120 : 593647 : Node Rewriter::extendedRewrite(TNode node, bool aggr)
121 : : {
122 : 593647 : quantifiers::ExtendedRewriter er(d_nm, *this, aggr);
123 : 1187294 : return er.extendedRewrite(node);
124 : 593647 : }
125 : :
126 : 225191 : TrustNode Rewriter::rewriteWithProof(TNode node, bool isExtEq)
127 : : {
128 : : // must set the proof checker before calling this
129 [ - + ][ - + ]: 225191 : Assert(d_tpg != nullptr);
[ - - ]
130 [ + + ]: 225191 : if (isExtEq)
131 : : {
132 : : // theory rewriter is responsible for rewriting the equality
133 : 702 : TheoryRewriter* tr = d_theoryRewriters[theoryOf(node)];
134 [ - + ][ - + ]: 702 : Assert(tr != nullptr);
[ - - ]
135 : 702 : return tr->rewriteEqualityExtWithProof(node);
136 : : }
137 : 448978 : Node ret = rewriteTo(theoryOf(node), node, d_tpg.get());
138 [ + - ]: 224489 : return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
139 : 224489 : }
140 : :
141 : 13593 : void Rewriter::finishInit(Env& env)
142 : : {
143 : : // if not already initialized with proof support
144 [ + - ]: 13593 : if (d_tpg == nullptr)
145 : : {
146 [ + - ]: 13593 : Trace("rewriter") << "Rewriter::finishInit" << std::endl;
147 : : // the rewriter is staticly determinstic, thus use static cache policy
148 : : // for the term conversion proof generator
149 : 27186 : d_tpg.reset(new TConvProofGenerator(env,
150 : : nullptr,
151 : : TConvPolicy::FIXPOINT,
152 : : TConvCachePolicy::STATIC,
153 : 13593 : "Rewriter::TConvProofGenerator"));
154 : : }
155 : 13593 : }
156 : :
157 : 43485 : Node Rewriter::rewriteEqualityExt(TNode node)
158 : : {
159 [ - + ][ - + ]: 43485 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
160 : : // note we don't force caching of this method currently
161 : 43485 : return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
162 : : }
163 : :
164 : 380328 : void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
165 : : TheoryRewriter* trew)
166 : : {
167 [ + + ]: 380328 : if (trew == nullptr)
168 : : {
169 : : // if nullptr, use the default (null) theory rewriter.
170 : 20 : d_nullTr.emplace_back(
171 : 40 : std::unique_ptr<NoOpTheoryRewriter>(new NoOpTheoryRewriter(d_nm, tid)));
172 : 20 : d_theoryRewriters[tid] = d_nullTr.back().get();
173 : : }
174 : : else
175 : : {
176 : 380308 : d_theoryRewriters[tid] = trew;
177 : : }
178 : 380328 : }
179 : :
180 : 2105951 : TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
181 : : {
182 : 2105951 : return d_theoryRewriters[theoryId];
183 : : }
184 : :
185 : 90980 : Node Rewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
186 : : {
187 : : // dispatches to the appropriate theory
188 : 90980 : TheoryId tid = theoryOf(n);
189 : 90980 : TheoryRewriter* tr = getTheoryRewriter(tid);
190 [ + - ]: 90980 : if (tr != nullptr)
191 : : {
192 : 90980 : return tr->rewriteViaRule(id, n);
193 : : }
194 : 0 : return Node::null();
195 : : }
196 : :
197 : 1810167 : ProofRewriteRule Rewriter::findRule(const Node& a,
198 : : const Node& b,
199 : : TheoryRewriteCtx ctx)
200 : : {
201 : : // dispatches to the appropriate theory
202 : 1810167 : TheoryId tid = theoryOf(a);
203 : 1810167 : TheoryRewriter* tr = getTheoryRewriter(tid);
204 [ + - ]: 1810167 : if (tr != nullptr)
205 : : {
206 : 1810167 : return tr->findRule(a, b, ctx);
207 : : }
208 : 0 : return ProofRewriteRule::NONE;
209 : : }
210 : :
211 : 91764496 : Node Rewriter::rewriteTo(theory::TheoryId theoryId,
212 : : Node node,
213 : : TConvProofGenerator* tcpg)
214 : : {
215 : : #ifdef CVC5_ASSERTIONS
216 : 183528992 : bool isEquality = node.getKind() == Kind::EQUAL
217 : 111741052 : && !node[0].getType().isBoolean()
218 : 111741052 : && !node[1].getType().isBoolean();
219 : :
220 [ + + ]: 91764496 : if (d_rewriteStack == nullptr)
221 : : {
222 : 25660 : d_rewriteStack.reset(new std::unordered_set<Node>());
223 : : }
224 : : #endif
225 : :
226 [ + - ]: 183528992 : Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"
227 : 91764496 : << std::endl;
228 : :
229 : : // Check if it's been cached already
230 : 91764496 : Node cached = getPostRewriteCache(theoryId, node);
231 [ + + ][ + + ]: 91764496 : if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node)))
[ + + ][ + + ]
[ + + ][ - - ]
232 : : {
233 : 78299638 : return cached;
234 : : }
235 : :
236 : : // Put the node on the stack in order to start the "recursive" rewrite
237 : : // Use deque since RewriteStackElement contains a live NodeBuilder; unlike a
238 : : // vector, pushing deep stacks will not relocate existing frames.
239 : 13464858 : deque<RewriteStackElement> rewriteStack;
240 : 13464858 : rewriteStack.push_back(RewriteStackElement(node, theoryId));
241 : :
242 : : // Rewrite until the stack is empty
243 : : for (;;)
244 : : {
245 [ + - ]: 219573706 : if (d_resourceManager != nullptr)
246 : : {
247 : 219573706 : d_resourceManager->spendResource(Resource::RewriteStep);
248 : : }
249 : :
250 : : // Get the top of the recursion stack
251 : 219573706 : RewriteStackElement& rewriteStackTop = rewriteStack.back();
252 : :
253 [ + - ]: 439147412 : Trace("rewriter") << "Rewriter::rewriting: "
254 : 219573706 : << rewriteStackTop.getTheoryId() << ","
255 : 219573706 : << rewriteStackTop.d_node << std::endl;
256 : :
257 : 219573706 : RewriteStackElement::State state = rewriteStackTop.getState();
258 [ + + ]: 219573706 : if (state == RewriteStackElement::PRE_REWRITE)
259 : : {
260 : : // Check if the pre-rewrite has already been done (it's in the cache)
261 : 127107072 : cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
262 : 127107072 : rewriteStackTop.d_node);
263 : 190660608 : if (cached.isNull()
264 [ + + ][ + + ]: 66529777 : || (tcpg != nullptr
265 [ + + ][ + + ]: 66529777 : && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
[ + + ][ - - ]
266 : : {
267 : : // Rewrite until fix-point is reached
268 : : for (;;)
269 : : {
270 : : // Perform the pre-rewrite
271 : 28199298 : Kind originalKind = rewriteStackTop.d_node.getKind();
272 : : RewriteResponse response = preRewrite(
273 : 28199298 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
274 : :
275 : : // Put the rewritten node to the top of the stack
276 : 28199298 : TNode newNode = response.d_node;
277 [ + - ]: 56398596 : Trace("rewriter-debug") << "Pre-Rewrite: " << rewriteStackTop.d_node
278 : 28199298 : << " to " << newNode << std::endl;
279 : 28199298 : TheoryId newTheory = theoryOf(newNode);
280 : 28199298 : rewriteStackTop.d_node = newNode;
281 : 28199298 : rewriteStackTop.d_theoryId = newTheory;
282 [ - + ][ - - ]: 56398596 : Assert(newNode.getType().isComparableTo(
283 : : rewriteStackTop.d_node.getType()))
284 : 28199298 : << "Pre-rewriting " << rewriteStackTop.d_node << " to " << newNode
285 : 0 : << " does not preserve type";
286 : : // In the pre-rewrite, if changing theories, we just call the other
287 : : // theories pre-rewrite. If the kind of the node was changed, then we
288 : : // pre-rewrite again.
289 : 28199298 : if ((originalKind == newNode.getKind()
290 [ + + ]: 24451020 : && response.d_status == REWRITE_DONE)
291 [ + + ][ + + ]: 52650318 : || newNode.getNumChildren() == 0)
[ + + ]
292 : : {
293 [ + - ]: 23563866 : if (Configuration::isAssertionBuild())
294 : : {
295 : : // REWRITE_DONE should imply that no other pre-rewriting can be
296 : : // done.
297 : : Node rewrittenAgain =
298 : 47127732 : preRewrite(newTheory, newNode, nullptr).d_node;
299 : 23563866 : Assert(newNode == rewrittenAgain)
300 [ - + ][ - + ]: 23563866 : << "Rewriter returned REWRITE_DONE for " << newNode
[ - - ]
301 : 0 : << " but it can be rewritten to " << rewrittenAgain;
302 : 23563866 : }
303 : 23563866 : break;
304 : : }
305 [ + + ][ + + ]: 56398596 : }
306 : :
307 : : // Cache the rewrite
308 : 23563866 : setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
309 : 23563866 : rewriteStackTop.d_original,
310 : 23563866 : rewriteStackTop.d_node);
311 : : }
312 : : // Otherwise we've already been pre-rewritten (in pre-rewrite cache)
313 : : else
314 : : {
315 : : // Continue with the cached version
316 : 39989670 : rewriteStackTop.d_node = cached;
317 : 39989670 : rewriteStackTop.d_theoryId = theoryOf(cached);
318 : : }
319 : 63553536 : rewriteStackTop.d_original = rewriteStackTop.d_node;
320 : 127107072 : rewriteStackTop.d_postRewriteCache = getPostRewriteCache(
321 : 127107072 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
322 : 190660608 : if (!rewriteStackTop.d_postRewriteCache.isNull()
323 [ + + ][ + + ]: 66470047 : && (tcpg == nullptr
324 [ + + ][ + + ]: 66470047 : || hasRewrittenWithProofs(rewriteStackTop.d_node)))
[ + + ][ - - ]
325 : : {
326 : 42364558 : rewriteStackTop.d_node = rewriteStackTop.d_postRewriteCache;
327 : 42364558 : rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
328 : 42364558 : rewriteStackTop.setState(RewriteStackElement::FINALIZE);
329 : : }
330 : : else
331 : : {
332 : 21188978 : rewriteStackTop.setState(RewriteStackElement::REWRITE_CHILDREN);
333 : : }
334 : 63553536 : continue;
335 : 63553536 : }
336 : :
337 [ + + ]: 156020170 : if (state == RewriteStackElement::REWRITE_CHILDREN)
338 : : {
339 : 68815596 : size_t numChildren = rewriteStackTop.d_node.getNumChildren();
340 [ + + ][ + + ]: 68815596 : if (rewriteStackTop.d_nextChild == 0 && numChildren > 0)
341 : : {
342 : : // The children will add themselves to the builder once they're done.
343 : 20212460 : rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
344 : 20212460 : kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
345 [ + + ]: 20212460 : if (metaKind == kind::metakind::PARAMETERIZED)
346 : : {
347 : 1217899 : rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
348 : : }
349 : : }
350 [ + + ]: 68815596 : if (rewriteStackTop.d_nextChild < numChildren)
351 : : {
352 : 47626618 : Node childNode = rewriteStackTop.d_node[rewriteStackTop.d_nextChild++];
353 : 47626618 : rewriteStack.push_back(
354 : 95253236 : RewriteStackElement(childNode, theoryOf(childNode)));
355 : 47626618 : continue;
356 : 47626618 : }
357 [ + + ]: 21188978 : if (numChildren > 0)
358 : : {
359 : 20212460 : rewriteStackTop.d_node = rewriteStackTop.d_builder;
360 : 20212460 : rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
361 : : }
362 : 21188978 : rewriteStackTop.setState(RewriteStackElement::POST_REWRITE);
363 : 21188978 : continue;
364 : 21188978 : }
365 : :
366 [ + + ]: 87204574 : if (state == RewriteStackElement::POST_REWRITE)
367 : : {
368 : : for (;;)
369 : : {
370 : : // Do the post-rewrite
371 : 24613727 : Kind originalKind = rewriteStackTop.d_node.getKind();
372 : : RewriteResponse response = postRewrite(
373 : 24613727 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
374 : 24613727 : TNode newNode = response.d_node;
375 [ + - ]: 49227454 : Trace("rewriter-debug") << "Post-Rewrite: " << rewriteStackTop.d_node
376 : 24613727 : << " to " << newNode << std::endl;
377 : 24613727 : TheoryId newTheoryId = theoryOf(newNode);
378 [ - + ][ - - ]: 49227454 : Assert(
379 : : newNode.getType().isComparableTo(rewriteStackTop.d_node.getType()))
380 : 24613727 : << "Post-rewriting " << rewriteStackTop.d_node << " to " << newNode
381 : 0 : << " does not preserve type";
382 : 24613727 : if (newTheoryId != rewriteStackTop.getTheoryId()
383 [ + + ][ + + ]: 24613727 : || response.d_status == REWRITE_AGAIN_FULL)
[ + + ]
384 : : {
385 : : // In the post rewrite if we've changed theories, do the full rewrite
386 : : // by pushing it onto the explicit stack instead of recursing.
387 [ - + ][ - + ]: 2462060 : Assert(response.d_node != rewriteStackTop.d_node);
[ - - ]
388 : : // TODO: this is not thread-safe - should make this assertion
389 : : // dependent on sequential build
390 : : #ifdef CVC5_ASSERTIONS
391 : 2462060 : Assert(d_rewriteStack->find(response.d_node) == d_rewriteStack->end())
392 : 0 : << "Non-terminating rewriting detected for: " << response.d_node;
393 : 2462060 : d_rewriteStack->insert(response.d_node);
394 : : #endif
395 : 2462060 : rewriteStackTop.d_fullRewriteNode = response.d_node;
396 : 2462060 : rewriteStackTop.setState(RewriteStackElement::WAIT_FOR_FULL_REWRITE);
397 : 2462060 : rewriteStack.push_back(
398 : 4924120 : RewriteStackElement(response.d_node, newTheoryId));
399 : 2462060 : break;
400 : : }
401 : 44303334 : else if ((response.d_status == REWRITE_DONE
402 [ + + ]: 21147755 : && originalKind == newNode.getKind())
403 [ + + ][ + + ]: 43299422 : || newNode.getNumChildren() == 0)
[ + + ]
404 : : {
405 : : #ifdef CVC5_ASSERTIONS
406 : : RewriteResponse r2 =
407 : 21188978 : d_theoryRewriters[newTheoryId]->postRewrite(newNode);
408 : 21188978 : Assert(r2.d_node == newNode)
409 [ - + ][ - + ]: 21188978 : << "Non-idempotent rewriting: " << r2.d_node << " != " << newNode;
[ - - ]
410 : : #endif
411 : 21188978 : rewriteStackTop.d_node = newNode;
412 : 21188978 : rewriteStackTop.d_theoryId = newTheoryId;
413 : 21188978 : rewriteStackTop.setState(RewriteStackElement::FINALIZE);
414 : 21188978 : break;
415 : 21188978 : }
416 : : // Check for trivial rewrite loops of size 1 or 2
417 [ - + ][ - + ]: 962689 : Assert(response.d_node != rewriteStackTop.d_node);
[ - - ]
418 [ - + ][ - + ]: 962689 : Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
[ - - ]
419 : : ->postRewrite(response.d_node)
420 : : .d_node
421 : : != rewriteStackTop.d_node);
422 : 962689 : rewriteStackTop.d_node = response.d_node;
423 : 962689 : rewriteStackTop.d_theoryId = newTheoryId;
424 [ + + ][ + + ]: 49227454 : }
425 : 23651038 : continue;
426 : 23651038 : }
427 : :
428 [ + - ]: 63553536 : if (state == RewriteStackElement::FINALIZE)
429 : : {
430 : : // We're done with the post rewrite, so we add to the cache.
431 [ + + ]: 63553536 : if (tcpg != nullptr)
432 : : {
433 : : // if proofs are enabled, mark that we've rewritten with proofs
434 : 2985719 : d_tpgNodes.insert(rewriteStackTop.d_original);
435 [ + + ]: 2985719 : if (!rewriteStackTop.d_postRewriteCache.isNull())
436 : : {
437 : : // We may have gotten a different node, due to non-determinism in
438 : : // theory rewriters (e.g. quantifiers rewriter which introduces
439 : : // fresh BOUND_VARIABLE). This can happen if we wrote once without
440 : : // proofs and then rewrote again with proofs.
441 [ - + ]: 2916511 : if (rewriteStackTop.d_node != rewriteStackTop.d_postRewriteCache)
442 : : {
443 [ - - ]: 0 : Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
444 : 0 : "without proofs were not equivalent"
445 : 0 : << std::endl;
446 [ - - ]: 0 : Trace("rewriter-proof")
447 : 0 : << " original: " << rewriteStackTop.d_original << std::endl;
448 [ - - ]: 0 : Trace("rewriter-proof")
449 : 0 : << "with proofs: " << rewriteStackTop.d_node << std::endl;
450 [ - - ]: 0 : Trace("rewriter-proof")
451 : 0 : << " w/o proofs: " << rewriteStackTop.d_postRewriteCache
452 : 0 : << std::endl;
453 : : Node eq = rewriteStackTop.d_node.eqNode(
454 : 0 : rewriteStackTop.d_postRewriteCache);
455 : : // we make this a post-rewrite, since we are processing a node that
456 : : // has finished post-rewriting above
457 : 0 : Node trrid = mkTrustId(d_nm, TrustId::REWRITE_NO_ELABORATE);
458 : 0 : tcpg->addRewriteStep(rewriteStackTop.d_node,
459 : 0 : rewriteStackTop.d_postRewriteCache,
460 : : ProofRule::TRUST,
461 : : {},
462 : : {trrid, eq},
463 : : false);
464 : : // don't overwrite the cache, should be the same
465 : 0 : rewriteStackTop.d_node = rewriteStackTop.d_postRewriteCache;
466 : 0 : }
467 : : }
468 : : }
469 : 63553536 : setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
470 : 63553536 : rewriteStackTop.d_original,
471 : 63553536 : rewriteStackTop.d_node);
472 : :
473 : : // If this is the last node, just return.
474 [ + + ]: 63553536 : if (rewriteStack.size() == 1)
475 : : {
476 [ + + ][ + + ]: 13464858 : Assert(!isEquality || rewriteStackTop.d_node.getKind() == Kind::EQUAL
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
477 : : || rewriteStackTop.d_node.isConst());
478 [ - + ][ - - ]: 26929716 : Assert(rewriteStackTop.d_node.getType().isComparableTo(node.getType()))
479 : 13464858 : << "Rewriting " << node << " to " << rewriteStackTop.d_node
480 : 0 : << " does not preserve type";
481 : 13464858 : return rewriteStackTop.d_node;
482 : : }
483 : :
484 : 50088678 : RewriteStackElement& parent = rewriteStack[rewriteStack.size() - 2];
485 [ + + ]: 50088678 : if (parent.getState() == RewriteStackElement::WAIT_FOR_FULL_REWRITE)
486 : : {
487 : : #ifdef CVC5_ASSERTIONS
488 : 2462060 : d_rewriteStack->erase(parent.d_fullRewriteNode);
489 : : #endif
490 : 2462060 : parent.d_node = rewriteStackTop.d_node;
491 : 2462060 : parent.d_theoryId = theoryOf(parent.d_node);
492 : 2462060 : parent.d_fullRewriteNode = Node::null();
493 : : // Resume the parent's post-rewrite fixpoint on the fully rewritten
494 : : // node. This preserves the recursive behavior where a full rewrite
495 : : // requested from post-rewrite returns to post-rewrite, and only
496 : : // finalizes once post-rewriting is done.
497 : 2462060 : parent.setState(RewriteStackElement::POST_REWRITE);
498 : : }
499 : : else
500 : : {
501 : 47626618 : parent.d_builder << rewriteStackTop.d_node;
502 : : }
503 : 50088678 : rewriteStack.pop_back();
504 : 50088678 : continue;
505 : 50088678 : }
506 : :
507 : 0 : Assert(state == RewriteStackElement::WAIT_FOR_FULL_REWRITE);
508 : 206108848 : }
509 : :
510 : : Unreachable();
511 : 91764496 : } /* Rewriter::rewriteTo() */
512 : :
513 : 51763164 : RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
514 : : TNode n,
515 : : TConvProofGenerator* tcpg)
516 : : {
517 [ + + ]: 51763164 : if (tcpg != nullptr)
518 : : {
519 : : // call the trust rewrite response interface
520 : : TrustRewriteResponse tresponse =
521 : 1837963 : d_theoryRewriters[theoryId]->preRewriteWithProof(n);
522 : : // process the trust rewrite response: store the proof step into
523 : : // tcpg if necessary and then convert to rewrite response.
524 : 1837963 : return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
525 : 1837963 : }
526 : 49925201 : return d_theoryRewriters[theoryId]->preRewrite(n);
527 : : }
528 : :
529 : 24613727 : RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
530 : : TNode n,
531 : : TConvProofGenerator* tcpg)
532 : : {
533 [ + + ]: 24613727 : if (tcpg != nullptr)
534 : : {
535 : : // same as above, for post-rewrite
536 : : TrustRewriteResponse tresponse =
537 : 1443626 : d_theoryRewriters[theoryId]->postRewriteWithProof(n);
538 : 1443626 : return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
539 : 1443626 : }
540 : 23170101 : return d_theoryRewriters[theoryId]->postRewrite(n);
541 : : }
542 : :
543 : 3281589 : RewriteResponse Rewriter::processTrustRewriteResponse(
544 : : theory::TheoryId theoryId,
545 : : const TrustRewriteResponse& tresponse,
546 : : bool isPre,
547 : : TConvProofGenerator* tcpg)
548 : : {
549 [ - + ][ - + ]: 3281589 : Assert(tcpg != nullptr);
[ - - ]
550 : 3281589 : TrustNode trn = tresponse.d_node;
551 [ - + ][ - + ]: 3281589 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
552 : 3281589 : Node proven = trn.getProven();
553 [ + + ]: 3281589 : if (proven[0] != proven[1])
554 : : {
555 : 882624 : ProofGenerator* pg = trn.getGenerator();
556 [ + - ]: 882624 : if (pg == nullptr)
557 : : {
558 : : Node tidn =
559 : 882624 : builtin::BuiltinProofRuleChecker::mkTheoryIdNode(d_nm, theoryId);
560 : : // add small step trusted rewrite
561 : : Node rid = mkMethodId(d_nm,
562 : : isPre ? MethodId::RW_REWRITE_THEORY_PRE
563 [ + + ]: 882624 : : MethodId::RW_REWRITE_THEORY_POST);
564 [ + + ][ - - ]: 3530496 : tcpg->addRewriteStep(proven[0],
565 : : proven[1],
566 : : ProofRule::TRUST_THEORY_REWRITE,
567 : : {},
568 : : {proven, tidn, rid},
569 : : isPre);
570 : 882624 : }
571 : : else
572 : : {
573 : : // store proven rewrite step
574 : 0 : tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
575 : : }
576 : : }
577 : 9844767 : return RewriteResponse(tresponse.d_status, trn.getNode());
578 : 3281589 : }
579 : :
580 : 6011933 : bool Rewriter::hasRewrittenWithProofs(TNode n) const
581 : : {
582 : 6011933 : return d_tpgNodes.find(n) != d_tpgNodes.end();
583 : : }
584 : :
585 : : } // namespace theory
586 : : } // namespace cvc5::internal
|
