Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Haniel Barbosa
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 setting default options.
14 : : */
15 : :
16 : : #include "smt/set_defaults.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "base/output.h"
21 : : #include "options/arith_options.h"
22 : : #include "options/arrays_options.h"
23 : : #include "options/bags_options.h"
24 : : #include "options/base_options.h"
25 : : #include "options/booleans_options.h"
26 : : #include "options/bv_options.h"
27 : : #include "options/datatypes_options.h"
28 : : #include "options/decision_options.h"
29 : : #include "options/ff_options.h"
30 : : #include "options/fp_options.h"
31 : : #include "options/language.h"
32 : : #include "options/main_options.h"
33 : : #include "options/option_exception.h"
34 : : #include "options/parallel_options.h"
35 : : #include "options/parser_options.h"
36 : : #include "options/printer_options.h"
37 : : #include "options/proof_options.h"
38 : : #include "options/prop_options.h"
39 : : #include "options/quantifiers_options.h"
40 : : #include "options/sep_options.h"
41 : : #include "options/sets_options.h"
42 : : #include "options/smt_options.h"
43 : : #include "options/strings_options.h"
44 : : #include "options/theory_options.h"
45 : : #include "options/uf_options.h"
46 : : #include "smt/logic_exception.h"
47 : : #include "theory/theory.h"
48 : :
49 : : using namespace cvc5::internal::theory;
50 : :
51 : : namespace cvc5::internal {
52 : : namespace smt {
53 : :
54 : : /**
55 : : * Set domain.optName to value due to reason. Notify if value changes.
56 : : * Note this macro should be used if the value is concrete.
57 : : */
58 : : #define SET_AND_NOTIFY(domain, optName, value, reason) \
59 : : if (opts.write_##domain().optName != value) \
60 : : { \
61 : : notifyModifyOption(options::domain::longName::optName, #value, reason); \
62 : : opts.write_##domain().optName = value; \
63 : : }
64 : : /**
65 : : * Set domain.optName to value due to reason. Notify if value changes.
66 : : *
67 : : * Note this macro should be used if the value passed to the macro is not
68 : : * concrete (i.e., stored in a variable).
69 : : */
70 : : #define SET_AND_NOTIFY_VAL_SYM(domain, optName, value, reason) \
71 : : if (opts.write_##domain().optName != value) \
72 : : { \
73 : : std::stringstream sstmp; \
74 : : sstmp << value; \
75 : : notifyModifyOption( \
76 : : options::domain::longName::optName, sstmp.str(), reason); \
77 : : opts.write_##domain().optName = value; \
78 : : }
79 : : /**
80 : : * Set domain.optName to value due to reason if the option was not already set
81 : : * by the user. Notify if value changes.
82 : : * Note this macro should be used if the value is concrete.
83 : : */
84 : : #define SET_AND_NOTIFY_IF_NOT_USER(domain, optName, value, reason) \
85 : : if (!opts.write_##domain().optName##WasSetByUser \
86 : : && opts.write_##domain().optName != value) \
87 : : { \
88 : : notifyModifyOption(options::domain::longName::optName, #value, reason); \
89 : : opts.write_##domain().optName = value; \
90 : : }
91 : : /**
92 : : * Set domain.optName to value due to reason if the option was not already set
93 : : * by the user. Notify if value changes.
94 : : */
95 : : #define SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(domain, optName, value, reason) \
96 : : if (!opts.write_##domain().optName##WasSetByUser \
97 : : && opts.write_##domain().optName != value) \
98 : : { \
99 : : std::stringstream sstmp; \
100 : : sstmp << value; \
101 : : notifyModifyOption( \
102 : : options::domain::longName::optName, sstmp.str(), reason); \
103 : : opts.write_##domain().optName = value; \
104 : : }
105 : :
106 : 49267 : SetDefaults::SetDefaults(Env& env, bool isInternalSubsolver)
107 : 49267 : : EnvObj(env), d_isInternalSubsolver(isInternalSubsolver)
108 : : {
109 : 49267 : }
110 : :
111 : 49267 : void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
112 : : {
113 : : // initial changes that are independent of logic, and may impact the logic
114 : 49267 : setDefaultsPre(opts);
115 : : // now, finalize the logic
116 : 49266 : finalizeLogic(logic, opts);
117 : : // further changes to options based on the logic
118 : 49265 : setDefaultsPost(logic, opts);
119 : 49262 : }
120 : :
121 : 49267 : void SetDefaults::setDefaultsPre(Options& opts)
122 : : {
123 : : // safe options
124 [ + + ]: 49267 : if (options().base.safeOptions)
125 : : {
126 : : // all "experimental" theories that are enabled by default should be
127 : : // disabled here
128 [ + - ][ + - ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(uf, hoExp, false, "safe options");
[ + - ]
129 [ + - ][ + - ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(arith, arithExp, false, "safe options");
[ + - ]
130 [ + - ][ + - ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(sep, sepExp, false, "safe options");
[ + - ]
131 [ + - ][ - + ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(bags, bagsExp, false, "safe options");
[ - + ]
132 [ + - ][ + - ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(ff, ffExp, false, "safe options");
[ + - ]
133 : : // these are disabled by default but are listed here in case they are
134 : : // enabled by default later
135 [ + - ][ - + ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(fp, fpExp, false, "safe options");
[ - + ]
136 [ + - ][ - + ]: 1 : SET_AND_NOTIFY_IF_NOT_USER(sets, setsExp, false, "safe options");
[ - + ]
137 : : }
138 : : // implied options
139 [ + + ]: 49267 : if (opts.smt.debugCheckModels)
140 : : {
141 [ + + ]: 1906 : SET_AND_NOTIFY(smt, checkModels, true, "debugCheckModels");
142 : : }
143 [ + + ][ + + ]: 49267 : if (opts.smt.checkModels || opts.driver.dumpModels)
144 : : {
145 [ + + ]: 2371 : SET_AND_NOTIFY(smt, produceModels, true, "check or dump models");
146 : : }
147 [ + + ]: 49267 : if (opts.smt.checkModels)
148 : : {
149 [ + + ]: 2368 : SET_AND_NOTIFY(smt, produceAssignments, true, "checkModels");
150 : : }
151 : : // unsat cores and proofs shenanigans
152 [ + + ]: 49267 : if (opts.driver.dumpDifficulty)
153 : : {
154 [ + + ]: 15 : SET_AND_NOTIFY(smt, produceDifficulty, true, "dumpDifficulty");
155 : : }
156 [ + + ][ + + ]: 49267 : if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
157 [ + - ][ + + ]: 47613 : || opts.driver.dumpUnsatCoresLemmas || opts.smt.unsatAssumptions
158 [ + + ]: 47373 : || opts.smt.minimalUnsatCores
159 [ + + ]: 47352 : || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
160 : : {
161 [ + + ]: 5588 : SET_AND_NOTIFY(
162 : : smt, produceUnsatCores, true, "option requiring unsat cores");
163 : : }
164 [ + + ]: 49267 : if (opts.smt.produceUnsatCores
165 [ + + ]: 9863 : && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
166 : : {
167 [ + - ]: 6163 : SET_AND_NOTIFY(smt,
168 : : unsatCoresMode,
169 : : options::UnsatCoresMode::ASSUMPTIONS,
170 : : "enabling unsat cores");
171 : : }
172 [ + + ]: 49267 : if (opts.proof.checkProofSteps)
173 : : {
174 [ + + ]: 6 : SET_AND_NOTIFY(smt, checkProofs, true, "check-proof-steps");
175 : : // maximize the granularity
176 [ + + ][ + - ]: 6 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + + ]
177 : : proof,
178 : : proofGranularityMode,
179 : : options::ProofGranularityMode::DSL_REWRITE,
180 : : "check-proof-steps");
181 : : }
182 : : // if check-proofs, dump-proofs, dump-unsat-cores-lemmas, or proof-mode=full,
183 : : // then proofs being fully enabled is implied
184 [ + + ][ + + ]: 49267 : if (opts.smt.checkProofs || opts.driver.dumpProofs
185 [ + - ]: 41128 : || opts.driver.dumpUnsatCoresLemmas
186 [ + + ]: 41128 : || opts.smt.proofMode == options::ProofMode::FULL
187 [ - + ]: 40975 : || opts.smt.proofMode == options::ProofMode::FULL_STRICT)
188 : : {
189 [ + + ]: 8292 : SET_AND_NOTIFY(smt, produceProofs, true, "option requiring proofs");
190 : : }
191 : :
192 : : // this check assumes the user has requested *full* proofs
193 [ + + ]: 49267 : if (opts.smt.produceProofs)
194 : : {
195 : : // if the user requested proofs, proof mode is (at least) full
196 [ + + ]: 10376 : if (opts.smt.proofMode < options::ProofMode::FULL)
197 : : {
198 [ + + ][ + - ]: 10056 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
199 : : smt, proofMode, options::ProofMode::FULL, "enabling proofs");
200 : : }
201 : : // Default granularity is theory rewrite if we are intentionally using
202 : : // proofs, otherwise it is MACRO (e.g. if produce unsat cores is true)
203 [ + + ]: 10376 : if (!opts.proof.proofGranularityModeWasSetByUser
204 [ + + ]: 3995 : && opts.proof.proofGranularityMode
205 : : < options::ProofGranularityMode::THEORY_REWRITE)
206 : : {
207 [ + - ]: 3926 : SET_AND_NOTIFY(proof,
208 : : proofGranularityMode,
209 : : options::ProofGranularityMode::THEORY_REWRITE,
210 : : "enabling proofs");
211 : : }
212 : : // unsat cores are available due to proofs being enabled, as long as
213 : : // SAT proofs are available
214 [ + + ]: 10376 : if (opts.smt.unsatCoresMode != options::UnsatCoresMode::SAT_PROOF
215 [ + + ]: 10047 : && opts.smt.proofMode != options::ProofMode::PP_ONLY)
216 : : {
217 [ + + ]: 10040 : SET_AND_NOTIFY(smt, produceUnsatCores, true, "enabling proofs");
218 [ + + ]: 10040 : if (options().prop.satSolver == options::SatSolverMode::MINISAT)
219 : : {
220 : : // if full proofs are available in minisat, use them for unsat cores
221 [ + - ]: 10032 : SET_AND_NOTIFY(smt,
222 : : unsatCoresMode,
223 : : options::UnsatCoresMode::SAT_PROOF,
224 : : "enabling proofs, minisat");
225 : : }
226 [ + - ]: 8 : else if (options().prop.satSolver == options::SatSolverMode::CADICAL)
227 : : {
228 : : // unsat cores available by assumptions by default if proofs are enabled
229 : : // with CaDiCaL.
230 [ + - ]: 8 : SET_AND_NOTIFY(smt,
231 : : unsatCoresMode,
232 : : options::UnsatCoresMode::ASSUMPTIONS,
233 : : "enabling proofs, non-minisat");
234 : : }
235 : : }
236 : : // note that this test assumes that granularity modes are ordered and
237 : : // THEORY_REWRITE is gonna be, in the enum, after the lower granularity
238 : : // levels
239 [ + + ]: 10376 : if (opts.proof.proofFormatMode == options::ProofFormatMode::ALETHE)
240 : : {
241 [ - + ]: 1476 : if (opts.proof.proofGranularityMode
242 : : < options::ProofGranularityMode::THEORY_REWRITE)
243 : : {
244 [ - - ]: 0 : SET_AND_NOTIFY_VAL_SYM(
245 : : proof,
246 : : proofGranularityMode,
247 : : options::ProofGranularityMode::THEORY_REWRITE,
248 : : "Alethe requires granularity at least theory-rewrite");
249 : : }
250 : : }
251 : : }
252 [ + + ]: 49267 : if (!opts.smt.produceProofs)
253 : : {
254 [ + + ]: 38891 : if (opts.smt.proofMode != options::ProofMode::OFF)
255 : : {
256 : : // if (expert) user set proof mode to something other than off, enable
257 : : // proofs
258 [ + - ]: 1964 : SET_AND_NOTIFY(smt, produceProofs, true, "proof mode");
259 : : }
260 : : // if proofs weren't enabled by user, and we are producing difficulty
261 [ + + ]: 38891 : if (opts.smt.produceDifficulty)
262 : : {
263 [ + + ]: 401 : SET_AND_NOTIFY(smt, produceProofs, true, "produce difficulty");
264 : : // ensure at least preprocessing proofs are enabled
265 [ + + ]: 401 : if (opts.smt.proofMode == options::ProofMode::OFF)
266 : : {
267 [ + - ]: 400 : SET_AND_NOTIFY_VAL_SYM(
268 : : smt, proofMode, options::ProofMode::PP_ONLY, "produce difficulty");
269 : : }
270 : : }
271 : : // if proofs weren't enabled by user, and we are producing unsat cores
272 [ + + ]: 38891 : if (opts.smt.produceUnsatCores)
273 : : {
274 [ + + ]: 7845 : SET_AND_NOTIFY(smt, produceProofs, true, "unsat cores");
275 [ + + ]: 7845 : if (opts.smt.unsatCoresMode == options::UnsatCoresMode::SAT_PROOF)
276 : : {
277 : : // if requested to be based on proofs, we produce (preprocessing +) SAT
278 : : // proofs
279 [ + + ]: 208 : SET_AND_NOTIFY_VAL_SYM(
280 : : smt, proofMode, options::ProofMode::SAT, "unsat cores SAT proof");
281 : : }
282 [ + + ]: 7637 : else if (opts.smt.proofMode == options::ProofMode::OFF)
283 : : {
284 : : // otherwise, we always produce preprocessing proofs
285 [ + - ]: 5677 : SET_AND_NOTIFY_VAL_SYM(
286 : : smt, proofMode, options::ProofMode::PP_ONLY, "unsat cores");
287 : : }
288 : : }
289 : : }
290 [ + + ]: 49267 : if (opts.smt.produceProofs)
291 : : {
292 : : // determine the prop proof mode, based on which SAT solver we are using
293 [ + - ]: 18622 : if (!opts.proof.propProofModeWasSetByUser)
294 : : {
295 [ + + ]: 18622 : if (opts.prop.satSolver == options::SatSolverMode::CADICAL)
296 : : {
297 : : // use SAT_EXTERNAL_PROVE for cadical by default
298 [ + + ]: 24 : SET_AND_NOTIFY(proof,
299 : : propProofMode,
300 : : options::PropProofMode::SAT_EXTERNAL_PROVE,
301 : : "cadical");
302 : : }
303 : : }
304 : : }
305 : :
306 : : // if unsat cores are disabled, then unsat cores mode should be OFF. Similarly
307 : : // for proof mode.
308 [ - + ][ - + ]: 49267 : Assert(opts.smt.produceUnsatCores
[ - - ]
309 : : == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF));
310 [ - + ][ - + ]: 49267 : Assert(opts.smt.produceProofs
[ - - ]
311 : : == (opts.smt.proofMode != options::ProofMode::OFF));
312 : :
313 : : // if we require disabling options due to proofs, disable them now
314 [ + + ]: 49267 : if (opts.smt.produceProofs)
315 : : {
316 : 37244 : std::stringstream reasonNoProofs;
317 [ + + ]: 18622 : if (incompatibleWithProofs(opts, reasonNoProofs))
318 : : {
319 : 2 : std::stringstream ss;
320 : 1 : ss << reasonNoProofs.str() << " not supported with proofs or unsat cores";
321 : 1 : throw OptionException(ss.str());
322 : : }
323 : : }
324 [ + + ]: 49266 : if (d_isInternalSubsolver)
325 : : {
326 : : // these options must be disabled on internal subsolvers, as they are
327 : : // used by the user to rephrase the input.
328 [ + + ]: 15108 : SET_AND_NOTIFY_VAL_SYM(quantifiers,
329 : : sygusInference,
330 : : options::SygusInferenceMode::OFF,
331 : : "internal subsolver");
332 : : // deep restart does not work with internal subsolvers?
333 [ - + ]: 15108 : SET_AND_NOTIFY_VAL_SYM(smt,
334 : : deepRestartMode,
335 : : options::DeepRestartMode::NONE,
336 : : "internal subsolver");
337 : : }
338 : 49266 : }
339 : :
340 : 49266 : void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
341 : : {
342 [ + + ]: 49266 : if (opts.quantifiers.sygusInstWasSetByUser)
343 : : {
344 [ + + ][ - + ]: 129 : if (opts.quantifiers.sygusInst && isSygus(opts))
[ - + ]
345 : : {
346 : 0 : throw OptionException(std::string(
347 : : "SyGuS instantiation quantifiers module cannot be enabled "
348 : 0 : "for SyGuS inputs."));
349 : : }
350 : : }
351 [ + + ]: 91007 : else if (!isSygus(opts) && logic.isQuantified()
352 [ + - ]: 33437 : && (logic.isPure(THEORY_FP)
353 [ + + ][ + + ]: 33437 : || (logic.isPure(THEORY_ARITH) && !logic.isLinear()
354 [ + + ]: 91 : && logic.areIntegersUsed()))
355 [ + + ][ + + ]: 91007 : && !opts.base.incrementalSolving)
[ + + ]
356 : : {
357 [ + - ]: 32 : SET_AND_NOTIFY(quantifiers, sygusInst, true, "logic");
358 : : }
359 : :
360 [ + + ]: 49266 : if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
361 : : {
362 : 138 : if (opts.smt.produceModels
363 [ + + ][ + - ]: 76 : && (logic.isTheoryEnabled(THEORY_ARRAYS)
[ - + ]
364 [ - + ]: 7 : || logic.isTheoryEnabled(THEORY_UF)))
365 : : {
366 [ - - ]: 0 : if (opts.bv.bitblastModeWasSetByUser
367 [ - - ]: 0 : || opts.smt.produceModelsWasSetByUser)
368 : : {
369 : 0 : std::stringstream ss;
370 : 0 : ss << "Eager bit-blasting currently does not support model generation ";
371 : 0 : ss << "for the combination of bit-vectors with arrays or uinterpreted ";
372 : 0 : ss << "functions. Try --" << options::bv::longName::bitblastMode << "="
373 : 0 : << options::BitblastMode::LAZY << ".";
374 : 0 : throw OptionException(ss.str());
375 : : }
376 [ - - ]: 0 : SET_AND_NOTIFY(
377 : : bv, bitblastMode, options::BitblastMode::LAZY, "model generation");
378 : : }
379 [ + + ]: 69 : else if (!opts.base.incrementalSolving)
380 : : {
381 : : // if not incremental, we rely on ackermann to eliminate other theories.
382 [ + + ]: 56 : SET_AND_NOTIFY(smt, ackermann, true, "bit-blast eager");
383 : : }
384 [ + + ][ - + ]: 13 : else if (logic.isQuantified() || !logic.isPure(THEORY_BV))
[ + + ]
385 : : {
386 : : // requested bitblast=eager in incremental mode, must be QF_BV only.
387 : : throw OptionException(
388 : 2 : std::string("Eager bit-blasting is only support in incremental mode "
389 : 3 : "if the logic is quantifier-free bit-vectors"));
390 : : }
391 : : }
392 : :
393 [ + + ]: 49265 : if (opts.smt.solveIntAsBV > 0)
394 : : {
395 : : // Int to BV currently always eliminates arithmetic completely (or otherwise
396 : : // fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors
397 : : // are required.
398 : 21 : logic = logic.getUnlockedCopy();
399 : 21 : logic.enableTheory(THEORY_BV);
400 : 21 : logic.disableTheory(THEORY_ARITH);
401 : 21 : logic.lock();
402 : : }
403 : :
404 [ + + ]: 49265 : if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
405 : : {
406 [ - + ]: 510 : if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
407 : : {
408 : 0 : std::stringstream ss;
409 : : ss << "solving bitvectors as integers is incompatible with --"
410 : 0 : << options::bv::longName::boolToBitvector << ".";
411 : 0 : throw OptionException(ss.str());
412 : : }
413 [ + + ]: 510 : if (logic.isTheoryEnabled(THEORY_BV))
414 : : {
415 : 502 : logic = logic.getUnlockedCopy();
416 : 502 : logic.enableIntegers();
417 : 502 : logic.arithNonLinear();
418 : 502 : logic.lock();
419 : : }
420 : : }
421 : :
422 : : // set options about ackermannization
423 [ + + ]: 137 : if (opts.smt.ackermann && opts.smt.produceModels
424 [ + + ][ + - ]: 49412 : && (logic.isTheoryEnabled(THEORY_ARRAYS)
[ + + ]
425 [ + + ]: 10 : || logic.isTheoryEnabled(THEORY_UF)))
426 : : {
427 [ - + ]: 4 : if (opts.smt.produceModelsWasSetByUser)
428 : : {
429 : 0 : throw OptionException(std::string(
430 : 0 : "Ackermannization currently does not support model generation."));
431 : : }
432 [ + - ]: 4 : SET_AND_NOTIFY(smt, ackermann, false, "model generation");
433 : : // we are not relying on ackermann to eliminate theories in this case
434 [ - + ][ - + ]: 4 : Assert(opts.bv.bitblastMode != options::BitblastMode::EAGER);
[ - - ]
435 : : }
436 : :
437 [ + + ]: 49265 : if (opts.smt.ackermann)
438 : : {
439 [ + + ]: 133 : if (logic.isTheoryEnabled(THEORY_UF))
440 : : {
441 : 69 : logic = logic.getUnlockedCopy();
442 : 69 : logic.disableTheory(THEORY_UF);
443 : 69 : logic.lock();
444 : : }
445 : : }
446 : :
447 : : // Set default options associated with strings-exp, which is enabled by
448 : : // default if the logic includes strings. Note that enabling stringExp
449 : : // enables quantifiers in the logic, and enables the bounded integer
450 : : // quantifiers module for processing *only* bounded quantifiers generated by
451 : : // the strings theory. It should not have an impact otherwise.
452 : 49265 : if (logic.isTheoryEnabled(THEORY_STRINGS)
453 [ + + ][ + + ]: 49265 : && !options().strings.stringExpWasSetByUser)
[ + + ]
454 : : {
455 [ + + ]: 29827 : SET_AND_NOTIFY(strings, stringExp, true, "logic including strings");
456 : : }
457 : : // If strings-exp is enabled, we require quantifiers. We also enable them
458 : : // if we are using eager string preprocessing or aggressive regular expression
459 : : // elimination, which may introduce quantified formulas at preprocess time.
460 [ + + ][ + - ]: 49265 : if (opts.strings.stringExp || !opts.strings.stringLazyPreproc
461 [ + + ]: 17992 : || opts.strings.regExpElim == options::RegExpElimMode::AGG)
462 : : {
463 : : // We require quantifiers since extended functions reduce using them.
464 [ + + ]: 31275 : if (!logic.isQuantified())
465 : : {
466 : 1304 : logic = logic.getUnlockedCopy();
467 : 1304 : logic.enableQuantifiers();
468 : 1304 : logic.lock();
469 [ + - ]: 2608 : Trace("smt") << "turning on quantifier logic, for strings-exp"
470 : 1304 : << std::endl;
471 : : }
472 : : // Note we allow E-matching by default to support combinations of sequences
473 : : // and quantifiers. We also do not enable fmfBound here, which would
474 : : // enable bounded integer instantiation for *all* quantifiers. Instead,
475 : : // the bounded integers module will always process internally generated
476 : : // quantifiers (those marked with InternalQuantAttribute).
477 : : }
478 : :
479 [ + + ]: 49265 : if (opts.arrays.arraysExp)
480 : : {
481 [ + + ]: 20 : if (!logic.isQuantified())
482 : : {
483 : 4 : logic = logic.getUnlockedCopy();
484 : 4 : logic.enableQuantifiers();
485 : 4 : logic.lock();
486 : : }
487 : : }
488 : :
489 : : // We now know whether the input uses sygus. Update the logic to incorporate
490 : : // the theories we need internally for handling sygus problems.
491 [ + + ]: 49265 : if (usesSygus(opts))
492 : : {
493 : 7399 : logic = logic.getUnlockedCopy();
494 : 7399 : logic.enableSygus();
495 : 7399 : logic.lock();
496 : : }
497 : :
498 : : // widen the logic
499 : 49265 : widenLogic(logic, opts);
500 : :
501 : : // check if we have any options that are not supported with quantified logics
502 [ + + ]: 49265 : if (logic.isQuantified())
503 : : {
504 : 84250 : std::stringstream reasonNoQuant;
505 [ - + ]: 42125 : if (incompatibleWithQuantifiers(opts, reasonNoQuant))
506 : : {
507 : 0 : std::stringstream ss;
508 : 0 : ss << reasonNoQuant.str() << " not supported in quantified logics.";
509 : 0 : throw OptionException(ss.str());
510 : : }
511 : : }
512 : : // check if we have separation logic heap types
513 [ + + ]: 49265 : if (d_env.hasSepHeap())
514 : : {
515 : 1642 : std::stringstream reasonNoSepLogic;
516 [ - + ]: 821 : if (incompatibleWithSeparationLogic(opts, reasonNoSepLogic))
517 : : {
518 : 0 : std::stringstream ss;
519 : 0 : ss << reasonNoSepLogic.str()
520 : 0 : << " not supported when using separation logic.";
521 : 0 : throw OptionException(ss.str());
522 : : }
523 : : }
524 : 49265 : }
525 : :
526 : 49265 : void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
527 : : {
528 [ - + ]: 49265 : SET_AND_NOTIFY(smt, produceAssertions, true, "always enabled");
529 : :
530 [ + + ]: 49265 : if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
531 : : {
532 : : /**
533 : : * Operations on 1 bits are better handled as Boolean operations
534 : : * than as integer operations.
535 : : * Therefore, we enable bv-to-bool, which runs before
536 : : * the translation to integers.
537 : : */
538 [ + + ]: 510 : SET_AND_NOTIFY(bv, bitvectorToBool, true, "solve-bv-as-int");
539 : : }
540 : :
541 : : // Disable options incompatible with incremental solving, or output an error
542 : : // if enabled explicitly.
543 [ + + ]: 49265 : if (opts.base.incrementalSolving)
544 : : {
545 : 42530 : std::stringstream reasonNoInc;
546 : 42530 : std::stringstream suggestNoInc;
547 [ - + ]: 21265 : if (incompatibleWithIncremental(logic, opts, reasonNoInc, suggestNoInc))
548 : : {
549 : 0 : std::stringstream ss;
550 : 0 : ss << reasonNoInc.str() << " not supported with incremental solving. "
551 : 0 : << suggestNoInc.str();
552 : 0 : throw OptionException(ss.str());
553 : : }
554 : : }
555 : :
556 : : // Disable options incompatible with unsat cores or output an error if enabled
557 : : // explicitly
558 [ + + ]: 49265 : if (opts.smt.produceUnsatCores)
559 : : {
560 : : // check if the options are not compatible with unsat cores
561 : 36428 : std::stringstream reasonNoUc;
562 [ - + ]: 18214 : if (incompatibleWithUnsatCores(opts, reasonNoUc))
563 : : {
564 : 0 : std::stringstream ss;
565 : 0 : ss << reasonNoUc.str() << " not supported with unsat cores";
566 : 0 : throw OptionException(ss.str());
567 : : }
568 : : }
569 : : else
570 : : {
571 : : // Turn on unconstrained simplification for QF_AUFBV
572 [ + + ]: 31051 : if (!opts.smt.unconstrainedSimpWasSetByUser
573 [ + + ]: 30964 : && !opts.base.incrementalSolving)
574 : : {
575 : : // It is also currently incompatible with arithmetic, force the option
576 : : // off.
577 [ + + ]: 15002 : bool uncSimp = !opts.base.incrementalSolving && !logic.isQuantified()
578 [ + + ][ + + ]: 1993 : && !opts.smt.produceModels && !opts.smt.produceAssignments
579 [ + - ]: 1183 : && !opts.smt.checkModels
580 [ + + ]: 1183 : && logic.isTheoryEnabled(THEORY_ARRAYS)
581 [ + + ]: 145 : && logic.isTheoryEnabled(THEORY_BV)
582 [ + - ][ + + ]: 30004 : && !logic.isTheoryEnabled(THEORY_ARITH);
583 [ + + ]: 15002 : SET_AND_NOTIFY_VAL_SYM(
584 : : smt, unconstrainedSimp, uncSimp, "logic and options");
585 : : }
586 : :
587 : : // by default, nonclausal simplification is off for QF_SAT
588 [ + + ]: 31051 : if (!opts.smt.simplificationModeWasSetByUser)
589 : : {
590 [ + + ][ + + ]: 31018 : bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
591 : : // simplification=none works better for SMT LIB benchmarks with
592 : : // quantifiers, not others
593 [ + + ]: 31018 : if (qf_sat)
594 : : {
595 [ + - ]: 5 : SET_AND_NOTIFY_VAL_SYM(smt,
596 : : simplificationMode,
597 : : options::SimplificationMode::NONE,
598 : : "logic");
599 : : }
600 : : else
601 : : {
602 [ - + ]: 31013 : SET_AND_NOTIFY_VAL_SYM(smt,
603 : : simplificationMode,
604 : : options::SimplificationMode::BATCH,
605 : : "logic");
606 : : }
607 : : }
608 : : }
609 : :
610 [ + + ][ + + ]: 49265 : if (opts.quantifiers.cegqiBv && logic.isQuantified())
[ + + ]
611 : : {
612 [ - + ]: 30512 : if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
613 : : {
614 [ - - ]: 0 : if (opts.bv.boolToBitvectorWasSetByUser)
615 : : {
616 : : throw OptionException(
617 : : "bool-to-bv != off not supported with CEGQI BV for quantified "
618 : 0 : "logics");
619 : : }
620 [ - - ]: 0 : SET_AND_NOTIFY_VAL_SYM(
621 : : bv, boolToBitvector, options::BoolToBVMode::OFF, "cegqiBv");
622 : : }
623 : : }
624 : :
625 : : // cases where we need produce models
626 [ + + ][ + + ]: 49265 : if (opts.smt.produceAssignments || usesSygus(opts))
[ + + ]
627 : : {
628 [ + + ]: 9714 : SET_AND_NOTIFY(smt, produceModels, true, "produce assignments or sygus");
629 : : }
630 : :
631 : : // --ite-simp is an experimental option designed for QF_LIA/nec. This
632 : : // technique is experimental. This benchmark set also requires removing ITEs
633 : : // during preprocessing, before repeating simplification. Hence, we enable
634 : : // this by default.
635 [ + + ]: 49265 : if (opts.smt.doITESimp)
636 : : {
637 [ + - ][ + - ]: 3 : SET_AND_NOTIFY_IF_NOT_USER(smt, earlyIteRemoval, true, "doITESimp");
[ + - ]
638 : : }
639 : :
640 : : // Set the options for the theoryOf
641 [ + + ]: 49265 : if (!opts.theory.theoryOfModeWasSetByUser)
642 : : {
643 [ + + ]: 93389 : if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
644 [ + + ]: 12657 : && !logic.isTheoryEnabled(THEORY_STRINGS)
645 [ + + ]: 11380 : && !logic.isTheoryEnabled(THEORY_SETS)
646 [ + - ]: 11247 : && !logic.isTheoryEnabled(THEORY_BAGS)
647 [ + + ][ + + ]: 94821 : && !(logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
[ + + ][ + + ]
648 [ + + ]: 1432 : && !logic.isQuantified()))
649 : : {
650 [ + + ]: 10347 : SET_AND_NOTIFY_VAL_SYM(theory,
651 : : theoryOfMode,
652 : : options::TheoryOfMode::THEORY_OF_TERM_BASED,
653 : : "logic");
654 : : }
655 : : }
656 : :
657 : : // by default, symmetry breaker is on only for non-incremental QF_UF
658 [ + - ]: 49265 : if (!opts.uf.ufSymmetryBreakerWasSetByUser)
659 : : {
660 : : // Only applies to non-incremental QF_UF.
661 [ + + ]: 49890 : bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
662 [ + + ][ + + ]: 49890 : && !opts.base.incrementalSolving;
663 : : // We disable this technique when using unsat core production, since it
664 : : // uses a non-standard implementation that sends (unsound) lemmas during
665 : : // presolve.
666 : : // We also disable it by default if safe unsat cores are enabled, or if
667 : : // the proof mode is FULL_STRICT.
668 [ + + ]: 462 : bool val = qf_uf_noinc && !safeUnsatCores(opts)
669 [ + + ][ + - ]: 49727 : && opts.smt.proofMode != options::ProofMode::FULL_STRICT;
670 [ + + ]: 49265 : SET_AND_NOTIFY_VAL_SYM(uf, ufSymmetryBreaker, val, "logic and options");
671 : : }
672 : :
673 : : // If in arrays, set the UF handler to arrays
674 [ + + ]: 80844 : if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder()
675 [ + + ]: 30609 : && !opts.quantifiers.finiteModelFind
676 [ + + ][ + + ]: 110137 : && (!logic.isQuantified()
[ + + ]
677 [ + - ][ - + ]: 29293 : || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
678 : : {
679 : 880 : d_env.setUninterpretedSortOwner(THEORY_ARRAYS);
680 : : }
681 : : else
682 : : {
683 : 48385 : d_env.setUninterpretedSortOwner(THEORY_UF);
684 : : }
685 : :
686 [ + - ]: 49265 : if (!opts.smt.simplifyWithCareEnabledWasSetByUser)
687 : : {
688 : : bool qf_aufbv =
689 [ + + ]: 56405 : !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
690 [ + + ][ + - ]: 56405 : && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV);
[ + + ]
691 [ + + ]: 49265 : SET_AND_NOTIFY_VAL_SYM(smt, simplifyWithCareEnabled, qf_aufbv, "logic");
692 : : }
693 : : // Turn off array eager index splitting for QF_AUFLIA
694 [ + - ]: 49265 : if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser)
695 : : {
696 [ + + ]: 56405 : if (!logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
697 [ + - ]: 888 : && logic.isTheoryEnabled(THEORY_UF)
698 [ + + ][ + + ]: 56405 : && logic.isTheoryEnabled(THEORY_ARITH))
[ + + ]
699 : : {
700 [ + + ]: 338 : SET_AND_NOTIFY(arrays, arraysEagerIndexSplitting, false, "logic");
701 : : }
702 : : }
703 : : // Turn on multiple-pass non-clausal simplification for QF_AUFBV
704 [ + + ]: 49265 : if (!opts.smt.repeatSimpWasSetByUser)
705 : : {
706 : 49245 : bool repeatSimp = !logic.isQuantified()
707 [ + + ]: 7130 : && (logic.isTheoryEnabled(THEORY_ARRAYS)
708 [ + - ]: 884 : && logic.isTheoryEnabled(THEORY_UF)
709 [ + + ]: 884 : && logic.isTheoryEnabled(THEORY_BV))
710 [ + + ][ + + ]: 56375 : && !safeUnsatCores(opts);
711 [ + + ]: 49245 : SET_AND_NOTIFY_VAL_SYM(smt, repeatSimp, repeatSimp, "logic");
712 : : }
713 : :
714 : : /* Disable bit-level propagation by default for the BITBLAST solver. */
715 [ + + ]: 49265 : if (opts.bv.bvSolver == options::BVSolver::BITBLAST)
716 : : {
717 [ + + ]: 38874 : SET_AND_NOTIFY(bv, bitvectorPropagate, false, "bitblast solver");
718 : : }
719 : :
720 : 98530 : if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL
721 [ + + ][ - + ]: 49265 : && !logic.isTheoryEnabled(THEORY_BV))
[ - + ]
722 : : {
723 [ - - ]: 0 : if (opts.bv.boolToBitvectorWasSetByUser)
724 : : {
725 : : throw OptionException(
726 : 0 : "bool-to-bv=all not supported for non-bitvector logics.");
727 : : }
728 [ - - ]: 0 : SET_AND_NOTIFY_VAL_SYM(
729 : : bv, boolToBitvector, options::BoolToBVMode::OFF, "non-BV logic");
730 : : }
731 : :
732 : : // Turn on arith rewrite equalities only for pure arithmetic
733 [ + + ]: 49265 : if (!opts.arith.arithRewriteEqWasSetByUser)
734 : : {
735 : : bool arithRewriteEq =
736 [ + + ][ + - ]: 49255 : logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
[ + + ]
737 [ + + ]: 49255 : SET_AND_NOTIFY_VAL_SYM(arith, arithRewriteEq, arithRewriteEq, "logic");
738 : : }
739 [ + - ]: 49265 : if (!opts.arith.arithHeuristicPivotsWasSetByUser)
740 : : {
741 : 49265 : int16_t heuristicPivots = 5;
742 [ + + ][ + + ]: 49265 : if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
[ + + ]
743 : : {
744 [ + + ]: 1092 : if (logic.isDifferenceLogic())
745 : : {
746 : 33 : heuristicPivots = -1;
747 : : }
748 [ + + ]: 1059 : else if (!logic.areIntegersUsed())
749 : : {
750 : 386 : heuristicPivots = 0;
751 : : }
752 : : }
753 [ + + ]: 49265 : SET_AND_NOTIFY_VAL_SYM(
754 : : arith, arithHeuristicPivots, heuristicPivots, "logic");
755 : : }
756 [ + - ]: 49265 : if (!opts.arith.arithPivotThresholdWasSetByUser)
757 : : {
758 : 49265 : uint16_t pivotThreshold = 2;
759 [ + + ][ + + ]: 49265 : if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
[ + + ]
760 : : {
761 [ + + ]: 1092 : if (logic.isDifferenceLogic())
762 : : {
763 : 33 : pivotThreshold = 16;
764 : : }
765 : : }
766 [ + + ]: 49265 : SET_AND_NOTIFY_VAL_SYM(arith, arithPivotThreshold, pivotThreshold, "logic");
767 : : }
768 [ + - ]: 49265 : if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser)
769 : : {
770 : 49265 : int16_t varOrderPivots = -1;
771 [ + + ][ + + ]: 49265 : if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
[ + + ]
772 : : {
773 : 1092 : varOrderPivots = 200;
774 : : }
775 [ + + ]: 49265 : SET_AND_NOTIFY_VAL_SYM(
776 : : arith, arithStandardCheckVarOrderPivots, varOrderPivots, "logic");
777 : : }
778 [ + + ][ + + ]: 49265 : if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
[ + + ]
779 : : {
780 [ + + ]: 734 : SET_AND_NOTIFY(
781 : : arith, nlExtTangentPlanesInterleave, true, "pure integer logic");
782 : : }
783 [ + - ]: 49265 : if (!opts.arith.nlRlvAssertBoundsWasSetByUser)
784 : : {
785 : 49265 : bool val = !logic.isQuantified();
786 : : // use bound inference to determine when bounds are irrelevant only when
787 : : // the logic is quantifier-free
788 [ + + ]: 49265 : SET_AND_NOTIFY_VAL_SYM(
789 : : arith, nlRlvAssertBounds, val, "non-quantified logic");
790 : : }
791 : :
792 : : // set the default decision mode
793 : 49265 : setDefaultDecisionMode(logic, opts);
794 : :
795 : : // set up of central equality engine
796 [ + + ]: 49265 : if (opts.theory.eeMode == options::EqEngineMode::CENTRAL)
797 : : {
798 : : // use the arithmetic equality solver by default
799 [ + + ][ + + ]: 59 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
800 : : arith, arithEqSolver, true, "central equality engine");
801 : : }
802 : :
803 [ + + ]: 49265 : if (logic.isHigherOrder())
804 : : {
805 [ + + ]: 1160 : SET_AND_NOTIFY(theory, assignFunctionValues, true, "higher-order logic");
806 : : }
807 : :
808 : : // set all defaults in the quantifiers theory, which includes sygus
809 : 49265 : setDefaultsQuantifiers(logic, opts);
810 : :
811 : : // shared selectors are generally not good to combine with standard
812 : : // quantifier techniques e.g. E-matching
813 [ + + ][ + + ]: 49263 : if (logic.isQuantified() && !usesSygus(opts))
[ + + ]
814 : : {
815 [ + + ][ + + ]: 34726 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
816 : : datatypes, dtSharedSelectors, false, "quantified logic without SyGuS");
817 : : }
818 : :
819 [ + + ]: 49263 : if (opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL)
820 : : {
821 : : // cannot use minisat variable elimination for logics where a theory solver
822 : : // introduces new literals into the search, or for parametric theories
823 : : // which may introduce Boolean term variables. This includes quantifiers
824 : : // (quantifier instantiation), and the lemma schemas used in non-linear
825 : : // and sets. We also can't use it if models are enabled.
826 [ + - ]: 45414 : if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS)
827 [ + + ]: 10613 : || logic.isTheoryEnabled(THEORY_ARRAYS)
828 [ + + ]: 9189 : || logic.isTheoryEnabled(THEORY_STRINGS)
829 [ + + ][ + + ]: 8106 : || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isQuantified()
830 [ + + ][ + - ]: 5995 : || opts.smt.produceModels || opts.smt.produceAssignments
831 [ + - ]: 5130 : || opts.smt.checkModels
832 [ + + ][ + + ]: 45414 : || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
[ + + ][ + + ]
833 : : {
834 [ + - ][ + - ]: 30565 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(prop,
[ + - ]
835 : : minisatSimpMode,
836 : : options::MinisatSimpMode::CLAUSE_ELIM,
837 : : "non-basic logic");
838 : : }
839 : : }
840 : :
841 [ + + ]: 93899 : if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
842 [ + + ][ + + ]: 93899 : && opts.arith.nlRlvMode != options::NlRlvMode::NONE)
[ + + ]
843 : : {
844 [ + - ]: 8 : SET_AND_NOTIFY(theory, relevanceFilter, true, "nl relevance mode");
845 : : }
846 : :
847 : : // For now, these array theory optimizations do not support model-building
848 [ + + ][ + - ]: 49263 : if (opts.smt.produceModels || opts.smt.produceAssignments
849 [ - + ]: 27244 : || opts.smt.checkModels)
850 : : {
851 [ + + ]: 22019 : SET_AND_NOTIFY(arrays, arraysOptimizeLinear, false, "models");
852 : : }
853 : :
854 [ + + ]: 49263 : if (opts.strings.stringFMF)
855 : : {
856 [ + - ][ + + ]: 60 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(strings,
[ + + ]
857 : : stringProcessLoopMode,
858 : : options::ProcessLoopMode::SIMPLE,
859 : : "strings-fmf");
860 : : }
861 : :
862 : : // !!! All options that require disabling models go here
863 : 98526 : std::stringstream reasonNoModel;
864 [ + + ]: 49263 : if (incompatibleWithModels(opts, reasonNoModel))
865 : : {
866 : 8892 : std::string sOptNoModel = reasonNoModel.str();
867 [ + + ]: 4446 : if (opts.smt.produceModels)
868 : : {
869 [ + + ]: 48 : if (opts.smt.produceModelsWasSetByUser)
870 : : {
871 : 2 : std::stringstream ss;
872 : 1 : ss << "Cannot use " << sOptNoModel << " with model generation.";
873 : 1 : throw OptionException(ss.str());
874 : : }
875 [ + - ]: 47 : SET_AND_NOTIFY(smt, produceModels, false, sOptNoModel);
876 : : }
877 [ + + ]: 4445 : if (opts.smt.produceAssignments)
878 : : {
879 [ - + ]: 47 : if (opts.smt.produceAssignmentsWasSetByUser)
880 : : {
881 : 0 : std::stringstream ss;
882 : : ss << "Cannot use " << sOptNoModel
883 : 0 : << " with model generation (produce-assignments).";
884 : 0 : throw OptionException(ss.str());
885 : : }
886 [ + - ]: 47 : SET_AND_NOTIFY(smt, produceAssignments, false, sOptNoModel);
887 : : }
888 [ + + ]: 4445 : if (opts.smt.checkModels)
889 : : {
890 [ - + ]: 47 : if (opts.smt.checkModelsWasSetByUser)
891 : : {
892 : 0 : std::stringstream ss;
893 : : ss << "Cannot use " << sOptNoModel
894 : 0 : << " with model generation (check-models).";
895 : 0 : throw OptionException(ss.str());
896 : : }
897 [ + - ]: 47 : SET_AND_NOTIFY(smt, checkModels, false, sOptNoModel);
898 : : }
899 : : }
900 : :
901 : 98524 : if (opts.bv.bitblastMode == options::BitblastMode::EAGER
902 [ + + ][ - + ]: 49262 : && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV")
[ - - ][ - + ]
[ - + ][ - - ]
903 : : {
904 : : throw OptionException(
905 : : "Eager bit-blasting does not currently support theory combination with "
906 : 0 : "any theory other than UF. ");
907 : : }
908 : :
909 : : #ifdef CVC5_USE_POLY
910 [ + + ]: 49262 : if (logic == LogicInfo("QF_UFNRA"))
911 : : {
912 [ + + ][ + - ]: 265 : if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
913 : : {
914 [ + - ]: 236 : SET_AND_NOTIFY(arith, nlCov, true, "QF_UFNRA");
915 [ + + ][ + - ]: 236 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + + ]
916 : : arith, nlExt, options::NlExtMode::LIGHT, "QF_UFNRA");
917 : : }
918 : : }
919 [ + + ]: 91119 : else if (logic.isQuantified() && logic.isTheoryEnabled(theory::THEORY_ARITH)
920 [ + + ][ + + ]: 41531 : && logic.areRealsUsed() && !logic.areIntegersUsed()
921 [ + + ][ + + ]: 91119 : && !logic.areTranscendentalsUsed())
[ + + ]
922 : : {
923 [ + + ][ + - ]: 168 : if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
924 : : {
925 [ + - ]: 136 : SET_AND_NOTIFY(arith, nlCov, true, "logic with reals");
926 [ + - ][ + - ]: 136 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + - ]
927 : : arith, nlExt, options::NlExtMode::LIGHT, "logic with reals");
928 : : }
929 : : }
930 : : #else
931 : : if (opts.arith.nlCov)
932 : : {
933 : : if (opts.arith.nlCovWasSetByUser)
934 : : {
935 : : std::stringstream ss;
936 : : ss << "Cannot use --" << options::arith::longName::nlCov
937 : : << " without configuring with --poly.";
938 : : throw OptionException(ss.str());
939 : : }
940 : : else
941 : : {
942 : : SET_AND_NOTIFY(arith, nlCov, false, "no support for libpoly");
943 : : SET_AND_NOTIFY_VAL_SYM(
944 : : arith, nlExt, options::NlExtMode::FULL, "no support for libpoly");
945 : : }
946 : : }
947 : : #endif
948 [ + + ][ + + ]: 49262 : if (logic.isTheoryEnabled(theory::THEORY_ARITH) && logic.areTranscendentalsUsed())
[ + + ]
949 : : {
950 [ + + ][ - + ]: 30236 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ - + ]
951 : : arith, nlExt, options::NlExtMode::FULL, "logic with transcendentals");
952 : : }
953 : 49262 : }
954 : :
955 : 304405 : bool SetDefaults::isSygus(const Options& opts) const
956 : : {
957 [ + + ]: 304405 : if (opts.quantifiers.sygus)
958 : : {
959 : 40226 : return true;
960 : : }
961 [ + + ]: 264179 : if (!d_isInternalSubsolver)
962 : : {
963 [ + + ][ + + ]: 195832 : if (opts.smt.produceAbducts || opts.smt.produceInterpolants
964 [ + + ]: 192838 : || opts.quantifiers.sygusInference != options::SygusInferenceMode::OFF)
965 : : {
966 : : // since we are trying to recast as sygus, we assume the input is sygus
967 : 3287 : return true;
968 : : }
969 : : }
970 : 260892 : return false;
971 : : }
972 : :
973 : 187271 : bool SetDefaults::usesSygus(const Options& opts) const
974 : : {
975 [ + + ]: 187271 : if (isSygus(opts))
976 : : {
977 : 28947 : return true;
978 : : }
979 [ + + ][ + + ]: 158324 : if (!d_isInternalSubsolver && opts.quantifiers.sygusInst)
980 : : {
981 : : // sygus instantiation uses sygus, but it is not a sygus problem
982 : 508 : return true;
983 : : }
984 : 157816 : return false;
985 : : }
986 : :
987 : 7267 : bool SetDefaults::usesInputConversion(const Options& opts,
988 : : std::ostream& reason) const
989 : : {
990 [ + + ]: 7267 : if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
991 : : {
992 : 1 : reason << "solveBVAsInt";
993 : 1 : return true;
994 : : }
995 [ - + ]: 7266 : if (opts.smt.solveIntAsBV > 0)
996 : : {
997 : 0 : reason << "solveIntAsBV";
998 : 0 : return true;
999 : : }
1000 [ - + ]: 7266 : if (opts.smt.solveRealAsInt)
1001 : : {
1002 : 0 : reason << "solveRealAsInt";
1003 : 0 : return true;
1004 : : }
1005 : 7266 : return false;
1006 : : }
1007 : :
1008 : 18622 : bool SetDefaults::incompatibleWithProofs(Options& opts,
1009 : : std::ostream& reason) const
1010 : : {
1011 [ - + ]: 18622 : if (opts.parser.freshBinders)
1012 : : {
1013 : : // When fresh-binders is true, we do not support proof output.
1014 : 0 : reason << "fresh-binders";
1015 : 0 : return true;
1016 : : }
1017 [ + + ]: 18622 : if (opts.quantifiers.globalNegate)
1018 : : {
1019 : : // When global negate answers "unsat", it is not due to showing a set of
1020 : : // formulas is unsat. Thus, proofs do not apply.
1021 : 1 : reason << "global-negate";
1022 : 1 : return true;
1023 : : }
1024 : 37242 : bool isFullPf = (opts.smt.proofMode == options::ProofMode::FULL
1025 [ + + ][ - + ]: 18621 : || opts.smt.proofMode == options::ProofMode::FULL_STRICT);
1026 [ + + ]: 18621 : if (isSygus(opts))
1027 : : {
1028 : : // we don't support proofs with SyGuS. One issue is that SyGuS evaluation
1029 : : // functions are incompatible with our equality proofs. Moreover, enabling
1030 : : // proofs for sygus (sub)solvers is irrelevant, since they are not given
1031 : : // check-sat queries. Note however that we allow proofs in non-full modes
1032 : : // (e.g. unsat cores).
1033 [ - + ]: 32 : if (isFullPf)
1034 : : {
1035 : 0 : reason << "sygus";
1036 : 0 : return true;
1037 : : }
1038 : : }
1039 : : // options that are automatically set to support proofs
1040 [ + + ]: 18621 : if (opts.bv.bvAssertInput)
1041 : : {
1042 [ + - ]: 3 : SET_AND_NOTIFY_VAL_SYM(bv, bvAssertInput, false, "proofs");
1043 : : }
1044 : : // If proofs are required and the user did not specify a specific BV solver,
1045 : : // we make sure to use the proof producing BITBLAST_INTERNAL solver.
1046 [ + + ]: 18621 : if (isFullPf)
1047 : : {
1048 [ + + ][ + + ]: 10364 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + + ]
1049 : : bv, bvSolver, options::BVSolver::BITBLAST_INTERNAL, "proofs");
1050 : : }
1051 [ + - ][ + + ]: 18621 : SET_AND_NOTIFY_IF_NOT_USER(arith, nlCovVarElim, false, "proofs");
[ + + ]
1052 [ - + ]: 18621 : if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
1053 : : {
1054 : 0 : reason << "deep restarts";
1055 : 0 : return true;
1056 : : }
1057 : : // specific to SAT solver
1058 [ + + ]: 18621 : if (opts.prop.satSolver == options::SatSolverMode::CADICAL)
1059 : : {
1060 [ - + ]: 24 : if (opts.proof.propProofMode == options::PropProofMode::PROOF)
1061 : : {
1062 : 0 : reason << "(resolution) proofs not supported in cadical";
1063 : 0 : return true;
1064 : : }
1065 : : }
1066 [ + - ]: 18597 : else if (opts.prop.satSolver == options::SatSolverMode::MINISAT)
1067 : : {
1068 [ - + ]: 18597 : if (opts.proof.propProofMode == options::PropProofMode::SKETCH)
1069 : : {
1070 : 0 : reason << "(DRAT) proof sketch not supported in minisat";
1071 : 0 : return true;
1072 : : }
1073 : : }
1074 [ - + ]: 18621 : if (options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE)
1075 : : {
1076 : : // lemma inprocessing introduces depencencies from learned unit literals
1077 : : // that are not tracked.
1078 : 0 : reason << "lemma inprocessing";
1079 : 0 : return true;
1080 : : }
1081 : 18621 : return false;
1082 : : }
1083 : :
1084 : 49263 : bool SetDefaults::incompatibleWithModels(const Options& opts,
1085 : : std::ostream& reason) const
1086 : : {
1087 [ + + ][ + + ]: 49263 : if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp)
1088 : : {
1089 : 166 : reason << "unconstrained-simp";
1090 : 166 : return true;
1091 : : }
1092 [ + + ]: 49097 : else if (opts.smt.sortInference)
1093 : : {
1094 : 35 : reason << "sort-inference";
1095 : 35 : return true;
1096 : : }
1097 [ + + ]: 49062 : else if (opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL)
1098 : : {
1099 : 4235 : reason << "minisat-simplification";
1100 : 4235 : return true;
1101 : : }
1102 [ + + ]: 44827 : else if (opts.quantifiers.globalNegate)
1103 : : {
1104 : 9 : reason << "global-negate";
1105 : 9 : return true;
1106 : : }
1107 [ + + ]: 44818 : else if (opts.arrays.arraysWeakEquivalence)
1108 : : {
1109 : 1 : reason << "arrays-weak-equiv";
1110 : 1 : return true;
1111 : : }
1112 : 44817 : return false;
1113 : : }
1114 : :
1115 : 21265 : bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
1116 : : Options& opts,
1117 : : std::ostream& reason,
1118 : : std::ostream& suggest) const
1119 : : {
1120 [ - + ]: 21265 : if (d_env.hasSepHeap())
1121 : : {
1122 : 0 : reason << "separation logic";
1123 : 0 : return true;
1124 : : }
1125 [ - + ]: 21265 : if (opts.smt.ackermann)
1126 : : {
1127 : 0 : reason << "ackermann";
1128 : 0 : return true;
1129 : : }
1130 [ - + ]: 21265 : if (opts.smt.unconstrainedSimp)
1131 : : {
1132 [ - - ]: 0 : if (opts.smt.unconstrainedSimpWasSetByUser)
1133 : : {
1134 : 0 : reason << "unconstrained simplification";
1135 : 0 : return true;
1136 : : }
1137 [ - - ]: 0 : SET_AND_NOTIFY(smt, unconstrainedSimp, false, "incremental solving");
1138 : : }
1139 : 42530 : if (opts.bv.bitblastMode == options::BitblastMode::EAGER
1140 [ + + ][ - + ]: 21265 : && !logic.isPure(THEORY_BV))
[ - + ]
1141 : : {
1142 : 0 : reason << "eager bit-blasting in non-QF_BV logic";
1143 : 0 : suggest << "Try --" << options::bv::longName::bitblastMode << "="
1144 : 0 : << options::BitblastMode::LAZY << ".";
1145 : 0 : return true;
1146 : : }
1147 [ - + ]: 21265 : if (opts.quantifiers.sygusInference != options::SygusInferenceMode::OFF)
1148 : : {
1149 [ - - ]: 0 : if (opts.quantifiers.sygusInferenceWasSetByUser)
1150 : : {
1151 : 0 : reason << "sygus inference";
1152 : 0 : return true;
1153 : : }
1154 [ - - ]: 0 : SET_AND_NOTIFY_VAL_SYM(quantifiers,
1155 : : sygusInference,
1156 : : options::SygusInferenceMode::OFF,
1157 : : "incremental solving");
1158 : : }
1159 [ - + ]: 21265 : if (opts.quantifiers.sygusInst)
1160 : : {
1161 [ - - ]: 0 : if (opts.quantifiers.sygusInstWasSetByUser)
1162 : : {
1163 : 0 : reason << "sygus inst";
1164 : 0 : return true;
1165 : : }
1166 [ - - ]: 0 : SET_AND_NOTIFY(quantifiers, sygusInst, false, "incremental solving");
1167 : : }
1168 [ - + ]: 21265 : if (opts.smt.solveIntAsBV > 0)
1169 : : {
1170 : 0 : reason << "solveIntAsBV";
1171 : 0 : return true;
1172 : : }
1173 [ - + ]: 21265 : if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
1174 : : {
1175 : 0 : reason << "deep restarts";
1176 : 0 : return true;
1177 : : }
1178 [ - + ]: 21265 : if (opts.parallel.computePartitions > 1)
1179 : : {
1180 : 0 : reason << "compute partitions";
1181 : 0 : return true;
1182 : : }
1183 : :
1184 : : // disable modes not supported by incremental
1185 [ - + ]: 21265 : SET_AND_NOTIFY(smt, sortInference, false, "incremental solving");
1186 [ - + ]: 21265 : SET_AND_NOTIFY(uf, ufssFairnessMonotone, false, "incremental solving");
1187 [ - + ]: 21265 : SET_AND_NOTIFY(quantifiers, globalNegate, false, "incremental solving");
1188 [ - + ]: 21265 : SET_AND_NOTIFY(quantifiers, cegqiNestedQE, false, "incremental solving");
1189 [ - + ]: 21265 : SET_AND_NOTIFY(arith, arithMLTrick, false, "incremental solving");
1190 : 21265 : return false;
1191 : : }
1192 : :
1193 : 18214 : bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
1194 : : std::ostream& reason) const
1195 : : {
1196 : : // All techniques that are incompatible with unsat cores are listed here.
1197 : : // A preprocessing pass is incompatible with unsat cores if
1198 : : // (A) its reasoning is not local, i.e. it may replace an assertion A by A'
1199 : : // where A does not imply A', or if it adds new assertions B that are not
1200 : : // tautologies, AND
1201 : : // (B) it does not track proofs.
1202 [ - + ]: 18214 : if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
1203 : : {
1204 [ - - ]: 0 : if (opts.smt.deepRestartModeWasSetByUser)
1205 : : {
1206 : 0 : reason << "deep restarts";
1207 : 0 : return true;
1208 : : }
1209 [ - - ]: 0 : SET_AND_NOTIFY_VAL_SYM(
1210 : : smt, deepRestartMode, options::DeepRestartMode::NONE, "unsat cores");
1211 : : }
1212 [ - + ]: 18214 : if (opts.smt.learnedRewrite)
1213 : : {
1214 [ - - ]: 0 : if (opts.smt.learnedRewriteWasSetByUser)
1215 : : {
1216 : 0 : reason << "learned rewrites";
1217 : 0 : return true;
1218 : : }
1219 [ - - ]: 0 : SET_AND_NOTIFY(smt, learnedRewrite, false, "unsat cores");
1220 : : }
1221 : : // most static learning techniques are local, although arithmetic static
1222 : : // learning is not.
1223 [ + + ]: 18214 : if (opts.arith.arithStaticLearning)
1224 : : {
1225 [ - + ]: 14728 : if (opts.arith.arithStaticLearningWasSetByUser)
1226 : : {
1227 : 0 : reason << "arith static learning";
1228 : 0 : return true;
1229 : : }
1230 [ + - ]: 14728 : SET_AND_NOTIFY(arith, arithStaticLearning, false, "unsat cores");
1231 : : }
1232 : :
1233 [ - + ]: 18214 : if (opts.arith.pbRewrites)
1234 : : {
1235 [ - - ]: 0 : if (opts.arith.pbRewritesWasSetByUser)
1236 : : {
1237 : 0 : reason << "pseudoboolean rewrites";
1238 : 0 : return true;
1239 : : }
1240 [ - - ]: 0 : SET_AND_NOTIFY(arith, pbRewrites, false, "unsat cores");
1241 : : }
1242 : :
1243 [ - + ]: 18214 : if (opts.quantifiers.globalNegate)
1244 : : {
1245 [ - - ]: 0 : if (opts.quantifiers.globalNegateWasSetByUser)
1246 : : {
1247 : 0 : reason << "global-negate";
1248 : 0 : return true;
1249 : : }
1250 [ - - ]: 0 : SET_AND_NOTIFY(quantifiers, globalNegate, false, "unsat cores");
1251 : : }
1252 : :
1253 [ - + ]: 18214 : if (opts.smt.doITESimp)
1254 : : {
1255 : 0 : reason << "ITE simp";
1256 : 0 : return true;
1257 : : }
1258 : 18214 : return false;
1259 : : }
1260 : :
1261 : 962 : bool SetDefaults::safeUnsatCores(const Options& opts) const
1262 : : {
1263 : : // whether we want to force safe unsat cores, i.e., if we are in the default
1264 : : // ASSUMPTIONS mode, since other ones are experimental
1265 : 962 : return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
1266 : : }
1267 : :
1268 : 7267 : bool SetDefaults::incompatibleWithSygus(const Options& opts,
1269 : : std::ostream& reason) const
1270 : : {
1271 : : // sygus should not be combined with preprocessing passes that convert the
1272 : : // input
1273 [ + + ]: 7267 : if (usesInputConversion(opts, reason))
1274 : : {
1275 : 1 : return true;
1276 : : }
1277 [ - + ]: 7266 : if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
1278 : : {
1279 : 0 : reason << "deep restarts";
1280 : 0 : return true;
1281 : : }
1282 [ + + ]: 7266 : if (opts.quantifiers.globalNegate)
1283 : : {
1284 : 1 : reason << "global negate";
1285 : 1 : return true;
1286 : : }
1287 : 7265 : return false;
1288 : : }
1289 : :
1290 : 42125 : bool SetDefaults::incompatibleWithQuantifiers(const Options& opts,
1291 : : std::ostream& reason) const
1292 : : {
1293 [ - + ]: 42125 : if (opts.smt.ackermann)
1294 : : {
1295 : 0 : reason << "ackermann";
1296 : 0 : return true;
1297 : : }
1298 [ - + ]: 42125 : if (opts.arith.nlRlvMode != options::NlRlvMode::NONE)
1299 : : {
1300 : : // Theory relevance is incompatible with CEGQI and SyQI, since there is no
1301 : : // appropriate policy for the relevance of counterexample lemmas (when their
1302 : : // guard is entailed to be false, the entire lemma is relevant, not just the
1303 : : // guard). Hence, we throw an option exception if quantifiers are enabled.
1304 : 0 : reason << "--" << options::arith::longName::nlRlvMode;
1305 : 0 : return true;
1306 : : }
1307 : 42125 : return false;
1308 : : }
1309 : :
1310 : 821 : bool SetDefaults::incompatibleWithSeparationLogic(Options& opts,
1311 : : std::ostream& reason) const
1312 : : {
1313 : : // Spatial formulas in separation logic have a semantics that depends on
1314 : : // their position in the AST (e.g. their nesting beneath separation
1315 : : // conjunctions). Thus, we cannot apply BCP as a substitution for spatial
1316 : : // predicates to the input formula. We disable this option altogether to
1317 : : // ensure this is the case
1318 [ - + ]: 821 : SET_AND_NOTIFY(smt, simplificationBoolConstProp, false, "separation logic");
1319 : 821 : return false;
1320 : : }
1321 : :
1322 : 49265 : void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
1323 : : {
1324 : 49265 : bool needsUf = false;
1325 : : // strings require LIA, UF; widen the logic
1326 [ + + ]: 49265 : if (logic.isTheoryEnabled(THEORY_STRINGS))
1327 : : {
1328 : 62502 : LogicInfo log(logic.getUnlockedCopy());
1329 : : // Strings requires arith for length constraints, and also UF
1330 : 31251 : needsUf = true;
1331 [ + + ][ - + ]: 31251 : if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
[ + + ]
1332 : : {
1333 : 257 : verbose(1)
1334 : 257 : << "Enabling linear integer arithmetic because strings are enabled"
1335 : 257 : << std::endl;
1336 : 257 : log.enableTheory(THEORY_ARITH);
1337 : 257 : log.enableIntegers();
1338 : 257 : log.arithOnlyLinear();
1339 : : }
1340 [ - + ]: 30994 : else if (!logic.areIntegersUsed())
1341 : : {
1342 : 0 : verbose(1) << "Enabling integer arithmetic because strings are enabled"
1343 : 0 : << std::endl;
1344 : 0 : log.enableIntegers();
1345 : : }
1346 : 31251 : logic = log;
1347 : 31251 : logic.lock();
1348 : : }
1349 [ + + ]: 49265 : if (opts.quantifiers.globalNegate)
1350 : : {
1351 : 20 : LogicInfo log(logic.getUnlockedCopy());
1352 : 10 : log.enableQuantifiers();
1353 : 10 : logic = log;
1354 : 10 : logic.lock();
1355 : : }
1356 [ + + ]: 49265 : if (opts.quantifiers.preSkolemQuantNested
1357 [ + + ]: 49236 : && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
1358 : : {
1359 : : // if pre-skolem nested is explictly set, then we require UF. If it is
1360 : : // not explicitly set, it is disabled below if UF is not present.
1361 : 2 : verbose(1) << "Enabling UF because preSkolemQuantNested requires it."
1362 : 2 : << std::endl;
1363 : 2 : needsUf = true;
1364 : : }
1365 : 49265 : if (needsUf
1366 : : // Arrays, datatypes and sets permit Boolean terms and thus require UF
1367 [ + + ]: 18012 : || logic.isTheoryEnabled(THEORY_ARRAYS)
1368 [ + + ]: 16407 : || logic.isTheoryEnabled(THEORY_DATATYPES)
1369 [ + + ]: 7459 : || logic.isTheoryEnabled(THEORY_SETS)
1370 [ + - ]: 7351 : || logic.isTheoryEnabled(THEORY_BAGS)
1371 : : // Non-linear arithmetic requires UF to deal with division/mod because
1372 : : // their expansion introduces UFs for the division/mod-by-zero case.
1373 : : // If we are eliminating non-linear arithmetic via solve-int-as-bv,
1374 : : // then this is not required, since non-linear arithmetic will be
1375 : : // eliminated altogether (or otherwise fail at preprocessing).
1376 [ + + ][ + + ]: 7351 : || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
1377 [ - + ]: 1428 : && opts.smt.solveIntAsBV == 0)
1378 : : // If arithmetic and bv are enabled, it is possible to use bv2nat and
1379 : : // int2bv, which require the UF theory.
1380 [ + + ]: 5923 : || (logic.isTheoryEnabled(THEORY_ARITH)
1381 [ + + ]: 1921 : && logic.isTheoryEnabled(THEORY_BV))
1382 : : // FP requires UF since there are multiple operators that are partially
1383 : : // defined (see http://smt-lib.org/papers/BTRW15.pdf for more
1384 : : // details).
1385 [ + + ][ + + ]: 67277 : || logic.isTheoryEnabled(THEORY_FP))
[ + + ]
1386 : : {
1387 [ + + ]: 43502 : if (!logic.isTheoryEnabled(THEORY_UF))
1388 : : {
1389 : 4734 : LogicInfo log(logic.getUnlockedCopy());
1390 [ + + ]: 2367 : if (!needsUf)
1391 : : {
1392 : 1419 : verbose(1) << "Enabling UF because " << logic << " requires it."
1393 : 1419 : << std::endl;
1394 : : }
1395 : 2367 : log.enableTheory(THEORY_UF);
1396 : 2367 : logic = log;
1397 : 2367 : logic.lock();
1398 : : }
1399 : : }
1400 [ + + ]: 49265 : if (opts.arith.arithMLTrick)
1401 : : {
1402 [ - + ]: 8 : if (!logic.areIntegersUsed())
1403 : : {
1404 : : // enable integers
1405 : 0 : LogicInfo log(logic.getUnlockedCopy());
1406 : 0 : verbose(1) << "Enabling integers because arithMLTrick requires it."
1407 : 0 : << std::endl;
1408 : 0 : log.enableIntegers();
1409 : 0 : logic = log;
1410 : 0 : logic.lock();
1411 : : }
1412 : : }
1413 : 49265 : }
1414 : :
1415 : 49265 : void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
1416 : : Options& opts) const
1417 : : {
1418 [ + + ]: 49265 : if (opts.quantifiers.fullSaturateQuant)
1419 : : {
1420 [ + + ]: 252 : SET_AND_NOTIFY(quantifiers, enumInst, true, "full-saturate-quant");
1421 : : }
1422 [ + + ]: 49265 : if (opts.arrays.arraysExp)
1423 : : {
1424 : : // Allows to answer sat more often by default.
1425 [ + - ][ + + ]: 20 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, fmfBound, true, "arrays-exp");
[ + + ]
1426 : : }
1427 [ + + ]: 49265 : if (logic.hasCardinalityConstraints())
1428 : : {
1429 : : // must have finite model finding on
1430 [ + + ]: 44 : SET_AND_NOTIFY(quantifiers,
1431 : : finiteModelFind,
1432 : : true,
1433 : : "logic with cardinality constraints");
1434 : : }
1435 [ + + ]: 49265 : if (opts.quantifiers.instMaxLevel != -1)
1436 : : {
1437 [ - + ]: 6 : SET_AND_NOTIFY(quantifiers, cegqi, false, "instMaxLevel");
1438 : : }
1439 : : // enable MBQI if --mbqi-fast-sygus is provided
1440 [ + + ]: 49265 : if (opts.quantifiers.mbqiFastSygus)
1441 : : {
1442 [ + + ][ + + ]: 333 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, mbqi, true, "mbqiFastSygus");
[ + + ]
1443 : : }
1444 [ + + ]: 49265 : if (opts.quantifiers.mbqi)
1445 : : {
1446 : : // MBQI is an alternative to CEGQI/SyQI
1447 [ + + ][ + + ]: 517 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqi, false, "mbqi");
[ + + ]
1448 [ + - ][ - + ]: 517 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, sygusInst, false, "mbqi");
[ - + ]
1449 : : }
1450 : :
1451 [ + + ]: 49265 : if (opts.quantifiers.fmfBoundLazy)
1452 : : {
1453 [ + - ][ + + ]: 8 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, fmfBound, true, "fmfBoundLazy");
[ + + ]
1454 : : }
1455 : : // now have determined whether fmfBound is on/off
1456 : : // apply fmfBound options
1457 [ + + ]: 49265 : if (opts.quantifiers.fmfBound)
1458 : : {
1459 : : // if bounded integers are set, use no MBQI by default
1460 [ + - ][ + + ]: 219 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + + ]
1461 : : quantifiers, fmfMbqiMode, options::FmfMbqiMode::NONE, "fmfBound");
1462 [ + - ][ + + ]: 219 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + + ]
1463 : : quantifiers, prenexQuant, options::PrenexQuantMode::NONE, "fmfBound");
1464 : : }
1465 [ + + ]: 49265 : if (logic.isHigherOrder())
1466 : : {
1467 : : // if higher-order, then current variants of model-based instantiation
1468 : : // cannot be used
1469 [ + + ]: 1160 : SET_AND_NOTIFY_VAL_SYM(quantifiers,
1470 : : fmfMbqiMode,
1471 : : options::FmfMbqiMode::NONE,
1472 : : "higher-order logic");
1473 : : // by default, use store axioms only if --ho-elim is set
1474 [ + + ][ + + ]: 1160 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1475 : : hoElimStoreAx,
1476 : : opts.quantifiers.hoElim,
1477 : : "higher-order logic");
1478 : : // Cannot use macros, since lambda lifting and macro elimination are inverse
1479 : : // operations.
1480 [ - + ]: 1160 : SET_AND_NOTIFY(quantifiers, macrosQuant, false, "higher-order logic");
1481 : : }
1482 [ + + ]: 49265 : if (opts.quantifiers.fmfFunWellDefinedRelevant)
1483 : : {
1484 [ + - ][ + + ]: 32 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1485 : : quantifiers, fmfFunWellDefined, true, "fmfFunWellDefinedRelevant");
1486 : : }
1487 [ + + ]: 49265 : if (opts.quantifiers.fmfFunWellDefined)
1488 : : {
1489 [ + + ][ + + ]: 159 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1490 : : quantifiers, finiteModelFind, true, "fmfFunWellDefined");
1491 : : }
1492 : :
1493 : : // now, have determined whether finite model find is on/off
1494 : : // apply finite model finding options
1495 [ + + ]: 49265 : if (opts.quantifiers.finiteModelFind)
1496 : : {
1497 : : // apply conservative quantifiers splitting
1498 [ + - ][ + + ]: 721 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1499 : : quantDynamicSplit,
1500 : : options::QuantDSplitMode::DEFAULT,
1501 : : "finiteModelFind");
1502 : : // do not use E-matching by default. For E-matching + FMF, the user should
1503 : : // specify --finite-model-find --e-matching.
1504 [ + + ][ + + ]: 721 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1505 : : quantifiers, eMatching, false, "finiteModelFind");
1506 : : // instantiate only on last call
1507 [ + + ]: 721 : if (opts.quantifiers.eMatching)
1508 : : {
1509 [ + - ][ + + ]: 12 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1510 : : instWhenMode,
1511 : : options::InstWhenMode::LAST_CALL,
1512 : : "finiteModelFind");
1513 : : }
1514 : : }
1515 : :
1516 : : // apply sygus options
1517 : : // if we are attempting to rewrite everything to SyGuS, use sygus()
1518 [ + + ]: 49265 : if (isSygus(opts))
1519 : : {
1520 : 14534 : std::stringstream reasonNoSygus;
1521 [ + + ]: 7267 : if (incompatibleWithSygus(opts, reasonNoSygus))
1522 : : {
1523 : 4 : std::stringstream ss;
1524 : 2 : ss << reasonNoSygus.str() << " not supported in sygus.";
1525 : 2 : throw OptionException(ss.str());
1526 : : }
1527 : : // now, set defaults based on sygus
1528 : 7265 : setDefaultsSygus(opts);
1529 : : }
1530 : : // counterexample-guided instantiation for non-sygus
1531 : : // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
1532 : 49263 : if ((logic.isQuantified()
1533 [ + + ]: 42123 : && (logic.isTheoryEnabled(THEORY_ARITH)
1534 [ + + ]: 591 : || logic.isTheoryEnabled(THEORY_DATATYPES)
1535 [ + + ]: 575 : || logic.isTheoryEnabled(THEORY_BV)
1536 [ + - ]: 169 : || logic.isTheoryEnabled(THEORY_FP)))
1537 [ + + ][ - + ]: 91386 : || opts.quantifiers.cegqiAll)
[ + + ]
1538 : : {
1539 [ + + ][ + + ]: 41954 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqi, true, "logic");
[ + + ]
1540 : : // check whether we should apply full cbqi
1541 [ + + ]: 41954 : if (logic.isPure(THEORY_BV))
1542 : : {
1543 [ + + ][ + + ]: 345 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1544 : : quantifiers, cegqiFullEffort, true, "pure BV logic");
1545 : : }
1546 : : }
1547 [ + + ]: 49263 : if (opts.quantifiers.cegqi)
1548 : : {
1549 [ + + ][ + + ]: 41821 : if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
[ + + ]
1550 : : {
1551 [ + - ][ + + ]: 453 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1552 : : quantifiers, conflictBasedInst, false, "cegqi pure logic");
1553 [ + - ][ + + ]: 453 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1554 : : quantifiers, instNoEntail, false, "cegqi pure logic");
1555 : : // only instantiation should happen at last call when model is avaiable
1556 [ + - ][ + + ]: 453 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1557 : : instWhenMode,
1558 : : options::InstWhenMode::LAST_CALL,
1559 : : "cegqi pure logic");
1560 : : }
1561 : : else
1562 : : {
1563 : : // only supported in pure arithmetic or pure BV
1564 [ + + ]: 41368 : SET_AND_NOTIFY(quantifiers, cegqiNestedQE, false, "cegqi non-pure logic");
1565 : : }
1566 [ + + ]: 41821 : if (opts.quantifiers.globalNegate)
1567 : : {
1568 [ + - ][ + + ]: 9 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1569 : : prenexQuant,
1570 : : options::PrenexQuantMode::NONE,
1571 : : "globalNegate");
1572 : : }
1573 : : }
1574 : : // implied options...
1575 [ + - ][ + + ]: 49263 : if (opts.quantifiers.cbqiModeWasSetByUser || opts.quantifiers.cbqiTConstraint)
1576 : : {
1577 [ - + ]: 15 : SET_AND_NOTIFY(quantifiers, conflictBasedInst, true, "cbqi option");
1578 : : }
1579 [ + + ]: 49263 : if (opts.quantifiers.cegqiNestedQE)
1580 : : {
1581 [ + + ]: 55 : SET_AND_NOTIFY(quantifiers, prenexQuantUser, true, "cegqiNestedQE");
1582 [ + - ][ + + ]: 55 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1583 : : preSkolemQuant,
1584 : : options::PreSkolemQuantMode::ON,
1585 : : "cegqiNestedQE");
1586 : : }
1587 : : // for induction techniques
1588 [ + + ]: 49263 : if (opts.quantifiers.quantInduction)
1589 : : {
1590 [ + - ][ + + ]: 23 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1591 : : quantifiers, dtStcInduction, true, "quantInduction");
1592 [ + - ][ + + ]: 23 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1593 : : quantifiers, intWfInduction, true, "quantInduction");
1594 : : }
1595 [ + + ]: 49263 : if (opts.quantifiers.dtStcInduction)
1596 : : {
1597 : : // try to remove ITEs from quantified formulas
1598 [ + - ][ + + ]: 23 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1599 : : quantifiers, iteDtTesterSplitQuant, true, "dtStcInduction");
1600 [ + - ][ + + ]: 23 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1601 : : iteLiftQuant,
1602 : : options::IteLiftQuantMode::ALL,
1603 : : "dtStcInduction");
1604 : : }
1605 [ + + ]: 49263 : if (opts.quantifiers.intWfInduction)
1606 : : {
1607 [ + - ][ + + ]: 32 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1608 : : quantifiers, purifyTriggers, true, "intWfInduction");
1609 : : }
1610 [ - + ]: 49263 : if (opts.quantifiers.conjectureGenPerRoundWasSetByUser)
1611 : : {
1612 : 0 : bool conjNZero = (opts.quantifiers.conjectureGenPerRound > 0);
1613 [ - - ]: 0 : SET_AND_NOTIFY_VAL_SYM(
1614 : : quantifiers, conjectureGen, conjNZero, "conjectureGenPerRound");
1615 : : }
1616 : : // can't pre-skolemize nested quantifiers without UF theory
1617 : 49263 : if (!logic.isTheoryEnabled(THEORY_UF)
1618 [ + + ][ + + ]: 49263 : && opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
[ + + ]
1619 : : {
1620 [ + - ][ + + ]: 55 : SET_AND_NOTIFY_IF_NOT_USER(
[ + + ]
1621 : : quantifiers, preSkolemQuantNested, false, "preSkolemQuant");
1622 : : }
1623 [ + + ]: 49263 : if (!logic.isTheoryEnabled(THEORY_DATATYPES))
1624 : : {
1625 [ + + ]: 10031 : SET_AND_NOTIFY_VAL_SYM(quantifiers,
1626 : : quantDynamicSplit,
1627 : : options::QuantDSplitMode::NONE,
1628 : : "non-datatypes logic");
1629 : : }
1630 [ + + ]: 49263 : if (opts.quantifiers.globalNegate)
1631 : : {
1632 [ - + ]: 9 : SET_AND_NOTIFY_VAL_SYM(
1633 : : smt, deepRestartMode, options::DeepRestartMode::NONE, "globalNegate");
1634 : : }
1635 : 49263 : }
1636 : :
1637 : 7265 : void SetDefaults::setDefaultsSygus(Options& opts) const
1638 : : {
1639 [ + + ]: 7265 : SET_AND_NOTIFY(quantifiers, sygus, true, "enabling sygus");
1640 : : // full verify mode enables options to ensure full effort on candidates
1641 [ - + ]: 7265 : if (opts.quantifiers.fullSygusVerify)
1642 : : {
1643 [ - - ]: 0 : SET_AND_NOTIFY(
1644 : : quantifiers, sygusVerifyInstMaxRounds, -1, "full sygus verify");
1645 [ - - ]: 0 : SET_AND_NOTIFY(quantifiers, fullSaturateQuant, true, "full sygus verify");
1646 : : }
1647 : : // must use Ferrante/Rackoff for real arithmetic
1648 [ + + ]: 7265 : SET_AND_NOTIFY(quantifiers, cegqiMidpoint, true, "sygus");
1649 : : // must disable cegqi-bv since it may introduce witness terms, which
1650 : : // cannot appear in synthesis solutions
1651 [ + + ][ + + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqiBv, false, "sygus");
[ + + ]
1652 [ + + ]: 7265 : if (opts.quantifiers.sygusRepairConst)
1653 : : {
1654 [ + + ][ + + ]: 7242 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqi, true, "sygusRepairConst");
[ + + ]
1655 : : }
1656 [ + + ]: 7265 : if (opts.quantifiers.sygusInference != options::SygusInferenceMode::OFF)
1657 : : {
1658 : : // optimization: apply preskolemization, makes it succeed more often
1659 [ + - ][ + - ]: 64 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + - ]
1660 : : preSkolemQuant,
1661 : : options::PreSkolemQuantMode::ON,
1662 : : "sygusInference");
1663 [ + - ][ - + ]: 64 : SET_AND_NOTIFY_IF_NOT_USER(
[ - + ]
1664 : : quantifiers, preSkolemQuantNested, true, "sygusInference");
1665 : : }
1666 : : // counterexample-guided instantiation for sygus
1667 [ + + ][ + + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1668 : : cegqiSingleInvMode,
1669 : : options::CegqiSingleInvMode::USE,
1670 : : "sygus");
1671 [ + - ][ + + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, conflictBasedInst, false, "sygus");
[ + + ]
1672 [ + - ][ + + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, instNoEntail, false, "sygus");
[ + + ]
1673 : : // should use full effort cbqi for single invocation and repair const
1674 [ + - ][ + + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, cegqiFullEffort, true, "sygus");
[ + + ]
1675 : : // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
1676 : : // is one that is specialized for returning a single solution. Non-basic
1677 : : // sygus algorithms currently include the PBE solver, UNIF+PI, static
1678 : : // template inference for invariant synthesis, and single invocation
1679 : : // techniques.
1680 : 7265 : bool reqBasicSygus = false;
1681 [ + + ]: 7265 : if (opts.smt.produceAbducts)
1682 : : {
1683 : : // if doing abduction, we should filter strong solutions
1684 [ + - ][ + + ]: 1877 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1685 : : sygusFilterSolMode,
1686 : : options::SygusFilterSolMode::STRONG,
1687 : : "produceAbducts");
1688 : : // we must use basic sygus algorithms, since e.g. we require checking
1689 : : // a sygus side condition for consistency with axioms.
1690 : 1877 : reqBasicSygus = true;
1691 : : }
1692 [ + + ][ + + ]: 7265 : if (opts.quantifiers.sygusStream || opts.base.incrementalSolving)
1693 : : {
1694 : : // Streaming and incremental mode are incompatible with techniques that
1695 : : // focus the search towards finding a single solution.
1696 : 4491 : reqBasicSygus = true;
1697 : : }
1698 : : // Now, disable options for non-basic sygus algorithms, if necessary.
1699 [ + + ]: 7265 : if (reqBasicSygus)
1700 : : {
1701 [ + - ][ + + ]: 4852 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, sygusUnifPbe, false, "basic sygus");
[ + + ]
1702 [ + - ][ - + ]: 4852 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ - + ]
1703 : : sygusUnifPi,
1704 : : options::SygusUnifPiMode::NONE,
1705 : : "basic sygus");
1706 [ + - ][ + + ]: 4852 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1707 : : sygusInvTemplMode,
1708 : : options::SygusInvTemplMode::NONE,
1709 : : "basic sygus");
1710 [ + + ][ + - ]: 4852 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(quantifiers,
[ + + ]
1711 : : cegqiSingleInvMode,
1712 : : options::CegqiSingleInvMode::NONE,
1713 : : "basic sygus");
1714 : : }
1715 : : // do not miniscope
1716 [ + + ][ + + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER_VAL_SYM(
[ + + ]
1717 : : quantifiers, miniscopeQuant, options::MiniscopeQuantMode::OFF, "sygus");
1718 : : // do not do macros
1719 [ + - ][ - + ]: 7265 : SET_AND_NOTIFY_IF_NOT_USER(quantifiers, macrosQuant, false, "sygus");
[ - + ]
1720 : 7265 : }
1721 : 49265 : void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic,
1722 : : Options& opts) const
1723 : : {
1724 : : // Set decision mode based on logic (if not set by user)
1725 [ + + ]: 49265 : if (opts.decision.decisionModeWasSetByUser)
1726 : : {
1727 : 239 : return;
1728 : : }
1729 : : options::DecisionMode decMode =
1730 : : // anything that uses sygus uses internal
1731 [ + + ]: 90699 : usesSygus(opts) ? options::DecisionMode::INTERNAL :
1732 : : // ALL or its supersets
1733 : 41673 : logic.hasEverything()
1734 [ + + ]: 57456 : ? options::DecisionMode::JUSTIFICATION
1735 : : : ( // QF_BV
1736 [ + + ]: 22835 : (!logic.isQuantified() && logic.isPure(THEORY_BV)) ||
1737 : : // QF_AUFBV or QF_ABV or QF_UFBV
1738 [ + + ]: 13229 : (!logic.isQuantified()
1739 [ + + ]: 4498 : && (logic.isTheoryEnabled(THEORY_ARRAYS)
1740 [ + + ]: 3638 : || logic.isTheoryEnabled(THEORY_UF))
1741 [ + + ]: 3176 : && logic.isTheoryEnabled(THEORY_BV))
1742 : 12265 : ||
1743 : : // QF_AUFLIA (and may be ends up enabling
1744 : : // QF_AUFLRA?)
1745 [ + + ]: 12265 : (!logic.isQuantified()
1746 [ + + ]: 3534 : && logic.isTheoryEnabled(THEORY_ARRAYS)
1747 [ + - ]: 372 : && logic.isTheoryEnabled(THEORY_UF)
1748 [ + + ]: 372 : && logic.isTheoryEnabled(THEORY_ARITH))
1749 : 12100 : ||
1750 : : // QF_LRA
1751 [ + + ][ + + ]: 12100 : (!logic.isQuantified() && logic.isPure(THEORY_ARITH)
1752 [ + - ][ + + ]: 1092 : && logic.isLinear() && !logic.isDifferenceLogic()
1753 [ + + ]: 1059 : && !logic.areIntegersUsed())
1754 : 11714 : ||
1755 : : // Quantifiers
1756 [ + + ]: 11714 : logic.isQuantified() ||
1757 : : // Strings
1758 [ - + ]: 2983 : logic.isTheoryEnabled(THEORY_STRINGS)
1759 [ + + ]: 31566 : ? options::DecisionMode::JUSTIFICATION
1760 : 49026 : : options::DecisionMode::INTERNAL);
1761 : :
1762 : : bool stoponly =
1763 : : // ALL or its supersets
1764 [ + + ]: 68109 : logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
1765 [ + + ]: 68109 : ? false
1766 : : : ( // QF_AUFLIA
1767 [ + + ][ + + ]: 17802 : (!logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
1768 [ + - ]: 860 : && logic.isTheoryEnabled(THEORY_UF)
1769 [ + + ]: 860 : && logic.isTheoryEnabled(THEORY_ARITH))
1770 : : ||
1771 : : // QF_LRA
1772 [ + + ]: 24210 : (!logic.isQuantified() && logic.isPure(THEORY_ARITH)
1773 [ + - ][ + + ]: 1092 : && logic.isLinear() && !logic.isDifferenceLogic()
1774 [ + + ]: 1059 : && !logic.areIntegersUsed())
1775 [ + + ]: 17480 : ? true
1776 : 49026 : : false);
1777 : :
1778 [ + + ]: 49026 : if (stoponly)
1779 : : {
1780 [ + - ]: 708 : if (decMode == options::DecisionMode::JUSTIFICATION)
1781 : : {
1782 : 708 : decMode = options::DecisionMode::STOPONLY;
1783 : : }
1784 : : else
1785 : : {
1786 : 0 : Assert(decMode == options::DecisionMode::INTERNAL);
1787 : : }
1788 : : }
1789 [ + + ]: 49026 : SET_AND_NOTIFY_VAL_SYM(decision, decisionMode, decMode, "logic");
1790 : : }
1791 : :
1792 : 385946 : void SetDefaults::notifyModifyOption(const std::string& x,
1793 : : const std::string& val,
1794 : : const std::string& reason) const
1795 : : {
1796 : 385946 : verbose(1) << "SetDefaults: setting " << x << " to " << val;
1797 [ + - ]: 385946 : if (!reason.empty())
1798 : : {
1799 : 385946 : verbose(1) << " due to " << reason;
1800 : : }
1801 : 385946 : verbose(1) << std::endl;
1802 : : // don't print -o options-auto for internal subsolvers
1803 [ + + ]: 385946 : if (!d_isInternalSubsolver)
1804 : : {
1805 [ + + ]: 339347 : if (isOutputOn(OutputTag::OPTIONS_AUTO))
1806 : : {
1807 : 17 : output(OutputTag::OPTIONS_AUTO) << "(options-auto";
1808 : 17 : output(OutputTag::OPTIONS_AUTO) << " " << x;
1809 : 17 : output(OutputTag::OPTIONS_AUTO) << " " << val;
1810 [ + - ]: 17 : if (!reason.empty())
1811 : : {
1812 : 17 : output(OutputTag::OPTIONS_AUTO) << " :reason \"" << reason << "\"";
1813 : : }
1814 : 17 : output(OutputTag::OPTIONS_AUTO) << ")" << std::endl;
1815 : : }
1816 : : }
1817 : 385946 : }
1818 : :
1819 : 11986 : void SetDefaults::disableChecking(Options& opts)
1820 : : {
1821 : 11986 : opts.write_smt().checkUnsatCores = false;
1822 : 11986 : opts.write_smt().produceProofs = false;
1823 : 11986 : opts.write_smt().checkProofs = false;
1824 : 11986 : opts.write_smt().debugCheckModels = false;
1825 : 11986 : opts.write_smt().checkModels = false;
1826 : 11986 : opts.write_proof().checkProofSteps = false;
1827 : 11986 : }
1828 : :
1829 : : } // namespace smt
1830 : : } // namespace cvc5::internal
|
