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