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