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