Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Dejan Jovanovic, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * The Rewriter class.
14 : : */
15 : :
16 : : #include "theory/rewriter.h"
17 : :
18 : : #include "options/theory_options.h"
19 : : #include "proof/conv_proof_generator.h"
20 : : #include "theory/builtin/proof_checker.h"
21 : : #include "theory/evaluator.h"
22 : : #include "theory/quantifiers/extended_rewrite.h"
23 : : #include "theory/rewriter_tables.h"
24 : : #include "theory/theory.h"
25 : : #include "util/resource_manager.h"
26 : :
27 : : using namespace std;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : :
32 : : // Note that this function is a simplified version of Theory::theoryOf for
33 : : // (type-based) theoryOfMode. We expand and simplify it here for the sake of
34 : : // efficiency.
35 : 294190000 : static TheoryId theoryOf(TNode node) {
36 [ + + ]: 294190000 : if (node.getKind() == Kind::EQUAL)
37 : : {
38 : : // Equality is owned by the theory that owns the domain
39 : 48079300 : return Theory::theoryOf(node[0].getType());
40 : : }
41 : : // Regular nodes are owned by the kind
42 : 246111000 : 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 : : * Construct a fresh stack element.
53 : : */
54 : 65405500 : RewriteStackElement(TNode node, TheoryId theoryId)
55 : 65405500 : : d_node(node),
56 : : d_original(node),
57 : : d_theoryId(theoryId),
58 : : d_originalTheoryId(theoryId),
59 : : d_nextChild(0),
60 : 65405500 : d_builder(NodeManager::currentNM())
61 : : {
62 : 65405500 : }
63 : :
64 : 254565000 : TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }
65 : :
66 : 45385400 : TheoryId getOriginalTheoryId()
67 : : {
68 : 45385400 : return static_cast<TheoryId>(d_originalTheoryId);
69 : : }
70 : :
71 : : /** The node we're currently rewriting */
72 : : Node d_node;
73 : : /** Original node (either the unrewritten node or the node after prerewriting)
74 : : */
75 : : Node d_original;
76 : : /** Id of the theory that's currently rewriting this node */
77 : : unsigned d_theoryId : 8;
78 : : /** Id of the original theory that started the rewrite */
79 : : unsigned d_originalTheoryId : 8;
80 : : /** Index of the child this node is done rewriting */
81 : : unsigned d_nextChild : 32;
82 : : /** Builder for this node */
83 : : NodeBuilder d_builder;
84 : : };
85 : :
86 : :
87 : 95876800 : Node Rewriter::rewrite(TNode node) {
88 [ + + ]: 95876800 : if (node.getNumChildren() == 0)
89 : : {
90 : : // Nodes with zero children should never change via rewriting. We return
91 : : // eagerly for the sake of efficiency here.
92 : 10274000 : return node;
93 : : }
94 : 85602800 : return rewriteTo(theoryOf(node), node);
95 : : }
96 : :
97 : 557580 : Node Rewriter::extendedRewrite(TNode node, bool aggr)
98 : : {
99 : 557580 : quantifiers::ExtendedRewriter er(d_nm, *this, aggr);
100 : 1115160 : return er.extendedRewrite(node);
101 : : }
102 : :
103 : 378392 : TrustNode Rewriter::rewriteWithProof(TNode node,
104 : : bool isExtEq)
105 : : {
106 : : // must set the proof checker before calling this
107 [ - + ][ - + ]: 378392 : Assert(d_tpg != nullptr);
[ - - ]
108 [ + + ]: 378392 : if (isExtEq)
109 : : {
110 : : // theory rewriter is responsible for rewriting the equality
111 : 772 : TheoryRewriter* tr = d_theoryRewriters[theoryOf(node)];
112 [ - + ][ - + ]: 772 : Assert(tr != nullptr);
[ - - ]
113 : 772 : return tr->rewriteEqualityExtWithProof(node);
114 : : }
115 : 755240 : Node ret = rewriteTo(theoryOf(node), node, d_tpg.get());
116 [ + - ]: 377620 : return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
117 : : }
118 : :
119 : 19659 : void Rewriter::finishInit(Env& env)
120 : : {
121 : : // if not already initialized with proof support
122 [ + - ]: 19659 : if (d_tpg == nullptr)
123 : : {
124 [ + - ]: 19659 : Trace("rewriter") << "Rewriter::finishInit" << std::endl;
125 : : // the rewriter is staticly determinstic, thus use static cache policy
126 : : // for the term conversion proof generator
127 : 39318 : d_tpg.reset(new TConvProofGenerator(env,
128 : : nullptr,
129 : : TConvPolicy::FIXPOINT,
130 : : TConvCachePolicy::STATIC,
131 : 19659 : "Rewriter::TConvProofGenerator"));
132 : : }
133 : 19659 : }
134 : :
135 : 2412 : Node Rewriter::rewriteEqualityExt(TNode node)
136 : : {
137 [ - + ][ - + ]: 2412 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
138 : : // note we don't force caching of this method currently
139 : 2412 : return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
140 : : }
141 : :
142 : 705884 : void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
143 : : TheoryRewriter* trew)
144 : : {
145 [ + + ]: 705884 : if (trew == nullptr)
146 : : {
147 : : // if nullptr, use the default (null) theory rewriter.
148 : 4 : d_theoryRewriters[tid] = &d_nullTr;
149 : : }
150 : : else
151 : : {
152 : 705880 : d_theoryRewriters[tid] = trew;
153 : : }
154 : 705884 : }
155 : :
156 : 2047890 : TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
157 : : {
158 : 2047890 : return d_theoryRewriters[theoryId];
159 : : }
160 : :
161 : 13250 : Node Rewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
162 : : {
163 : : // dispatches to the appropriate theory
164 : 13250 : TheoryId tid = theoryOf(n);
165 : 13250 : TheoryRewriter* tr = getTheoryRewriter(tid);
166 [ + - ]: 13250 : if (tr != nullptr)
167 : : {
168 : 13250 : return tr->rewriteViaRule(id, n);
169 : : }
170 : 0 : return Node::null();
171 : : }
172 : :
173 : 1830610 : ProofRewriteRule Rewriter::findRule(const Node& a,
174 : : const Node& b,
175 : : TheoryRewriteCtx ctx)
176 : : {
177 : : // dispatches to the appropriate theory
178 : 1830610 : TheoryId tid = theoryOf(a);
179 : 1830610 : TheoryRewriter* tr = getTheoryRewriter(tid);
180 [ + - ]: 1830610 : if (tr != nullptr)
181 : : {
182 : 1830610 : return tr->findRule(a, b, ctx);
183 : : }
184 : 0 : return ProofRewriteRule::NONE;
185 : : }
186 : :
187 : 88543500 : Node Rewriter::rewriteTo(theory::TheoryId theoryId,
188 : : Node node,
189 : : TConvProofGenerator* tcpg)
190 : : {
191 : : #ifdef CVC5_ASSERTIONS
192 : 177087000 : bool isEquality = node.getKind() == Kind::EQUAL
193 : 109520000 : && !node[0].getType().isBoolean()
194 : 109520000 : && !node[1].getType().isBoolean();
195 : :
196 [ + + ]: 88543500 : if (d_rewriteStack == nullptr)
197 : : {
198 : 37119 : d_rewriteStack.reset(new std::unordered_set<Node>());
199 : : }
200 : : #endif
201 : :
202 [ + - ]: 88543500 : Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
203 : :
204 : : // Check if it's been cached already
205 : 177087000 : Node cached = getPostRewriteCache(theoryId, node);
206 [ + + ][ + + ]: 88543500 : if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node)))
[ + + ][ + + ]
[ + + ][ - - ]
207 : : {
208 : 72753200 : return cached;
209 : : }
210 : :
211 : : // Put the node on the stack in order to start the "recursive" rewrite
212 : 31580600 : vector<RewriteStackElement> rewriteStack;
213 : 15790300 : rewriteStack.push_back(RewriteStackElement(node, theoryId));
214 : :
215 : : // Rewrite until the stack is empty
216 : : for (;;){
217 [ + - ]: 115021000 : if (d_resourceManager != nullptr)
218 : : {
219 : 115021000 : d_resourceManager->spendResource(Resource::RewriteStep);
220 : : }
221 : :
222 : : // Get the top of the recursion stack
223 : 115021000 : RewriteStackElement& rewriteStackTop = rewriteStack.back();
224 : :
225 [ + - ]: 230041000 : Trace("rewriter") << "Rewriter::rewriting: "
226 : 115021000 : << rewriteStackTop.getTheoryId() << ","
227 : 115021000 : << rewriteStackTop.d_node << std::endl;
228 : :
229 : : // Before rewriting children we need to do a pre-rewrite of the node
230 [ + + ]: 115021000 : if (rewriteStackTop.d_nextChild == 0)
231 : : {
232 : : // Check if the pre-rewrite has already been done (it's in the cache)
233 : 130811000 : cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
234 : 130811000 : rewriteStackTop.d_node);
235 : 196216000 : if (cached.isNull()
236 [ + + ][ + + ]: 70102900 : || (tcpg != nullptr
237 [ + + ][ + + ]: 70102900 : && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
[ + + ][ - - ]
238 : : {
239 : : // Rewrite until fix-point is reached
240 : : for(;;) {
241 : : // Perform the pre-rewrite
242 : 28271200 : Kind originalKind = rewriteStackTop.d_node.getKind();
243 : : RewriteResponse response = preRewrite(
244 : 28271200 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
245 : :
246 : : // Put the rewritten node to the top of the stack
247 : 28271200 : TNode newNode = response.d_node;
248 [ + - ]: 56542500 : Trace("rewriter-debug") << "Pre-Rewrite: " << rewriteStackTop.d_node
249 : 28271200 : << " to " << newNode << std::endl;
250 : 28271200 : TheoryId newTheory = theoryOf(newNode);
251 : 28271200 : rewriteStackTop.d_node = newNode;
252 : 28271200 : rewriteStackTop.d_theoryId = newTheory;
253 [ - + ][ - - ]: 56542500 : Assert(newNode.getType().isComparableTo(
254 : : rewriteStackTop.d_node.getType()))
255 : 28271200 : << "Pre-rewriting " << rewriteStackTop.d_node << " to " << newNode
256 : 0 : << " does not preserve type";
257 : : // In the pre-rewrite, if changing theories, we just call the other
258 : : // theories pre-rewrite. If the kind of the node was changed, then we
259 : : // pre-rewrite again.
260 : 28271200 : if ((originalKind == newNode.getKind()
261 [ + + ]: 24259800 : && response.d_status == REWRITE_DONE)
262 [ + + ][ + + ]: 52531000 : || newNode.getNumChildren() == 0)
[ + + ]
263 : : {
264 [ + - ]: 23770300 : if (Configuration::isAssertionBuild())
265 : : {
266 : : // REWRITE_DONE should imply that no other pre-rewriting can be
267 : : // done.
268 : : Node rewrittenAgain =
269 : 47540600 : preRewrite(newTheory, newNode, nullptr).d_node;
270 : 47540600 : Assert(newNode == rewrittenAgain)
271 [ - + ][ - + ]: 23770300 : << "Rewriter returned REWRITE_DONE for " << newNode
[ - - ]
272 : 0 : << " but it can be rewritten to " << rewrittenAgain;
273 : : }
274 : 23770300 : break;
275 : : }
276 : 4500940 : }
277 : :
278 : : // Cache the rewrite
279 : 23770300 : setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
280 : 23770300 : rewriteStackTop.d_original,
281 : 23770300 : rewriteStackTop.d_node);
282 : : }
283 : : // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
284 : : else {
285 : : // Continue with the cached version
286 : 41635200 : rewriteStackTop.d_node = cached;
287 : 41635200 : rewriteStackTop.d_theoryId = theoryOf(cached);
288 : : }
289 : : }
290 : :
291 : 115021000 : rewriteStackTop.d_original = rewriteStackTop.d_node;
292 : : // Now it's time to rewrite the children, check if this has already been done
293 : 230041000 : cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
294 : 230041000 : rewriteStackTop.d_node);
295 : : // If not, go through the children
296 : 345062000 : if (cached.isNull()
297 [ + + ][ + + ]: 115021000 : || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
[ + + ][ + + ]
[ + + ][ - - ]
298 : : {
299 : : // The child we need to rewrite
300 : 71230200 : unsigned child = rewriteStackTop.d_nextChild++;
301 : :
302 : : // To build the rewritten expression we set up the builder
303 [ + + ]: 71230200 : if(child == 0) {
304 [ + + ]: 21615100 : if (rewriteStackTop.d_node.getNumChildren() > 0)
305 : : {
306 : : // The children will add themselves to the builder once they're done
307 : 20556200 : rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
308 : 20556200 : kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
309 [ + + ]: 20556200 : if (metaKind == kind::metakind::PARAMETERIZED) {
310 : 1258530 : rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
311 : : }
312 : : }
313 : : }
314 : :
315 : : // Process the next child
316 [ + + ]: 71230200 : if (child < rewriteStackTop.d_node.getNumChildren())
317 : : {
318 : : // The child node
319 : 99230300 : Node childNode = rewriteStackTop.d_node[child];
320 : : // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
321 : 49615200 : rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
322 : : // Go on with the rewriting
323 : 49615200 : continue;
324 : : }
325 : :
326 : : // Incorporate the children if necessary
327 [ + + ]: 21615100 : if (rewriteStackTop.d_node.getNumChildren() > 0)
328 : : {
329 : 20556200 : Node rewritten = rewriteStackTop.d_builder;
330 : 20556200 : rewriteStackTop.d_node = rewritten;
331 : 20556200 : rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
332 : : }
333 : :
334 : : // Done with all pre-rewriting, so let's do the post rewrite
335 : : for(;;) {
336 : : // Do the post-rewrite
337 : 22494200 : Kind originalKind = rewriteStackTop.d_node.getKind();
338 : : RewriteResponse response = postRewrite(
339 : 22494200 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
340 : : // We continue with the response we got
341 : 22494200 : TNode newNode = response.d_node;
342 [ + - ]: 44988400 : Trace("rewriter-debug") << "Post-Rewrite: " << rewriteStackTop.d_node
343 : 22494200 : << " to " << newNode << std::endl;
344 : 22494200 : TheoryId newTheoryId = theoryOf(newNode);
345 [ - + ][ - - ]: 44988400 : Assert(
346 : : newNode.getType().isComparableTo(rewriteStackTop.d_node.getType()))
347 : 22494200 : << "Post-rewriting " << rewriteStackTop.d_node << " to " << newNode
348 : 0 : << " does not preserve type";
349 : 22494200 : if (newTheoryId != rewriteStackTop.getTheoryId()
350 [ + + ][ + + ]: 22494200 : || response.d_status == REWRITE_AGAIN_FULL)
[ + + ]
351 : : {
352 : : // In the post rewrite if we've changed theories, we must do a full rewrite
353 [ - + ][ - + ]: 2563070 : Assert(response.d_node != rewriteStackTop.d_node);
[ - - ]
354 : : //TODO: this is not thread-safe - should make this assertion dependent on sequential build
355 : : #ifdef CVC5_ASSERTIONS
356 : 2563070 : Assert(d_rewriteStack->find(response.d_node) == d_rewriteStack->end())
357 : 0 : << "Non-terminating rewriting detected for: " << response.d_node;
358 : 2563070 : d_rewriteStack->insert(response.d_node);
359 : : #endif
360 : 5126140 : Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
361 : 2563070 : rewriteStackTop.d_node = rewritten;
362 : : #ifdef CVC5_ASSERTIONS
363 : 2563070 : d_rewriteStack->erase(response.d_node);
364 : : #endif
365 : 2563070 : break;
366 : : }
367 : 39862200 : else if ((response.d_status == REWRITE_DONE
368 [ + + ]: 19375000 : && originalKind == newNode.getKind())
369 [ + + ][ + + ]: 39306100 : || newNode.getNumChildren() == 0)
[ + + ]
370 : : {
371 : : #ifdef CVC5_ASSERTIONS
372 : : RewriteResponse r2 =
373 : 38104000 : d_theoryRewriters[newTheoryId]->postRewrite(newNode);
374 : 19052000 : Assert(r2.d_node == newNode)
375 [ - + ][ - + ]: 19052000 : << "Non-idempotent rewriting: " << r2.d_node << " != " << newNode;
[ - - ]
376 : : #endif
377 : 19052000 : rewriteStackTop.d_node = newNode;
378 : 19052000 : break;
379 : : }
380 : : // Check for trivial rewrite loops of size 1 or 2
381 [ - + ][ - + ]: 879111 : Assert(response.d_node != rewriteStackTop.d_node);
[ - - ]
382 [ - + ][ - + ]: 879111 : Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
[ - - ]
383 : : ->postRewrite(response.d_node)
384 : : .d_node
385 : : != rewriteStackTop.d_node);
386 : 879111 : rewriteStackTop.d_node = response.d_node;
387 : 879111 : }
388 : :
389 : : // We're done with the post rewrite, so we add to the cache
390 [ + + ]: 21615100 : if (tcpg != nullptr)
391 : : {
392 : : // if proofs are enabled, mark that we've rewritten with proofs
393 : 1913430 : d_tpgNodes.insert(rewriteStackTop.d_original);
394 [ + + ]: 1913430 : if (!cached.isNull())
395 : : {
396 : : // We may have gotten a different node, due to non-determinism in
397 : : // theory rewriters (e.g. quantifiers rewriter which introduces
398 : : // fresh BOUND_VARIABLE). This can happen if we wrote once without
399 : : // proofs and then rewrote again with proofs.
400 [ - + ]: 1838110 : if (rewriteStackTop.d_node != cached)
401 : : {
402 [ - - ]: 0 : Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
403 : 0 : "without proofs were not equivalent"
404 : 0 : << std::endl;
405 [ - - ]: 0 : Trace("rewriter-proof")
406 : 0 : << " original: " << rewriteStackTop.d_original << std::endl;
407 [ - - ]: 0 : Trace("rewriter-proof")
408 : 0 : << "with proofs: " << rewriteStackTop.d_node << std::endl;
409 [ - - ]: 0 : Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
410 : 0 : Node eq = rewriteStackTop.d_node.eqNode(cached);
411 : : // we make this a post-rewrite, since we are processing a node that
412 : : // has finished post-rewriting above
413 : 0 : Node trrid = mkTrustId(d_nm, TrustId::REWRITE_NO_ELABORATE);
414 : 0 : tcpg->addRewriteStep(rewriteStackTop.d_node,
415 : : cached,
416 : : ProofRule::TRUST,
417 : : {},
418 : : {trrid, eq},
419 : 0 : false);
420 : : // don't overwrite the cache, should be the same
421 : 0 : rewriteStackTop.d_node = cached;
422 : : }
423 : : }
424 : : }
425 : 21615100 : setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
426 : 21615100 : rewriteStackTop.d_original,
427 : 21615100 : rewriteStackTop.d_node);
428 : : }
429 : : else
430 : : {
431 : : // We were already in cache, so just remember it
432 : 43790400 : rewriteStackTop.d_node = cached;
433 : 43790400 : rewriteStackTop.d_theoryId = theoryOf(cached);
434 : : }
435 : :
436 : : // If this is the last node, just return
437 [ + + ]: 65405500 : if (rewriteStack.size() == 1) {
438 [ + + ][ + + ]: 15790300 : Assert(!isEquality || rewriteStackTop.d_node.getKind() == Kind::EQUAL
[ - + ][ - + ]
[ - - ]
439 : : || rewriteStackTop.d_node.isConst());
440 [ - + ][ - - ]: 31580600 : Assert(rewriteStackTop.d_node.getType().isComparableTo(node.getType()))
441 : 15790300 : << "Rewriting " << node << " to " << rewriteStackTop.d_node
442 : 0 : << " does not preserve type";
443 : 15790300 : return rewriteStackTop.d_node;
444 : : }
445 : :
446 : : // We're done with this node, append it to the parent
447 : 49615200 : rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node;
448 : 49615200 : rewriteStack.pop_back();
449 : 99230300 : }
450 : :
451 : : Unreachable();
452 : : } /* Rewriter::rewriteTo() */
453 : :
454 : 52041500 : RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
455 : : TNode n,
456 : : TConvProofGenerator* tcpg)
457 : : {
458 [ + + ]: 52041500 : if (tcpg != nullptr)
459 : : {
460 : : // call the trust rewrite response interface
461 : : TrustRewriteResponse tresponse =
462 : 5280980 : d_theoryRewriters[theoryId]->preRewriteWithProof(n);
463 : : // process the trust rewrite response: store the proof step into
464 : : // tcpg if necessary and then convert to rewrite response.
465 : 2640490 : return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
466 : : }
467 : 49401000 : return d_theoryRewriters[theoryId]->preRewrite(n);
468 : : }
469 : :
470 : 22494200 : RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
471 : : TNode n,
472 : : TConvProofGenerator* tcpg)
473 : : {
474 [ + + ]: 22494200 : if (tcpg != nullptr)
475 : : {
476 : : // same as above, for post-rewrite
477 : : TrustRewriteResponse tresponse =
478 : 4005220 : d_theoryRewriters[theoryId]->postRewriteWithProof(n);
479 : 2002610 : return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
480 : : }
481 : 20491600 : return d_theoryRewriters[theoryId]->postRewrite(n);
482 : : }
483 : :
484 : 4643100 : RewriteResponse Rewriter::processTrustRewriteResponse(
485 : : theory::TheoryId theoryId,
486 : : const TrustRewriteResponse& tresponse,
487 : : bool isPre,
488 : : TConvProofGenerator* tcpg)
489 : : {
490 [ - + ][ - + ]: 4643100 : Assert(tcpg != nullptr);
[ - - ]
491 : 9286200 : TrustNode trn = tresponse.d_node;
492 [ - + ][ - + ]: 4643100 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
493 : 4643100 : Node proven = trn.getProven();
494 [ + + ]: 4643100 : if (proven[0] != proven[1])
495 : : {
496 : 1231800 : ProofGenerator* pg = trn.getGenerator();
497 [ + - ]: 1231800 : if (pg == nullptr)
498 : : {
499 : : Node tidn =
500 : 2463610 : builtin::BuiltinProofRuleChecker::mkTheoryIdNode(d_nm, theoryId);
501 : : // add small step trusted rewrite
502 : : Node rid = mkMethodId(d_nm,
503 : : isPre ? MethodId::RW_REWRITE_THEORY_PRE
504 [ + + ]: 1231800 : : MethodId::RW_REWRITE_THEORY_POST);
505 [ + + ][ - - ]: 4927210 : tcpg->addRewriteStep(proven[0],
506 : : proven[1],
507 : : ProofRule::TRUST_THEORY_REWRITE,
508 : : {},
509 : : {proven, tidn, rid},
510 : 3695410 : isPre);
511 : : }
512 : : else
513 : : {
514 : : // store proven rewrite step
515 : 0 : tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
516 : : }
517 : : }
518 : 13929300 : return RewriteResponse(tresponse.d_status, trn.getNode());
519 : : }
520 : :
521 : 13700100 : bool Rewriter::hasRewrittenWithProofs(TNode n) const
522 : : {
523 : 13700100 : return d_tpgNodes.find(n) != d_tpgNodes.end();
524 : : }
525 : :
526 : : } // namespace theory
527 : : } // namespace cvc5::internal
|
