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