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 theory preprocessor.
11 : : */
12 : :
13 : : #include "theory/theory_preprocessor.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "expr/term_context_stack.h"
17 : : #include "proof/lazy_proof.h"
18 : : #include "smt/logic_exception.h"
19 : : #include "theory/logic_info.h"
20 : : #include "theory/rewriter.h"
21 : : #include "theory/theory_engine.h"
22 : :
23 : : using namespace std;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : :
28 : 50950 : TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine)
29 : : : EnvObj(env),
30 : 50950 : d_engine(engine),
31 : 50950 : d_cache(userContext()),
32 : 50950 : d_tfr(env),
33 : 50950 : d_tpg(nullptr),
34 : 50950 : d_tpgRew(nullptr),
35 : 50950 : d_tspg(nullptr),
36 : 101900 : d_lp(nullptr)
37 : : {
38 : : // proofs are enabled in the theory preprocessor regardless of the proof mode
39 : 50950 : ProofNodeManager* pnm = env.getProofNodeManager();
40 [ + + ]: 50950 : if (pnm != nullptr)
41 : : {
42 : 19375 : context::Context* u = userContext();
43 : 38750 : d_tpg.reset(
44 : : new TConvProofGenerator(env,
45 : : u,
46 : : TConvPolicy::FIXPOINT,
47 : : TConvCachePolicy::NEVER,
48 : : "TheoryPreprocessor::preprocess_rewrite",
49 : 19375 : &d_rtfc));
50 : 38750 : d_tpgRew.reset(new TConvProofGenerator(env,
51 : : u,
52 : : TConvPolicy::ONCE,
53 : : TConvCachePolicy::NEVER,
54 : 19375 : "TheoryPreprocessor::pprew"));
55 : 38750 : d_lp.reset(
56 : 19375 : new LazyCDProof(env, nullptr, u, "TheoryPreprocessor::LazyCDProof"));
57 : : // Make the main term conversion sequence generator, which tracks up to
58 : : // three conversions made in succession:
59 : : // (1) rewriting
60 : : // (2) (theory preprocessing+rewriting until fixed point)+term formula
61 : : // removal+rewriting.
62 : 19375 : std::vector<ProofGenerator*> ts;
63 [ + - ]: 19375 : ts.push_back(d_tpgRew.get());
64 [ + - ]: 19375 : ts.push_back(d_tpg.get());
65 : 38750 : d_tspg.reset(new TConvSeqProofGenerator(
66 : 38750 : pnm, ts, userContext(), "TheoryPreprocessor::sequence"));
67 : 19375 : }
68 : 50950 : }
69 : :
70 : 50605 : TheoryPreprocessor::~TheoryPreprocessor() {}
71 : :
72 : 895507 : TrustNode TheoryPreprocessor::preprocess(TNode node,
73 : : std::vector<SkolemLemma>& newLemmas)
74 : : {
75 : 895507 : return preprocessInternal(node, newLemmas, true);
76 : : }
77 : :
78 : 1857165 : TrustNode TheoryPreprocessor::preprocessInternal(
79 : : TNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
80 : : {
81 : : // In this method, all rewriting steps of node are stored in d_tpg.
82 : :
83 [ + - ]: 1857165 : Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;
84 : :
85 : : // We must rewrite before preprocessing, because some terms when rewritten
86 : : // may introduce new terms that are not top-level and require preprocessing.
87 : : // An example of this is (forall ((x Int)) (and (tail L) (P x))) which
88 : : // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L)
89 : : // must be preprocessed as a child here.
90 : 1857165 : Node irNode = rewriteWithProof(node, d_tpgRew.get(), true, 0);
91 : :
92 : : // run theory preprocessing
93 : 1857176 : TrustNode tpp = theoryPreprocess(irNode, newLemmas);
94 : 1857154 : Node ppNode = tpp.getNode();
95 : :
96 [ - + ]: 1857154 : if (TraceIsOn("tpp-debug"))
97 : : {
98 [ - - ]: 0 : if (node != irNode)
99 : : {
100 [ - - ]: 0 : Trace("tpp-debug") << "after initial rewriting : " << irNode << std::endl;
101 : : }
102 [ - - ]: 0 : if (irNode != ppNode)
103 : : {
104 [ - - ]: 0 : Trace("tpp-debug")
105 : 0 : << "after preprocessing + rewriting and term formula removal : "
106 : 0 : << ppNode << std::endl;
107 : : }
108 [ - - ]: 0 : Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
109 : : }
110 : :
111 [ + + ]: 1857154 : if (procLemmas)
112 : : {
113 : : // Also must preprocess the new lemmas. This is especially important for
114 : : // formulas containing witness terms whose bodies are not in preprocessed
115 : : // form, as term formula removal introduces new lemmas for these that
116 : : // require theory-preprocessing.
117 : 1796166 : size_t i = 0;
118 [ + + ]: 1857154 : while (i < newLemmas.size())
119 : : {
120 : 60988 : TrustNode cur = newLemmas[i].d_lemma;
121 : 60988 : newLemmas[i].d_lemma = preprocessLemmaInternal(cur, newLemmas, false);
122 [ + - ][ - + ]: 60988 : Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
[ - - ]
123 : 60988 : i++;
124 : 60988 : }
125 : : }
126 : :
127 [ + + ]: 1857154 : if (node == ppNode)
128 : : {
129 [ + - ]: 2888354 : Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
130 : 1444177 : << std::endl;
131 : : // no change
132 : 1444177 : return TrustNode::null();
133 : : }
134 : :
135 : : // Now, sequence the conversion steps if proofs are enabled.
136 : 412977 : TrustNode tret;
137 [ + + ]: 412977 : if (isProofEnabled())
138 : : {
139 : 247497 : std::vector<Node> cterms;
140 : 247497 : cterms.push_back(node);
141 : 247497 : cterms.push_back(irNode);
142 : 247497 : cterms.push_back(ppNode);
143 : : // We have that:
144 : : // node -> irNode via rewriting
145 : : // irNode -> ppNode via theory-preprocessing + rewriting + tf removal
146 : 247497 : tret = d_tspg->mkTrustRewriteSequence(cterms);
147 : 247497 : tret.debugCheckClosed(
148 : : options(), "tpp-debug", "TheoryPreprocessor::lemma_ret");
149 : 247497 : }
150 : : else
151 : : {
152 : 165480 : tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr);
153 : : }
154 : :
155 [ + - ]: 825954 : Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
156 [ - + ][ - - ]: 412977 : << tret.getNode() << std::endl;
157 [ + - ][ - - ]: 825954 : Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
158 : 0 : << ", procLemmas=" << procLemmas
159 [ - + ]: 412977 : << ", # lemmas = " << newLemmas.size() << std::endl;
160 : 412977 : return tret;
161 : 1857165 : }
162 : :
163 : 900670 : TrustNode TheoryPreprocessor::preprocessLemma(
164 : : TrustNode node, std::vector<SkolemLemma>& newLemmas)
165 : : {
166 : 900670 : return preprocessLemmaInternal(node, newLemmas, true);
167 : : }
168 : :
169 : 961658 : TrustNode TheoryPreprocessor::preprocessLemmaInternal(
170 : : TrustNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
171 : : {
172 : : // what was originally proven
173 : 961658 : Node lemma = node.getProven();
174 : 961659 : TrustNode tplemma = preprocessInternal(lemma, newLemmas, procLemmas);
175 [ + + ]: 961657 : if (tplemma.isNull())
176 : : {
177 : : // no change needed
178 : 665582 : return node;
179 : : }
180 [ - + ][ - + ]: 296075 : Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
[ - - ]
181 : : // what it was preprocessed to
182 : 296075 : Node lemmap = tplemma.getNode();
183 [ - + ][ - + ]: 296075 : Assert(lemmap != node.getProven());
[ - - ]
184 : : // process the preprocessing
185 [ + + ]: 296075 : if (isProofEnabled())
186 : : {
187 [ - + ][ - + ]: 160447 : Assert(d_lp != nullptr);
[ - - ]
188 : : // add the original proof to the lazy proof
189 : 160447 : d_lp->addLazyStep(node.getProven(),
190 : : node.getGenerator(),
191 : : TrustId::THEORY_PREPROCESS_LEMMA);
192 : : // only need to do anything if lemmap changed in a non-trivial way
193 [ + + ]: 160447 : if (!CDProof::isSame(lemmap, lemma))
194 : : {
195 : 151496 : d_lp->addLazyStep(tplemma.getProven(),
196 : : tplemma.getGenerator(),
197 : : TrustId::THEORY_PREPROCESS,
198 : : true,
199 : : "TheoryEngine::lemma_pp");
200 : : // ---------- from node -------------- from theory preprocess
201 : : // lemma lemma = lemmap
202 : : // ------------------------------------------ EQ_RESOLVE
203 : : // lemmap
204 : 151496 : std::vector<Node> pfChildren;
205 : 151496 : pfChildren.push_back(lemma);
206 : 151496 : pfChildren.push_back(tplemma.getProven());
207 : 151496 : d_lp->addStep(lemmap, ProofRule::EQ_RESOLVE, pfChildren, {});
208 : 151496 : }
209 : : }
210 [ + + ]: 296075 : return TrustNode::mkTrustLemma(lemmap, d_lp.get());
211 : 961658 : }
212 : :
213 : 1309 : RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
214 : : {
215 : 1309 : return d_tfr;
216 : : }
217 : :
218 : 1857165 : TrustNode TheoryPreprocessor::theoryPreprocess(
219 : : TNode assertion, std::vector<SkolemLemma>& newLemmas)
220 : : {
221 : : // Map from (term, term context identifier) to the term that it was
222 : : // theory-preprocessed to. This is used when the result of the current node
223 : : // should be set to the final result of converting its theory-preprocessed
224 : : // form.
225 : : std::unordered_map<std::pair<Node, uint32_t>,
226 : : Node,
227 : : PairHashFunction<Node, uint32_t, std::hash<Node>>>
228 : 1857165 : wasPreprocessed;
229 : : std::unordered_map<
230 : : std::pair<Node, uint32_t>,
231 : : Node,
232 : 1857165 : PairHashFunction<Node, uint32_t, std::hash<Node>>>::iterator itw;
233 : 1857165 : NodeManager* nm = nodeManager();
234 : 1857165 : TCtxStack ctx(&d_rtfc);
235 : 1857165 : std::vector<bool> processedChildren;
236 : 1857165 : ctx.pushInitial(assertion);
237 : 1857165 : processedChildren.push_back(false);
238 : 1857165 : std::pair<Node, uint32_t> initial = ctx.getCurrent();
239 : 1857165 : std::pair<Node, uint32_t> curr;
240 : 1857165 : Node node;
241 : : uint32_t nodeVal;
242 : 1857165 : TppCache::const_iterator itc;
243 [ + + ]: 20922335 : while (!ctx.empty())
244 : : {
245 : 19065181 : curr = ctx.getCurrent();
246 : 19065181 : itc = d_cache.find(curr);
247 : 19065181 : node = curr.first;
248 : 19065181 : nodeVal = curr.second;
249 [ + - ]: 19065181 : Trace("tpp-debug") << "Visit " << node << ", " << nodeVal << std::endl;
250 [ + + ]: 19065181 : if (itc != d_cache.end())
251 : : {
252 [ + - ]: 8769765 : Trace("tpp-debug") << "...already computed" << std::endl;
253 : 8769765 : ctx.pop();
254 : 8769765 : processedChildren.pop_back();
255 : : // already computed
256 : 13694941 : continue;
257 : : }
258 : : // if we have yet to process children
259 [ + + ]: 10295416 : if (!processedChildren.back())
260 : : {
261 : : // check if we should replace the current node by a Skolem
262 : 5476446 : TrustNode newLem;
263 : : bool inQuant, inTerm;
264 : 5476446 : RtfTermContext::getFlags(nodeVal, inQuant, inTerm);
265 [ - + ][ - + ]: 5476446 : Assert(!inQuant);
[ - - ]
266 : 5476448 : TrustNode currTrn = d_tfr.runCurrent(node, inTerm, newLem);
267 : : // if we replaced by a skolem, we do not recurse
268 [ + + ]: 5476444 : if (!currTrn.isNull())
269 : : {
270 : 52516 : Node ret = currTrn.getNode();
271 : : // if this is the first time we've seen this term, we have a new lemma
272 : : // which we add to our vectors
273 [ + + ]: 52516 : if (!newLem.isNull())
274 : : {
275 : 46505 : newLemmas.push_back(theory::SkolemLemma(newLem, ret));
276 : : }
277 : : // register the rewrite into the proof generator
278 [ + + ]: 52516 : if (isProofEnabled())
279 : : {
280 : 33024 : registerTrustedRewrite(currTrn, d_tpg.get(), true, nodeVal);
281 : : }
282 [ + - ]: 52516 : Trace("tpp-debug") << "...replace by skolem" << std::endl;
283 : 52516 : d_cache.insert(curr, ret);
284 : 52516 : continue;
285 : 52516 : }
286 : 5423928 : size_t nchild = node.getNumChildren();
287 [ + + ]: 5423928 : if (nchild > 0)
288 : : {
289 [ + + ]: 4825258 : if (node.isClosure())
290 : : {
291 : : // currently, we never do any term formula removal in quantifier
292 : : // bodies
293 : : }
294 : : else
295 : : {
296 [ + - ]: 4765324 : Trace("tpp-debug") << "...recurse to children" << std::endl;
297 : : // recurse if we have children
298 : 4765324 : processedChildren[processedChildren.size() - 1] = true;
299 [ + + ]: 17048203 : for (size_t i = 0; i < nchild; i++)
300 : : {
301 : 12282879 : ctx.pushChild(node, nodeVal, i);
302 : 12282879 : processedChildren.push_back(false);
303 : : }
304 : 4765324 : continue;
305 : 4765324 : }
306 : : }
307 : : else
308 : : {
309 [ + - ]: 598670 : Trace("tpp-debug") << "...base case" << std::endl;
310 : : }
311 [ + + ][ + + ]: 10294286 : }
312 [ + - ]: 5477574 : Trace("tpp-debug") << "...reconstruct" << std::endl;
313 : : // otherwise, we are now finished processing children, pop the current node
314 : : // and compute the result
315 : 5477574 : ctx.pop();
316 : 5477574 : processedChildren.pop_back();
317 : : // if this was preprocessed previously, we set our result to the final
318 : : // form of the preprocessed form of this.
319 : 5477574 : itw = wasPreprocessed.find(curr);
320 [ + + ]: 5477574 : if (itw != wasPreprocessed.end())
321 : : {
322 : : // we preprocessed it to something else, carry that
323 : 53668 : std::pair<Node, uint32_t> key(itw->second, nodeVal);
324 : 53668 : itc = d_cache.find(key);
325 [ - + ][ - + ]: 53668 : Assert(itc != d_cache.end());
[ - - ]
326 : 53668 : d_cache.insert(curr, itc->second);
327 : 53668 : wasPreprocessed.erase(curr);
328 : 53668 : continue;
329 : 53668 : }
330 : 5423906 : Node ret = node;
331 : 5423906 : Node pret = node;
332 [ + + ][ + + ]: 5423906 : if (!node.isClosure() && node.getNumChildren() > 0)
[ + + ]
333 : : {
334 : : // if we have not already computed the result
335 : 4765302 : std::vector<Node> newChildren;
336 : 4765302 : bool childChanged = false;
337 [ + + ]: 4765302 : if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
338 : : {
339 : 468913 : newChildren.push_back(node.getOperator());
340 : : }
341 : : // reconstruct from the children
342 : 4765302 : std::pair<Node, uint32_t> currChild;
343 [ + + ]: 17048137 : for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
344 : : {
345 : : // recompute the value of the child
346 : 12282835 : uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
347 : 12282835 : currChild = std::pair<Node, uint32_t>(node[i], val);
348 : 12282835 : itc = d_cache.find(currChild);
349 [ - + ][ - + ]: 12282835 : Assert(itc != d_cache.end());
[ - - ]
350 : 12282835 : Node newChild = (*itc).second;
351 [ - + ][ - + ]: 12282835 : Assert(!newChild.isNull());
[ - - ]
352 : 12282835 : childChanged |= (newChild != node[i]);
353 : 12282835 : newChildren.push_back(newChild);
354 : 12282835 : }
355 : : // If changes, we reconstruct the node
356 [ + + ]: 4765302 : if (childChanged)
357 : : {
358 : 323492 : ret = nm->mkNode(node.getKind(), newChildren);
359 : : }
360 : : // Finish the conversion by rewriting. Notice that we must consider this a
361 : : // pre-rewrite since we do not recursively register the rewriting steps
362 : : // of subterms of rtfNode. For example, if this step rewrites
363 : : // (not A) ---> B, then if registered a pre-rewrite, it will apply when
364 : : // reconstructing proofs via d_tpg. However, if it is a post-rewrite
365 : : // it will fail to apply if another call to this class registers A -> C,
366 : : // in which case (not C) will be returned instead of B (see issue 6754).
367 : 4765302 : pret = rewriteWithProof(ret, d_tpg.get(), false, nodeVal);
368 : 4765302 : }
369 : : // if we did not rewrite above, we are ready to theory preprocess
370 [ + + ]: 5423906 : if (pret == ret)
371 : : {
372 : 5392432 : pret = preprocessWithProof(ret, newLemmas, nodeVal);
373 : : }
374 : : // if we changed due to rewriting or preprocessing, we traverse again
375 [ + + ]: 5423897 : if (pret != ret)
376 : : {
377 : : // must restart
378 : 53668 : ctx.push(node, nodeVal);
379 : 53668 : processedChildren.push_back(true);
380 : 53668 : ctx.push(pret, nodeVal);
381 : 53668 : processedChildren.push_back(false);
382 : 53668 : wasPreprocessed[curr] = pret;
383 : 53668 : continue;
384 : : }
385 : : // cache
386 : 5370229 : d_cache.insert(curr, ret);
387 [ + + ][ + + ]: 5477583 : }
388 : 1857154 : itc = d_cache.find(initial);
389 [ - + ][ - + ]: 1857154 : Assert(itc != d_cache.end());
[ - - ]
390 [ + + ]: 3714308 : return TrustNode::mkTrustRewrite(assertion, (*itc).second, d_tpg.get());
391 : 1857220 : }
392 : :
393 : 6644652 : Node TheoryPreprocessor::rewriteWithProof(Node term,
394 : : TConvProofGenerator* pg,
395 : : bool isPre,
396 : : uint32_t tctx)
397 : : {
398 : 6644652 : Node termr = rewrite(term);
399 : : // store rewrite step if tracking proofs and it rewrites
400 [ + + ]: 6644652 : if (isProofEnabled())
401 : : {
402 : : // may rewrite the same term more than once, thus check hasRewriteStep
403 [ + + ]: 4061571 : if (termr != term)
404 : : {
405 [ + - ]: 460468 : Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
406 : 230234 : << term << " -> " << termr << std::endl;
407 : 460468 : pg->addRewriteStep(
408 : : term, termr, ProofRule::MACRO_REWRITE, {}, {term}, isPre, tctx);
409 : : }
410 : : }
411 : 6644652 : return termr;
412 : 0 : }
413 : :
414 : 5392423 : Node TheoryPreprocessor::preprocessWithProof(Node term,
415 : : std::vector<SkolemLemma>& lems,
416 : : uint32_t tctx)
417 : : {
418 : : // Important that it is in rewritten form, to ensure that the rewrite steps
419 : : // recorded in d_tpg are functional. In other words, there should not
420 : : // be steps from the same term to multiple rewritten forms, which would be
421 : : // the case if we registered a preprocessing step for a non-rewritten term.
422 [ - + ][ - + ]: 5392423 : Assert(term == rewrite(term));
[ - - ]
423 [ + - ]: 10784846 : Trace("tpp-debug2") << "preprocessWithProof " << term
424 : 5392423 : << ", #lems = " << lems.size() << std::endl;
425 : : // We never call ppRewrite on equalities here, since equalities have a
426 : : // special status. In particular, notice that theory preprocessing can be
427 : : // called on all formulas asserted to theory engine, including those generated
428 : : // as new literals appearing in lemmas. Calling ppRewrite on equalities is
429 : : // incompatible with theory combination where a split on equality requested
430 : : // by a theory could be preprocessed to something else, thus making theory
431 : : // combination either non-terminating or result in solution soundness.
432 : : // Notice that an alternative solution is to ensure that certain lemmas
433 : : // (e.g. splits from theory combination) can never have theory preprocessing
434 : : // applied to them. However, it is more uniform to say that theory
435 : : // preprocessing is applied to all formulas. This makes it so that e.g.
436 : : // theory solvers do not need to specify whether they want their lemmas to
437 : : // be theory-preprocessed or not.
438 [ + + ]: 5392423 : if (term.getKind() == Kind::EQUAL)
439 : : {
440 : 753987 : return term;
441 : : }
442 : : // call ppRewrite for the given theory
443 : 4638436 : std::vector<SkolemLemma> newLems;
444 : 4638445 : TrustNode trn = d_engine.ppRewrite(term, newLems);
445 [ + - ]: 9276854 : Trace("tpp-debug2") << "preprocessWithProof returned " << trn
446 : 4638427 : << ", #lems = " << newLems.size() << std::endl;
447 : 4638427 : lems.insert(lems.end(), newLems.begin(), newLems.end());
448 [ + + ]: 4638427 : if (trn.isNull())
449 : : {
450 : : // no change, return
451 : 4616242 : return term;
452 : : }
453 : 22185 : Node termr = trn.getNode();
454 [ - + ][ - + ]: 22185 : Assert(term != termr);
[ - - ]
455 [ + + ]: 22185 : if (isProofEnabled())
456 : : {
457 : 9174 : registerTrustedRewrite(trn, d_tpg.get(), false, tctx);
458 : : }
459 : : // Rewrite again here, which notice is a *pre* rewrite.
460 : 22185 : return rewriteWithProof(termr, d_tpg.get(), true, tctx);
461 : 4638436 : }
462 : :
463 : 7470603 : bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
464 : :
465 : 42198 : void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
466 : : TConvProofGenerator* pg,
467 : : bool isPre,
468 : : uint32_t tctx)
469 : : {
470 [ + - ][ - + ]: 42198 : if (!isProofEnabled() || trn.isNull())
[ - + ]
471 : : {
472 : 0 : return;
473 : : }
474 [ - + ][ - + ]: 42198 : Assert(trn.getKind() == TrustNodeKind::REWRITE);
[ - - ]
475 : 42198 : Node eq = trn.getProven();
476 : 42198 : Node term = eq[0];
477 : 42198 : Node termr = eq[1];
478 [ + - ]: 84396 : Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
479 : 42198 : << term << " -> " << termr << std::endl;
480 [ + + ]: 42198 : if (trn.getGenerator() != nullptr)
481 : : {
482 : 37255 : trn.debugCheckClosed(
483 : : options(), "tpp-debug", "TheoryPreprocessor::preprocessWithProof");
484 : : }
485 : : // always use term context hash 0 (default)
486 : 42198 : pg->addRewriteStep(term,
487 : : termr,
488 : : trn.getGenerator(),
489 : : isPre,
490 : : TrustId::THEORY_PREPROCESS,
491 : : true,
492 : : tctx);
493 : 42198 : }
494 : :
495 : : } // namespace theory
496 : : } // namespace cvc5::internal
|
