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