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