1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Aina Niemetz |
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 |
|
* Option template for option modules. |
14 |
|
* |
15 |
|
* For each <module>_options.toml configuration file, mkoptions.py |
16 |
|
* expands this template and generates a <module>_options.cpp file. |
17 |
|
*/ |
18 |
|
#include "options/smt_options.h" |
19 |
|
|
20 |
|
#include <iostream> |
21 |
|
|
22 |
|
#include "base/check.h" |
23 |
|
#include "options/option_exception.h" |
24 |
|
|
25 |
|
namespace cvc5::options { |
26 |
|
|
27 |
|
// clang-format off |
28 |
|
std::ostream& operator<<(std::ostream& os, BlockModelsMode mode) |
29 |
|
{ |
30 |
|
switch(mode) |
31 |
|
{ |
32 |
|
case BlockModelsMode::NONE: return os << "BlockModelsMode::NONE"; |
33 |
|
case BlockModelsMode::VALUES: return os << "BlockModelsMode::VALUES"; |
34 |
|
case BlockModelsMode::LITERALS: return os << "BlockModelsMode::LITERALS"; |
35 |
|
default: Unreachable(); |
36 |
|
} |
37 |
|
return os; |
38 |
|
} |
39 |
21 |
BlockModelsMode stringToBlockModelsMode(const std::string& optarg) |
40 |
|
{ |
41 |
21 |
if (optarg == "none") return BlockModelsMode::NONE; |
42 |
21 |
else if (optarg == "values") return BlockModelsMode::VALUES; |
43 |
18 |
else if (optarg == "literals") return BlockModelsMode::LITERALS; |
44 |
|
else if (optarg == "help") |
45 |
|
{ |
46 |
|
std::cerr << R"FOOBAR( |
47 |
|
Blocking models modes. |
48 |
|
Available modes for --block-models are: |
49 |
|
+ none (default) |
50 |
|
Do not block models. |
51 |
|
+ values |
52 |
|
Block models based on the concrete model values for the free variables. |
53 |
|
+ literals |
54 |
|
Block models based on the SAT skeleton. |
55 |
|
)FOOBAR"; |
56 |
|
std::exit(1); |
57 |
|
} |
58 |
|
throw OptionException(std::string("unknown option for --block-models: `") + |
59 |
|
optarg + "'. Try --block-models=help."); |
60 |
|
} |
61 |
|
std::ostream& operator<<(std::ostream& os, DifficultyMode mode) |
62 |
|
{ |
63 |
|
switch(mode) |
64 |
|
{ |
65 |
|
case DifficultyMode::MODEL_CHECK: return os << "DifficultyMode::MODEL_CHECK"; |
66 |
|
case DifficultyMode::LEMMA_LITERAL: return os << "DifficultyMode::LEMMA_LITERAL"; |
67 |
|
default: Unreachable(); |
68 |
|
} |
69 |
|
return os; |
70 |
|
} |
71 |
|
DifficultyMode stringToDifficultyMode(const std::string& optarg) |
72 |
|
{ |
73 |
|
if (optarg == "model-check") return DifficultyMode::MODEL_CHECK; |
74 |
|
else if (optarg == "lemma-literal") return DifficultyMode::LEMMA_LITERAL; |
75 |
|
else if (optarg == "help") |
76 |
|
{ |
77 |
|
std::cerr << R"FOOBAR( |
78 |
|
difficulty output modes. |
79 |
|
Available modes for --difficulty-mode are: |
80 |
|
+ model-check |
81 |
|
Difficulty of an assertion is how many times it was not satisfied in a |
82 |
|
candidate model. |
83 |
|
+ lemma-literal (default) |
84 |
|
Difficulty of an assertion is how many lemmas use a literal that the assertion |
85 |
|
depends on to be satisfied. |
86 |
|
)FOOBAR"; |
87 |
|
std::exit(1); |
88 |
|
} |
89 |
|
throw OptionException(std::string("unknown option for --difficulty-mode: `") + |
90 |
|
optarg + "'. Try --difficulty-mode=help."); |
91 |
|
} |
92 |
|
std::ostream& operator<<(std::ostream& os, IandMode mode) |
93 |
|
{ |
94 |
|
switch(mode) |
95 |
|
{ |
96 |
|
case IandMode::VALUE: return os << "IandMode::VALUE"; |
97 |
|
case IandMode::SUM: return os << "IandMode::SUM"; |
98 |
|
case IandMode::BITWISE: return os << "IandMode::BITWISE"; |
99 |
|
default: Unreachable(); |
100 |
|
} |
101 |
|
return os; |
102 |
|
} |
103 |
67 |
IandMode stringToIandMode(const std::string& optarg) |
104 |
|
{ |
105 |
67 |
if (optarg == "value") return IandMode::VALUE; |
106 |
48 |
else if (optarg == "sum") return IandMode::SUM; |
107 |
30 |
else if (optarg == "bitwise") return IandMode::BITWISE; |
108 |
|
else if (optarg == "help") |
109 |
|
{ |
110 |
|
std::cerr << R"FOOBAR( |
111 |
|
Refinement modes for integer AND |
112 |
|
Available modes for --iand-mode are: |
113 |
|
+ value (default) |
114 |
|
value-based refinement |
115 |
|
+ sum |
116 |
|
use sum to represent integer AND in refinement |
117 |
|
+ bitwise |
118 |
|
use bitwise comparisons on binary representation of integer for refinement |
119 |
|
(experimental) |
120 |
|
)FOOBAR"; |
121 |
|
std::exit(1); |
122 |
|
} |
123 |
|
throw OptionException(std::string("unknown option for --iand-mode: `") + |
124 |
|
optarg + "'. Try --iand-mode=help."); |
125 |
|
} |
126 |
|
std::ostream& operator<<(std::ostream& os, ModelCoresMode mode) |
127 |
|
{ |
128 |
|
switch(mode) |
129 |
|
{ |
130 |
|
case ModelCoresMode::NON_IMPLIED: return os << "ModelCoresMode::NON_IMPLIED"; |
131 |
|
case ModelCoresMode::NONE: return os << "ModelCoresMode::NONE"; |
132 |
|
case ModelCoresMode::SIMPLE: return os << "ModelCoresMode::SIMPLE"; |
133 |
|
default: Unreachable(); |
134 |
|
} |
135 |
|
return os; |
136 |
|
} |
137 |
8 |
ModelCoresMode stringToModelCoresMode(const std::string& optarg) |
138 |
|
{ |
139 |
8 |
if (optarg == "non-implied") return ModelCoresMode::NON_IMPLIED; |
140 |
4 |
else if (optarg == "none") return ModelCoresMode::NONE; |
141 |
4 |
else if (optarg == "simple") return ModelCoresMode::SIMPLE; |
142 |
|
else if (optarg == "help") |
143 |
|
{ |
144 |
|
std::cerr << R"FOOBAR( |
145 |
|
Model cores modes. |
146 |
|
Available modes for --model-cores are: |
147 |
|
+ non-implied |
148 |
|
Only include a subset of variables whose values, in addition to the values of |
149 |
|
variables whose values are implied, are sufficient to show the input formula |
150 |
|
is satisfied by the given model. |
151 |
|
+ none (default) |
152 |
|
Do not compute model cores. |
153 |
|
+ simple |
154 |
|
Only include a subset of variables whose values are sufficient to show the |
155 |
|
input formula is satisfied by the given model. |
156 |
|
)FOOBAR"; |
157 |
|
std::exit(1); |
158 |
|
} |
159 |
|
throw OptionException(std::string("unknown option for --model-cores: `") + |
160 |
|
optarg + "'. Try --model-cores=help."); |
161 |
|
} |
162 |
|
std::ostream& operator<<(std::ostream& os, ModelUninterpPrintMode mode) |
163 |
|
{ |
164 |
|
switch(mode) |
165 |
|
{ |
166 |
|
case ModelUninterpPrintMode::DeclFun: return os << "ModelUninterpPrintMode::DeclFun"; |
167 |
|
case ModelUninterpPrintMode::DeclSortAndFun: return os << "ModelUninterpPrintMode::DeclSortAndFun"; |
168 |
|
case ModelUninterpPrintMode::None: return os << "ModelUninterpPrintMode::None"; |
169 |
|
default: Unreachable(); |
170 |
|
} |
171 |
|
return os; |
172 |
|
} |
173 |
1 |
ModelUninterpPrintMode stringToModelUninterpPrintMode(const std::string& optarg) |
174 |
|
{ |
175 |
1 |
if (optarg == "decl-fun") return ModelUninterpPrintMode::DeclFun; |
176 |
|
else if (optarg == "decl-sort-and-fun") return ModelUninterpPrintMode::DeclSortAndFun; |
177 |
|
else if (optarg == "none") return ModelUninterpPrintMode::None; |
178 |
|
else if (optarg == "help") |
179 |
|
{ |
180 |
|
std::cerr << R"FOOBAR( |
181 |
|
uninterpreted elements in models printing modes. |
182 |
|
Available modes for --model-u-print are: |
183 |
|
+ decl-fun |
184 |
|
print uninterpreted elements declare-fun, but don't include a declare-sort for |
185 |
|
the sort |
186 |
|
+ decl-sort-and-fun |
187 |
|
print uninterpreted elements declare-fun, and also include a declare-sort for |
188 |
|
the sort |
189 |
|
+ none (default) |
190 |
|
(default) do not print declarations of uninterpreted elements in models. |
191 |
|
)FOOBAR"; |
192 |
|
std::exit(1); |
193 |
|
} |
194 |
|
throw OptionException(std::string("unknown option for --model-u-print: `") + |
195 |
|
optarg + "'. Try --model-u-print=help."); |
196 |
|
} |
197 |
|
std::ostream& operator<<(std::ostream& os, ProduceInterpols mode) |
198 |
|
{ |
199 |
|
switch(mode) |
200 |
|
{ |
201 |
|
case ProduceInterpols::CONJECTURE: return os << "ProduceInterpols::CONJECTURE"; |
202 |
|
case ProduceInterpols::NONE: return os << "ProduceInterpols::NONE"; |
203 |
|
case ProduceInterpols::DEFAULT: return os << "ProduceInterpols::DEFAULT"; |
204 |
|
case ProduceInterpols::ALL: return os << "ProduceInterpols::ALL"; |
205 |
|
case ProduceInterpols::SHARED: return os << "ProduceInterpols::SHARED"; |
206 |
|
case ProduceInterpols::ASSUMPTIONS: return os << "ProduceInterpols::ASSUMPTIONS"; |
207 |
|
default: Unreachable(); |
208 |
|
} |
209 |
|
return os; |
210 |
|
} |
211 |
11 |
ProduceInterpols stringToProduceInterpols(const std::string& optarg) |
212 |
|
{ |
213 |
11 |
if (optarg == "conjecture") return ProduceInterpols::CONJECTURE; |
214 |
9 |
else if (optarg == "none") return ProduceInterpols::NONE; |
215 |
9 |
else if (optarg == "default") return ProduceInterpols::DEFAULT; |
216 |
|
else if (optarg == "all") return ProduceInterpols::ALL; |
217 |
|
else if (optarg == "shared") return ProduceInterpols::SHARED; |
218 |
|
else if (optarg == "assumptions") return ProduceInterpols::ASSUMPTIONS; |
219 |
|
else if (optarg == "help") |
220 |
|
{ |
221 |
|
std::cerr << R"FOOBAR( |
222 |
|
Interpolants grammar mode |
223 |
|
Available modes for --produce-interpols are: |
224 |
|
+ conjecture |
225 |
|
use only operators that occur in the conjecture |
226 |
|
+ none (default) |
227 |
|
don't compute interpolants |
228 |
|
+ default |
229 |
|
use the default grammar for the theory or the user-defined grammar if given |
230 |
|
+ all |
231 |
|
use only operators that occur either in the assumptions or the conjecture |
232 |
|
+ shared |
233 |
|
use only operators that occur both in the assumptions and the conjecture |
234 |
|
+ assumptions |
235 |
|
use only operators that occur in the assumptions |
236 |
|
)FOOBAR"; |
237 |
|
std::exit(1); |
238 |
|
} |
239 |
|
throw OptionException(std::string("unknown option for --produce-interpols: `") + |
240 |
|
optarg + "'. Try --produce-interpols=help."); |
241 |
|
} |
242 |
1 |
std::ostream& operator<<(std::ostream& os, SimplificationMode mode) |
243 |
|
{ |
244 |
1 |
switch(mode) |
245 |
|
{ |
246 |
1 |
case SimplificationMode::NONE: return os << "SimplificationMode::NONE"; |
247 |
|
case SimplificationMode::BATCH: return os << "SimplificationMode::BATCH"; |
248 |
|
default: Unreachable(); |
249 |
|
} |
250 |
|
return os; |
251 |
|
} |
252 |
32 |
SimplificationMode stringToSimplificationMode(const std::string& optarg) |
253 |
|
{ |
254 |
32 |
if (optarg == "none") return SimplificationMode::NONE; |
255 |
|
else if (optarg == "batch") return SimplificationMode::BATCH; |
256 |
|
else if (optarg == "help") |
257 |
|
{ |
258 |
|
std::cerr << R"FOOBAR( |
259 |
|
Simplification modes. |
260 |
|
Available modes for --simplification are: |
261 |
|
+ none |
262 |
|
Do not perform nonclausal simplification. |
263 |
|
+ batch (default) |
264 |
|
Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) |
265 |
|
propagation for all of them only after reaching a querying command (CHECKSAT |
266 |
|
or QUERY or predicate SUBTYPE declaration). |
267 |
|
)FOOBAR"; |
268 |
|
std::exit(1); |
269 |
|
} |
270 |
|
throw OptionException(std::string("unknown option for --simplification: `") + |
271 |
|
optarg + "'. Try --simplification=help."); |
272 |
|
} |
273 |
|
std::ostream& operator<<(std::ostream& os, SolveBVAsIntMode mode) |
274 |
|
{ |
275 |
|
switch(mode) |
276 |
|
{ |
277 |
|
case SolveBVAsIntMode::OFF: return os << "SolveBVAsIntMode::OFF"; |
278 |
|
case SolveBVAsIntMode::IAND: return os << "SolveBVAsIntMode::IAND"; |
279 |
|
case SolveBVAsIntMode::BV: return os << "SolveBVAsIntMode::BV"; |
280 |
|
case SolveBVAsIntMode::SUM: return os << "SolveBVAsIntMode::SUM"; |
281 |
|
default: Unreachable(); |
282 |
|
} |
283 |
|
return os; |
284 |
|
} |
285 |
148 |
SolveBVAsIntMode stringToSolveBVAsIntMode(const std::string& optarg) |
286 |
|
{ |
287 |
148 |
if (optarg == "off") return SolveBVAsIntMode::OFF; |
288 |
148 |
else if (optarg == "iand") return SolveBVAsIntMode::IAND; |
289 |
116 |
else if (optarg == "bv") return SolveBVAsIntMode::BV; |
290 |
95 |
else if (optarg == "sum") return SolveBVAsIntMode::SUM; |
291 |
|
else if (optarg == "help") |
292 |
|
{ |
293 |
|
std::cerr << R"FOOBAR( |
294 |
|
solve-bv-as-int modes. |
295 |
|
Available modes for --solve-bv-as-int are: |
296 |
|
+ off (default) |
297 |
|
Do not translate bit-vectors to integers |
298 |
|
+ iand |
299 |
|
Translate bvand to the iand operator (experimental) |
300 |
|
+ bv |
301 |
|
Translate bvand back to bit-vectors |
302 |
|
+ sum |
303 |
|
Generate a sum expression for each bvand instance, based on the value in |
304 |
|
--solbv-bv-as-int-granularity |
305 |
|
)FOOBAR"; |
306 |
|
std::exit(1); |
307 |
|
} |
308 |
|
throw OptionException(std::string("unknown option for --solve-bv-as-int: `") + |
309 |
|
optarg + "'. Try --solve-bv-as-int=help."); |
310 |
|
} |
311 |
|
std::ostream& operator<<(std::ostream& os, SygusSolutionOutMode mode) |
312 |
|
{ |
313 |
|
switch(mode) |
314 |
|
{ |
315 |
|
case SygusSolutionOutMode::STATUS_AND_DEF: return os << "SygusSolutionOutMode::STATUS_AND_DEF"; |
316 |
|
case SygusSolutionOutMode::STATUS: return os << "SygusSolutionOutMode::STATUS"; |
317 |
|
case SygusSolutionOutMode::STATUS_OR_DEF: return os << "SygusSolutionOutMode::STATUS_OR_DEF"; |
318 |
|
case SygusSolutionOutMode::STANDARD: return os << "SygusSolutionOutMode::STANDARD"; |
319 |
|
default: Unreachable(); |
320 |
|
} |
321 |
|
return os; |
322 |
|
} |
323 |
185 |
SygusSolutionOutMode stringToSygusSolutionOutMode(const std::string& optarg) |
324 |
|
{ |
325 |
185 |
if (optarg == "status-and-def") return SygusSolutionOutMode::STATUS_AND_DEF; |
326 |
185 |
else if (optarg == "status") return SygusSolutionOutMode::STATUS; |
327 |
|
else if (optarg == "status-or-def") return SygusSolutionOutMode::STATUS_OR_DEF; |
328 |
|
else if (optarg == "sygus-standard") return SygusSolutionOutMode::STANDARD; |
329 |
|
else if (optarg == "help") |
330 |
|
{ |
331 |
|
std::cerr << R"FOOBAR( |
332 |
|
Modes for sygus solution output. |
333 |
|
Available modes for --sygus-out are: |
334 |
|
+ status-and-def |
335 |
|
Print status followed by definition corresponding to solution. |
336 |
|
+ status |
337 |
|
Print only status for check-synth calls. |
338 |
|
+ status-or-def |
339 |
|
Print status if infeasible, or definition corresponding to solution if |
340 |
|
feasible. |
341 |
|
+ sygus-standard (default) |
342 |
|
Print based on SyGuS standard. |
343 |
|
)FOOBAR"; |
344 |
|
std::exit(1); |
345 |
|
} |
346 |
|
throw OptionException(std::string("unknown option for --sygus-out: `") + |
347 |
|
optarg + "'. Try --sygus-out=help."); |
348 |
|
} |
349 |
|
std::ostream& operator<<(std::ostream& os, UnsatCoresMode mode) |
350 |
|
{ |
351 |
|
switch(mode) |
352 |
|
{ |
353 |
|
case UnsatCoresMode::OFF: return os << "UnsatCoresMode::OFF"; |
354 |
|
case UnsatCoresMode::FULL_PROOF: return os << "UnsatCoresMode::FULL_PROOF"; |
355 |
|
case UnsatCoresMode::SAT_PROOF: return os << "UnsatCoresMode::SAT_PROOF"; |
356 |
|
case UnsatCoresMode::ASSUMPTIONS: return os << "UnsatCoresMode::ASSUMPTIONS"; |
357 |
|
case UnsatCoresMode::PP_ONLY: return os << "UnsatCoresMode::PP_ONLY"; |
358 |
|
default: Unreachable(); |
359 |
|
} |
360 |
|
return os; |
361 |
|
} |
362 |
2 |
UnsatCoresMode stringToUnsatCoresMode(const std::string& optarg) |
363 |
|
{ |
364 |
2 |
if (optarg == "off") return UnsatCoresMode::OFF; |
365 |
2 |
else if (optarg == "full-proof") return UnsatCoresMode::FULL_PROOF; |
366 |
2 |
else if (optarg == "sat-proof") return UnsatCoresMode::SAT_PROOF; |
367 |
|
else if (optarg == "assumptions") return UnsatCoresMode::ASSUMPTIONS; |
368 |
|
else if (optarg == "pp-only") return UnsatCoresMode::PP_ONLY; |
369 |
|
else if (optarg == "help") |
370 |
|
{ |
371 |
|
std::cerr << R"FOOBAR( |
372 |
|
unsat cores modes. |
373 |
|
Available modes for --unsat-cores-mode are: |
374 |
|
+ off (default) |
375 |
|
Do not produce unsat cores. |
376 |
|
+ full-proof |
377 |
|
Produce unsat cores from full proofs. |
378 |
|
+ sat-proof |
379 |
|
Produce unsat cores from SAT and preprocessing proofs. |
380 |
|
+ assumptions |
381 |
|
Produce unsat cores using solving under assumptions and preprocessing proofs. |
382 |
|
+ pp-only |
383 |
|
Not producing unsat cores, but tracking proofs of preprocessing (internal |
384 |
|
only). |
385 |
|
)FOOBAR"; |
386 |
|
std::exit(1); |
387 |
|
} |
388 |
|
throw OptionException(std::string("unknown option for --unsat-cores-mode: `") + |
389 |
|
optarg + "'. Try --unsat-cores-mode=help."); |
390 |
|
} |
391 |
|
// clang-format on |
392 |
|
|
393 |
|
namespace smt |
394 |
|
{ |
395 |
|
// clang-format off |
396 |
|
void setDefaultAbstractValues(Options& opts, bool value) |
397 |
|
{ |
398 |
|
if (!opts.smt.abstractValuesWasSetByUser) opts.smt.abstractValues = value; |
399 |
|
} |
400 |
|
void setDefaultAckermann(Options& opts, bool value) |
401 |
|
{ |
402 |
|
if (!opts.smt.ackermannWasSetByUser) opts.smt.ackermann = value; |
403 |
|
} |
404 |
|
void setDefaultBlockModelsMode(Options& opts, BlockModelsMode value) |
405 |
|
{ |
406 |
|
if (!opts.smt.blockModelsModeWasSetByUser) opts.smt.blockModelsMode = value; |
407 |
|
} |
408 |
|
void setDefaultBVAndIntegerGranularity(Options& opts, uint64_t value) |
409 |
|
{ |
410 |
|
if (!opts.smt.BVAndIntegerGranularityWasSetByUser) opts.smt.BVAndIntegerGranularity = value; |
411 |
|
} |
412 |
|
void setDefaultCheckAbducts(Options& opts, bool value) |
413 |
|
{ |
414 |
|
if (!opts.smt.checkAbductsWasSetByUser) opts.smt.checkAbducts = value; |
415 |
|
} |
416 |
|
void setDefaultCheckInterpols(Options& opts, bool value) |
417 |
|
{ |
418 |
|
if (!opts.smt.checkInterpolsWasSetByUser) opts.smt.checkInterpols = value; |
419 |
|
} |
420 |
|
void setDefaultCheckModels(Options& opts, bool value) |
421 |
|
{ |
422 |
|
if (!opts.smt.checkModelsWasSetByUser) opts.smt.checkModels = value; |
423 |
|
} |
424 |
|
void setDefaultCheckProofs(Options& opts, bool value) |
425 |
|
{ |
426 |
|
if (!opts.smt.checkProofsWasSetByUser) opts.smt.checkProofs = value; |
427 |
|
} |
428 |
|
void setDefaultCheckSynthSol(Options& opts, bool value) |
429 |
|
{ |
430 |
|
if (!opts.smt.checkSynthSolWasSetByUser) opts.smt.checkSynthSol = value; |
431 |
|
} |
432 |
|
void setDefaultCheckUnsatCores(Options& opts, bool value) |
433 |
|
{ |
434 |
|
if (!opts.smt.checkUnsatCoresWasSetByUser) opts.smt.checkUnsatCores = value; |
435 |
|
} |
436 |
|
void setDefaultDebugCheckModels(Options& opts, bool value) |
437 |
|
{ |
438 |
|
if (!opts.smt.debugCheckModelsWasSetByUser) opts.smt.debugCheckModels = value; |
439 |
|
} |
440 |
|
void setDefaultDifficultyMode(Options& opts, DifficultyMode value) |
441 |
|
{ |
442 |
|
if (!opts.smt.difficultyModeWasSetByUser) opts.smt.difficultyMode = value; |
443 |
|
} |
444 |
|
void setDefaultDumpModeString(Options& opts, std::string value) |
445 |
|
{ |
446 |
|
if (!opts.smt.dumpModeStringWasSetByUser) opts.smt.dumpModeString = value; |
447 |
|
} |
448 |
|
void setDefaultDumpToFileName(Options& opts, ManagedOut value) |
449 |
|
{ |
450 |
|
if (!opts.smt.dumpToFileNameWasSetByUser) opts.smt.dumpToFileName = value; |
451 |
|
} |
452 |
|
void setDefaultEarlyIteRemoval(Options& opts, bool value) |
453 |
|
{ |
454 |
|
if (!opts.smt.earlyIteRemovalWasSetByUser) opts.smt.earlyIteRemoval = value; |
455 |
|
} |
456 |
|
void setDefaultExpandDefinitions(Options& opts, bool value) |
457 |
|
{ |
458 |
|
if (!opts.smt.expandDefinitionsWasSetByUser) opts.smt.expandDefinitions = value; |
459 |
|
} |
460 |
|
void setDefaultExtRewPrep(Options& opts, bool value) |
461 |
|
{ |
462 |
|
if (!opts.smt.extRewPrepWasSetByUser) opts.smt.extRewPrep = value; |
463 |
|
} |
464 |
|
void setDefaultExtRewPrepAgg(Options& opts, bool value) |
465 |
|
{ |
466 |
|
if (!opts.smt.extRewPrepAggWasSetByUser) opts.smt.extRewPrepAgg = value; |
467 |
|
} |
468 |
|
void setDefaultForeignTheoryRewrite(Options& opts, bool value) |
469 |
|
{ |
470 |
|
if (!opts.smt.foreignTheoryRewriteWasSetByUser) opts.smt.foreignTheoryRewrite = value; |
471 |
|
} |
472 |
|
void setDefaultIandMode(Options& opts, IandMode value) |
473 |
|
{ |
474 |
|
if (!opts.smt.iandModeWasSetByUser) opts.smt.iandMode = value; |
475 |
|
} |
476 |
|
void setDefaultInteractiveMode(Options& opts, bool value) |
477 |
|
{ |
478 |
|
if (!opts.smt.interactiveModeWasSetByUser) opts.smt.interactiveMode = value; |
479 |
|
} |
480 |
|
void setDefaultDoITESimp(Options& opts, bool value) |
481 |
|
{ |
482 |
|
if (!opts.smt.doITESimpWasSetByUser) opts.smt.doITESimp = value; |
483 |
|
} |
484 |
|
void setDefaultLearnedRewrite(Options& opts, bool value) |
485 |
|
{ |
486 |
|
if (!opts.smt.learnedRewriteWasSetByUser) opts.smt.learnedRewrite = value; |
487 |
|
} |
488 |
|
void setDefaultMinimalUnsatCores(Options& opts, bool value) |
489 |
|
{ |
490 |
|
if (!opts.smt.minimalUnsatCoresWasSetByUser) opts.smt.minimalUnsatCores = value; |
491 |
|
} |
492 |
|
void setDefaultModelCoresMode(Options& opts, ModelCoresMode value) |
493 |
|
{ |
494 |
|
if (!opts.smt.modelCoresModeWasSetByUser) opts.smt.modelCoresMode = value; |
495 |
|
} |
496 |
|
void setDefaultModelUninterpPrint(Options& opts, ModelUninterpPrintMode value) |
497 |
|
{ |
498 |
|
if (!opts.smt.modelUninterpPrintWasSetByUser) opts.smt.modelUninterpPrint = value; |
499 |
|
} |
500 |
|
void setDefaultModelWitnessValue(Options& opts, bool value) |
501 |
|
{ |
502 |
|
if (!opts.smt.modelWitnessValueWasSetByUser) opts.smt.modelWitnessValue = value; |
503 |
|
} |
504 |
|
void setDefaultDoITESimpOnRepeat(Options& opts, bool value) |
505 |
|
{ |
506 |
|
if (!opts.smt.doITESimpOnRepeatWasSetByUser) opts.smt.doITESimpOnRepeat = value; |
507 |
|
} |
508 |
|
void setDefaultProduceAbducts(Options& opts, bool value) |
509 |
|
{ |
510 |
|
if (!opts.smt.produceAbductsWasSetByUser) opts.smt.produceAbducts = value; |
511 |
|
} |
512 |
|
void setDefaultProduceAssertions(Options& opts, bool value) |
513 |
|
{ |
514 |
|
if (!opts.smt.produceAssertionsWasSetByUser) opts.smt.produceAssertions = value; |
515 |
|
} |
516 |
|
void setDefaultProduceAssignments(Options& opts, bool value) |
517 |
|
{ |
518 |
|
if (!opts.smt.produceAssignmentsWasSetByUser) opts.smt.produceAssignments = value; |
519 |
|
} |
520 |
|
void setDefaultProduceDifficulty(Options& opts, bool value) |
521 |
|
{ |
522 |
|
if (!opts.smt.produceDifficultyWasSetByUser) opts.smt.produceDifficulty = value; |
523 |
|
} |
524 |
|
void setDefaultProduceInterpols(Options& opts, ProduceInterpols value) |
525 |
|
{ |
526 |
|
if (!opts.smt.produceInterpolsWasSetByUser) opts.smt.produceInterpols = value; |
527 |
|
} |
528 |
|
void setDefaultProduceModels(Options& opts, bool value) |
529 |
|
{ |
530 |
|
if (!opts.smt.produceModelsWasSetByUser) opts.smt.produceModels = value; |
531 |
|
} |
532 |
|
void setDefaultProduceProofs(Options& opts, bool value) |
533 |
|
{ |
534 |
|
if (!opts.smt.produceProofsWasSetByUser) opts.smt.produceProofs = value; |
535 |
|
} |
536 |
|
void setDefaultUnsatAssumptions(Options& opts, bool value) |
537 |
|
{ |
538 |
|
if (!opts.smt.unsatAssumptionsWasSetByUser) opts.smt.unsatAssumptions = value; |
539 |
|
} |
540 |
|
void setDefaultUnsatCores(Options& opts, bool value) |
541 |
|
{ |
542 |
|
if (!opts.smt.unsatCoresWasSetByUser) opts.smt.unsatCores = value; |
543 |
|
} |
544 |
|
void setDefaultRepeatSimp(Options& opts, bool value) |
545 |
|
{ |
546 |
|
if (!opts.smt.repeatSimpWasSetByUser) opts.smt.repeatSimp = value; |
547 |
|
} |
548 |
|
void setDefaultCompressItes(Options& opts, bool value) |
549 |
|
{ |
550 |
|
if (!opts.smt.compressItesWasSetByUser) opts.smt.compressItes = value; |
551 |
|
} |
552 |
|
void setDefaultZombieHuntThreshold(Options& opts, uint64_t value) |
553 |
|
{ |
554 |
|
if (!opts.smt.zombieHuntThresholdWasSetByUser) opts.smt.zombieHuntThreshold = value; |
555 |
|
} |
556 |
|
void setDefaultSimplifyWithCareEnabled(Options& opts, bool value) |
557 |
|
{ |
558 |
|
if (!opts.smt.simplifyWithCareEnabledWasSetByUser) opts.smt.simplifyWithCareEnabled = value; |
559 |
|
} |
560 |
|
void setDefaultSimplificationMode(Options& opts, SimplificationMode value) |
561 |
|
{ |
562 |
|
if (!opts.smt.simplificationModeWasSetByUser) opts.smt.simplificationMode = value; |
563 |
|
} |
564 |
|
void setDefaultSolveBVAsInt(Options& opts, SolveBVAsIntMode value) |
565 |
|
{ |
566 |
|
if (!opts.smt.solveBVAsIntWasSetByUser) opts.smt.solveBVAsInt = value; |
567 |
|
} |
568 |
|
void setDefaultSolveIntAsBV(Options& opts, uint64_t value) |
569 |
|
{ |
570 |
|
if (!opts.smt.solveIntAsBVWasSetByUser) opts.smt.solveIntAsBV = value; |
571 |
|
} |
572 |
|
void setDefaultSolveRealAsInt(Options& opts, bool value) |
573 |
|
{ |
574 |
|
if (!opts.smt.solveRealAsIntWasSetByUser) opts.smt.solveRealAsInt = value; |
575 |
|
} |
576 |
|
void setDefaultSortInference(Options& opts, bool value) |
577 |
|
{ |
578 |
|
if (!opts.smt.sortInferenceWasSetByUser) opts.smt.sortInference = value; |
579 |
|
} |
580 |
|
void setDefaultDoStaticLearning(Options& opts, bool value) |
581 |
|
{ |
582 |
|
if (!opts.smt.doStaticLearningWasSetByUser) opts.smt.doStaticLearning = value; |
583 |
|
} |
584 |
|
void setDefaultSygusOut(Options& opts, SygusSolutionOutMode value) |
585 |
|
{ |
586 |
|
if (!opts.smt.sygusOutWasSetByUser) opts.smt.sygusOut = value; |
587 |
|
} |
588 |
|
void setDefaultSygusPrintCallbacks(Options& opts, bool value) |
589 |
|
{ |
590 |
|
if (!opts.smt.sygusPrintCallbacksWasSetByUser) opts.smt.sygusPrintCallbacks = value; |
591 |
|
} |
592 |
|
void setDefaultUnconstrainedSimp(Options& opts, bool value) |
593 |
|
{ |
594 |
|
if (!opts.smt.unconstrainedSimpWasSetByUser) opts.smt.unconstrainedSimp = value; |
595 |
|
} |
596 |
|
void setDefaultUnsatCoresMode(Options& opts, UnsatCoresMode value) |
597 |
|
{ |
598 |
|
if (!opts.smt.unsatCoresModeWasSetByUser) opts.smt.unsatCoresMode = value; |
599 |
|
} |
600 |
|
// clang-format on |
601 |
|
} |
602 |
|
|
603 |
29577 |
} // namespace cvc5::options |