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