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