Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Andrew Reynolds, Gereon Kremer
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 : : * Non-clausal simplification preprocessing pass.
14 : : *
15 : : * Run the nonclausal solver and try to solve all assigned theory literals.
16 : : */
17 : :
18 : : #include "preprocessing/passes/non_clausal_simp.h"
19 : :
20 : : #include <vector>
21 : :
22 : : #include "context/cdo.h"
23 : : #include "options/smt_options.h"
24 : : #include "preprocessing/assertion_pipeline.h"
25 : : #include "preprocessing/preprocessing_pass_context.h"
26 : : #include "smt/preprocess_proof_generator.h"
27 : : #include "theory/booleans/circuit_propagator.h"
28 : : #include "theory/theory.h"
29 : : #include "theory/theory_engine.h"
30 : : #include "theory/theory_model.h"
31 : : #include "theory/trust_substitutions.h"
32 : :
33 : : using namespace cvc5::internal;
34 : : using namespace cvc5::internal::theory;
35 : :
36 : : namespace cvc5::internal {
37 : : namespace preprocessing {
38 : : namespace passes {
39 : :
40 : : /* -------------------------------------------------------------------------- */
41 : :
42 : 48144 : NonClausalSimp::Statistics::Statistics(StatisticsRegistry& reg)
43 : : : d_numConstantProps(reg.registerInt(
44 : 48144 : "preprocessing::passes::NonClausalSimp::NumConstantProps"))
45 : : {
46 : 48144 : }
47 : :
48 : :
49 : : /* -------------------------------------------------------------------------- */
50 : :
51 : 48144 : NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
52 : : : PreprocessingPass(preprocContext, "non-clausal-simp"),
53 : : d_statistics(statisticsRegistry()),
54 : 96288 : d_llpg(options().smt.produceProofs ? new smt::PreprocessProofGenerator(
55 : 34482 : d_env, userContext(), "NonClausalSimp::llpg")
56 : : : nullptr),
57 : 82626 : d_tsubsList(userContext())
58 : : {
59 : 48144 : }
60 : :
61 : 39223 : PreprocessingPassResult NonClausalSimp::applyInternal(
62 : : AssertionPipeline* assertionsToPreprocess)
63 : : {
64 : 39223 : d_preprocContext->spendResource(Resource::PreprocessStep);
65 : :
66 [ - + ]: 39223 : if (TraceIsOn("non-clausal-simplify"))
67 : : {
68 [ - - ]: 0 : for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
69 : : {
70 [ - - ]: 0 : Trace("non-clausal-simplify")
71 : 0 : << "Assertion #" << i << " : " << (*assertionsToPreprocess)[i]
72 : 0 : << std::endl;
73 : : }
74 : : }
75 : :
76 : : theory::booleans::CircuitPropagator* propagator =
77 : 39223 : d_preprocContext->getCircuitPropagator();
78 : 39223 : propagator->initialize();
79 : :
80 : : // Assert all the assertions to the propagator
81 [ + - ]: 39223 : Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
82 [ + + ]: 482380 : for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
83 : : {
84 : 443157 : Assert(rewrite((*assertionsToPreprocess)[i])
85 : 0 : == (*assertionsToPreprocess)[i]) << (*assertionsToPreprocess)[i];
86 : : // Don't reprocess substitutions
87 [ + + ]: 443157 : if (assertionsToPreprocess->isSubstsIndex(i))
88 : : {
89 : 30 : continue;
90 : : }
91 [ + - ]: 886254 : Trace("non-clausal-simplify")
92 : 443127 : << "asserting " << (*assertionsToPreprocess)[i] << std::endl;
93 [ + - ]: 886254 : Trace("cores") << "propagator->assertTrue: " << (*assertionsToPreprocess)[i]
94 : 443127 : << std::endl;
95 : 443127 : propagator->assertTrue((*assertionsToPreprocess)[i]);
96 : : }
97 : :
98 [ + - ]: 39223 : Trace("non-clausal-simplify") << "propagating" << std::endl;
99 : 78446 : TrustNode conf = propagator->propagate();
100 [ + + ]: 39223 : if (!conf.isNull())
101 : : {
102 : : // If in conflict, just return false
103 [ + - ]: 4932 : Trace("non-clausal-simplify")
104 : 2466 : << "conflict in non-clausal propagation" << std::endl;
105 : 2466 : assertionsToPreprocess->pushBackTrusted(conf);
106 : 2466 : return PreprocessingPassResult::CONFLICT;
107 : : }
108 : :
109 [ + - ]: 73514 : Trace("non-clausal-simplify")
110 : 36757 : << "Iterate through " << propagator->getLearnedLiterals().size()
111 : 36757 : << " learned literals." << std::endl;
112 : : // No conflict, go through the literals and solve them
113 : 36757 : NodeManager* nm = nodeManager();
114 : 36757 : context::Context* u = userContext();
115 : 36757 : Rewriter* rw = d_env.getRewriter();
116 : 36757 : TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
117 : 36757 : CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get();
118 : : // constant propagations
119 : : std::shared_ptr<TrustSubstitutionMap> constantPropagations =
120 : : std::make_shared<TrustSubstitutionMap>(
121 : 73514 : d_env, u, "NonClausalSimp::cprop", TrustId::PREPROCESS_LEMMA);
122 : 36757 : SubstitutionMap& cps = constantPropagations->get();
123 : : // new substitutions
124 : : std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
125 : : std::make_shared<TrustSubstitutionMap>(
126 : 73514 : d_env, u, "NonClausalSimp::newSubs", TrustId::PREPROCESS_LEMMA);
127 : 36757 : SubstitutionMap& nss = newSubstitutions->get();
128 : :
129 : 36757 : size_t j = 0;
130 : 36757 : std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals();
131 : : // if proofs are enabled, we will need to track the proofs of learned literals
132 [ + + ]: 36757 : if (isProofEnabled())
133 : : {
134 : 15307 : d_tsubsList.push_back(constantPropagations);
135 : 15307 : d_tsubsList.push_back(newSubstitutions);
136 [ + + ]: 194514 : for (const TrustNode& tll : learned_literals)
137 : : {
138 : 179207 : d_llpg->notifyNewTrustedAssert(tll);
139 : : }
140 : : }
141 [ + + ]: 301606 : for (size_t i = 0, size = learned_literals.size(); i < size; ++i)
142 : : {
143 : : // Simplify the literal we learned wrt previous substitutions
144 : 265778 : Node learnedLiteral = learned_literals[i].getNode();
145 [ + - ]: 531554 : Trace("non-clausal-simplify")
146 : 265777 : << "Process learnedLiteral : " << learnedLiteral;
147 [ - + ][ - + ]: 265777 : Assert(rewrite(learnedLiteral) == learnedLiteral);
[ - - ]
148 : 531554 : Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral)
149 [ - + ][ - - ]: 265777 : << learnedLiteral << " after subs is "
150 : 265777 : << top_level_substs.apply(learnedLiteral);
151 : : // process the learned literal with substitutions and const propagations
152 : 531554 : learnedLiteral = processLearnedLit(
153 : 265777 : learnedLiteral, newSubstitutions.get(), constantPropagations.get());
154 [ + - ]: 531554 : Trace("non-clausal-simplify")
155 : 0 : << "Process learnedLiteral, after constProp : " << learnedLiteral
156 : 265777 : << std::endl;
157 : : // It might just simplify to a constant
158 [ + + ]: 265777 : if (learnedLiteral.isConst())
159 : : {
160 [ + + ]: 2069 : if (learnedLiteral.getConst<bool>())
161 : : {
162 : : // If the learned literal simplifies to true, it's redundant
163 : 1142 : continue;
164 : : }
165 : : else
166 : : {
167 : : // If the learned literal simplifies to false, we're in conflict
168 [ + - ]: 1854 : Trace("non-clausal-simplify")
169 [ - + ][ - - ]: 927 : << "conflict with " << learned_literals[i].getNode() << std::endl;
170 : 927 : Node n = nm->mkConst<bool>(false);
171 [ + + ]: 927 : assertionsToPreprocess->push_back(n, false, d_llpg.get());
172 : 927 : return PreprocessingPassResult::CONFLICT;
173 : : }
174 : : }
175 : :
176 : : // Solve it with the corresponding theory, possibly adding new
177 : : // substitutions to newSubstitutions
178 [ + - ]: 263708 : Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
179 : :
180 : : TrustNode tlearnedLiteral =
181 [ + + ]: 263709 : TrustNode::mkTrustLemma(learnedLiteral, d_llpg.get());
182 : : Theory::PPAssertStatus solveStatus =
183 : 527417 : d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
184 : 263708 : *newSubstitutions.get());
185 : :
186 [ + - ][ + ]: 263707 : switch (solveStatus)
187 : : {
188 : 53934 : case Theory::PP_ASSERT_STATUS_SOLVED:
189 : : {
190 : : // The literal should rewrite to true
191 [ + - ]: 107868 : Trace("non-clausal-simplify")
192 : 53934 : << "solved " << learnedLiteral << std::endl;
193 [ - + ][ - + ]: 53934 : Assert(rewrite(nss.apply(learnedLiteral)).isConst());
[ - - ]
194 : : // else fall through
195 : 263707 : break;
196 : : }
197 : 0 : case Theory::PP_ASSERT_STATUS_CONFLICT:
198 : : {
199 : : // If in conflict, we return false
200 [ - - ]: 0 : Trace("non-clausal-simplify")
201 : 0 : << "conflict while solving " << learnedLiteral << std::endl;
202 : 0 : Node n = nm->mkConst<bool>(false);
203 : 0 : assertionsToPreprocess->push_back(n);
204 : 0 : return PreprocessingPassResult::CONFLICT;
205 : : }
206 : 209773 : default:
207 : 419546 : TNode t;
208 : 419546 : TNode c;
209 : 629319 : if (learnedLiteral.getKind() == Kind::EQUAL
210 : 209773 : && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst()))
211 : : {
212 : : // constant propagation
213 [ + + ]: 15354 : if (learnedLiteral[0].isConst())
214 : : {
215 : 1587 : t = learnedLiteral[1];
216 : 1587 : c = learnedLiteral[0];
217 : : }
218 : : else
219 : : {
220 : 13767 : t = learnedLiteral[0];
221 : 13767 : c = learnedLiteral[1];
222 : : }
223 : : }
224 [ - + ]: 194419 : else if (options().smt.simplificationBoolConstProp)
225 : : {
226 : : // From non-equalities, learn the Boolean equality. Notice that
227 : : // the equality case above is strictly more powerful that this, since
228 : : // e.g. (= t c) * { t -> c } also simplifies to true.
229 : 0 : bool pol = learnedLiteral.getKind() != Kind::NOT;
230 : 0 : c = nm->mkConst(pol);
231 [ - - ]: 0 : t = pol ? learnedLiteral : learnedLiteral[0];
232 : : }
233 [ + + ]: 209773 : if (!t.isNull())
234 : : {
235 [ - + ][ - + ]: 15354 : Assert(!t.isConst());
[ - - ]
236 [ - + ][ - + ]: 15354 : Assert(rewrite(cps.apply(t)) == t);
[ - - ]
237 [ - + ][ - + ]: 15354 : Assert(top_level_substs.apply(t) == t);
[ - - ]
238 [ - + ][ - + ]: 15354 : Assert(nss.apply(t) == t);
[ - - ]
239 : : // also add to learned literal
240 : 15354 : ProofGenerator* cpg = constantPropagations->addSubstitutionSolved(
241 : : t, c, tlearnedLiteral);
242 : : // We need to justify (= t c) as a literal, since it is reasserted
243 : : // to the assertion pipeline below. We do this with the proof
244 : : // generator returned by the above call.
245 [ + + ]: 15354 : if (isProofEnabled())
246 : : {
247 : 9679 : d_llpg->notifyNewAssert(t.eqNode(c), cpg);
248 : : }
249 : : }
250 : : else
251 : : {
252 : : // Keep the learned literal
253 : 194419 : learned_literals[j++] = learned_literals[i];
254 : : }
255 : : // Its a literal that could not be processed as a substitution or
256 : : // conflict. In this case, we notify the context of the learned
257 : : // literal, which will process it with the learned literal manager.
258 : 209773 : d_preprocContext->notifyLearnedLiteral(learnedLiteral);
259 : 209773 : break;
260 : : }
261 : : }
262 : :
263 : : #ifdef CVC5_ASSERTIONS
264 : : // NOTE: When debugging this code, consider moving this check inside of the
265 : : // loop over propagator->getLearnedLiterals(). This check has been moved
266 : : // outside because it is costly for certain inputs (see bug 508).
267 : : //
268 : : // Check data structure invariants:
269 : : // 1. for each lhs of top_level_substs, does not appear anywhere in rhs of
270 : : // top_level_substs or anywhere in constantPropagations
271 : : // 2. each lhs of constantPropagations rewrites to itself
272 : : // 3. if l -> r is a constant propagation and l is a subterm of l' with l' ->
273 : : // r' another constant propagation, then l'[l/r] -> r' should be a
274 : : // constant propagation too
275 : : // 4. each lhs of constantPropagations is different from each rhs
276 [ + + ]: 87658 : for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
277 : : {
278 [ - + ][ - + ]: 51829 : Assert((*pos).first.isVar());
[ - - ]
279 [ - + ][ - + ]: 51829 : Assert(top_level_substs.apply((*pos).first) == (*pos).first);
[ - - ]
280 [ - + ][ - + ]: 51829 : Assert(top_level_substs.apply((*pos).second) == (*pos).second);
[ - - ]
281 : 51829 : Node app = nss.apply((*pos).second);
282 [ - + ][ - + ]: 51829 : Assert(nss.apply(app) == app);
[ - - ]
283 : : }
284 [ + + ]: 51138 : for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
285 : : {
286 [ - + ][ - + ]: 15309 : Assert((*pos).second.isConst());
[ - - ]
287 [ - + ][ - + ]: 15309 : Assert(rewrite((*pos).first) == (*pos).first);
[ - - ]
288 [ - + ][ - + ]: 15309 : Assert(cps.apply((*pos).second) == (*pos).second);
[ - - ]
289 : : }
290 : : #endif /* CVC5_ASSERTIONS */
291 : :
292 : : // Resize the learnt
293 [ + - ]: 71658 : Trace("non-clausal-simplify")
294 : 35829 : << "Resize non-clausal learned literals to " << j << std::endl;
295 : 35829 : learned_literals.resize(j);
296 : :
297 : 71658 : std::unordered_set<TNode> s;
298 [ + + ]: 452945 : for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
299 : : {
300 : 417391 : Node assertion = (*assertionsToPreprocess)[i];
301 [ + - ]: 417391 : Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
302 : 417391 : TrustNode assertionNew = newSubstitutions->applyTrusted(assertion, rw);
303 [ + + ]: 417391 : if (!assertionNew.isNull())
304 : : {
305 [ + - ]: 239142 : Trace("non-clausal-simplify")
306 [ - + ][ - - ]: 119571 : << "assertionNew = " << assertionNew.getNode() << std::endl;
307 : 119571 : assertionsToPreprocess->replaceTrusted(i, assertionNew);
308 : 119571 : assertion = assertionNew.getNode();
309 [ - + ][ - + ]: 119571 : Assert(rewrite(assertion) == assertion);
[ - - ]
310 : : }
311 : : for (;;)
312 : : {
313 : 422768 : assertionNew = constantPropagations->applyTrusted(assertion, rw);
314 [ + + ]: 422768 : if (assertionNew.isNull())
315 : : {
316 : 417391 : break;
317 : : }
318 [ - + ][ - + ]: 5377 : Assert(assertionNew.getNode() != assertion);
[ - - ]
319 : 5377 : assertionsToPreprocess->replaceTrusted(i, assertionNew);
320 : 5377 : assertion = assertionNew.getNode();
321 : 5377 : d_statistics.d_numConstantProps += 1;
322 [ + - ]: 10754 : Trace("non-clausal-simplify")
323 : 5377 : << "assertionNew = " << assertion << std::endl;
324 : : }
325 : 417391 : s.insert(assertion);
326 [ + - ]: 834782 : Trace("non-clausal-simplify")
327 : 417391 : << "non-clausal preprocessed: " << assertion << std::endl;
328 [ + + ]: 417391 : if (assertionsToPreprocess->isInConflict())
329 : : {
330 : 275 : return PreprocessingPassResult::CONFLICT;
331 : : }
332 : : }
333 : :
334 : : // If necessary, add as assertions if needed (when incremental). This is
335 : : // necessary because certain variables cannot truly be eliminated when
336 : : // we are in incremental mode. For example, say our first call to check-sat
337 : : // is a formula F containing variable x. On the second call to check-sat,
338 : : // say we solve a top-level assertion (= x t). Since the solver already has
339 : : // constraints involving x, we must still keep (= x t) as an assertion.
340 : : // However, notice that we do not retract the substitution { x -> t }. This
341 : : // means that all *subsequent* assertions after (= x t) will replace x by t.
342 [ + + ]: 35554 : if (assertionsToPreprocess->storeSubstsInAsserts())
343 : : {
344 [ + + ]: 7562 : for (const std::pair<const Node, const Node>& pos: nss)
345 : : {
346 : 7398 : Node lhs = pos.first;
347 : : // If using incremental, we must check whether this variable has occurred
348 : : // before now. If it has, we must add as an assertion.
349 [ + + ]: 3699 : if (d_preprocContext->getSymsInAssertions().contains(lhs))
350 : : {
351 : : // if it has, the substitution becomes an assertion
352 : 2306 : TrustNode trhs = newSubstitutions->applyTrusted(lhs, rw);
353 [ - + ][ - + ]: 2306 : Assert(!trhs.isNull());
[ - - ]
354 [ + - ]: 4612 : Trace("non-clausal-simplify")
355 : 0 : << "substitute: will notify SAT layer of substitution: "
356 [ - + ][ - - ]: 2306 : << trhs.getProven() << std::endl;
357 : : // note that trhs.getProven() may not be in rewritten form (e.g. the
358 : : // rewriter may swap order). This is handled internally within
359 : : // addSubstitutionNode.
360 : 2306 : assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
361 : : trhs.getGenerator());
362 : : }
363 : : }
364 : : }
365 : :
366 : : // Learned literals to conjoin. If proofs are enabled, all these are
367 : : // justified by d_llpg.
368 : 35554 : std::vector<Node> learnedLitsToConjoin;
369 : :
370 [ + + ]: 226565 : for (size_t i = 0; i < learned_literals.size(); ++i)
371 : : {
372 : 191011 : Node learned = learned_literals[i].getNode();
373 [ - + ][ - + ]: 191011 : Assert(top_level_substs.apply(learned) == learned);
[ - - ]
374 : : // process learned literal
375 : 382022 : learned = processLearnedLit(
376 : 191011 : learned, newSubstitutions.get(), constantPropagations.get());
377 [ + + ]: 191011 : if (s.find(learned) != s.end())
378 : : {
379 : 109633 : continue;
380 : : }
381 : 81378 : s.insert(learned);
382 : 81378 : learnedLitsToConjoin.push_back(learned);
383 [ + - ]: 162756 : Trace("non-clausal-simplify")
384 : 81378 : << "non-clausal learned : " << learned << std::endl;
385 : : }
386 : 35554 : learned_literals.clear();
387 : :
388 [ + + ]: 50785 : for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
389 : : {
390 : 15231 : Node cProp = (*pos).first.eqNode((*pos).second);
391 [ - + ][ - + ]: 15231 : Assert(top_level_substs.apply(cProp) == cProp);
[ - - ]
392 : : // process learned literal (substitutions only)
393 : 15231 : cProp = processLearnedLit(cProp, newSubstitutions.get(), nullptr);
394 [ + + ]: 15231 : if (s.find(cProp) != s.end())
395 : : {
396 : 9554 : continue;
397 : : }
398 : 5677 : s.insert(cProp);
399 : 5677 : learnedLitsToConjoin.push_back(cProp);
400 [ + - ]: 11354 : Trace("non-clausal-simplify")
401 : 5677 : << "non-clausal constant propagation : " << cProp << std::endl;
402 : : }
403 : :
404 : : // Add new substitutions to topLevelSubstitutions
405 : : // Note that we don't have to keep rhs's in full solved form
406 : : // because SubstitutionMap::apply does a fixed-point iteration when
407 : : // substituting
408 : 35554 : d_preprocContext->addSubstitutions(*newSubstitutions.get());
409 : :
410 [ + + ]: 35554 : if (!learnedLitsToConjoin.empty())
411 : : {
412 [ + - ]: 9566 : Trace("non-clausal-simplify")
413 : 0 : << "non-clausal simplification, reassert: " << learnedLitsToConjoin
414 : 4783 : << std::endl;
415 [ + + ]: 91838 : for (const Node& lit : learnedLitsToConjoin)
416 : : {
417 [ + + ]: 87055 : assertionsToPreprocess->push_back(lit, false, d_llpg.get());
418 : : }
419 : : }
420 : :
421 : : // Note that typically ttls.apply(assert)==assert here.
422 : : // However, this invariant is invalidated for cases where we use explicit
423 : : // equality assertions for variables solved in incremental mode that already
424 : : // exist in assertions, as described above.
425 : :
426 : 35554 : return PreprocessingPassResult::NO_CONFLICT;
427 : : }
428 : :
429 : 170807 : bool NonClausalSimp::isProofEnabled() const
430 : : {
431 : 170807 : return options().smt.produceProofs;
432 : : }
433 : :
434 : 472019 : Node NonClausalSimp::processLearnedLit(Node lit,
435 : : theory::TrustSubstitutionMap* subs,
436 : : theory::TrustSubstitutionMap* cp)
437 : : {
438 : 472019 : Rewriter* rw = d_env.getRewriter();
439 : 944038 : TrustNode tlit;
440 [ + - ]: 472019 : if (subs != nullptr)
441 : : {
442 : 472019 : tlit = subs->applyTrusted(lit, rw);
443 [ + + ]: 472019 : if (!tlit.isNull())
444 : : {
445 : 118146 : lit = processRewrittenLearnedLit(tlit);
446 : : }
447 [ + - ]: 944038 : Trace("non-clausal-simplify")
448 : 472019 : << "Process learnedLiteral, after newSubs : " << lit << std::endl;
449 : : }
450 : : // apply to fixed point
451 [ + + ]: 472019 : if (cp != nullptr)
452 : : {
453 : : for (;;)
454 : : {
455 : 457338 : tlit = cp->applyTrusted(lit, rw);
456 [ + + ]: 457338 : if (tlit.isNull())
457 : : {
458 : 456788 : break;
459 : : }
460 [ - + ][ - + ]: 550 : Assert(lit != tlit.getNode());
[ - - ]
461 : 550 : lit = processRewrittenLearnedLit(tlit);
462 : 550 : d_statistics.d_numConstantProps += 1;
463 : : }
464 : : }
465 : 944038 : return lit;
466 : : }
467 : :
468 : 118696 : Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn)
469 : : {
470 [ + + ]: 118696 : if (isProofEnabled())
471 : : {
472 : 90640 : d_llpg->notifyTrustedPreprocessed(trn);
473 : : }
474 : : // return the node
475 : 118696 : return trn.getNode();
476 : : }
477 : :
478 : : } // namespace passes
479 : : } // namespace preprocessing
480 : : } // namespace cvc5::internal
|
