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::VALUES: return os << "values"; |
33 |
|
case BlockModelsMode::NONE: return os << "none"; |
34 |
|
case BlockModelsMode::LITERALS: return os << "literals"; |
35 |
|
default: Unreachable(); |
36 |
|
} |
37 |
|
return os; |
38 |
|
} |
39 |
21 |
BlockModelsMode stringToBlockModelsMode(const std::string& optarg) |
40 |
|
{ |
41 |
21 |
if (optarg == "values") return BlockModelsMode::VALUES; |
42 |
18 |
else if (optarg == "none") return BlockModelsMode::NONE; |
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 |
|
+ values |
50 |
|
Block models based on the concrete model values for the free variables. |
51 |
|
+ none (default) |
52 |
|
Do not block models. |
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::LEMMA_LITERAL: return os << "lemma-literal"; |
66 |
|
case DifficultyMode::MODEL_CHECK: return os << "model-check"; |
67 |
|
default: Unreachable(); |
68 |
|
} |
69 |
|
return os; |
70 |
|
} |
71 |
|
DifficultyMode stringToDifficultyMode(const std::string& optarg) |
72 |
|
{ |
73 |
|
if (optarg == "lemma-literal") return DifficultyMode::LEMMA_LITERAL; |
74 |
|
else if (optarg == "model-check") return DifficultyMode::MODEL_CHECK; |
75 |
|
else if (optarg == "help") |
76 |
|
{ |
77 |
|
std::cerr << R"FOOBAR( |
78 |
|
difficulty output modes. |
79 |
|
Available modes for --difficulty-mode are: |
80 |
|
+ lemma-literal (default) |
81 |
|
Difficulty of an assertion is how many lemmas use a literal that the assertion |
82 |
|
depends on to be satisfied. |
83 |
|
+ model-check |
84 |
|
Difficulty of an assertion is how many times it was not satisfied in a |
85 |
|
candidate model. |
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 << "value"; |
97 |
|
case IandMode::BITWISE: return os << "bitwise"; |
98 |
|
case IandMode::SUM: return os << "sum"; |
99 |
|
default: Unreachable(); |
100 |
|
} |
101 |
|
return os; |
102 |
|
} |
103 |
62 |
IandMode stringToIandMode(const std::string& optarg) |
104 |
|
{ |
105 |
62 |
if (optarg == "value") return IandMode::VALUE; |
106 |
46 |
else if (optarg == "bitwise") return IandMode::BITWISE; |
107 |
16 |
else if (optarg == "sum") return IandMode::SUM; |
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 |
|
+ bitwise |
116 |
|
use bitwise comparisons on binary representation of integer for refinement |
117 |
|
(experimental) |
118 |
|
+ sum |
119 |
|
use sum to represent integer AND in refinement |
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::SIMPLE: return os << "simple"; |
131 |
|
case ModelCoresMode::NONE: return os << "none"; |
132 |
|
case ModelCoresMode::NON_IMPLIED: return os << "non-implied"; |
133 |
|
default: Unreachable(); |
134 |
|
} |
135 |
|
return os; |
136 |
|
} |
137 |
8 |
ModelCoresMode stringToModelCoresMode(const std::string& optarg) |
138 |
|
{ |
139 |
8 |
if (optarg == "simple") return ModelCoresMode::SIMPLE; |
140 |
4 |
else if (optarg == "none") return ModelCoresMode::NONE; |
141 |
4 |
else if (optarg == "non-implied") return ModelCoresMode::NON_IMPLIED; |
142 |
|
else if (optarg == "help") |
143 |
|
{ |
144 |
|
std::cerr << R"FOOBAR( |
145 |
|
Model cores modes. |
146 |
|
Available modes for --model-cores are: |
147 |
|
+ simple |
148 |
|
Only include a subset of variables whose values are sufficient to show the |
149 |
|
input formula is satisfied by the given model. |
150 |
|
+ none (default) |
151 |
|
Do not compute model cores. |
152 |
|
+ non-implied |
153 |
|
Only include a subset of variables whose values, in addition to the values of |
154 |
|
variables whose values are implied, are sufficient to show the input formula |
155 |
|
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::DeclSortAndFun: return os << "decl-sort-and-fun"; |
167 |
|
case ModelUninterpPrintMode::None: return os << "none"; |
168 |
|
case ModelUninterpPrintMode::DeclFun: return os << "decl-fun"; |
169 |
|
default: Unreachable(); |
170 |
|
} |
171 |
|
return os; |
172 |
|
} |
173 |
1 |
ModelUninterpPrintMode stringToModelUninterpPrintMode(const std::string& optarg) |
174 |
|
{ |
175 |
1 |
if (optarg == "decl-sort-and-fun") return ModelUninterpPrintMode::DeclSortAndFun; |
176 |
1 |
else if (optarg == "none") return ModelUninterpPrintMode::None; |
177 |
1 |
else if (optarg == "decl-fun") return ModelUninterpPrintMode::DeclFun; |
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-sort-and-fun |
184 |
|
print uninterpreted elements declare-fun, and also include a declare-sort for |
185 |
|
the sort |
186 |
|
+ none (default) |
187 |
|
(default) do not print declarations of uninterpreted elements in models. |
188 |
|
+ decl-fun |
189 |
|
print uninterpreted elements declare-fun, but don't include a declare-sort for |
190 |
|
the sort |
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::ALL: return os << "all"; |
202 |
|
case ProduceInterpols::NONE: return os << "none"; |
203 |
|
case ProduceInterpols::ASSUMPTIONS: return os << "assumptions"; |
204 |
|
case ProduceInterpols::CONJECTURE: return os << "conjecture"; |
205 |
|
case ProduceInterpols::SHARED: return os << "shared"; |
206 |
|
case ProduceInterpols::DEFAULT: return os << "default"; |
207 |
|
default: Unreachable(); |
208 |
|
} |
209 |
|
return os; |
210 |
|
} |
211 |
11 |
ProduceInterpols stringToProduceInterpols(const std::string& optarg) |
212 |
|
{ |
213 |
11 |
if (optarg == "all") return ProduceInterpols::ALL; |
214 |
11 |
else if (optarg == "none") return ProduceInterpols::NONE; |
215 |
11 |
else if (optarg == "assumptions") return ProduceInterpols::ASSUMPTIONS; |
216 |
11 |
else if (optarg == "conjecture") return ProduceInterpols::CONJECTURE; |
217 |
9 |
else if (optarg == "shared") return ProduceInterpols::SHARED; |
218 |
9 |
else if (optarg == "default") return ProduceInterpols::DEFAULT; |
219 |
|
else if (optarg == "help") |
220 |
|
{ |
221 |
|
std::cerr << R"FOOBAR( |
222 |
|
Interpolants grammar mode |
223 |
|
Available modes for --produce-interpols are: |
224 |
|
+ all |
225 |
|
use only operators that occur either in the assumptions or the conjecture |
226 |
|
+ none (default) |
227 |
|
don't compute interpolants |
228 |
|
+ assumptions |
229 |
|
use only operators that occur in the assumptions |
230 |
|
+ conjecture |
231 |
|
use only operators that occur in the conjecture |
232 |
|
+ shared |
233 |
|
use only operators that occur both in the assumptions and the conjecture |
234 |
|
+ default |
235 |
|
use the default grammar for the theory or the user-defined grammar if given |
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 << "none"; |
247 |
|
case SimplificationMode::BATCH: return os << "batch"; |
248 |
|
default: Unreachable(); |
249 |
|
} |
250 |
|
return os; |
251 |
|
} |
252 |
34 |
SimplificationMode stringToSimplificationMode(const std::string& optarg) |
253 |
|
{ |
254 |
34 |
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::IAND: return os << "iand"; |
278 |
|
case SolveBVAsIntMode::SUM: return os << "sum"; |
279 |
|
case SolveBVAsIntMode::BV: return os << "bv"; |
280 |
|
case SolveBVAsIntMode::OFF: return os << "off"; |
281 |
|
default: Unreachable(); |
282 |
|
} |
283 |
|
return os; |
284 |
|
} |
285 |
139 |
SolveBVAsIntMode stringToSolveBVAsIntMode(const std::string& optarg) |
286 |
|
{ |
287 |
139 |
if (optarg == "iand") return SolveBVAsIntMode::IAND; |
288 |
112 |
else if (optarg == "sum") return SolveBVAsIntMode::SUM; |
289 |
19 |
else if (optarg == "bv") return SolveBVAsIntMode::BV; |
290 |
|
else if (optarg == "off") return SolveBVAsIntMode::OFF; |
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 |
|
+ iand |
297 |
|
Translate bvand to the iand operator (experimental) |
298 |
|
+ sum |
299 |
|
Generate a sum expression for each bvand instance, based on the value in |
300 |
|
--solbv-bv-as-int-granularity |
301 |
|
+ bv |
302 |
|
Translate bvand back to bit-vectors |
303 |
|
+ off (default) |
304 |
|
Do not translate bit-vectors to integers |
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 << "status-and-def"; |
316 |
|
case SygusSolutionOutMode::STATUS_OR_DEF: return os << "status-or-def"; |
317 |
|
case SygusSolutionOutMode::STANDARD: return os << "sygus-standard"; |
318 |
|
case SygusSolutionOutMode::STATUS: return os << "status"; |
319 |
|
default: Unreachable(); |
320 |
|
} |
321 |
|
return os; |
322 |
|
} |
323 |
360 |
SygusSolutionOutMode stringToSygusSolutionOutMode(const std::string& optarg) |
324 |
|
{ |
325 |
360 |
if (optarg == "status-and-def") return SygusSolutionOutMode::STATUS_AND_DEF; |
326 |
360 |
else if (optarg == "status-or-def") return SygusSolutionOutMode::STATUS_OR_DEF; |
327 |
360 |
else if (optarg == "sygus-standard") return SygusSolutionOutMode::STANDARD; |
328 |
360 |
else if (optarg == "status") return SygusSolutionOutMode::STATUS; |
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-or-def |
337 |
|
Print status if infeasible, or definition corresponding to solution if |
338 |
|
feasible. |
339 |
|
+ sygus-standard (default) |
340 |
|
Print based on SyGuS standard. |
341 |
|
+ status |
342 |
|
Print only status for check-synth calls. |
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::PP_ONLY: return os << "pp-only"; |
354 |
|
case UnsatCoresMode::FULL_PROOF: return os << "full-proof"; |
355 |
|
case UnsatCoresMode::ASSUMPTIONS: return os << "assumptions"; |
356 |
|
case UnsatCoresMode::SAT_PROOF: return os << "sat-proof"; |
357 |
|
case UnsatCoresMode::OFF: return os << "off"; |
358 |
|
default: Unreachable(); |
359 |
|
} |
360 |
|
return os; |
361 |
|
} |
362 |
2 |
UnsatCoresMode stringToUnsatCoresMode(const std::string& optarg) |
363 |
|
{ |
364 |
2 |
if (optarg == "pp-only") return UnsatCoresMode::PP_ONLY; |
365 |
2 |
else if (optarg == "full-proof") return UnsatCoresMode::FULL_PROOF; |
366 |
2 |
else if (optarg == "assumptions") return UnsatCoresMode::ASSUMPTIONS; |
367 |
2 |
else if (optarg == "sat-proof") return UnsatCoresMode::SAT_PROOF; |
368 |
|
else if (optarg == "off") return UnsatCoresMode::OFF; |
369 |
|
else if (optarg == "help") |
370 |
|
{ |
371 |
|
std::cerr << R"FOOBAR( |
372 |
|
unsat cores modes. |
373 |
|
Available modes for --unsat-cores-mode are: |
374 |
|
+ pp-only |
375 |
|
Not producing unsat cores, but tracking proofs of preprocessing (internal |
376 |
|
only). |
377 |
|
+ full-proof |
378 |
|
Produce unsat cores from full proofs. |
379 |
|
+ assumptions |
380 |
|
Produce unsat cores using solving under assumptions and preprocessing proofs. |
381 |
|
+ sat-proof |
382 |
|
Produce unsat cores from SAT and preprocessing proofs. |
383 |
|
+ off (default) |
384 |
|
Do not produce unsat cores. |
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 |
31137 |
} // namespace cvc5::options |