1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Andres Noetzli, Haniel Barbosa |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of setting default options. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "smt/set_defaults.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "base/output.h" |
21 |
|
#include "options/arith_options.h" |
22 |
|
#include "options/arrays_options.h" |
23 |
|
#include "options/base_options.h" |
24 |
|
#include "options/booleans_options.h" |
25 |
|
#include "options/bv_options.h" |
26 |
|
#include "options/datatypes_options.h" |
27 |
|
#include "options/decision_options.h" |
28 |
|
#include "options/language.h" |
29 |
|
#include "options/main_options.h" |
30 |
|
#include "options/option_exception.h" |
31 |
|
#include "options/printer_options.h" |
32 |
|
#include "options/proof_options.h" |
33 |
|
#include "options/prop_options.h" |
34 |
|
#include "options/quantifiers_options.h" |
35 |
|
#include "options/sep_options.h" |
36 |
|
#include "options/set_language.h" |
37 |
|
#include "options/smt_options.h" |
38 |
|
#include "options/strings_options.h" |
39 |
|
#include "options/theory_options.h" |
40 |
|
#include "options/uf_options.h" |
41 |
|
#include "smt/logic_exception.h" |
42 |
|
#include "theory/theory.h" |
43 |
|
|
44 |
|
using namespace cvc5::theory; |
45 |
|
|
46 |
|
namespace cvc5 { |
47 |
|
namespace smt { |
48 |
|
|
49 |
9918 |
SetDefaults::SetDefaults(bool isInternalSubsolver) |
50 |
9918 |
: d_isInternalSubsolver(isInternalSubsolver) |
51 |
|
{ |
52 |
9918 |
} |
53 |
|
|
54 |
9918 |
void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) |
55 |
|
{ |
56 |
|
// initial changes that are independent of logic, and may impact the logic |
57 |
9918 |
setDefaultsPre(opts); |
58 |
|
// now, finalize the logic |
59 |
9918 |
finalizeLogic(logic, opts); |
60 |
|
// further changes to options based on the logic |
61 |
9918 |
setDefaultsPost(logic, opts); |
62 |
9917 |
} |
63 |
|
|
64 |
9918 |
void SetDefaults::setDefaultsPre(Options& opts) |
65 |
|
{ |
66 |
|
// implied options |
67 |
9918 |
if (opts.smt.debugCheckModels) |
68 |
|
{ |
69 |
1285 |
opts.smt.checkModels = true; |
70 |
|
} |
71 |
9918 |
if (opts.smt.checkModels || opts.driver.dumpModels) |
72 |
|
{ |
73 |
1308 |
opts.smt.produceModels = true; |
74 |
|
} |
75 |
9918 |
if (opts.smt.checkModels) |
76 |
|
{ |
77 |
1305 |
opts.smt.produceAssignments = true; |
78 |
|
} |
79 |
|
// unsat cores and proofs shenanigans |
80 |
9918 |
if (opts.driver.dumpUnsatCoresFull) |
81 |
|
{ |
82 |
4 |
opts.driver.dumpUnsatCores = true; |
83 |
|
} |
84 |
9918 |
if (opts.smt.produceDifficulty) |
85 |
|
{ |
86 |
|
if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) |
87 |
|
{ |
88 |
|
opts.smt.unsatCoresMode = options::UnsatCoresMode::PP_ONLY; |
89 |
|
} |
90 |
|
opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; |
91 |
|
} |
92 |
9918 |
if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores |
93 |
8753 |
|| opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores |
94 |
8733 |
|| opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) |
95 |
|
{ |
96 |
2622 |
opts.smt.unsatCores = true; |
97 |
|
} |
98 |
9918 |
if (opts.smt.unsatCores |
99 |
2634 |
&& opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) |
100 |
|
{ |
101 |
1183 |
if (opts.smt.unsatCoresModeWasSetByUser) |
102 |
|
{ |
103 |
|
Notice() |
104 |
|
<< "Overriding OFF unsat-core mode since cores were requested.\n"; |
105 |
|
} |
106 |
1183 |
opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; |
107 |
|
} |
108 |
|
|
109 |
9918 |
if (opts.smt.checkProofs || opts.driver.dumpProofs) |
110 |
|
{ |
111 |
1165 |
opts.smt.produceProofs = true; |
112 |
|
} |
113 |
|
|
114 |
9918 |
if (opts.smt.produceProofs |
115 |
1233 |
&& opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) |
116 |
|
{ |
117 |
1230 |
if (opts.smt.unsatCoresModeWasSetByUser) |
118 |
|
{ |
119 |
|
Notice() << "Forcing full-proof mode for unsat cores mode since proofs " |
120 |
|
"were requested.\n"; |
121 |
|
} |
122 |
|
// enable unsat cores, because they are available as a consequence of proofs |
123 |
1230 |
opts.smt.unsatCores = true; |
124 |
1230 |
opts.smt.unsatCoresMode = options::UnsatCoresMode::FULL_PROOF; |
125 |
|
} |
126 |
|
|
127 |
|
// set proofs on if not yet set |
128 |
9918 |
if (opts.smt.unsatCores && !opts.smt.produceProofs) |
129 |
|
{ |
130 |
2559 |
if (opts.smt.produceProofsWasSetByUser) |
131 |
|
{ |
132 |
18 |
Notice() |
133 |
|
<< "Forcing proof production since new unsat cores were requested.\n"; |
134 |
|
} |
135 |
2559 |
opts.smt.produceProofs = true; |
136 |
|
} |
137 |
|
|
138 |
|
// if unsat cores are disabled, then unsat cores mode should be OFF |
139 |
9918 |
Assert(opts.smt.unsatCores |
140 |
|
== (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); |
141 |
|
|
142 |
|
// new unsat core specific restrictions for proofs |
143 |
9918 |
if (opts.smt.unsatCores |
144 |
3792 |
&& opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) |
145 |
|
{ |
146 |
|
// no fine-graininess |
147 |
2544 |
if (!opts.proof.proofGranularityModeWasSetByUser) |
148 |
|
{ |
149 |
2544 |
opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; |
150 |
|
} |
151 |
|
} |
152 |
|
|
153 |
9918 |
if (opts.bv.bitvectorAigSimplificationsWasSetByUser) |
154 |
|
{ |
155 |
|
Notice() << "SmtEngine: setting bitvectorAig" << std::endl; |
156 |
|
opts.bv.bitvectorAig = true; |
157 |
|
} |
158 |
9918 |
if (opts.bv.bitvectorAlgebraicBudgetWasSetByUser) |
159 |
|
{ |
160 |
|
Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; |
161 |
|
opts.bv.bitvectorAlgebraicSolver = true; |
162 |
|
} |
163 |
|
|
164 |
|
// if we requiring disabling proofs, disable them now |
165 |
9918 |
if (opts.smt.produceProofs) |
166 |
|
{ |
167 |
7584 |
std::stringstream reasonNoProofs; |
168 |
3792 |
if (incompatibleWithProofs(opts, reasonNoProofs)) |
169 |
|
{ |
170 |
8 |
opts.smt.unsatCores = false; |
171 |
8 |
opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; |
172 |
16 |
Notice() << "SmtEngine: turning off produce-proofs due to " |
173 |
8 |
<< reasonNoProofs.str() << "." << std::endl; |
174 |
8 |
opts.smt.produceProofs = false; |
175 |
8 |
opts.smt.checkProofs = false; |
176 |
|
} |
177 |
|
} |
178 |
9918 |
} |
179 |
|
|
180 |
9918 |
void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const |
181 |
|
{ |
182 |
9918 |
if (opts.quantifiers.sygusInstWasSetByUser) |
183 |
|
{ |
184 |
30 |
if (isSygus(opts)) |
185 |
|
{ |
186 |
|
throw OptionException(std::string( |
187 |
|
"SyGuS instantiation quantifiers module cannot be enabled " |
188 |
|
"for SyGuS inputs.")); |
189 |
|
} |
190 |
|
} |
191 |
29034 |
else if (!isSygus(opts) && logic.isQuantified() |
192 |
15538 |
&& (logic.isPure(THEORY_FP) |
193 |
5617 |
|| (logic.isPure(THEORY_ARITH) && !logic.isLinear()))) |
194 |
|
{ |
195 |
33 |
opts.quantifiers.sygusInst = true; |
196 |
|
} |
197 |
|
|
198 |
9918 |
if (opts.bv.bitblastMode == options::BitblastMode::EAGER) |
199 |
|
{ |
200 |
88 |
if (opts.smt.produceModels |
201 |
44 |
&& (logic.isTheoryEnabled(THEORY_ARRAYS) |
202 |
9 |
|| logic.isTheoryEnabled(THEORY_UF))) |
203 |
|
{ |
204 |
|
if (opts.bv.bitblastModeWasSetByUser |
205 |
|
|| opts.smt.produceModelsWasSetByUser) |
206 |
|
{ |
207 |
|
throw OptionException(std::string( |
208 |
|
"Eager bit-blasting currently does not support model generation " |
209 |
|
"for the combination of bit-vectors with arrays or uinterpreted " |
210 |
|
"functions. Try --bitblast=lazy")); |
211 |
|
} |
212 |
|
Notice() << "SmtEngine: setting bit-blast mode to lazy to support model" |
213 |
|
<< "generation" << std::endl; |
214 |
|
opts.bv.bitblastMode = options::BitblastMode::LAZY; |
215 |
|
} |
216 |
44 |
else if (!opts.base.incrementalSolving) |
217 |
|
{ |
218 |
34 |
opts.smt.ackermann = true; |
219 |
|
} |
220 |
|
} |
221 |
|
|
222 |
9918 |
if (opts.smt.solveIntAsBV > 0) |
223 |
|
{ |
224 |
|
// Int to BV currently always eliminates arithmetic completely (or otherwise |
225 |
|
// fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors |
226 |
|
// are required. |
227 |
17 |
logic = logic.getUnlockedCopy(); |
228 |
17 |
logic.enableTheory(THEORY_BV); |
229 |
17 |
logic.disableTheory(THEORY_ARITH); |
230 |
17 |
logic.lock(); |
231 |
|
} |
232 |
|
|
233 |
9918 |
if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) |
234 |
|
{ |
235 |
175 |
if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) |
236 |
|
{ |
237 |
|
throw OptionException( |
238 |
|
"solving bitvectors as integers is incompatible with --bool-to-bv."); |
239 |
|
} |
240 |
175 |
if (opts.smt.BVAndIntegerGranularity > 8) |
241 |
|
{ |
242 |
|
/** |
243 |
|
* The granularity sets the size of the ITE in each element |
244 |
|
* of the sum that is generated for bitwise operators. |
245 |
|
* The size of the ITE is 2^{2*granularity}. |
246 |
|
* Since we don't want to introduce ITEs with unbounded size, |
247 |
|
* we bound the granularity. |
248 |
|
*/ |
249 |
|
throw OptionException("solve-bv-as-int accepts values from 0 to 8."); |
250 |
|
} |
251 |
175 |
if (logic.isTheoryEnabled(THEORY_BV)) |
252 |
|
{ |
253 |
171 |
logic = logic.getUnlockedCopy(); |
254 |
171 |
logic.enableTheory(THEORY_ARITH); |
255 |
171 |
logic.arithNonLinear(); |
256 |
171 |
logic.lock(); |
257 |
|
} |
258 |
|
} |
259 |
|
|
260 |
|
// set options about ackermannization |
261 |
19908 |
if (opts.smt.ackermann && opts.smt.produceModels |
262 |
9933 |
&& (logic.isTheoryEnabled(THEORY_ARRAYS) |
263 |
11 |
|| logic.isTheoryEnabled(THEORY_UF))) |
264 |
|
{ |
265 |
4 |
if (opts.smt.produceModelsWasSetByUser) |
266 |
|
{ |
267 |
|
throw OptionException(std::string( |
268 |
|
"Ackermannization currently does not support model generation.")); |
269 |
|
} |
270 |
4 |
Notice() << "SmtEngine: turn off ackermannization to support model" |
271 |
|
<< "generation" << std::endl; |
272 |
4 |
opts.smt.ackermann = false; |
273 |
|
} |
274 |
|
|
275 |
9918 |
if (opts.smt.ackermann) |
276 |
|
{ |
277 |
68 |
if (logic.isTheoryEnabled(THEORY_UF)) |
278 |
|
{ |
279 |
33 |
logic = logic.getUnlockedCopy(); |
280 |
33 |
logic.disableTheory(THEORY_UF); |
281 |
33 |
logic.lock(); |
282 |
|
} |
283 |
68 |
if (logic.isTheoryEnabled(THEORY_ARRAYS)) |
284 |
|
{ |
285 |
7 |
logic = logic.getUnlockedCopy(); |
286 |
7 |
logic.disableTheory(THEORY_ARRAYS); |
287 |
7 |
logic.lock(); |
288 |
|
} |
289 |
|
} |
290 |
|
|
291 |
|
// Set default options associated with strings-exp. We also set these options |
292 |
|
// if we are using eager string preprocessing, which may introduce quantified |
293 |
|
// formulas at preprocess time. |
294 |
|
// |
295 |
|
// We don't want to set this option when we are in logics that contain ALL. |
296 |
9918 |
if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) |
297 |
|
{ |
298 |
|
// If the user explicitly set a logic that includes strings, but is not |
299 |
|
// the generic "ALL" logic, then enable stringsExp. |
300 |
744 |
opts.strings.stringExp = true; |
301 |
744 |
Trace("smt") << "Turning stringExp on since logic does not have everything " |
302 |
|
"and string theory is enabled\n"; |
303 |
|
} |
304 |
9918 |
if (opts.strings.stringExp || !opts.strings.stringLazyPreproc) |
305 |
|
{ |
306 |
|
// We require quantifiers since extended functions reduce using them. |
307 |
1153 |
if (!logic.isQuantified()) |
308 |
|
{ |
309 |
547 |
logic = logic.getUnlockedCopy(); |
310 |
547 |
logic.enableQuantifiers(); |
311 |
547 |
logic.lock(); |
312 |
1094 |
Trace("smt") << "turning on quantifier logic, for strings-exp" |
313 |
547 |
<< std::endl; |
314 |
|
} |
315 |
|
// Note we allow E-matching by default to support combinations of sequences |
316 |
|
// and quantifiers. We also do not enable fmfBound here, which would |
317 |
|
// enable bounded integer instantiation for *all* quantifiers. Instead, |
318 |
|
// the bounded integers module will always process internally generated |
319 |
|
// quantifiers (those marked with InternalQuantAttribute). |
320 |
|
} |
321 |
|
|
322 |
9918 |
if (opts.arrays.arraysExp) |
323 |
|
{ |
324 |
12 |
if (!logic.isQuantified()) |
325 |
|
{ |
326 |
4 |
logic = logic.getUnlockedCopy(); |
327 |
4 |
logic.enableQuantifiers(); |
328 |
4 |
logic.lock(); |
329 |
|
} |
330 |
|
} |
331 |
|
|
332 |
|
// We now know whether the input uses sygus. Update the logic to incorporate |
333 |
|
// the theories we need internally for handling sygus problems. |
334 |
9918 |
if (usesSygus(opts)) |
335 |
|
{ |
336 |
680 |
logic = logic.getUnlockedCopy(); |
337 |
680 |
logic.enableSygus(); |
338 |
680 |
logic.lock(); |
339 |
|
} |
340 |
|
|
341 |
|
// widen the logic |
342 |
9918 |
widenLogic(logic, opts); |
343 |
|
|
344 |
|
// check if we have any options that are not supported with quantified logics |
345 |
9918 |
if (logic.isQuantified()) |
346 |
|
{ |
347 |
13652 |
std::stringstream reasonNoQuant; |
348 |
6826 |
if (incompatibleWithQuantifiers(opts, reasonNoQuant)) |
349 |
|
{ |
350 |
|
std::stringstream ss; |
351 |
|
ss << reasonNoQuant.str() << " not supported in quantified logics."; |
352 |
|
throw OptionException(ss.str()); |
353 |
|
} |
354 |
|
} |
355 |
9918 |
} |
356 |
|
|
357 |
9918 |
void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const |
358 |
|
{ |
359 |
|
|
360 |
|
// sygus core connective requires unsat cores |
361 |
9918 |
if (opts.quantifiers.sygusCoreConnective) |
362 |
|
{ |
363 |
69 |
opts.smt.unsatCores = true; |
364 |
69 |
if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) |
365 |
|
{ |
366 |
5 |
opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; |
367 |
|
} |
368 |
|
} |
369 |
|
|
370 |
9918 |
if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts |
371 |
7593 |
|| opts.smt.produceInterpols != options::ProduceInterpols::NONE |
372 |
7473 |
|| opts.smt.modelCoresMode != options::ModelCoresMode::NONE |
373 |
7468 |
|| opts.smt.blockModelsMode != options::BlockModelsMode::NONE |
374 |
7448 |
|| opts.smt.produceProofs) |
375 |
6152 |
&& !opts.smt.produceAssertions) |
376 |
|
{ |
377 |
3795 |
Notice() << "SmtEngine: turning on produce-assertions to support " |
378 |
1 |
<< "option requiring assertions." << std::endl; |
379 |
3794 |
opts.smt.produceAssertions = true; |
380 |
|
} |
381 |
|
|
382 |
9918 |
if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) |
383 |
|
{ |
384 |
|
/** |
385 |
|
* Operations on 1 bits are better handled as Boolean operations |
386 |
|
* than as integer operations. |
387 |
|
* Therefore, we enable bv-to-bool, which runs before |
388 |
|
* the translation to integers. |
389 |
|
*/ |
390 |
175 |
opts.bv.bitvectorToBool = true; |
391 |
|
} |
392 |
|
|
393 |
|
// Disable options incompatible with incremental solving, or output an error |
394 |
|
// if enabled explicitly. |
395 |
9918 |
if (opts.base.incrementalSolving) |
396 |
|
{ |
397 |
4408 |
std::stringstream reasonNoInc; |
398 |
4408 |
std::stringstream suggestNoInc; |
399 |
2204 |
if (incompatibleWithIncremental(logic, opts, reasonNoInc, suggestNoInc)) |
400 |
|
{ |
401 |
|
std::stringstream ss; |
402 |
|
ss << reasonNoInc.str() << " not supported with incremental solving. " |
403 |
|
<< suggestNoInc.str(); |
404 |
|
throw OptionException(ss.str()); |
405 |
|
} |
406 |
|
} |
407 |
|
|
408 |
|
// Disable options incompatible with unsat cores or output an error if enabled |
409 |
|
// explicitly |
410 |
9918 |
if (safeUnsatCores(opts)) |
411 |
|
{ |
412 |
|
// check if the options are not compatible with unsat cores |
413 |
5094 |
std::stringstream reasonNoUc; |
414 |
2547 |
if (incompatibleWithUnsatCores(opts, reasonNoUc)) |
415 |
|
{ |
416 |
2 |
std::stringstream ss; |
417 |
1 |
ss << reasonNoUc.str() << " not supported with unsat cores"; |
418 |
1 |
throw OptionException(ss.str()); |
419 |
|
} |
420 |
|
} |
421 |
|
else |
422 |
|
{ |
423 |
|
// Turn on unconstrained simplification for QF_AUFBV |
424 |
7371 |
if (!opts.smt.unconstrainedSimpWasSetByUser |
425 |
7265 |
&& !opts.base.incrementalSolving) |
426 |
|
{ |
427 |
|
// It is also currently incompatible with arithmetic, force the option |
428 |
|
// off. |
429 |
11246 |
bool uncSimp = !opts.base.incrementalSolving && !logic.isQuantified() |
430 |
1547 |
&& !opts.smt.produceModels && !opts.smt.produceAssignments |
431 |
1145 |
&& !opts.smt.checkModels |
432 |
1145 |
&& logic.isTheoryEnabled(THEORY_ARRAYS) |
433 |
164 |
&& logic.isTheoryEnabled(THEORY_BV) |
434 |
5705 |
&& !logic.isTheoryEnabled(THEORY_ARITH); |
435 |
11246 |
Trace("smt") << "setting unconstrained simplification to " << uncSimp |
436 |
5623 |
<< std::endl; |
437 |
5623 |
opts.smt.unconstrainedSimp = uncSimp; |
438 |
|
} |
439 |
|
|
440 |
|
// by default, nonclausal simplification is off for QF_SAT |
441 |
7371 |
if (!opts.smt.simplificationModeWasSetByUser) |
442 |
|
{ |
443 |
7345 |
bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified(); |
444 |
14690 |
Trace("smt") << "setting simplification mode to <" |
445 |
7345 |
<< logic.getLogicString() << "> " << (!qf_sat) << std::endl; |
446 |
|
// simplification=none works better for SMT LIB benchmarks with |
447 |
|
// quantifiers, not others opts.set(options::simplificationMode, qf_sat || |
448 |
|
// quantifiers ? options::SimplificationMode::NONE : |
449 |
|
// options::SimplificationMode::BATCH); |
450 |
7345 |
opts.smt.simplificationMode = qf_sat ? options::SimplificationMode::NONE |
451 |
|
: options::SimplificationMode::BATCH; |
452 |
|
} |
453 |
|
} |
454 |
|
|
455 |
9917 |
if (opts.quantifiers.cegqiBv && logic.isQuantified()) |
456 |
|
{ |
457 |
5556 |
if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) |
458 |
|
{ |
459 |
|
if (opts.bv.boolToBitvectorWasSetByUser) |
460 |
|
{ |
461 |
|
throw OptionException( |
462 |
|
"bool-to-bv != off not supported with CBQI BV for quantified " |
463 |
|
"logics"); |
464 |
|
} |
465 |
|
Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" |
466 |
|
<< std::endl; |
467 |
|
opts.bv.boolToBitvector = options::BoolToBVMode::OFF; |
468 |
|
} |
469 |
|
} |
470 |
|
|
471 |
|
// cases where we need produce models |
472 |
19834 |
if (!opts.smt.produceModels |
473 |
10217 |
&& (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck |
474 |
6630 |
|| usesSygus(opts))) |
475 |
|
{ |
476 |
300 |
Notice() << "SmtEngine: turning on produce-models" << std::endl; |
477 |
300 |
opts.smt.produceModels = true; |
478 |
|
} |
479 |
|
|
480 |
|
// --ite-simp is an experimental option designed for QF_LIA/nec. This |
481 |
|
// technique is experimental. This benchmark set also requires removing ITEs |
482 |
|
// during preprocessing, before repeating simplification. Hence, we enable |
483 |
|
// this by default. |
484 |
9917 |
if (opts.smt.doITESimp) |
485 |
|
{ |
486 |
1 |
if (!opts.smt.earlyIteRemovalWasSetByUser) |
487 |
|
{ |
488 |
1 |
opts.smt.earlyIteRemoval = true; |
489 |
|
} |
490 |
|
} |
491 |
|
|
492 |
|
// Set the options for the theoryOf |
493 |
9917 |
if (!opts.theory.theoryOfModeWasSetByUser) |
494 |
|
{ |
495 |
27612 |
if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) |
496 |
2894 |
&& !logic.isTheoryEnabled(THEORY_STRINGS) |
497 |
2328 |
&& !logic.isTheoryEnabled(THEORY_SETS) |
498 |
2242 |
&& !logic.isTheoryEnabled(THEORY_BAGS) |
499 |
12854 |
&& !(logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() |
500 |
701 |
&& !logic.isQuantified())) |
501 |
|
{ |
502 |
1804 |
Trace("smt") << "setting theoryof-mode to term-based" << std::endl; |
503 |
1804 |
opts.theory.theoryOfMode = options::TheoryOfMode::THEORY_OF_TERM_BASED; |
504 |
|
} |
505 |
|
} |
506 |
|
|
507 |
|
// by default, symmetry breaker is on only for non-incremental QF_UF |
508 |
9917 |
if (!opts.uf.ufSymmetryBreakerWasSetByUser) |
509 |
|
{ |
510 |
10275 |
bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified() |
511 |
264 |
&& !opts.base.incrementalSolving |
512 |
10170 |
&& !safeUnsatCores(opts); |
513 |
19834 |
Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc |
514 |
9917 |
<< std::endl; |
515 |
9917 |
opts.uf.ufSymmetryBreaker = qf_uf_noinc; |
516 |
|
} |
517 |
|
|
518 |
|
// If in arrays, set the UF handler to arrays |
519 |
24689 |
if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder() |
520 |
4728 |
&& !opts.quantifiers.finiteModelFind |
521 |
14947 |
&& (!logic.isQuantified() |
522 |
4136 |
|| (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF)))) |
523 |
|
{ |
524 |
447 |
Theory::setUninterpretedSortOwner(THEORY_ARRAYS); |
525 |
|
} |
526 |
|
else |
527 |
|
{ |
528 |
9470 |
Theory::setUninterpretedSortOwner(THEORY_UF); |
529 |
|
} |
530 |
|
|
531 |
9917 |
if (!opts.smt.simplifyWithCareEnabledWasSetByUser) |
532 |
|
{ |
533 |
|
bool qf_aufbv = |
534 |
13008 |
!logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) |
535 |
10368 |
&& logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV); |
536 |
|
|
537 |
9917 |
bool withCare = qf_aufbv; |
538 |
19834 |
Trace("smt") << "setting ite simplify with care to " << withCare |
539 |
9917 |
<< std::endl; |
540 |
9917 |
opts.smt.simplifyWithCareEnabled = withCare; |
541 |
|
} |
542 |
|
// Turn off array eager index splitting for QF_AUFLIA |
543 |
9917 |
if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser) |
544 |
|
{ |
545 |
22925 |
if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) |
546 |
451 |
&& logic.isTheoryEnabled(THEORY_UF) |
547 |
10368 |
&& logic.isTheoryEnabled(THEORY_ARITH)) |
548 |
|
{ |
549 |
352 |
Trace("smt") << "setting array eager index splitting to false" |
550 |
176 |
<< std::endl; |
551 |
176 |
opts.arrays.arraysEagerIndexSplitting = false; |
552 |
|
} |
553 |
|
} |
554 |
|
// Turn on multiple-pass non-clausal simplification for QF_AUFBV |
555 |
9917 |
if (!opts.smt.repeatSimpWasSetByUser) |
556 |
|
{ |
557 |
9913 |
bool repeatSimp = !logic.isQuantified() |
558 |
3089 |
&& (logic.isTheoryEnabled(THEORY_ARRAYS) |
559 |
451 |
&& logic.isTheoryEnabled(THEORY_UF) |
560 |
451 |
&& logic.isTheoryEnabled(THEORY_BV)) |
561 |
10182 |
&& !safeUnsatCores(opts); |
562 |
19826 |
Trace("smt") << "setting repeat simplification to " << repeatSimp |
563 |
9913 |
<< std::endl; |
564 |
9913 |
opts.smt.repeatSimp = repeatSimp; |
565 |
|
} |
566 |
|
|
567 |
|
/* Disable bit-level propagation by default for the BITBLAST solver. */ |
568 |
9917 |
if (opts.bv.bvSolver == options::BVSolver::BITBLAST) |
569 |
|
{ |
570 |
6148 |
opts.bv.bitvectorPropagate = false; |
571 |
|
} |
572 |
|
|
573 |
19834 |
if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL |
574 |
9917 |
&& !logic.isTheoryEnabled(THEORY_BV)) |
575 |
|
{ |
576 |
|
if (opts.bv.boolToBitvectorWasSetByUser) |
577 |
|
{ |
578 |
|
throw OptionException( |
579 |
|
"bool-to-bv=all not supported for non-bitvector logics."); |
580 |
|
} |
581 |
|
Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: " |
582 |
|
<< logic.getLogicString() << std::endl; |
583 |
|
opts.bv.boolToBitvector = options::BoolToBVMode::OFF; |
584 |
|
} |
585 |
|
|
586 |
19834 |
if (!opts.bv.bvEagerExplanationsWasSetByUser |
587 |
9917 |
&& logic.isTheoryEnabled(THEORY_ARRAYS) |
588 |
14772 |
&& logic.isTheoryEnabled(THEORY_BV)) |
589 |
|
{ |
590 |
4441 |
Trace("smt") << "enabling eager bit-vector explanations " << std::endl; |
591 |
4441 |
opts.bv.bvEagerExplanations = true; |
592 |
|
} |
593 |
|
|
594 |
|
// Turn on arith rewrite equalities only for pure arithmetic |
595 |
9917 |
if (!opts.arith.arithRewriteEqWasSetByUser) |
596 |
|
{ |
597 |
|
bool arithRewriteEq = |
598 |
9908 |
logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified(); |
599 |
19816 |
Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq |
600 |
9908 |
<< std::endl; |
601 |
9908 |
opts.arith.arithRewriteEq = arithRewriteEq; |
602 |
|
} |
603 |
9917 |
if (!opts.arith.arithHeuristicPivotsWasSetByUser) |
604 |
|
{ |
605 |
9917 |
int16_t heuristicPivots = 5; |
606 |
9917 |
if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) |
607 |
|
{ |
608 |
729 |
if (logic.isDifferenceLogic()) |
609 |
|
{ |
610 |
17 |
heuristicPivots = -1; |
611 |
|
} |
612 |
712 |
else if (!logic.areIntegersUsed()) |
613 |
|
{ |
614 |
248 |
heuristicPivots = 0; |
615 |
|
} |
616 |
|
} |
617 |
19834 |
Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots |
618 |
9917 |
<< std::endl; |
619 |
9917 |
opts.arith.arithHeuristicPivots = heuristicPivots; |
620 |
|
} |
621 |
9917 |
if (!opts.arith.arithPivotThresholdWasSetByUser) |
622 |
|
{ |
623 |
9917 |
uint16_t pivotThreshold = 2; |
624 |
9917 |
if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) |
625 |
|
{ |
626 |
729 |
if (logic.isDifferenceLogic()) |
627 |
|
{ |
628 |
17 |
pivotThreshold = 16; |
629 |
|
} |
630 |
|
} |
631 |
19834 |
Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold |
632 |
9917 |
<< std::endl; |
633 |
9917 |
opts.arith.arithPivotThreshold = pivotThreshold; |
634 |
|
} |
635 |
9917 |
if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser) |
636 |
|
{ |
637 |
9917 |
int16_t varOrderPivots = -1; |
638 |
9917 |
if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) |
639 |
|
{ |
640 |
729 |
varOrderPivots = 200; |
641 |
|
} |
642 |
19834 |
Trace("smt") << "setting arithStandardCheckVarOrderPivots " |
643 |
9917 |
<< varOrderPivots << std::endl; |
644 |
9917 |
opts.arith.arithStandardCheckVarOrderPivots = varOrderPivots; |
645 |
|
} |
646 |
9917 |
if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed()) |
647 |
|
{ |
648 |
502 |
if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser) |
649 |
|
{ |
650 |
1004 |
Trace("smt") << "setting nlExtTangentPlanesInterleave to true" |
651 |
502 |
<< std::endl; |
652 |
502 |
opts.arith.nlExtTangentPlanesInterleave = true; |
653 |
|
} |
654 |
|
} |
655 |
9917 |
if (!opts.arith.nlRlvAssertBoundsWasSetByUser) |
656 |
|
{ |
657 |
|
// use bound inference to determine when bounds are irrelevant only when |
658 |
|
// the logic is quantifier-free |
659 |
9917 |
opts.arith.nlRlvAssertBounds = !logic.isQuantified(); |
660 |
|
} |
661 |
|
|
662 |
|
// set the default decision mode |
663 |
9917 |
setDefaultDecisionMode(logic, opts); |
664 |
|
|
665 |
|
// set up of central equality engine |
666 |
9917 |
if (opts.theory.eeMode == options::EqEngineMode::CENTRAL) |
667 |
|
{ |
668 |
35 |
if (!opts.arith.arithEqSolverWasSetByUser) |
669 |
|
{ |
670 |
|
// use the arithmetic equality solver by default |
671 |
31 |
opts.arith.arithEqSolver = true; |
672 |
|
} |
673 |
|
} |
674 |
9917 |
if (opts.arith.arithEqSolver) |
675 |
|
{ |
676 |
39 |
if (!opts.arith.arithCongManWasSetByUser) |
677 |
|
{ |
678 |
|
// if we are using the arithmetic equality solver, do not use the |
679 |
|
// arithmetic congruence manager by default |
680 |
39 |
opts.arith.arithCongMan = false; |
681 |
|
} |
682 |
|
} |
683 |
|
|
684 |
9917 |
if (logic.isHigherOrder()) |
685 |
|
{ |
686 |
191 |
opts.uf.ufHo = true; |
687 |
191 |
if (!opts.theory.assignFunctionValues) |
688 |
|
{ |
689 |
|
// must assign function values |
690 |
2 |
opts.theory.assignFunctionValues = true; |
691 |
|
} |
692 |
|
} |
693 |
|
|
694 |
|
// set all defaults in the quantifiers theory, which includes sygus |
695 |
9917 |
setDefaultsQuantifiers(logic, opts); |
696 |
|
|
697 |
|
// shared selectors are generally not good to combine with standard |
698 |
|
// quantifier techniques e.g. E-matching |
699 |
9917 |
if (!opts.datatypes.dtSharedSelectorsWasSetByUser) |
700 |
|
{ |
701 |
9862 |
if (logic.isQuantified() && !usesSygus(opts)) |
702 |
|
{ |
703 |
6116 |
opts.datatypes.dtSharedSelectors = false; |
704 |
|
} |
705 |
|
} |
706 |
|
|
707 |
|
// until bugs 371,431 are fixed |
708 |
9917 |
if (!opts.prop.minisatUseElimWasSetByUser) |
709 |
|
{ |
710 |
|
// cannot use minisat elimination for logics where a theory solver |
711 |
|
// introduces new literals into the search. This includes quantifiers |
712 |
|
// (quantifier instantiation), and the lemma schemas used in non-linear |
713 |
|
// and sets. We also can't use it if models are enabled. |
714 |
25538 |
if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS) |
715 |
5704 |
|| logic.isQuantified() || opts.smt.produceModels |
716 |
2453 |
|| opts.smt.produceAssignments || opts.smt.checkModels |
717 |
12370 |
|| (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) |
718 |
|
{ |
719 |
7903 |
opts.prop.minisatUseElim = false; |
720 |
|
} |
721 |
|
} |
722 |
|
|
723 |
28067 |
if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() |
724 |
15112 |
&& opts.arith.nlRlvMode != options::NlRlvMode::NONE) |
725 |
|
{ |
726 |
18 |
if (!opts.theory.relevanceFilter) |
727 |
|
{ |
728 |
18 |
if (opts.theory.relevanceFilterWasSetByUser) |
729 |
|
{ |
730 |
|
Warning() << "SmtEngine: turning on relevance filtering to support " |
731 |
|
"--nl-ext-rlv=" |
732 |
|
<< opts.arith.nlRlvMode << std::endl; |
733 |
|
} |
734 |
|
// must use relevance filtering techniques |
735 |
18 |
opts.theory.relevanceFilter = true; |
736 |
|
} |
737 |
|
} |
738 |
|
|
739 |
|
// For now, these array theory optimizations do not support model-building |
740 |
9917 |
if (opts.smt.produceModels || opts.smt.produceAssignments |
741 |
6335 |
|| opts.smt.checkModels) |
742 |
|
{ |
743 |
3582 |
opts.arrays.arraysOptimizeLinear = false; |
744 |
|
} |
745 |
|
|
746 |
9917 |
if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser) |
747 |
|
{ |
748 |
100 |
Trace("smt") << "settting stringProcessLoopMode to 'simple' since " |
749 |
50 |
"--strings-fmf enabled" |
750 |
50 |
<< std::endl; |
751 |
50 |
opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE; |
752 |
|
} |
753 |
|
|
754 |
|
// !!! All options that require disabling models go here |
755 |
19834 |
std::stringstream reasonNoModel; |
756 |
9917 |
if (incompatibleWithModels(opts, reasonNoModel)) |
757 |
|
{ |
758 |
4162 |
std::string sOptNoModel = reasonNoModel.str(); |
759 |
2081 |
if (opts.smt.produceModels) |
760 |
|
{ |
761 |
47 |
if (opts.smt.produceModelsWasSetByUser) |
762 |
|
{ |
763 |
|
std::stringstream ss; |
764 |
|
ss << "Cannot use " << sOptNoModel << " with model generation."; |
765 |
|
throw OptionException(ss.str()); |
766 |
|
} |
767 |
47 |
Notice() << "SmtEngine: turning off produce-models to support " |
768 |
|
<< sOptNoModel << std::endl; |
769 |
47 |
opts.smt.produceModels = false; |
770 |
|
} |
771 |
2081 |
if (opts.smt.produceAssignments) |
772 |
|
{ |
773 |
46 |
if (opts.smt.produceAssignmentsWasSetByUser) |
774 |
|
{ |
775 |
|
std::stringstream ss; |
776 |
|
ss << "Cannot use " << sOptNoModel |
777 |
|
<< " with model generation (produce-assignments)."; |
778 |
|
throw OptionException(ss.str()); |
779 |
|
} |
780 |
46 |
Notice() << "SmtEngine: turning off produce-assignments to support " |
781 |
|
<< sOptNoModel << std::endl; |
782 |
46 |
opts.smt.produceAssignments = false; |
783 |
|
} |
784 |
2081 |
if (opts.smt.checkModels) |
785 |
|
{ |
786 |
46 |
if (opts.smt.checkModelsWasSetByUser) |
787 |
|
{ |
788 |
|
std::stringstream ss; |
789 |
|
ss << "Cannot use " << sOptNoModel |
790 |
|
<< " with model generation (check-models)."; |
791 |
|
throw OptionException(ss.str()); |
792 |
|
} |
793 |
46 |
Notice() << "SmtEngine: turning off check-models to support " |
794 |
|
<< sOptNoModel << std::endl; |
795 |
46 |
opts.smt.checkModels = false; |
796 |
|
} |
797 |
|
} |
798 |
|
|
799 |
19834 |
if (opts.bv.bitblastMode == options::BitblastMode::EAGER |
800 |
9961 |
&& !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV" |
801 |
19834 |
&& logic.getLogicString() != "QF_ABV") |
802 |
|
{ |
803 |
|
throw OptionException( |
804 |
|
"Eager bit-blasting does not currently support theory combination. " |
805 |
|
"Note that in a QF_BV problem UF symbols can be introduced for " |
806 |
|
"division. " |
807 |
|
"Try --bv-div-zero-const to interpret division by zero as a constant."); |
808 |
|
} |
809 |
|
|
810 |
|
#ifdef CVC5_USE_POLY |
811 |
9917 |
if (logic == LogicInfo("QF_UFNRA")) |
812 |
|
{ |
813 |
118 |
if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) |
814 |
|
{ |
815 |
97 |
opts.arith.nlCad = true; |
816 |
97 |
if (!opts.arith.nlExtWasSetByUser) |
817 |
|
{ |
818 |
48 |
opts.arith.nlExt = options::NlExtMode::LIGHT; |
819 |
|
} |
820 |
97 |
if (!opts.arith.nlRlvModeWasSetByUser) |
821 |
|
{ |
822 |
97 |
opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE; |
823 |
|
} |
824 |
|
} |
825 |
|
} |
826 |
|
#else |
827 |
|
if (opts.arith.nlCad) |
828 |
|
{ |
829 |
|
if (opts.arith.nlCadWasSetByUser) |
830 |
|
{ |
831 |
|
std::stringstream ss; |
832 |
|
ss << "Cannot use " << options::arith::nlCad__name |
833 |
|
<< " without configuring with --poly."; |
834 |
|
throw OptionException(ss.str()); |
835 |
|
} |
836 |
|
else |
837 |
|
{ |
838 |
|
Notice() << "Cannot use --" << options::arith::nlCad__name |
839 |
|
<< " without configuring with --poly." << std::endl; |
840 |
|
opts.arith.nlCad = false; |
841 |
|
opts.arith.nlExt = options::NlExtMode::FULL; |
842 |
|
} |
843 |
|
} |
844 |
|
#endif |
845 |
9917 |
} |
846 |
|
|
847 |
56726 |
bool SetDefaults::isSygus(const Options& opts) const |
848 |
|
{ |
849 |
56726 |
if (language::isLangSygus(opts.base.inputLanguage)) |
850 |
|
{ |
851 |
2886 |
return true; |
852 |
|
} |
853 |
53840 |
if (!d_isInternalSubsolver) |
854 |
|
{ |
855 |
40072 |
if (opts.smt.produceAbducts |
856 |
39977 |
|| opts.smt.produceInterpols != options::ProduceInterpols::NONE |
857 |
39917 |
|| opts.quantifiers.sygusInference |
858 |
39589 |
|| opts.quantifiers.sygusRewSynthInput) |
859 |
|
{ |
860 |
|
// since we are trying to recast as sygus, we assume the input is sygus |
861 |
483 |
return true; |
862 |
|
} |
863 |
|
} |
864 |
53357 |
return false; |
865 |
|
} |
866 |
|
|
867 |
43017 |
bool SetDefaults::usesSygus(const Options& opts) const |
868 |
|
{ |
869 |
43017 |
if (isSygus(opts)) |
870 |
|
{ |
871 |
2732 |
return true; |
872 |
|
} |
873 |
40285 |
if (!d_isInternalSubsolver && opts.quantifiers.sygusInst) |
874 |
|
{ |
875 |
|
// sygus instantiation uses sygus, but it is not a sygus problem |
876 |
242 |
return true; |
877 |
|
} |
878 |
40043 |
return false; |
879 |
|
} |
880 |
|
|
881 |
3792 |
bool SetDefaults::incompatibleWithProofs(Options& opts, |
882 |
|
std::ostream& reason) const |
883 |
|
{ |
884 |
3792 |
if (opts.quantifiers.globalNegate) |
885 |
|
{ |
886 |
|
// When global negate answers "unsat", it is not due to showing a set of |
887 |
|
// formulas is unsat. Thus, proofs do not apply. |
888 |
1 |
reason << "global-negate"; |
889 |
1 |
return true; |
890 |
|
} |
891 |
3791 |
if (isSygus(opts)) |
892 |
|
{ |
893 |
|
// When sygus answers "unsat", it is not due to showing a set of |
894 |
|
// formulas is unsat in the standard way. Thus, proofs do not apply. |
895 |
7 |
reason << "sygus"; |
896 |
7 |
return true; |
897 |
|
} |
898 |
|
// options that are automatically set to support proofs |
899 |
3784 |
if (opts.bv.bvAssertInput) |
900 |
|
{ |
901 |
2 |
Notice() |
902 |
|
<< "Disabling bv-assert-input since it is incompatible with proofs." |
903 |
|
<< std::endl; |
904 |
2 |
opts.bv.bvAssertInput = false; |
905 |
|
} |
906 |
|
// If proofs are required and the user did not specify a specific BV solver, |
907 |
|
// we make sure to use the proof producing BITBLAST_INTERNAL solver. |
908 |
3784 |
if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL |
909 |
2355 |
&& !opts.bv.bvSolverWasSetByUser |
910 |
2335 |
&& opts.bv.bvSatSolver == options::SatSolverMode::MINISAT) |
911 |
|
{ |
912 |
2323 |
Notice() << "Forcing internal bit-vector solver due to proof production." |
913 |
|
<< std::endl; |
914 |
2323 |
opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL; |
915 |
|
} |
916 |
3784 |
return false; |
917 |
|
} |
918 |
|
|
919 |
9917 |
bool SetDefaults::incompatibleWithModels(const Options& opts, |
920 |
|
std::ostream& reason) const |
921 |
|
{ |
922 |
9917 |
if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp) |
923 |
|
{ |
924 |
104 |
reason << "unconstrained-simp"; |
925 |
104 |
return true; |
926 |
|
} |
927 |
9813 |
else if (opts.smt.sortInference) |
928 |
|
{ |
929 |
20 |
reason << "sort-inference"; |
930 |
20 |
return true; |
931 |
|
} |
932 |
9793 |
else if (opts.prop.minisatUseElim) |
933 |
|
{ |
934 |
1951 |
reason << "minisat-elimination"; |
935 |
1951 |
return true; |
936 |
|
} |
937 |
7842 |
else if (opts.quantifiers.globalNegate) |
938 |
|
{ |
939 |
6 |
reason << "global-negate"; |
940 |
6 |
return true; |
941 |
|
} |
942 |
7836 |
return false; |
943 |
|
} |
944 |
|
|
945 |
2204 |
bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, |
946 |
|
Options& opts, |
947 |
|
std::ostream& reason, |
948 |
|
std::ostream& suggest) const |
949 |
|
{ |
950 |
2204 |
if (opts.smt.ackermann) |
951 |
|
{ |
952 |
|
reason << "ackermann"; |
953 |
|
return true; |
954 |
|
} |
955 |
2204 |
if (opts.smt.unconstrainedSimp) |
956 |
|
{ |
957 |
|
if (opts.smt.unconstrainedSimpWasSetByUser) |
958 |
|
{ |
959 |
|
reason << "unconstrained simplification"; |
960 |
|
return true; |
961 |
|
} |
962 |
|
Notice() << "SmtEngine: turning off unconstrained simplification to " |
963 |
|
"support incremental solving" |
964 |
|
<< std::endl; |
965 |
|
opts.smt.unconstrainedSimp = false; |
966 |
|
} |
967 |
4408 |
if (opts.bv.bitblastMode == options::BitblastMode::EAGER |
968 |
2204 |
&& !logic.isPure(THEORY_BV)) |
969 |
|
{ |
970 |
|
reason << "eager bit-blasting in non-QF_BV logic"; |
971 |
|
suggest << "Try --bitblast=lazy."; |
972 |
|
return true; |
973 |
|
} |
974 |
2204 |
if (opts.quantifiers.sygusInference) |
975 |
|
{ |
976 |
|
if (opts.quantifiers.sygusInferenceWasSetByUser) |
977 |
|
{ |
978 |
|
reason << "sygus inference"; |
979 |
|
return true; |
980 |
|
} |
981 |
|
Notice() << "SmtEngine: turning off sygus inference to support " |
982 |
|
"incremental solving" |
983 |
|
<< std::endl; |
984 |
|
opts.quantifiers.sygusInference = false; |
985 |
|
} |
986 |
2204 |
if (opts.smt.solveIntAsBV > 0) |
987 |
|
{ |
988 |
|
reason << "solveIntAsBV"; |
989 |
|
return true; |
990 |
|
} |
991 |
|
|
992 |
|
// disable modes not supported by incremental |
993 |
2204 |
opts.smt.sortInference = false; |
994 |
2204 |
opts.uf.ufssFairnessMonotone = false; |
995 |
2204 |
opts.quantifiers.globalNegate = false; |
996 |
2204 |
opts.quantifiers.cegqiNestedQE = false; |
997 |
2204 |
opts.bv.bvAbstraction = false; |
998 |
2204 |
opts.arith.arithMLTrick = false; |
999 |
|
|
1000 |
2204 |
return false; |
1001 |
|
} |
1002 |
|
|
1003 |
2547 |
bool SetDefaults::incompatibleWithUnsatCores(Options& opts, |
1004 |
|
std::ostream& reason) const |
1005 |
|
{ |
1006 |
2547 |
if (opts.smt.simplificationMode != options::SimplificationMode::NONE) |
1007 |
|
{ |
1008 |
1166 |
if (opts.smt.simplificationModeWasSetByUser) |
1009 |
|
{ |
1010 |
|
reason << "simplification"; |
1011 |
|
return true; |
1012 |
|
} |
1013 |
1166 |
Notice() << "SmtEngine: turning off simplification to support unsat " |
1014 |
|
"cores" |
1015 |
|
<< std::endl; |
1016 |
1166 |
opts.smt.simplificationMode = options::SimplificationMode::NONE; |
1017 |
|
} |
1018 |
|
|
1019 |
2547 |
if (opts.smt.learnedRewrite) |
1020 |
|
{ |
1021 |
|
if (opts.smt.learnedRewriteWasSetByUser) |
1022 |
|
{ |
1023 |
|
reason << "learned rewrites"; |
1024 |
|
return true; |
1025 |
|
} |
1026 |
|
Notice() << "SmtEngine: turning off learned rewrites to support " |
1027 |
|
"unsat cores\n"; |
1028 |
|
opts.smt.learnedRewrite = false; |
1029 |
|
} |
1030 |
|
|
1031 |
2547 |
if (opts.arith.pbRewrites) |
1032 |
|
{ |
1033 |
|
if (opts.arith.pbRewritesWasSetByUser) |
1034 |
|
{ |
1035 |
|
reason << "pseudoboolean rewrites"; |
1036 |
|
return true; |
1037 |
|
} |
1038 |
|
Notice() << "SmtEngine: turning off pseudoboolean rewrites to support " |
1039 |
|
"unsat cores\n"; |
1040 |
|
opts.arith.pbRewrites = false; |
1041 |
|
} |
1042 |
|
|
1043 |
2547 |
if (opts.smt.sortInference) |
1044 |
|
{ |
1045 |
|
if (opts.smt.sortInferenceWasSetByUser) |
1046 |
|
{ |
1047 |
|
reason << "sort inference"; |
1048 |
|
return true; |
1049 |
|
} |
1050 |
|
Notice() << "SmtEngine: turning off sort inference to support unsat " |
1051 |
|
"cores\n"; |
1052 |
|
opts.smt.sortInference = false; |
1053 |
|
} |
1054 |
|
|
1055 |
2547 |
if (opts.quantifiers.preSkolemQuant) |
1056 |
|
{ |
1057 |
3 |
if (opts.quantifiers.preSkolemQuantWasSetByUser) |
1058 |
|
{ |
1059 |
|
reason << "pre-skolemization"; |
1060 |
|
return true; |
1061 |
|
} |
1062 |
3 |
Notice() << "SmtEngine: turning off pre-skolemization to support " |
1063 |
|
"unsat cores\n"; |
1064 |
3 |
opts.quantifiers.preSkolemQuant = false; |
1065 |
|
} |
1066 |
|
|
1067 |
2547 |
if (opts.bv.bitvectorToBool) |
1068 |
|
{ |
1069 |
60 |
if (opts.bv.bitvectorToBoolWasSetByUser) |
1070 |
|
{ |
1071 |
|
reason << "bv-to-bool"; |
1072 |
|
return true; |
1073 |
|
} |
1074 |
60 |
Notice() << "SmtEngine: turning off bitvector-to-bool to support " |
1075 |
|
"unsat cores\n"; |
1076 |
60 |
opts.bv.bitvectorToBool = false; |
1077 |
|
} |
1078 |
|
|
1079 |
2547 |
if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) |
1080 |
|
{ |
1081 |
|
if (opts.bv.boolToBitvectorWasSetByUser) |
1082 |
|
{ |
1083 |
|
reason << "bool-to-bv != off"; |
1084 |
|
return true; |
1085 |
|
} |
1086 |
|
Notice() << "SmtEngine: turning off bool-to-bv to support unsat cores\n"; |
1087 |
|
opts.bv.boolToBitvector = options::BoolToBVMode::OFF; |
1088 |
|
} |
1089 |
|
|
1090 |
2547 |
if (opts.bv.bvIntroducePow2) |
1091 |
|
{ |
1092 |
|
if (opts.bv.bvIntroducePow2WasSetByUser) |
1093 |
|
{ |
1094 |
|
reason << "bv-intro-pow2"; |
1095 |
|
return true; |
1096 |
|
} |
1097 |
|
Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat cores"; |
1098 |
|
opts.bv.bvIntroducePow2 = false; |
1099 |
|
} |
1100 |
|
|
1101 |
2547 |
if (opts.smt.repeatSimp) |
1102 |
|
{ |
1103 |
|
if (opts.smt.repeatSimpWasSetByUser) |
1104 |
|
{ |
1105 |
|
reason << "repeat-simp"; |
1106 |
|
return true; |
1107 |
|
} |
1108 |
|
Notice() << "SmtEngine: turning off repeat-simp to support unsat cores\n"; |
1109 |
|
opts.smt.repeatSimp = false; |
1110 |
|
} |
1111 |
|
|
1112 |
2547 |
if (opts.quantifiers.globalNegate) |
1113 |
|
{ |
1114 |
|
if (opts.quantifiers.globalNegateWasSetByUser) |
1115 |
|
{ |
1116 |
|
reason << "global-negate"; |
1117 |
|
return true; |
1118 |
|
} |
1119 |
|
Notice() << "SmtEngine: turning off global-negate to support unsat " |
1120 |
|
"cores\n"; |
1121 |
|
opts.quantifiers.globalNegate = false; |
1122 |
|
} |
1123 |
|
|
1124 |
2547 |
if (opts.bv.bitvectorAig) |
1125 |
|
{ |
1126 |
|
reason << "bitblast-aig"; |
1127 |
|
return true; |
1128 |
|
} |
1129 |
|
|
1130 |
2547 |
if (opts.smt.doITESimp) |
1131 |
|
{ |
1132 |
1 |
reason << "ITE simp"; |
1133 |
1 |
return true; |
1134 |
|
} |
1135 |
2546 |
if (opts.smt.unconstrainedSimp) |
1136 |
|
{ |
1137 |
|
if (opts.smt.unconstrainedSimpWasSetByUser) |
1138 |
|
{ |
1139 |
|
reason << "unconstrained simplification"; |
1140 |
|
return true; |
1141 |
|
} |
1142 |
|
Notice() << "SmtEngine: turning off unconstrained simplification to " |
1143 |
|
"support unsat cores" |
1144 |
|
<< std::endl; |
1145 |
|
opts.smt.unconstrainedSimp = false; |
1146 |
|
} |
1147 |
2546 |
return false; |
1148 |
|
} |
1149 |
|
|
1150 |
10440 |
bool SetDefaults::safeUnsatCores(const Options& opts) const |
1151 |
|
{ |
1152 |
|
// whether we want to force safe unsat cores, i.e., if we are in the default |
1153 |
|
// ASSUMPTIONS mode or PP_ONLY, since other ones are experimental |
1154 |
10440 |
return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS |
1155 |
10440 |
|| opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY; |
1156 |
|
} |
1157 |
|
|
1158 |
6826 |
bool SetDefaults::incompatibleWithQuantifiers(Options& opts, |
1159 |
|
std::ostream& reason) const |
1160 |
|
{ |
1161 |
6826 |
if (opts.smt.ackermann) |
1162 |
|
{ |
1163 |
|
reason << "ackermann"; |
1164 |
|
return true; |
1165 |
|
} |
1166 |
6826 |
if (opts.arith.nlRlvMode != options::NlRlvMode::NONE) |
1167 |
|
{ |
1168 |
|
// Theory relevance is incompatible with CEGQI and SyQI, since there is no |
1169 |
|
// appropriate policy for the relevance of counterexample lemmas (when their |
1170 |
|
// guard is entailed to be false, the entire lemma is relevant, not just the |
1171 |
|
// guard). Hence, we throw an option exception if quantifiers are enabled. |
1172 |
|
reason << "--nl-ext-rlv"; |
1173 |
|
return true; |
1174 |
|
} |
1175 |
6826 |
return false; |
1176 |
|
} |
1177 |
|
|
1178 |
9918 |
void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const |
1179 |
|
{ |
1180 |
9918 |
bool needsUf = false; |
1181 |
|
// strings require LIA, UF; widen the logic |
1182 |
9918 |
if (logic.isTheoryEnabled(THEORY_STRINGS)) |
1183 |
|
{ |
1184 |
9362 |
LogicInfo log(logic.getUnlockedCopy()); |
1185 |
|
// Strings requires arith for length constraints, and also UF |
1186 |
4681 |
needsUf = true; |
1187 |
4681 |
if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) |
1188 |
|
{ |
1189 |
134 |
Notice() |
1190 |
|
<< "Enabling linear integer arithmetic because strings are enabled" |
1191 |
|
<< std::endl; |
1192 |
134 |
log.enableTheory(THEORY_ARITH); |
1193 |
134 |
log.enableIntegers(); |
1194 |
134 |
log.arithOnlyLinear(); |
1195 |
|
} |
1196 |
4547 |
else if (!logic.areIntegersUsed()) |
1197 |
|
{ |
1198 |
|
Notice() << "Enabling integer arithmetic because strings are enabled" |
1199 |
|
<< std::endl; |
1200 |
|
log.enableIntegers(); |
1201 |
|
} |
1202 |
4681 |
logic = log; |
1203 |
4681 |
logic.lock(); |
1204 |
|
} |
1205 |
9918 |
if (opts.bv.bvAbstraction) |
1206 |
|
{ |
1207 |
|
// bv abstraction may require UF |
1208 |
4 |
Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; |
1209 |
4 |
needsUf = true; |
1210 |
|
} |
1211 |
9914 |
else if (opts.quantifiers.preSkolemQuantNested |
1212 |
9897 |
&& opts.quantifiers.preSkolemQuantNestedWasSetByUser) |
1213 |
|
{ |
1214 |
|
// if pre-skolem nested is explictly set, then we require UF. If it is |
1215 |
|
// not explicitly set, it is disabled below if UF is not present. |
1216 |
2 |
Notice() << "Enabling UF because preSkolemQuantNested requires it." |
1217 |
|
<< std::endl; |
1218 |
2 |
needsUf = true; |
1219 |
|
} |
1220 |
9918 |
if (needsUf |
1221 |
|
// Arrays, datatypes and sets permit Boolean terms and thus require UF |
1222 |
5231 |
|| logic.isTheoryEnabled(THEORY_ARRAYS) |
1223 |
4493 |
|| logic.isTheoryEnabled(THEORY_DATATYPES) |
1224 |
3215 |
|| logic.isTheoryEnabled(THEORY_SETS) |
1225 |
3141 |
|| logic.isTheoryEnabled(THEORY_BAGS) |
1226 |
|
// Non-linear arithmetic requires UF to deal with division/mod because |
1227 |
|
// their expansion introduces UFs for the division/mod-by-zero case. |
1228 |
|
// If we are eliminating non-linear arithmetic via solve-int-as-bv, |
1229 |
|
// then this is not required, since non-linear arithmetic will be |
1230 |
|
// eliminated altogether (or otherwise fail at preprocessing). |
1231 |
3141 |
|| (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() |
1232 |
585 |
&& opts.smt.solveIntAsBV == 0) |
1233 |
|
// FP requires UF since there are multiple operators that are partially |
1234 |
|
// defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more |
1235 |
|
// details). |
1236 |
12474 |
|| logic.isTheoryEnabled(THEORY_FP)) |
1237 |
|
{ |
1238 |
7428 |
if (!logic.isTheoryEnabled(THEORY_UF)) |
1239 |
|
{ |
1240 |
1848 |
LogicInfo log(logic.getUnlockedCopy()); |
1241 |
924 |
if (!needsUf) |
1242 |
|
{ |
1243 |
515 |
Notice() << "Enabling UF because " << logic << " requires it." |
1244 |
|
<< std::endl; |
1245 |
|
} |
1246 |
924 |
log.enableTheory(THEORY_UF); |
1247 |
924 |
logic = log; |
1248 |
924 |
logic.lock(); |
1249 |
|
} |
1250 |
|
} |
1251 |
9918 |
if (opts.arith.arithMLTrick) |
1252 |
|
{ |
1253 |
8 |
if (!logic.areIntegersUsed()) |
1254 |
|
{ |
1255 |
|
// enable integers |
1256 |
|
LogicInfo log(logic.getUnlockedCopy()); |
1257 |
|
Notice() << "Enabling integers because arithMLTrick requires it." |
1258 |
|
<< std::endl; |
1259 |
|
log.enableIntegers(); |
1260 |
|
logic = log; |
1261 |
|
logic.lock(); |
1262 |
|
} |
1263 |
|
} |
1264 |
9918 |
} |
1265 |
|
|
1266 |
9917 |
void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, |
1267 |
|
Options& opts) const |
1268 |
|
{ |
1269 |
9917 |
if (opts.arrays.arraysExp) |
1270 |
|
{ |
1271 |
|
// Allows to answer sat more often by default. |
1272 |
12 |
if (!opts.quantifiers.fmfBoundWasSetByUser) |
1273 |
|
{ |
1274 |
12 |
opts.quantifiers.fmfBound = true; |
1275 |
12 |
Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; |
1276 |
|
} |
1277 |
|
} |
1278 |
9917 |
if (logic.hasCardinalityConstraints()) |
1279 |
|
{ |
1280 |
|
// must have finite model finding on |
1281 |
26 |
opts.quantifiers.finiteModelFind = true; |
1282 |
|
} |
1283 |
|
|
1284 |
9917 |
if (opts.quantifiers.instMaxLevel != -1) |
1285 |
|
{ |
1286 |
4 |
Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" |
1287 |
|
<< std::endl; |
1288 |
4 |
opts.quantifiers.cegqi = false; |
1289 |
|
} |
1290 |
|
|
1291 |
9917 |
if ((opts.quantifiers.fmfBoundLazyWasSetByUser |
1292 |
4 |
&& opts.quantifiers.fmfBoundLazy) |
1293 |
9913 |
|| (opts.quantifiers.fmfBoundIntWasSetByUser |
1294 |
14 |
&& opts.quantifiers.fmfBoundInt)) |
1295 |
|
{ |
1296 |
18 |
opts.quantifiers.fmfBound = true; |
1297 |
36 |
Trace("smt") |
1298 |
18 |
<< "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n"; |
1299 |
|
} |
1300 |
|
// now have determined whether fmfBound is on/off |
1301 |
|
// apply fmfBound options |
1302 |
9917 |
if (opts.quantifiers.fmfBound) |
1303 |
|
{ |
1304 |
79 |
if (!opts.quantifiers.mbqiModeWasSetByUser |
1305 |
|
|| (opts.quantifiers.mbqiMode != options::MbqiMode::NONE |
1306 |
|
&& opts.quantifiers.mbqiMode != options::MbqiMode::FMC)) |
1307 |
|
{ |
1308 |
|
// if bounded integers are set, use no MBQI by default |
1309 |
79 |
opts.quantifiers.mbqiMode = options::MbqiMode::NONE; |
1310 |
|
} |
1311 |
79 |
if (!opts.quantifiers.prenexQuantUserWasSetByUser) |
1312 |
|
{ |
1313 |
79 |
opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; |
1314 |
|
} |
1315 |
|
} |
1316 |
9917 |
if (logic.isHigherOrder()) |
1317 |
|
{ |
1318 |
|
// if higher-order, then current variants of model-based instantiation |
1319 |
|
// cannot be used |
1320 |
191 |
if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE) |
1321 |
|
{ |
1322 |
139 |
opts.quantifiers.mbqiMode = options::MbqiMode::NONE; |
1323 |
|
} |
1324 |
191 |
if (!opts.quantifiers.hoElimStoreAxWasSetByUser) |
1325 |
|
{ |
1326 |
|
// by default, use store axioms only if --ho-elim is set |
1327 |
190 |
opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim; |
1328 |
|
} |
1329 |
|
// Cannot use macros, since lambda lifting and macro elimination are inverse |
1330 |
|
// operations. |
1331 |
191 |
if (opts.quantifiers.macrosQuant) |
1332 |
|
{ |
1333 |
|
opts.quantifiers.macrosQuant = false; |
1334 |
|
} |
1335 |
|
// HOL is incompatible with fmfBound |
1336 |
191 |
if (opts.quantifiers.fmfBound) |
1337 |
|
{ |
1338 |
6 |
if (opts.quantifiers.fmfBoundWasSetByUser |
1339 |
4 |
|| opts.quantifiers.fmfBoundLazyWasSetByUser |
1340 |
4 |
|| opts.quantifiers.fmfBoundIntWasSetByUser) |
1341 |
|
{ |
1342 |
6 |
Notice() << "Disabling bound finite-model finding since it is " |
1343 |
|
"incompatible with HOL.\n"; |
1344 |
|
} |
1345 |
|
|
1346 |
6 |
opts.quantifiers.fmfBound = false; |
1347 |
6 |
Trace("smt") << "turning off fmf-bound, since HOL\n"; |
1348 |
|
} |
1349 |
|
} |
1350 |
9917 |
if (opts.quantifiers.fmfFunWellDefinedRelevant) |
1351 |
|
{ |
1352 |
12 |
if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) |
1353 |
|
{ |
1354 |
12 |
opts.quantifiers.fmfFunWellDefined = true; |
1355 |
|
} |
1356 |
|
} |
1357 |
9917 |
if (opts.quantifiers.fmfFunWellDefined) |
1358 |
|
{ |
1359 |
71 |
if (!opts.quantifiers.finiteModelFindWasSetByUser) |
1360 |
|
{ |
1361 |
69 |
opts.quantifiers.finiteModelFind = true; |
1362 |
|
} |
1363 |
|
} |
1364 |
|
|
1365 |
|
// now, have determined whether finite model find is on/off |
1366 |
|
// apply finite model finding options |
1367 |
9917 |
if (opts.quantifiers.finiteModelFind) |
1368 |
|
{ |
1369 |
|
// apply conservative quantifiers splitting |
1370 |
288 |
if (!opts.quantifiers.quantDynamicSplitWasSetByUser) |
1371 |
|
{ |
1372 |
288 |
opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT; |
1373 |
|
} |
1374 |
288 |
if (!opts.quantifiers.eMatchingWasSetByUser) |
1375 |
|
{ |
1376 |
288 |
opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine; |
1377 |
|
} |
1378 |
288 |
if (!opts.quantifiers.instWhenModeWasSetByUser) |
1379 |
|
{ |
1380 |
|
// instantiate only on last call |
1381 |
288 |
if (opts.quantifiers.eMatching) |
1382 |
|
{ |
1383 |
8 |
opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; |
1384 |
|
} |
1385 |
|
} |
1386 |
|
} |
1387 |
|
|
1388 |
|
// apply sygus options |
1389 |
|
// if we are attempting to rewrite everything to SyGuS, use sygus() |
1390 |
9917 |
if (usesSygus(opts)) |
1391 |
|
{ |
1392 |
680 |
setDefaultsSygus(opts); |
1393 |
|
} |
1394 |
|
// counterexample-guided instantiation for non-sygus |
1395 |
|
// enable if any possible quantifiers with arithmetic, datatypes or bitvectors |
1396 |
19834 |
if ((logic.isQuantified() |
1397 |
6826 |
&& (logic.isTheoryEnabled(THEORY_ARITH) |
1398 |
310 |
|| logic.isTheoryEnabled(THEORY_DATATYPES) |
1399 |
302 |
|| logic.isTheoryEnabled(THEORY_BV) |
1400 |
114 |
|| logic.isTheoryEnabled(THEORY_FP))) |
1401 |
13122 |
|| opts.quantifiers.cegqiAll) |
1402 |
|
{ |
1403 |
6712 |
if (!opts.quantifiers.cegqiWasSetByUser) |
1404 |
|
{ |
1405 |
6689 |
opts.quantifiers.cegqi = true; |
1406 |
|
} |
1407 |
|
// check whether we should apply full cbqi |
1408 |
6712 |
if (logic.isPure(THEORY_BV)) |
1409 |
|
{ |
1410 |
152 |
if (!opts.quantifiers.cegqiFullEffortWasSetByUser) |
1411 |
|
{ |
1412 |
60 |
opts.quantifiers.cegqiFullEffort = true; |
1413 |
|
} |
1414 |
|
} |
1415 |
|
} |
1416 |
9917 |
if (opts.quantifiers.cegqi) |
1417 |
|
{ |
1418 |
6710 |
if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) |
1419 |
|
{ |
1420 |
265 |
if (!opts.quantifiers.quantConflictFindWasSetByUser) |
1421 |
|
{ |
1422 |
265 |
opts.quantifiers.quantConflictFind = false; |
1423 |
|
} |
1424 |
265 |
if (!opts.quantifiers.instNoEntailWasSetByUser) |
1425 |
|
{ |
1426 |
265 |
opts.quantifiers.instNoEntail = false; |
1427 |
|
} |
1428 |
265 |
if (!opts.quantifiers.instWhenModeWasSetByUser |
1429 |
265 |
&& opts.quantifiers.cegqiModel) |
1430 |
|
{ |
1431 |
|
// only instantiation should happen at last call when model is avaiable |
1432 |
265 |
opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; |
1433 |
|
} |
1434 |
|
} |
1435 |
|
else |
1436 |
|
{ |
1437 |
|
// only supported in pure arithmetic or pure BV |
1438 |
6445 |
opts.quantifiers.cegqiNestedQE = false; |
1439 |
|
} |
1440 |
6710 |
if (opts.quantifiers.globalNegate) |
1441 |
|
{ |
1442 |
6 |
if (!opts.quantifiers.prenexQuantWasSetByUser) |
1443 |
|
{ |
1444 |
6 |
opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; |
1445 |
|
} |
1446 |
|
} |
1447 |
|
} |
1448 |
|
// implied options... |
1449 |
9917 |
if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint) |
1450 |
|
{ |
1451 |
8 |
opts.quantifiers.quantConflictFind = true; |
1452 |
|
} |
1453 |
9917 |
if (opts.quantifiers.cegqiNestedQE) |
1454 |
|
{ |
1455 |
30 |
opts.quantifiers.prenexQuantUser = true; |
1456 |
30 |
if (!opts.quantifiers.preSkolemQuantWasSetByUser) |
1457 |
|
{ |
1458 |
30 |
opts.quantifiers.preSkolemQuant = true; |
1459 |
|
} |
1460 |
|
} |
1461 |
|
// for induction techniques |
1462 |
9917 |
if (opts.quantifiers.quantInduction) |
1463 |
|
{ |
1464 |
14 |
if (!opts.quantifiers.dtStcInductionWasSetByUser) |
1465 |
|
{ |
1466 |
14 |
opts.quantifiers.dtStcInduction = true; |
1467 |
|
} |
1468 |
14 |
if (!opts.quantifiers.intWfInductionWasSetByUser) |
1469 |
|
{ |
1470 |
14 |
opts.quantifiers.intWfInduction = true; |
1471 |
|
} |
1472 |
|
} |
1473 |
9917 |
if (opts.quantifiers.dtStcInduction) |
1474 |
|
{ |
1475 |
|
// try to remove ITEs from quantified formulas |
1476 |
14 |
if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser) |
1477 |
|
{ |
1478 |
14 |
opts.quantifiers.iteDtTesterSplitQuant = true; |
1479 |
|
} |
1480 |
14 |
if (!opts.quantifiers.iteLiftQuantWasSetByUser) |
1481 |
|
{ |
1482 |
14 |
opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL; |
1483 |
|
} |
1484 |
|
} |
1485 |
9917 |
if (opts.quantifiers.intWfInduction) |
1486 |
|
{ |
1487 |
20 |
if (!opts.quantifiers.purifyTriggersWasSetByUser) |
1488 |
|
{ |
1489 |
20 |
opts.quantifiers.purifyTriggers = true; |
1490 |
|
} |
1491 |
|
} |
1492 |
9917 |
if (opts.quantifiers.conjectureNoFilter) |
1493 |
|
{ |
1494 |
4 |
if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser) |
1495 |
|
{ |
1496 |
4 |
opts.quantifiers.conjectureFilterActiveTerms = false; |
1497 |
|
} |
1498 |
4 |
if (!opts.quantifiers.conjectureFilterCanonicalWasSetByUser) |
1499 |
|
{ |
1500 |
4 |
opts.quantifiers.conjectureFilterCanonical = false; |
1501 |
|
} |
1502 |
4 |
if (!opts.quantifiers.conjectureFilterModelWasSetByUser) |
1503 |
|
{ |
1504 |
|
opts.quantifiers.conjectureFilterModel = false; |
1505 |
|
} |
1506 |
|
} |
1507 |
9917 |
if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) |
1508 |
|
{ |
1509 |
|
if (opts.quantifiers.conjectureGenPerRound > 0) |
1510 |
|
{ |
1511 |
|
opts.quantifiers.conjectureGen = true; |
1512 |
|
} |
1513 |
|
else |
1514 |
|
{ |
1515 |
|
opts.quantifiers.conjectureGen = false; |
1516 |
|
} |
1517 |
|
} |
1518 |
|
// can't pre-skolemize nested quantifiers without UF theory |
1519 |
9917 |
if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant) |
1520 |
|
{ |
1521 |
30 |
if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) |
1522 |
|
{ |
1523 |
30 |
opts.quantifiers.preSkolemQuantNested = false; |
1524 |
|
} |
1525 |
|
} |
1526 |
9917 |
if (!logic.isTheoryEnabled(THEORY_DATATYPES)) |
1527 |
|
{ |
1528 |
4392 |
opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE; |
1529 |
|
} |
1530 |
9917 |
} |
1531 |
|
|
1532 |
680 |
void SetDefaults::setDefaultsSygus(Options& opts) const |
1533 |
|
{ |
1534 |
680 |
if (!opts.quantifiers.sygus) |
1535 |
|
{ |
1536 |
332 |
Trace("smt") << "turning on sygus" << std::endl; |
1537 |
|
} |
1538 |
680 |
opts.quantifiers.sygus = true; |
1539 |
|
// must use Ferrante/Rackoff for real arithmetic |
1540 |
680 |
if (!opts.quantifiers.cegqiMidpointWasSetByUser) |
1541 |
|
{ |
1542 |
680 |
opts.quantifiers.cegqiMidpoint = true; |
1543 |
|
} |
1544 |
|
// must disable cegqi-bv since it may introduce witness terms, which |
1545 |
|
// cannot appear in synthesis solutions |
1546 |
680 |
if (!opts.quantifiers.cegqiBvWasSetByUser) |
1547 |
|
{ |
1548 |
677 |
opts.quantifiers.cegqiBv = false; |
1549 |
|
} |
1550 |
680 |
if (opts.quantifiers.sygusRepairConst) |
1551 |
|
{ |
1552 |
160 |
if (!opts.quantifiers.cegqiWasSetByUser) |
1553 |
|
{ |
1554 |
160 |
opts.quantifiers.cegqi = true; |
1555 |
|
} |
1556 |
|
} |
1557 |
680 |
if (opts.quantifiers.sygusInference) |
1558 |
|
{ |
1559 |
|
// optimization: apply preskolemization, makes it succeed more often |
1560 |
57 |
if (!opts.quantifiers.preSkolemQuantWasSetByUser) |
1561 |
|
{ |
1562 |
57 |
opts.quantifiers.preSkolemQuant = true; |
1563 |
|
} |
1564 |
57 |
if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) |
1565 |
|
{ |
1566 |
57 |
opts.quantifiers.preSkolemQuantNested = true; |
1567 |
|
} |
1568 |
|
} |
1569 |
|
// counterexample-guided instantiation for sygus |
1570 |
680 |
if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) |
1571 |
|
{ |
1572 |
572 |
opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; |
1573 |
|
} |
1574 |
680 |
if (!opts.quantifiers.quantConflictFindWasSetByUser) |
1575 |
|
{ |
1576 |
680 |
opts.quantifiers.quantConflictFind = false; |
1577 |
|
} |
1578 |
680 |
if (!opts.quantifiers.instNoEntailWasSetByUser) |
1579 |
|
{ |
1580 |
680 |
opts.quantifiers.instNoEntail = false; |
1581 |
|
} |
1582 |
680 |
if (!opts.quantifiers.cegqiFullEffortWasSetByUser) |
1583 |
|
{ |
1584 |
|
// should use full effort cbqi for single invocation and repair const |
1585 |
680 |
opts.quantifiers.cegqiFullEffort = true; |
1586 |
|
} |
1587 |
680 |
if (opts.quantifiers.sygusRew) |
1588 |
|
{ |
1589 |
6 |
opts.quantifiers.sygusRewSynth = true; |
1590 |
6 |
opts.quantifiers.sygusRewVerify = true; |
1591 |
|
} |
1592 |
680 |
if (opts.quantifiers.sygusRewSynthInput) |
1593 |
|
{ |
1594 |
|
// If we are using synthesis rewrite rules from input, we use |
1595 |
|
// sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for |
1596 |
|
// details on this technique. |
1597 |
|
opts.quantifiers.sygusRewSynth = true; |
1598 |
|
// we should not use the extended rewriter, since we are interested |
1599 |
|
// in rewrites that are not in the main rewriter |
1600 |
|
if (!opts.quantifiers.sygusExtRewWasSetByUser) |
1601 |
|
{ |
1602 |
|
opts.quantifiers.sygusExtRew = false; |
1603 |
|
} |
1604 |
|
} |
1605 |
|
// Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm |
1606 |
|
// is one that is specialized for returning a single solution. Non-basic |
1607 |
|
// sygus algorithms currently include the PBE solver, UNIF+PI, static |
1608 |
|
// template inference for invariant synthesis, and single invocation |
1609 |
|
// techniques. |
1610 |
680 |
bool reqBasicSygus = false; |
1611 |
680 |
if (opts.smt.produceAbducts) |
1612 |
|
{ |
1613 |
|
// if doing abduction, we should filter strong solutions |
1614 |
16 |
if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) |
1615 |
|
{ |
1616 |
16 |
opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; |
1617 |
|
} |
1618 |
|
// we must use basic sygus algorithms, since e.g. we require checking |
1619 |
|
// a sygus side condition for consistency with axioms. |
1620 |
16 |
reqBasicSygus = true; |
1621 |
|
} |
1622 |
680 |
if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify |
1623 |
673 |
|| opts.quantifiers.sygusQueryGen) |
1624 |
|
{ |
1625 |
|
// rewrite rule synthesis implies that sygus stream must be true |
1626 |
7 |
opts.quantifiers.sygusStream = true; |
1627 |
|
} |
1628 |
680 |
if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) |
1629 |
|
{ |
1630 |
|
// Streaming and incremental mode are incompatible with techniques that |
1631 |
|
// focus the search towards finding a single solution. |
1632 |
17 |
reqBasicSygus = true; |
1633 |
|
} |
1634 |
|
// Now, disable options for non-basic sygus algorithms, if necessary. |
1635 |
680 |
if (reqBasicSygus) |
1636 |
|
{ |
1637 |
31 |
if (!opts.quantifiers.sygusUnifPbeWasSetByUser) |
1638 |
|
{ |
1639 |
31 |
opts.quantifiers.sygusUnifPbe = false; |
1640 |
|
} |
1641 |
31 |
if (opts.quantifiers.sygusUnifPiWasSetByUser) |
1642 |
|
{ |
1643 |
|
opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; |
1644 |
|
} |
1645 |
31 |
if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) |
1646 |
|
{ |
1647 |
31 |
opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; |
1648 |
|
} |
1649 |
31 |
if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) |
1650 |
|
{ |
1651 |
31 |
opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; |
1652 |
|
} |
1653 |
|
} |
1654 |
|
// do not miniscope |
1655 |
680 |
if (!opts.quantifiers.miniscopeQuantWasSetByUser) |
1656 |
|
{ |
1657 |
528 |
opts.quantifiers.miniscopeQuant = false; |
1658 |
|
} |
1659 |
680 |
if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) |
1660 |
|
{ |
1661 |
530 |
opts.quantifiers.miniscopeQuantFreeVar = false; |
1662 |
|
} |
1663 |
680 |
if (!opts.quantifiers.quantSplitWasSetByUser) |
1664 |
|
{ |
1665 |
530 |
opts.quantifiers.quantSplit = false; |
1666 |
|
} |
1667 |
|
// do not do macros |
1668 |
680 |
if (!opts.quantifiers.macrosQuantWasSetByUser) |
1669 |
|
{ |
1670 |
680 |
opts.quantifiers.macrosQuant = false; |
1671 |
|
} |
1672 |
680 |
} |
1673 |
9917 |
void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic, |
1674 |
|
Options& opts) const |
1675 |
|
{ |
1676 |
|
// Set decision mode based on logic (if not set by user) |
1677 |
9917 |
if (opts.decision.decisionModeWasSetByUser) |
1678 |
|
{ |
1679 |
136 |
return; |
1680 |
|
} |
1681 |
|
options::DecisionMode decMode = |
1682 |
|
// anything that uses sygus uses internal |
1683 |
18898 |
usesSygus(opts) ? options::DecisionMode::INTERNAL : |
1684 |
|
// ALL or its supersets |
1685 |
9117 |
logic.hasEverything() |
1686 |
14276 |
? options::DecisionMode::JUSTIFICATION |
1687 |
|
: ( // QF_BV |
1688 |
12632 |
(not logic.isQuantified() && logic.isPure(THEORY_BV)) || |
1689 |
|
// QF_AUFBV or QF_ABV or QF_UFBV |
1690 |
4432 |
(not logic.isQuantified() |
1691 |
2314 |
&& (logic.isTheoryEnabled(THEORY_ARRAYS) |
1692 |
1880 |
|| logic.isTheoryEnabled(THEORY_UF)) |
1693 |
1559 |
&& logic.isTheoryEnabled(THEORY_BV)) |
1694 |
4007 |
|| |
1695 |
|
// QF_AUFLIA (and may be ends up enabling |
1696 |
|
// QF_AUFLRA?) |
1697 |
4007 |
(not logic.isQuantified() |
1698 |
1889 |
&& logic.isTheoryEnabled(THEORY_ARRAYS) |
1699 |
174 |
&& logic.isTheoryEnabled(THEORY_UF) |
1700 |
174 |
&& logic.isTheoryEnabled(THEORY_ARITH)) |
1701 |
3937 |
|| |
1702 |
|
// QF_LRA |
1703 |
3937 |
(not logic.isQuantified() |
1704 |
1819 |
&& logic.isPure(THEORY_ARITH) && logic.isLinear() |
1705 |
729 |
&& !logic.isDifferenceLogic() |
1706 |
712 |
&& !logic.areIntegersUsed()) |
1707 |
3689 |
|| |
1708 |
|
// Quantifiers |
1709 |
5260 |
logic.isQuantified() || |
1710 |
|
// Strings |
1711 |
1571 |
logic.isTheoryEnabled(THEORY_STRINGS) |
1712 |
8747 |
? options::DecisionMode::JUSTIFICATION |
1713 |
9781 |
: options::DecisionMode::INTERNAL); |
1714 |
|
|
1715 |
|
bool stoponly = |
1716 |
|
// ALL or its supersets |
1717 |
15461 |
logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS) |
1718 |
15309 |
? false |
1719 |
|
: ( // QF_AUFLIA |
1720 |
5112 |
(not logic.isQuantified() |
1721 |
3041 |
&& logic.isTheoryEnabled(THEORY_ARRAYS) |
1722 |
434 |
&& logic.isTheoryEnabled(THEORY_UF) |
1723 |
434 |
&& logic.isTheoryEnabled(THEORY_ARITH)) |
1724 |
|
|| |
1725 |
|
// QF_LRA |
1726 |
7817 |
(not logic.isQuantified() && logic.isPure(THEORY_ARITH) |
1727 |
729 |
&& logic.isLinear() && !logic.isDifferenceLogic() |
1728 |
712 |
&& !logic.areIntegersUsed()) |
1729 |
4944 |
? true |
1730 |
9781 |
: false); |
1731 |
|
|
1732 |
9781 |
opts.decision.decisionMode = decMode; |
1733 |
9781 |
if (stoponly) |
1734 |
|
{ |
1735 |
416 |
if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION) |
1736 |
|
{ |
1737 |
416 |
opts.decision.decisionMode = options::DecisionMode::STOPONLY; |
1738 |
|
} |
1739 |
|
else |
1740 |
|
{ |
1741 |
|
Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL); |
1742 |
|
} |
1743 |
|
} |
1744 |
19562 |
Trace("smt") << "setting decision mode to " << opts.decision.decisionMode |
1745 |
9781 |
<< std::endl; |
1746 |
|
} |
1747 |
|
|
1748 |
|
} // namespace smt |
1749 |
29517 |
} // namespace cvc5 |