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 : : * Implementation of module for processing assertions for an SMT engine.
11 : : */
12 : :
13 : : #include "smt/process_assertions.h"
14 : :
15 : : #include <utility>
16 : :
17 : : #include "expr/beta_reduce_converter.h"
18 : : #include "options/arith_options.h"
19 : : #include "options/base_options.h"
20 : : #include "options/bv_options.h"
21 : : #include "options/ff_options.h"
22 : : #include "options/quantifiers_options.h"
23 : : #include "options/sep_options.h"
24 : : #include "options/smt_options.h"
25 : : #include "options/strings_options.h"
26 : : #include "preprocessing/assertion_pipeline.h"
27 : : #include "preprocessing/preprocessing_pass_context.h"
28 : : #include "preprocessing/preprocessing_pass_registry.h"
29 : : #include "printer/printer.h"
30 : : #include "smt/assertions.h"
31 : : #include "smt/print_benchmark.h"
32 : : #include "smt/solver_engine_stats.h"
33 : : #include "theory/logic_info.h"
34 : : #include "theory/theory_engine.h"
35 : :
36 : : using namespace std;
37 : : using namespace cvc5::internal::preprocessing;
38 : : using namespace cvc5::internal::theory;
39 : : using namespace cvc5::internal::kind;
40 : :
41 : : namespace cvc5::internal {
42 : : namespace smt {
43 : :
44 : : /** Useful for counting the number of recursive calls. */
45 : : class ScopeCounter
46 : : {
47 : : public:
48 : 32399 : ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
49 : 32399 : ~ScopeCounter() { --d_depth; }
50 : :
51 : : private:
52 : : unsigned& d_depth;
53 : : };
54 : :
55 : 41622 : ProcessAssertions::ProcessAssertions(Env& env, SolverEngineStatistics& stats)
56 : : : EnvObj(env),
57 : 41622 : d_slvStats(stats),
58 : 41622 : d_preprocessingPassContext(nullptr),
59 : 41622 : d_simplifyAssertionsDepth(0)
60 : : {
61 : 41622 : d_true = nodeManager()->mkConst(true);
62 : 41622 : }
63 : :
64 : 37141 : ProcessAssertions::~ProcessAssertions() {}
65 : :
66 : 28827 : void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
67 : : {
68 : : // note that we may be replacing a stale preprocessing pass context here
69 : 28827 : d_preprocessingPassContext = pc;
70 : :
71 : 28827 : PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
72 : : // TODO: this will likely change when we add support for actually assembling
73 : : // preprocessing pipelines. For now, we just create an instance of each
74 : : // available preprocessing pass.
75 : 28827 : std::vector<std::string> passNames = ppReg.getAvailablePasses();
76 [ + + ]: 1095426 : for (const std::string& passName : passNames)
77 : : {
78 : 1066599 : d_passes[passName].reset(
79 : : ppReg.createPass(d_preprocessingPassContext, passName));
80 : : }
81 : 28827 : }
82 : :
83 : 37141 : void ProcessAssertions::cleanup() { d_passes.clear(); }
84 : :
85 : 31937 : void ProcessAssertions::spendResource(Resource r)
86 : : {
87 : 31937 : resourceManager()->spendResource(r);
88 : 31937 : }
89 : :
90 : 31485 : bool ProcessAssertions::apply(AssertionPipeline& ap)
91 : : {
92 [ - + ][ - + ]: 31485 : Assert(d_preprocessingPassContext != nullptr);
[ - - ]
93 : : // Dump the assertions
94 : 31485 : dumpAssertions("assertions::pre-everything", ap);
95 [ + - ]: 31485 : Trace("assertions::pre-everything") << std::endl;
96 [ + + ]: 31485 : if (isOutputOn(OutputTag::PRE_ASSERTS))
97 : : {
98 : 1 : std::ostream& outPA = d_env.output(OutputTag::PRE_ASSERTS);
99 : 1 : outPA << ";; pre-asserts start" << std::endl;
100 : 1 : dumpAssertionsToStream(outPA, ap, options().smt.printDefs);
101 : 1 : outPA << ";; pre-asserts end" << std::endl;
102 : : }
103 : :
104 [ + - ]: 31485 : Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
105 [ + - ]: 31485 : Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
106 : :
107 [ + - ]: 31485 : Trace("smt") << "#Assertions : " << ap.size() << endl;
108 : :
109 [ - + ]: 31485 : if (ap.size() == 0)
110 : : {
111 : : // nothing to do
112 : 0 : return true;
113 : : }
114 : :
115 [ + + ]: 31485 : if (options().bv.bvGaussElim)
116 : : {
117 : 2 : applyPass("bv-gauss", ap);
118 : : }
119 : :
120 : : // Add dummy assertion in last position - to be used as a
121 : : // placeholder for any new assertions to get added
122 : 31485 : ap.push_back(d_true);
123 : :
124 : : // Assertions are NOT guaranteed to be rewritten by this point
125 : :
126 [ + - ]: 62970 : Trace("smt-proc")
127 : 0 : << "ProcessAssertions::processAssertions() : pre-definition-expansion"
128 : 31485 : << endl;
129 : :
130 [ + + ]: 31485 : if (isOutputOn(OutputTag::NORMALIZE))
131 : : {
132 : : // For normalization, apply substitutions WITHOUT rewriting, then beta
133 : : // reduction This preserves the exact structure for normalization purposes
134 : 2 : BetaReduceNodeConverter bnc(nodeManager());
135 : : theory::SubstitutionMap& sm =
136 : 2 : d_preprocessingPassContext->getTopLevelSubstitutions().get();
137 : :
138 [ + + ]: 8 : for (size_t i = 0, size = ap.size(); i < size; ++i)
139 : : {
140 : 6 : Node ar = sm.apply(ap[i]);
141 : 6 : ar = bnc.convert(ar);
142 : 6 : ap.replace(i, ar);
143 : 6 : }
144 : :
145 : : // Now apply the normalize pass for variable renaming and sorting
146 : 2 : applyPass("normalize", ap);
147 : :
148 : 2 : std::ostream& outPA = d_env.output(OutputTag::NORMALIZE);
149 : 2 : outPA << ";; normalize start" << std::endl;
150 : 2 : dumpAssertionsToStream(outPA, ap, false);
151 : 2 : outPA << ";; normalize end" << std::endl;
152 : 2 : return true;
153 : 2 : }
154 : :
155 : : // Apply substitutions first. If we are non-incremental, this has only the
156 : : // effect of replacing defined functions with their definitions.
157 : : // We do not call theory-specific expand definitions here, since we want
158 : : // to give the opportunity to rewrite/preprocess terms before expansion.
159 : 31483 : applyPass("apply-substs", ap);
160 [ + - ]: 62966 : Trace("smt-proc")
161 : 0 : << "ProcessAssertions::processAssertions() : post-definition-expansion"
162 : 31483 : << endl;
163 : :
164 [ + - ]: 31483 : Trace("smt") << " assertions : " << ap.size() << endl;
165 : :
166 [ + + ]: 31483 : if (options().quantifiers.globalNegate)
167 : : {
168 : : // global negation of the formula
169 : 9 : applyPass("global-negate", ap);
170 : : }
171 : :
172 [ + + ]: 31483 : if (options().arith.nlExtPurify)
173 : : {
174 : 11 : applyPass("nl-ext-purify", ap);
175 : : }
176 : :
177 [ + + ]: 31483 : if (options().smt.solveRealAsInt)
178 : : {
179 : 30 : applyPass("real-to-int", ap);
180 : : }
181 : :
182 [ + + ]: 31483 : if (options().smt.ackermann)
183 : : {
184 : 120 : applyPass("ackermann", ap);
185 : : }
186 : :
187 [ + + ]: 31482 : if (options().smt.solveIntAsBV > 0)
188 : : {
189 : 32 : applyPass("int-to-bv", ap);
190 : : }
191 : :
192 [ + - ]: 31477 : Trace("smt") << " assertions : " << ap.size() << endl;
193 : :
194 : 31477 : bool noConflict = true;
195 : :
196 [ + + ]: 31477 : if (options().smt.extRewPrep != options::ExtRewPrepMode::OFF)
197 : : {
198 : 48 : applyPass("ext-rew-pre", ap);
199 : : }
200 : :
201 : : // Unconstrained simplification
202 [ + + ]: 31477 : if (options().smt.unconstrainedSimp)
203 : : {
204 : 230 : applyPass("rewrite", ap);
205 : 230 : applyPass("unconstrained-simplifier", ap);
206 : : }
207 : :
208 [ + + ]: 31477 : if (options().bv.bvIntroducePow2)
209 : : {
210 : 5 : applyPass("bv-intro-pow2", ap);
211 : : }
212 : :
213 : : // Lift bit-vectors of size 1 to bool
214 [ + + ]: 31477 : if (options().bv.bitvectorToBool)
215 : : {
216 : 638 : applyPass("bv-to-bool", ap);
217 : : }
218 [ + + ]: 31477 : if (options().smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
219 : : {
220 : 625 : applyPass("bv-to-int", ap);
221 : : }
222 [ + + ]: 31475 : if (options().smt.foreignTheoryRewrite)
223 : : {
224 : 10 : applyPass("foreign-theory-rewrite", ap);
225 : : }
226 : : // Eagerly eliminate distinct terms up to the configured threshold. Only run
227 : : // if the threshold option was explicitly set by the user (a value of 0 means
228 : : // no limit, i.e. eliminate all distinct terms).
229 [ + + ]: 31475 : if (options().smt.distinctElimThresholdWasSetByUser)
230 : : {
231 : 12 : applyPass("distinct-elim", ap);
232 : : }
233 : :
234 : : // Assertions MUST BE guaranteed to be rewritten by this point
235 : 31475 : applyPass("rewrite", ap);
236 : :
237 : : // Convert non-top-level Booleans to bit-vectors of size 1
238 [ + + ]: 31475 : if (options().bv.boolToBitvector != options::BoolToBVMode::OFF)
239 : : {
240 : 12 : applyPass("bool-to-bv", ap);
241 : : }
242 [ + + ]: 31475 : if (options().sep.sepPreSkolemEmp)
243 : : {
244 : 2 : applyPass("sep-skolem-emp", ap);
245 : : }
246 : :
247 [ + + ]: 31475 : if (logicInfo().isQuantified())
248 : : {
249 : : // remove rewrite rules, apply pre-skolemization to existential quantifiers
250 : 22410 : applyPass("quantifiers-preprocess", ap);
251 : :
252 : : // fmf-fun : assume admissible functions, applying preprocessing reduction
253 : : // to FMF
254 [ + + ]: 22410 : if (options().quantifiers.fmfFunWellDefined)
255 : : {
256 : 141 : applyPass("fun-def-fmf", ap);
257 : : }
258 : 22410 : if (options().quantifiers.preSkolemQuant
259 [ + + ]: 22410 : != options::PreSkolemQuantMode::OFF)
260 : : {
261 : : // needed since quantifier preprocessing may introduce skolems that were
262 : : // solved for already
263 : 250 : applyPass("apply-substs", ap);
264 : : }
265 : : }
266 [ + + ]: 31475 : if (!options().strings.stringLazyPreproc)
267 : : {
268 : 76 : applyPass("strings-eager-pp", ap);
269 : : // needed since strings eager preprocessing may reintroduce skolems that
270 : : // were already solved for in incremental mode
271 : 76 : applyPass("apply-substs", ap);
272 : : }
273 [ + + ]: 31475 : if (options().smt.sortInference)
274 : : {
275 : 45 : applyPass("sort-inference", ap);
276 : : }
277 : :
278 [ + + ]: 31475 : if (options().arith.pbRewrites)
279 : : {
280 : 2 : applyPass("pseudo-boolean-processor", ap);
281 : : }
282 : :
283 : : // rephrasing normal inputs as sygus problems
284 [ + + ]: 31475 : if (options().quantifiers.sygusInference != options::SygusInferenceMode::OFF)
285 : : {
286 : 72 : applyPass("sygus-infer", ap);
287 : : }
288 : :
289 [ + - ]: 62950 : Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
290 : 31475 : << endl;
291 : 31475 : dumpAssertions("assertions::pre-simplify", ap);
292 [ + - ]: 31475 : Trace("assertions::pre-simplify") << std::endl;
293 : 31475 : verbose(2) << "simplifying assertions..." << std::endl;
294 : 31475 : noConflict = simplifyAssertions(ap);
295 [ + + ]: 31475 : if (!noConflict)
296 : : {
297 : 6131 : ++(d_slvStats.d_simplifiedToFalse);
298 : : }
299 [ + - ]: 62950 : Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
300 : 31475 : << endl;
301 : 31475 : dumpAssertions("assertions::post-simplify", ap);
302 [ + - ]: 31475 : Trace("assertions::post-simplify") << std::endl;
303 : :
304 [ + - ]: 31475 : if (options().smt.staticLearning)
305 : : {
306 : 31475 : applyPass("static-learning", ap);
307 : : }
308 [ + - ]: 31475 : Trace("smt") << " assertions : " << ap.size() << endl;
309 : :
310 [ + + ]: 31475 : if (options().smt.learnedRewrite)
311 : : {
312 : 20 : applyPass("learned-rewrite", ap);
313 : : }
314 : :
315 [ + + ]: 31475 : if (options().smt.earlyIteRemoval)
316 : : {
317 : 10 : d_slvStats.d_numAssertionsPre += ap.size();
318 : 10 : applyPass("ite-removal", ap);
319 : : // This is needed because when solving incrementally, removeITEs may
320 : : // introduce skolems that were solved for earlier and thus appear in the
321 : : // substitution map.
322 : 10 : applyPass("apply-substs", ap);
323 : 10 : d_slvStats.d_numAssertionsPost += ap.size();
324 : : }
325 : :
326 [ + + ]: 31475 : if (options().smt.repeatSimp)
327 : : {
328 : 462 : dumpAssertions("assertions::pre-repeat-simplify", ap);
329 [ + - ]: 462 : Trace("assertions::pre-repeat-simplify") << std::endl;
330 [ + - ]: 924 : Trace("smt-proc")
331 : 0 : << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
332 : 462 : << endl;
333 : 462 : verbose(2) << "re-simplifying assertions..." << std::endl;
334 : 462 : ScopeCounter depth(d_simplifyAssertionsDepth);
335 : 462 : noConflict &= simplifyAssertions(ap);
336 [ + - ]: 924 : Trace("smt-proc")
337 : 0 : << "ProcessAssertions::processAssertions() : post-repeat-simplify"
338 : 462 : << endl;
339 : 462 : dumpAssertions("assertions::post-repeat-simplify", ap);
340 [ + - ]: 462 : Trace("assertions::post-repeat-simplify") << std::endl;
341 : 462 : }
342 : :
343 [ + + ]: 31475 : if (logicInfo().isHigherOrder())
344 : : {
345 : 1868 : applyPass("ho-elim", ap);
346 : : }
347 : :
348 : : // begin: INVARIANT to maintain: no reordering of assertions or
349 : : // introducing new ones
350 : :
351 [ + - ]: 31475 : Trace("smt") << " assertions : " << ap.size() << endl;
352 : :
353 [ + - ]: 62950 : Trace("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
354 : 31475 : << endl;
355 [ + - ]: 31475 : Trace("smt") << " assertions : " << ap.size() << endl;
356 : :
357 : : // ff
358 [ + - ]: 31475 : if (options().ff.ffElimDisjunctiveBit)
359 : : {
360 : 31475 : applyPass("ff-disjunctive-bit", ap);
361 : : }
362 : 31475 : if (options().ff.ffBitsum
363 [ + - ][ + + ]: 31475 : || options().ff.ffSolver == options::FfSolver::SPLIT_GB)
[ + + ]
364 : : {
365 : 68 : applyPass("ff-bitsum", ap);
366 : : }
367 : :
368 : : // ensure rewritten
369 : 31475 : applyPass("rewrite", ap);
370 : :
371 : : // Note the two passes below are very similar. Ideally, they could be
372 : : // done in a single traversal, e.g. do both static (ppStaticRewrite) and
373 : : // normal (ppRewrite) in one pass. However, we do theory-preprocess
374 : : // separately since it is cached in TheoryPreprocessor, which is subsequently
375 : : // used for theory preprocessing lemmas as well, whereas a combined
376 : : // pass could not be used for this purpose.
377 : :
378 : : // rewrite terms based on static theory-specific rewriting
379 : 31481 : applyPass("static-rewrite", ap);
380 : : // apply theory preprocess, which includes ITE removal
381 : 31492 : applyPass("theory-preprocess", ap);
382 : : // notice that we do not apply substitutions as a last step here, since
383 : : // the range of substitutions is not theory-preprocessed.
384 : :
385 [ + + ]: 31462 : if (options().bv.bitblastMode == options::BitblastMode::EAGER)
386 : : {
387 : 73 : applyPass("bv-eager-atoms", ap);
388 : : }
389 : :
390 [ + - ]: 31462 : Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
391 : 31462 : dumpAssertions("assertions::post-everything", ap);
392 [ + - ]: 31462 : Trace("assertions::post-everything") << std::endl;
393 [ + + ]: 31462 : if (isOutputOn(OutputTag::POST_ASSERTS))
394 : : {
395 : 18 : std::ostream& outPA = d_env.output(OutputTag::POST_ASSERTS);
396 : 18 : outPA << ";; post-asserts start" << std::endl;
397 : 18 : dumpAssertionsToStream(outPA, ap, options().smt.printDefs);
398 : 18 : outPA << ";; post-asserts end" << std::endl;
399 : : }
400 : :
401 : 31462 : return noConflict;
402 : : }
403 : :
404 : : // returns false if simplification led to "false"
405 : 31937 : bool ProcessAssertions::simplifyAssertions(AssertionPipeline& ap)
406 : : {
407 : 31937 : spendResource(Resource::PreprocessStep);
408 : : try
409 : : {
410 : 31937 : ScopeCounter depth(d_simplifyAssertionsDepth);
411 : :
412 [ + - ]: 31937 : Trace("simplify") << "ProcessAssertions::simplify()" << endl;
413 : :
414 [ + + ]: 31937 : if (options().smt.simplificationMode != options::SimplificationMode::NONE)
415 : : {
416 : : // Perform non-clausal simplification
417 : 31793 : PreprocessingPassResult res = applyPass("non-clausal-simp", ap);
418 [ + + ]: 31793 : if (res == PreprocessingPassResult::CONFLICT)
419 : : {
420 : 6179 : return false;
421 : : }
422 : :
423 : : // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
424 : : // do the miplib trick.
425 : 25614 : if ( // check that option is on
426 : 25614 : options().arith.arithMLTrick &&
427 : : // only useful in arith
428 [ + + ][ + - ]: 25622 : logicInfo().isTheoryEnabled(THEORY_ARITH) &&
[ + + ]
429 : : // disables miplib processing during re-simplification, which we don't
430 : : // expect to be useful
431 [ + - ]: 8 : d_simplifyAssertionsDepth <= 1)
432 : : {
433 : 8 : applyPass("miplib-trick", ap);
434 : : }
435 : : else
436 : : {
437 [ + - ]: 51212 : Trace("simplify") << "ProcessAssertions::simplify(): "
438 : 25606 : << "skipping miplib pseudobooleans pass..." << endl;
439 : : }
440 : : }
441 : :
442 [ + - ]: 25758 : Trace("smt") << " assertions : " << ap.size() << endl;
443 : :
444 : : // ITE simplification
445 : 25758 : if (options().smt.doITESimp
446 [ + + ][ + + ]: 25758 : && (d_simplifyAssertionsDepth <= 1 || options().smt.doITESimpOnRepeat))
[ + - ][ + + ]
447 : : {
448 : 5 : PreprocessingPassResult res = applyPass("ite-simp", ap);
449 [ - + ]: 5 : if (res == PreprocessingPassResult::CONFLICT)
450 : : {
451 : 0 : verbose(2) << "...ITE simplification found unsat..." << std::endl;
452 : 0 : return false;
453 : : }
454 : : }
455 : :
456 [ + - ]: 25758 : Trace("smt") << " assertions : " << ap.size() << endl;
457 : :
458 : : // Unconstrained simplification
459 [ + + ]: 25758 : if (options().smt.unconstrainedSimp)
460 : : {
461 : 386 : applyPass("unconstrained-simplifier", ap);
462 : : }
463 : :
464 : 25758 : if (options().smt.repeatSimp
465 [ + + ][ + + ]: 25758 : && options().smt.simplificationMode
[ + + ]
466 : : != options::SimplificationMode::NONE)
467 : : {
468 : 820 : PreprocessingPassResult res = applyPass("non-clausal-simp", ap);
469 [ - + ]: 820 : if (res == PreprocessingPassResult::CONFLICT)
470 : : {
471 : 0 : return false;
472 : : }
473 : : }
474 [ + + ]: 31937 : }
475 [ - - ]: 0 : catch (TypeCheckingExceptionPrivate& tcep)
476 : : {
477 : : // Calls to this function should have already weeded out any
478 : : // typechecking exceptions via (e.g.) ensureBoolean(). But a
479 : : // theory could still create a new expression that isn't
480 : : // well-typed, and we don't want the C++ runtime to abort our
481 : : // process without any error notice.
482 : 0 : InternalError()
483 : 0 : << "A bad expression was produced. Original exception follows:\n"
484 : 0 : << tcep;
485 : 0 : }
486 : 25758 : return true;
487 : : }
488 : :
489 : 687730 : void ProcessAssertions::dumpAssertions(const std::string& key,
490 : : const AssertionPipeline& ap)
491 : : {
492 : 687730 : bool isTraceOn = TraceIsOn(key);
493 [ + + ]: 687730 : if (!isTraceOn)
494 : : {
495 : 687729 : return;
496 : : }
497 : 1 : std::stringstream ss;
498 : 1 : dumpAssertionsToStream(ss, ap, options().smt.printDefs);
499 [ - + ]: 1 : Trace(key) << ";;; " << key << " start" << std::endl;
500 [ - + ][ + - ]: 1 : Trace(key) << ss.str();
[ - - ]
501 [ - + ]: 1 : Trace(key) << ";;; " << key << " end " << std::endl;
502 : 1 : }
503 : :
504 : 22 : void ProcessAssertions::dumpAssertionsToStream(std::ostream& os,
505 : : const AssertionPipeline& ap,
506 : : bool printDefs)
507 : : {
508 : 22 : PrintBenchmark pb(nodeManager(), Printer::getPrinter(os));
509 : 22 : std::vector<Node> assertions;
510 : : // Notice that users may define ordinary and recursive functions. The latter
511 : : // get added to the list of assertions as quantified formulas. Since we are
512 : : // interested in printing the result of preprocessed quantified formulas
513 : : // corresponding to recursive function definitions and not the original
514 : : // definitions, we do not explicitly record recursive function definitions.
515 : : //
516 : : // Furthermore, we may have eliminated user variables from the preprocessed
517 : : // input, often via solving an equality (= x t) and adding x -> t to the
518 : : // top-level substitutions. We include these in the output as well. Note that
519 : : // ordinary define-fun are also included in this substitution.
520 : : //
521 : : // In summary, this means that define-fun-rec are expanded to
522 : : // (declare-fun ...) + (assert (forall ...)) in the printing below, whereas
523 : : // define-fun are preserved. Further inferred top-level substitutions are
524 : : // also printed as define-fun.
525 : 22 : std::vector<Node> defs;
526 : 22 : const theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
527 : 22 : const std::unordered_map<Node, Node>& ss = sm.getSubstitutions();
528 : :
529 [ + + ]: 22 : if (printDefs)
530 : : {
531 [ + + ]: 28 : for (const std::pair<const Node, Node>& s : ss)
532 : : {
533 : 8 : defs.push_back(s.first.eqNode(s.second));
534 : : }
535 : : }
536 [ + + ]: 575 : for (size_t i = 0, size = ap.size(); i < size; i++)
537 : : {
538 : 553 : assertions.push_back(ap[i]);
539 : : }
540 : 22 : pb.printBenchmark(os, logicInfo().getLogicString(), defs, assertions);
541 : 22 : }
542 : :
543 : 280465 : PreprocessingPassResult ProcessAssertions::applyPass(const std::string& pname,
544 : : AssertionPipeline& ap)
545 : : {
546 : 280465 : dumpAssertions("assertions::pre-" + pname, ap);
547 : : PreprocessingPassResult res;
548 : : // note we do not apply preprocessing passes if we are already in conflict
549 [ + + ]: 280465 : if (!ap.isInConflict())
550 : : {
551 : 239335 : res = d_passes[pname]->apply(&ap);
552 : : }
553 : : else
554 : : {
555 : 41130 : res = PreprocessingPassResult::CONFLICT;
556 : : }
557 : 280444 : dumpAssertions("assertions::post-" + pname, ap);
558 : 280444 : return res;
559 : : }
560 : :
561 : : } // namespace smt
562 : : } // namespace cvc5::internal
|
