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 : 298968000 : static TheoryId theoryOf(TNode node) {
36 [ + + ]: 298968000 : if (node.getKind() == Kind::EQUAL)
37 : : {
38 : : // Equality is owned by the theory that owns the domain
39 : 48626900 : return Theory::theoryOf(node[0].getType());
40 : : }
41 : : // Regular nodes are owned by the kind
42 : 250341000 : 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 : 66726300 : RewriteStackElement(TNode node, TheoryId theoryId)
55 : 66726300 : : d_node(node),
56 : : d_original(node),
57 : : d_theoryId(theoryId),
58 : : d_originalTheoryId(theoryId),
59 : 66726300 : d_nextChild(0)
60 : : {
61 : 66726300 : }
62 : :
63 : 258131000 : TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }
64 : :
65 : 45763100 : TheoryId getOriginalTheoryId()
66 : : {
67 : 45763100 : return static_cast<TheoryId>(d_originalTheoryId);
68 : : }
69 : :
70 : : /** The node we're currently rewriting */
71 : : Node d_node;
72 : : /** Original node (either the unrewritten node or the node after prerewriting)
73 : : */
74 : : Node d_original;
75 : : /** Id of the theory that's currently rewriting this node */
76 : : unsigned d_theoryId : 8;
77 : : /** Id of the original theory that started the rewrite */
78 : : unsigned d_originalTheoryId : 8;
79 : : /** Index of the child this node is done rewriting */
80 : : unsigned d_nextChild : 32;
81 : : /** Builder for this node */
82 : : NodeBuilder d_builder;
83 : : };
84 : :
85 : :
86 : 96914200 : Node Rewriter::rewrite(TNode node) {
87 [ + + ]: 96914200 : if (node.getNumChildren() == 0)
88 : : {
89 : : // Nodes with zero children should never change via rewriting. We return
90 : : // eagerly for the sake of efficiency here.
91 : 9881040 : return node;
92 : : }
93 : 87033200 : return rewriteTo(theoryOf(node), node);
94 : : }
95 : :
96 : 585946 : Node Rewriter::extendedRewrite(TNode node, bool aggr)
97 : : {
98 : 585946 : quantifiers::ExtendedRewriter er(d_nm, *this, aggr);
99 : 1171890 : return er.extendedRewrite(node);
100 : : }
101 : :
102 : 347031 : TrustNode Rewriter::rewriteWithProof(TNode node,
103 : : bool isExtEq)
104 : : {
105 : : // must set the proof checker before calling this
106 [ - + ][ - + ]: 347031 : Assert(d_tpg != nullptr);
[ - - ]
107 [ + + ]: 347031 : if (isExtEq)
108 : : {
109 : : // theory rewriter is responsible for rewriting the equality
110 : 711 : TheoryRewriter* tr = d_theoryRewriters[theoryOf(node)];
111 [ - + ][ - + ]: 711 : Assert(tr != nullptr);
[ - - ]
112 : 711 : return tr->rewriteEqualityExtWithProof(node);
113 : : }
114 : 692640 : Node ret = rewriteTo(theoryOf(node), node, d_tpg.get());
115 [ + - ]: 346320 : return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
116 : : }
117 : :
118 : 18627 : void Rewriter::finishInit(Env& env)
119 : : {
120 : : // if not already initialized with proof support
121 [ + - ]: 18627 : if (d_tpg == nullptr)
122 : : {
123 [ + - ]: 18627 : Trace("rewriter") << "Rewriter::finishInit" << std::endl;
124 : : // the rewriter is staticly determinstic, thus use static cache policy
125 : : // for the term conversion proof generator
126 : 37254 : d_tpg.reset(new TConvProofGenerator(env,
127 : : nullptr,
128 : : TConvPolicy::FIXPOINT,
129 : : TConvCachePolicy::STATIC,
130 : 18627 : "Rewriter::TConvProofGenerator"));
131 : : }
132 : 18627 : }
133 : :
134 : 3557 : Node Rewriter::rewriteEqualityExt(TNode node)
135 : : {
136 [ - + ][ - + ]: 3557 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
137 : : // note we don't force caching of this method currently
138 : 3557 : return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
139 : : }
140 : :
141 : 689826 : void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
142 : : TheoryRewriter* trew)
143 : : {
144 : 689826 : d_theoryRewriters[tid] = trew;
145 : 689826 : }
146 : :
147 : 2152410 : TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
148 : : {
149 : 2152410 : return d_theoryRewriters[theoryId];
150 : : }
151 : :
152 : 8788 : Node Rewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
153 : : {
154 : : // dispatches to the appropriate theory
155 : 8788 : TheoryId tid = theoryOf(n);
156 : 8788 : TheoryRewriter* tr = getTheoryRewriter(tid);
157 [ + - ]: 8788 : if (tr != nullptr)
158 : : {
159 : 8788 : return tr->rewriteViaRule(id, n);
160 : : }
161 : 0 : return Node::null();
162 : : }
163 : :
164 : 1940860 : ProofRewriteRule Rewriter::findRule(const Node& a,
165 : : const Node& b,
166 : : TheoryRewriteCtx ctx)
167 : : {
168 : : // dispatches to the appropriate theory
169 : 1940860 : TheoryId tid = theoryOf(a);
170 : 1940860 : TheoryRewriter* tr = getTheoryRewriter(tid);
171 [ + - ]: 1940860 : if (tr != nullptr)
172 : : {
173 : 1940860 : return tr->findRule(a, b, ctx);
174 : : }
175 : 0 : return ProofRewriteRule::NONE;
176 : : }
177 : :
178 : 90235400 : Node Rewriter::rewriteTo(theory::TheoryId theoryId,
179 : : Node node,
180 : : TConvProofGenerator* tcpg)
181 : : {
182 : : #ifdef CVC5_ASSERTIONS
183 : 180471000 : bool isEquality = node.getKind() == Kind::EQUAL
184 : 110665000 : && !node[0].getType().isBoolean()
185 : 110665000 : && !node[1].getType().isBoolean();
186 : :
187 [ + + ]: 90235400 : if (d_rewriteStack == nullptr)
188 : : {
189 : 35617 : d_rewriteStack.reset(new std::unordered_set<Node>());
190 : : }
191 : : #endif
192 : :
193 [ + - ]: 90235400 : Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
194 : :
195 : : // Check if it's been cached already
196 : 180471000 : Node cached = getPostRewriteCache(theoryId, node);
197 [ + + ][ + + ]: 90235400 : if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node)))
[ + + ][ + + ]
[ + + ][ - - ]
198 : : {
199 : 73779400 : return cached;
200 : : }
201 : :
202 : : // Put the node on the stack in order to start the "recursive" rewrite
203 : 32912000 : vector<RewriteStackElement> rewriteStack;
204 : 16456000 : rewriteStack.push_back(RewriteStackElement(node, theoryId));
205 : :
206 : : // Rewrite until the stack is empty
207 : : for (;;){
208 [ + - ]: 116997000 : if (d_resourceManager != nullptr)
209 : : {
210 : 116997000 : d_resourceManager->spendResource(Resource::RewriteStep);
211 : : }
212 : :
213 : : // Get the top of the recursion stack
214 : 116997000 : RewriteStackElement& rewriteStackTop = rewriteStack.back();
215 : :
216 [ + - ]: 233993000 : Trace("rewriter") << "Rewriter::rewriting: "
217 : 116997000 : << rewriteStackTop.getTheoryId() << ","
218 : 116997000 : << rewriteStackTop.d_node << std::endl;
219 : :
220 : : // Before rewriting children we need to do a pre-rewrite of the node
221 [ + + ]: 116997000 : if (rewriteStackTop.d_nextChild == 0)
222 : : {
223 : : // Check if the pre-rewrite has already been done (it's in the cache)
224 : 133453000 : cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
225 : 133453000 : rewriteStackTop.d_node);
226 : 200179000 : if (cached.isNull()
227 [ + + ][ + + ]: 71058900 : || (tcpg != nullptr
228 [ + + ][ + + ]: 71058900 : && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
[ + + ][ - - ]
229 : : {
230 : : // Rewrite until fix-point is reached
231 : : for(;;) {
232 : : // Perform the pre-rewrite
233 : 28155200 : Kind originalKind = rewriteStackTop.d_node.getKind();
234 : : RewriteResponse response = preRewrite(
235 : 28155200 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
236 : :
237 : : // Put the rewritten node to the top of the stack
238 : 28155200 : TNode newNode = response.d_node;
239 [ + - ]: 56310400 : Trace("rewriter-debug") << "Pre-Rewrite: " << rewriteStackTop.d_node
240 : 28155200 : << " to " << newNode << std::endl;
241 : 28155200 : TheoryId newTheory = theoryOf(newNode);
242 : 28155200 : rewriteStackTop.d_node = newNode;
243 : 28155200 : rewriteStackTop.d_theoryId = newTheory;
244 [ - + ][ - - ]: 56310400 : Assert(newNode.getType().isComparableTo(
245 : : rewriteStackTop.d_node.getType()))
246 : 28155200 : << "Pre-rewriting " << rewriteStackTop.d_node << " to " << newNode
247 : 0 : << " does not preserve type";
248 : : // In the pre-rewrite, if changing theories, we just call the other
249 : : // theories pre-rewrite. If the kind of the node was changed, then we
250 : : // pre-rewrite again.
251 : 28155200 : if ((originalKind == newNode.getKind()
252 [ + + ]: 24426900 : && response.d_status == REWRITE_DONE)
253 [ + + ][ + + ]: 52582100 : || newNode.getNumChildren() == 0)
[ + + ]
254 : : {
255 [ + - ]: 23911900 : if (Configuration::isAssertionBuild())
256 : : {
257 : : // REWRITE_DONE should imply that no other pre-rewriting can be
258 : : // done.
259 : : Node rewrittenAgain =
260 : 47823800 : preRewrite(newTheory, newNode, nullptr).d_node;
261 : 47823800 : Assert(newNode == rewrittenAgain)
262 [ - + ][ - + ]: 23911900 : << "Rewriter returned REWRITE_DONE for " << newNode
[ - - ]
263 : 0 : << " but it can be rewritten to " << rewrittenAgain;
264 : : }
265 : 23911900 : break;
266 : : }
267 : 4243300 : }
268 : :
269 : : // Cache the rewrite
270 : 23911900 : setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
271 : 23911900 : rewriteStackTop.d_original,
272 : 23911900 : rewriteStackTop.d_node);
273 : : }
274 : : // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
275 : : else {
276 : : // Continue with the cached version
277 : 42814400 : rewriteStackTop.d_node = cached;
278 : 42814400 : rewriteStackTop.d_theoryId = theoryOf(cached);
279 : : }
280 : : }
281 : :
282 : 116997000 : rewriteStackTop.d_original = rewriteStackTop.d_node;
283 : : // Now it's time to rewrite the children, check if this has already been done
284 : 233993000 : cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
285 : 233993000 : rewriteStackTop.d_node);
286 : : // If not, go through the children
287 : 350990000 : if (cached.isNull()
288 [ + + ][ + + ]: 116997000 : || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
[ + + ][ + + ]
[ + + ][ - - ]
289 : : {
290 : : // The child we need to rewrite
291 : 72121500 : unsigned child = rewriteStackTop.d_nextChild++;
292 : :
293 : : // To build the rewritten expression we set up the builder
294 [ + + ]: 72121500 : if(child == 0) {
295 [ + + ]: 21851200 : if (rewriteStackTop.d_node.getNumChildren() > 0)
296 : : {
297 : : // The children will add themselves to the builder once they're done
298 : 20818100 : rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
299 : 20818100 : kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
300 [ + + ]: 20818100 : if (metaKind == kind::metakind::PARAMETERIZED) {
301 : 1243920 : rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
302 : : }
303 : : }
304 : : }
305 : :
306 : : // Process the next child
307 [ + + ]: 72121500 : if (child < rewriteStackTop.d_node.getNumChildren())
308 : : {
309 : : // The child node
310 : 100541000 : Node childNode = rewriteStackTop.d_node[child];
311 : : // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
312 : 50270300 : rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
313 : : // Go on with the rewriting
314 : 50270300 : continue;
315 : : }
316 : :
317 : : // Incorporate the children if necessary
318 [ + + ]: 21851200 : if (rewriteStackTop.d_node.getNumChildren() > 0)
319 : : {
320 : 20818100 : Node rewritten = rewriteStackTop.d_builder;
321 : 20818100 : rewriteStackTop.d_node = rewritten;
322 : 20818100 : rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
323 : : }
324 : :
325 : : // Done with all pre-rewriting, so let's do the post rewrite
326 : : for(;;) {
327 : : // Do the post-rewrite
328 : 22701200 : Kind originalKind = rewriteStackTop.d_node.getKind();
329 : : RewriteResponse response = postRewrite(
330 : 22701200 : rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
331 : : // We continue with the response we got
332 : 22701200 : TNode newNode = response.d_node;
333 [ + - ]: 45402500 : Trace("rewriter-debug") << "Post-Rewrite: " << rewriteStackTop.d_node
334 : 22701200 : << " to " << newNode << std::endl;
335 : 22701200 : TheoryId newTheoryId = theoryOf(newNode);
336 [ - + ][ - - ]: 45402500 : Assert(
337 : : newNode.getType().isComparableTo(rewriteStackTop.d_node.getType()))
338 : 22701200 : << "Post-rewriting " << rewriteStackTop.d_node << " to " << newNode
339 : 0 : << " does not preserve type";
340 : 22701200 : if (newTheoryId != rewriteStackTop.getTheoryId()
341 [ + + ][ + + ]: 22701200 : || response.d_status == REWRITE_AGAIN_FULL)
[ + + ]
342 : : {
343 : : // In the post rewrite if we've changed theories, we must do a full rewrite
344 [ - + ][ - + ]: 2855880 : Assert(response.d_node != rewriteStackTop.d_node);
[ - - ]
345 : : //TODO: this is not thread-safe - should make this assertion dependent on sequential build
346 : : #ifdef CVC5_ASSERTIONS
347 : 2855880 : Assert(d_rewriteStack->find(response.d_node) == d_rewriteStack->end())
348 : 0 : << "Non-terminating rewriting detected for: " << response.d_node;
349 : 2855880 : d_rewriteStack->insert(response.d_node);
350 : : #endif
351 : 5711750 : Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
352 : 2855880 : rewriteStackTop.d_node = rewritten;
353 : : #ifdef CVC5_ASSERTIONS
354 : 2855880 : d_rewriteStack->erase(response.d_node);
355 : : #endif
356 : 2855880 : break;
357 : : }
358 : 39690700 : else if ((response.d_status == REWRITE_DONE
359 [ + + ]: 19326700 : && originalKind == newNode.getKind())
360 [ + + ][ + + ]: 39172000 : || newNode.getNumChildren() == 0)
[ + + ]
361 : : {
362 : : #ifdef CVC5_ASSERTIONS
363 : : RewriteResponse r2 =
364 : 37990600 : d_theoryRewriters[newTheoryId]->postRewrite(newNode);
365 : 18995300 : Assert(r2.d_node == newNode)
366 [ - + ][ - + ]: 18995300 : << "Non-idempotent rewriting: " << r2.d_node << " != " << newNode;
[ - - ]
367 : : #endif
368 : 18995300 : rewriteStackTop.d_node = newNode;
369 : 18995300 : break;
370 : : }
371 : : // Check for trivial rewrite loops of size 1 or 2
372 [ - + ][ - + ]: 850093 : Assert(response.d_node != rewriteStackTop.d_node);
[ - - ]
373 [ - + ][ - + ]: 850093 : Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
[ - - ]
374 : : ->postRewrite(response.d_node)
375 : : .d_node
376 : : != rewriteStackTop.d_node);
377 : 850093 : rewriteStackTop.d_node = response.d_node;
378 : 850093 : }
379 : :
380 : : // We're done with the post rewrite, so we add to the cache
381 [ + + ]: 21851200 : if (tcpg != nullptr)
382 : : {
383 : : // if proofs are enabled, mark that we've rewritten with proofs
384 : 1768490 : d_tpgNodes.insert(rewriteStackTop.d_original);
385 [ + + ]: 1768490 : if (!cached.isNull())
386 : : {
387 : : // We may have gotten a different node, due to non-determinism in
388 : : // theory rewriters (e.g. quantifiers rewriter which introduces
389 : : // fresh BOUND_VARIABLE). This can happen if we wrote once without
390 : : // proofs and then rewrote again with proofs.
391 [ - + ]: 1701360 : if (rewriteStackTop.d_node != cached)
392 : : {
393 [ - - ]: 0 : Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
394 : 0 : "without proofs were not equivalent"
395 : 0 : << std::endl;
396 [ - - ]: 0 : Trace("rewriter-proof")
397 : 0 : << " original: " << rewriteStackTop.d_original << std::endl;
398 [ - - ]: 0 : Trace("rewriter-proof")
399 : 0 : << "with proofs: " << rewriteStackTop.d_node << std::endl;
400 [ - - ]: 0 : Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
401 : 0 : Node eq = rewriteStackTop.d_node.eqNode(cached);
402 : : // we make this a post-rewrite, since we are processing a node that
403 : : // has finished post-rewriting above
404 : 0 : Node trrid = mkTrustId(TrustId::REWRITE_NO_ELABORATE);
405 : 0 : tcpg->addRewriteStep(rewriteStackTop.d_node,
406 : : cached,
407 : : ProofRule::TRUST,
408 : : {},
409 : : {trrid, eq},
410 : 0 : false);
411 : : // don't overwrite the cache, should be the same
412 : 0 : rewriteStackTop.d_node = cached;
413 : : }
414 : : }
415 : : }
416 : 21851200 : setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
417 : 21851200 : rewriteStackTop.d_original,
418 : 21851200 : rewriteStackTop.d_node);
419 : : }
420 : : else
421 : : {
422 : : // We were already in cache, so just remember it
423 : 44875200 : rewriteStackTop.d_node = cached;
424 : 44875200 : rewriteStackTop.d_theoryId = theoryOf(cached);
425 : : }
426 : :
427 : : // If this is the last node, just return
428 [ + + ]: 66726300 : if (rewriteStack.size() == 1) {
429 [ + + ][ + + ]: 16456000 : Assert(!isEquality || rewriteStackTop.d_node.getKind() == Kind::EQUAL
[ - + ][ - + ]
[ - - ]
430 : : || rewriteStackTop.d_node.isConst());
431 [ - + ][ - - ]: 32912000 : Assert(rewriteStackTop.d_node.getType().isComparableTo(node.getType()))
432 : 16456000 : << "Rewriting " << node << " to " << rewriteStackTop.d_node
433 : 0 : << " does not preserve type";
434 : 16456000 : return rewriteStackTop.d_node;
435 : : }
436 : :
437 : : // We're done with this node, append it to the parent
438 : 50270300 : rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node;
439 : 50270300 : rewriteStack.pop_back();
440 : 100541000 : }
441 : :
442 : : Unreachable();
443 : : } /* Rewriter::rewriteTo() */
444 : :
445 : 52067100 : RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
446 : : TNode n,
447 : : TConvProofGenerator* tcpg)
448 : : {
449 [ + + ]: 52067100 : if (tcpg != nullptr)
450 : : {
451 : : // call the trust rewrite response interface
452 : : TrustRewriteResponse tresponse =
453 : 4880000 : d_theoryRewriters[theoryId]->preRewriteWithProof(n);
454 : : // process the trust rewrite response: store the proof step into
455 : : // tcpg if necessary and then convert to rewrite response.
456 : 2440000 : return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
457 : : }
458 : 49627100 : return d_theoryRewriters[theoryId]->preRewrite(n);
459 : : }
460 : :
461 : 22701200 : RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
462 : : TNode n,
463 : : TConvProofGenerator* tcpg)
464 : : {
465 [ + + ]: 22701200 : if (tcpg != nullptr)
466 : : {
467 : : // same as above, for post-rewrite
468 : : TrustRewriteResponse tresponse =
469 : 3686860 : d_theoryRewriters[theoryId]->postRewriteWithProof(n);
470 : 1843430 : return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
471 : : }
472 : 20857800 : return d_theoryRewriters[theoryId]->postRewrite(n);
473 : : }
474 : :
475 : 4283430 : RewriteResponse Rewriter::processTrustRewriteResponse(
476 : : theory::TheoryId theoryId,
477 : : const TrustRewriteResponse& tresponse,
478 : : bool isPre,
479 : : TConvProofGenerator* tcpg)
480 : : {
481 [ - + ][ - + ]: 4283430 : Assert(tcpg != nullptr);
[ - - ]
482 : 8566860 : TrustNode trn = tresponse.d_node;
483 [ - + ][ - + ]: 4283430 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
484 : 4283430 : Node proven = trn.getProven();
485 [ + + ]: 4283430 : if (proven[0] != proven[1])
486 : : {
487 : 1117980 : ProofGenerator* pg = trn.getGenerator();
488 [ + - ]: 1117980 : if (pg == nullptr)
489 : : {
490 : 2235950 : Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
491 : : // add small step trusted rewrite
492 : : Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
493 [ + + ]: 1117980 : : MethodId::RW_REWRITE_THEORY_POST);
494 [ + + ][ - - ]: 4471910 : tcpg->addRewriteStep(proven[0],
495 : : proven[1],
496 : : ProofRule::TRUST_THEORY_REWRITE,
497 : : {},
498 : : {proven, tidn, rid},
499 : 3353930 : isPre);
500 : : }
501 : : else
502 : : {
503 : : // store proven rewrite step
504 : 0 : tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
505 : : }
506 : : }
507 : 12850300 : return RewriteResponse(tresponse.d_status, trn.getNode());
508 : : }
509 : :
510 : 12633400 : bool Rewriter::hasRewrittenWithProofs(TNode n) const
511 : : {
512 : 12633400 : return d_tpgNodes.find(n) != d_tpgNodes.end();
513 : : }
514 : :
515 : : } // namespace theory
516 : : } // namespace cvc5::internal
|
