projects / cvc5.git / blob
? search:


01b9648ffbb46337d48bf62c6a145217aea25389
[cvc5.git] / src / util / options.cpp
1 /********************* */
2 /*! \file options.cpp
3 ** \verbatim
4 ** Original author: mdeters
5 ** Major contributors: cconway, taking
6 ** Minor contributors (to current version): barrett, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
13 **
14 ** \brief Contains code for handling command-line options.
15 **
16 ** Contains code for handling command-line options
17 **/
18
19 #include <cstdio>
20 #include <cstdlib>
21 #include <new>
22 #include <unistd.h>
23 #include <string.h>
24 #include <stdint.h>
25 #include <time.h>
26 #include <sstream>
27
28 #include <getopt.h>
29
30 #include "expr/expr.h"
31 #include "expr/command.h"
32 #include "util/configuration.h"
33 #include "util/exception.h"
34 #include "util/language.h"
35 #include "util/options.h"
36 #include "util/output.h"
37 #include "util/dump.h"
38 #include "prop/sat_solver_factory.h"
39
40 #include "cvc4autoconfig.h"
41
42 using namespace std;
43 using namespace CVC4;
44
45 namespace CVC4 {
46
47 CVC4_THREADLOCAL(const Options*) Options::s_current = NULL;
48
49 #ifdef CVC4_DEBUG
50 # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
51 #else /* CVC4_DEBUG */
52 # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
53 #endif /* CVC4_DEBUG */
54
55 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
56 # define DO_SEMANTIC_CHECKS_BY_DEFAULT false
57 #else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
58 # define DO_SEMANTIC_CHECKS_BY_DEFAULT true
59 #endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
60
61 Options::Options() :
62 binary_name(),
63 statistics(false),
64 in(&std::cin),
65 out(&std::cout),
66 err(&std::cerr),
67 verbosity(0),
68 inputLanguage(language::input::LANG_AUTO),
69 outputLanguage(language::output::LANG_AUTO),
70 help(false),
71 version(false),
72 languageHelp(false),
73 parseOnly(false),
74 preprocessOnly(false),
75 semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
76 theoryRegistration(true),
77 memoryMap(false),
78 strictParsing(false),
79 lazyDefinitionExpansion(false),
80 printWinner(false),
81 simplificationMode(SIMPLIFICATION_MODE_BATCH),
82 simplificationModeSetByUser(false),
83 decisionMode(DECISION_STRATEGY_INTERNAL),
84 decisionModeSetByUser(false),
85 doStaticLearning(true),
86 doITESimp(false),
87 doITESimpSetByUser(false),
88 repeatSimp(false),
89 repeatSimpSetByUser(false),
90 interactive(false),
91 interactiveSetByUser(false),
92 perCallResourceLimit(0),
93 cumulativeResourceLimit(0),
94 perCallMillisecondLimit(0),
95 cumulativeMillisecondLimit(0),
96 segvNoSpin(false),
97 produceModels(false),
98 proof(false),
99 produceAssignments(false),
100 typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
101 earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
102 incrementalSolving(false),
103 replayFilename(""),
104 replayStream(NULL),
105 replayLog(NULL),
106 satRandomFreq(0.0),
107 satRandomSeed(91648253),// Minisat's default value
108 satVarDecay(0.95),
109 satClauseDecay(0.999),
110 satRestartFirst(25),
111 satRestartInc(3.0),
112 arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
113 arithPropagationMode(BOTH_PROP),
114 arithPivotRule(MINIMUM),
115 arithPivotThreshold(16),
116 arithPropagateMaxLength(16),
117 arithDioSolver(true),
118 arithRewriteEq(false),
119 arithRewriteEqSetByUser(false),
120 ufSymmetryBreaker(false),
121 ufSymmetryBreakerSetByUser(false),
122 lemmaOutputChannel(NULL),
123 lemmaInputChannel(NULL),
124 threads(2),// default should be 1 probably, but say 2 for now
125 threadArgv(),
126 thread_id(-1),
127 separateOutput(false),
128 sharingFilterByLength(-1),
129 bitvectorEagerBitblast(false),
130 bitvectorEagerFullcheck(false),
131 bitvectorShareLemmas(false),
132 sat_refine_conflicts(false)
133 {
134 }
135
136 static const string mostCommonOptionsDescription = "\
137 Most commonly-used CVC4 options:\n\
138 --version | -V identify this CVC4 binary\n\
139 --help | -h full command line reference\n\
140 --lang | -L force input language\n\
141 (default is `auto'; see --lang help)\n\
142 --output-lang force output language\n\
143 (default is `auto'; see --lang help)\n\
144 --verbose | -v increase verbosity (may be repeated)\n\
145 --quiet | -q decrease verbosity (may be repeated)\n\
146 --stats give statistics on exit\n\
147 --parse-only exit after parsing input\n\
148 --preprocess-only exit after preproc (useful with --stats or --dump)\n\
149 --dump=MODE dump preprocessed assertions, etc., see --dump=help\n\
150 --dump-to=FILE all dumping goes to FILE (instead of stdout)\n\
151 --show-config show CVC4 static configuration\n\
152 --strict-parsing be less tolerant of non-conforming inputs\n\
153 --interactive force interactive mode\n\
154 --no-interactive force non-interactive mode\n\
155 --produce-models | -m support the get-value command\n\
156 --produce-assignments support the get-assignment command\n\
157 --print-success print the \"success\" output required of SMT-LIBv2\n\
158 --smtlib2 SMT-LIBv2 conformance mode (implies other options)\n\
159 --proof turn on proof generation\n\
160 --incremental | -i enable incremental solving\n\
161 --tlimit=MS enable time limiting (give milliseconds)\n\
162 --tlimit-per=MS enable time limiting per query (give milliseconds)\n\
163 --rlimit=N enable resource limiting\n\
164 --rlimit-per=N enable resource limiting per query\n\
165 ";
166
167 static const string optionsDescription = mostCommonOptionsDescription + "\
168 \n\
169 Additional CVC4 options:\n\
170 --mmap memory map file input\n\
171 --segv-nospin don't spin on segfault waiting for gdb\n\
172 --lazy-type-checking type check expressions only when necessary (default)\n\
173 --eager-type-checking type check expressions immediately on creation\n\
174 (debug builds only)\n\
175 --no-type-checking never type check expressions\n\
176 --no-checking disable ALL semantic checks, including type checks\n\
177 --no-theory-registration disable theory reg (not safe for some theories)\n\
178 --print-winner enable printing the winning thread (pcvc4 only)\n\
179 --trace | -t trace something (e.g. -t pushpop), can repeat\n\
180 --debug | -d debug something (e.g. -d arith), can repeat\n\
181 --show-debug-tags show all avalable tags for debugging\n\
182 --show-trace-tags show all avalable tags for tracing\n\
183 --show-sat-solvers show all available SAT solvers\n\
184 --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
185 --print-expr-types print types with variables when printing exprs\n\
186 --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
187 --simplification=MODE choose simplification mode, see --simplification=help\n\
188 --decision=MODE choose decision mode, see --decision=help\n\
189 --no-static-learning turn off static learning (e.g. diamond-breaking)\n\
190 --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
191 --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
192 --repeat-simp make multiple passes with nonclausal simplifier\n\
193 --no-repeat-simp do not make multiple passes with nonclausal simplifier\n\
194 --replay=file replay decisions from file\n\
195 --replay-log=file log decisions and propagations to file\n\
196 SAT:\n\
197 --random-freq=P frequency of random decisions in the sat solver\n\
198 (P=0.0 by default)\n\
199 --random-seed=S sets the random seed for the sat solver\n\
200 --restart-int-base=I sets the base restart interval for the sat solver\n\
201 (I=25 by default)\n\
202 --restart-int-inc=F restart interval increase factor for the sat solver\n\
203 (F=3.0 by default)\n\
204 ARITHMETIC:\n\
205 --arith-presolve-lemmas=MODE determines which lemmas to add before solving\n\
206 (default is 'all', see --arith-presolve-lemmas=help)\n\
207 --arith-prop=MODE turns on arithmetic propagation\n\
208 (default is 'old', see --arith-prop=help)\n\
209 --pivot-rule=RULE change the pivot rule for the basic variable\n\
210 (default is 'min', see --pivot-rule help)\n\
211 --pivot-threshold=N sets the number of pivots using --pivot-rule\n\
212 per basic variable per simplex instance before\n\
213 using variable order\n\
214 --prop-row-length=N sets the maximum row length to be used in propagation\n\
215 --disable-dio-solver turns off Linear Diophantine Equation solver \n\
216 (Griggio, JSAT 2012)\n\
217 --enable-arith-rewrite-equalities turns on the preprocessing rewrite\n\
218 turning equalities into a conjunction of inequalities.\n \
219 --disable-arith-rewrite-equalities turns off the preprocessing rewrite\n\
220 turning equalities into a conjunction of inequalities.\n \
221 UF:\n\
222 --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
223 CADE 2011) [on by default only for QF_UF]\n\
224 --disable-symmetry-breaker turns off UF symmetry breaker\n\
225 --threads=N sets the number of solver threads\n\
226 --threadN=string configures thread N (0..#threads-1)\n\
227 --filter-lemma-length=N don't share lemmas strictly longer than N\n\
228 --bitblast-eager eagerly bitblast the bitvectors to the main SAT solver\n\
229 --bitblast-share-lemmas share lemmas from the bitblsting solver with the main solver\n\
230 --bitblast-eager-fullcheck check the bitblasting eagerly\n\
231 --refine-conflicts refine theory conflict clauses\n\
232 ";
233
234
235
236 static const string languageDescription = "\
237 Languages currently supported as arguments to the -L / --lang option:\n\
238 auto attempt to automatically determine the input language\n\
239 pl | cvc4 CVC4 presentation language\n\
240 smt | smtlib SMT-LIB format 1.2\n\
241 smt2 | smtlib2 SMT-LIB format 2.0\n\
242 \n\
243 Languages currently supported as arguments to the --output-lang option:\n\
244 auto match the output language to the input language\n\
245 pl | cvc4 CVC4 presentation language\n\
246 smt | smtlib SMT-LIB format 1.2\n\
247 smt2 | smtlib2 SMT-LIB format 2.0\n\
248 ast internal format (simple syntax-tree language)\n\
249 ";
250
251 static const string simplificationHelp = "\
252 Simplification modes currently supported by the --simplification option:\n\
253 \n\
254 batch (default) \n\
255 + save up all ASSERTions; run nonclausal simplification and clausal\n\
256 (MiniSat) propagation for all of them only after reaching a querying command\n\
257 (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
258 \n\
259 incremental\n\
260 + run nonclausal simplification and clausal propagation at each ASSERT\n\
261 (and at CHECKSAT/QUERY/SUBTYPE)\n\
262 \n\
263 none\n\
264 + do not perform nonclausal simplification\n\
265 ";
266
267 static const string decisionHelp = "\
268 Decision modes currently supported by the --decision option:\n\
269 \n\
270 internal (default)\n\
271 + Use the internal decision hueristics of the SAT solver\n\
272 \n\
273 justification\n\
274 + An ATGP-inspired justification heuristic\n\
275 ";
276
277 static const string dumpHelp = "\
278 Dump modes currently supported by the --dump option:\n\
279 \n\
280 benchmark\n\
281 + Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
282 does not include any declarations or assertions. Implied by all following\n\
283 modes.\n\
284 \n\
285 declarations\n\
286 + Dump declarations. Implied by all following modes.\n\
287 \n\
288 assertions\n\
289 + Output the assertions after non-clausal simplification and static\n\
290 learning phases, but before presolve-time T-lemmas arrive. If\n\
291 non-clausal simplification and static learning are off\n\
292 (--simplification=none --no-static-learning), the output\n\
293 will closely resemble the input (with term-level ITEs removed).\n\
294 \n\
295 learned\n\
296 + Output the assertions after non-clausal simplification, static\n\
297 learning, and presolve-time T-lemmas. This should include all eager\n\
298 T-lemmas (in the form provided by the theory, which my or may not be\n\
299 clausal). Also includes level-0 BCP done by Minisat.\n\
300 \n\
301 clauses\n\
302 + Do all the preprocessing outlined above, and dump the CNF-converted\n\
303 output\n\
304 \n\
305 state\n\
306 + Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
307 Implied by all \"stateful\" modes below and conflicts with all\n\
308 non-stateful modes below.\n\
309 \n\
310 t-conflicts [non-stateful]\n\
311 + Output correctness queries for all theory conflicts\n\
312 \n\
313 missed-t-conflicts [stateful]\n\
314 + Output completeness queries for theory conflicts\n\
315 \n\
316 t-propagations [stateful]\n\
317 + Output correctness queries for all theory propagations\n\
318 \n\
319 missed-t-propagations [stateful]\n\
320 + Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
321 \n\
322 t-lemmas [non-stateful]\n\
323 + Output correctness queries for all theory lemmas\n\
324 \n\
325 t-explanations [non-stateful]\n\
326 + Output correctness queries for all theory explanations\n\
327 \n\
328 Dump modes can be combined with multiple uses of --dump. Generally you want\n\
329 one from the assertions category (either asertions, learned, or clauses), and\n\
330 perhaps one or more stateful or non-stateful modes for checking correctness\n\
331 and completeness of decision procedure implementations. Stateful modes dump\n\
332 the contextual assertions made by the core solver (all decisions and\n\
333 propagations as assertions; that affects the validity of the resulting\n\
334 correctness and completeness queries, so of course stateful and non-stateful\n\
335 modes cannot be mixed in the same run.\n\
336 \n\
337 The --output-language option controls the language used for dumping, and\n\
338 this allows you to connect CVC4 to another solver implementation via a UNIX\n\
339 pipe to perform on-line checking. The --dump-to option can be used to dump\n\
340 to a file.\n\
341 ";
342
343 static const string arithPresolveLemmasHelp = "\
344 Presolve lemmas are generated before SAT search begins using the relationship\n\
345 of constant terms and polynomials.\n\
346 Modes currently supported by the --arith-presolve-lemmas option:\n\
347 + none \n\
348 + ineqs \n\
349 Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
350 + eqs \n\
351 Outputs lemmas of the general forms\n\
352 (= p c) implies (<= p d) for c < d, or\n\
353 (= p c) implies (not (= p d)) for c != d.\n\
354 + all \n\
355 A combination of inequalities and equalities.\n\
356 ";
357
358 static const string propagationModeHelp = "\
359 This decides on kind of propagation arithmetic attempts to do during the search.\n\
360 + none\n\
361 + unate\n\
362 use constraints to do unate propagation\n\
363 + bi (Bounds Inference)\n\
364 infers bounds on basic variables using the upper and lower bounds of the\n\
365 non-basic variables in the tableau.\n\
366 +both\n\
367 ";
368
369 static const string pivotRulesHelp = "\
370 This decides on the rule used by simplex during hueristic rounds\n\
371 for deciding the next basic variable to select.\n\
372 Pivot rules available:\n\
373 +min\n\
374 The minimum abs() value of the variable's violation of its bound. (default)\n\
375 +min-break-ties\n\
376 The minimum violation with ties broken by variable order (total)\n\
377 +max\n\
378 The maximum violation the bound\n\
379 ";
380
381 string Options::getDescription() const {
382 return optionsDescription;
383 }
384
385 void Options::printUsage(const std::string msg, std::ostream& out) {
386 out << msg << optionsDescription << endl << flush;
387 }
388
389 void Options::printShortUsage(const std::string msg, std::ostream& out) {
390 out << msg << mostCommonOptionsDescription << endl
391 << "For full usage, please use --help." << endl << flush;
392 }
393
394 void Options::printLanguageHelp(std::ostream& out) {
395 out << languageDescription << flush;
396 }
397
398 /**
399 * For the main getopt() routine, we need ways to switch on long
400 * options without clashing with short option characters. This is an
401 * enum of those long options. For long options (e.g. "--verbose")
402 * with a short option equivalent ("-v"), we use the single-letter
403 * short option; therefore, this enumeration starts at 256 to avoid
404 * any collision.
405 */
406 enum OptionValue {
407 OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */
408 SMTCOMP,
409 STATS,
410 SEGV_NOSPIN,
411 OUTPUT_LANGUAGE,
412 PARSE_ONLY,
413 PREPROCESS_ONLY,
414 DUMP,
415 DUMP_TO,
416 NO_CHECKING,
417 NO_THEORY_REGISTRATION,
418 USE_MMAP,
419 SHOW_DEBUG_TAGS,
420 SHOW_TRACE_TAGS,
421 SHOW_SAT_SOLVERS,
422 SHOW_CONFIG,
423 STRICT_PARSING,
424 DEFAULT_EXPR_DEPTH,
425 PRINT_EXPR_TYPES,
426 UF_THEORY,
427 LAZY_DEFINITION_EXPANSION,
428 SIMPLIFICATION_MODE,
429 DECISION_MODE,
430 NO_STATIC_LEARNING,
431 ITE_SIMP,
432 NO_ITE_SIMP,
433 REPEAT_SIMP,
434 NO_REPEAT_SIMP,
435 INTERACTIVE,
436 NO_INTERACTIVE,
437 PRODUCE_ASSIGNMENTS,
438 PRINT_SUCCESS,
439 SMTLIB2,
440 PROOF,
441 NO_TYPE_CHECKING,
442 LAZY_TYPE_CHECKING,
443 EAGER_TYPE_CHECKING,
444 REPLAY,
445 REPLAY_LOG,
446 PRINT_WINNER,
447 RANDOM_FREQUENCY,
448 RANDOM_SEED,
449 SAT_RESTART_FIRST,
450 SAT_RESTART_INC,
451 ARITHMETIC_UNATE_LEMMA_MODE,
452 ARITHMETIC_PROPAGATION_MODE,
453 ARITHMETIC_PIVOT_RULE,
454 ARITHMETIC_PIVOT_THRESHOLD,
455 ARITHMETIC_PROP_MAX_LENGTH,
456 ARITHMETIC_DIO_SOLVER,
457 ENABLE_ARITHMETIC_REWRITE_EQUALITIES,
458 DISABLE_ARITHMETIC_REWRITE_EQUALITIES,
459 ENABLE_SYMMETRY_BREAKER,
460 DISABLE_SYMMETRY_BREAKER,
461 PARALLEL_THREADS,
462 PARALLEL_SEPARATE_OUTPUT,
463 PORTFOLIO_FILTER_LENGTH,
464 TIME_LIMIT,
465 TIME_LIMIT_PER,
466 RESOURCE_LIMIT,
467 RESOURCE_LIMIT_PER,
468 BITVECTOR_EAGER_BITBLAST,
469 BITVECTOR_SHARE_LEMMAS,
470 BITVECTOR_EAGER_FULLCHECK,
471 SAT_REFINE_CONFLICTS,
472 OPTION_VALUE_END
473 };/* enum OptionValue */
474
475 /**
476 * This is a table of long options. By policy, each short option
477 * should have an equivalent long option (but the reverse isn't the
478 * case), so this table should thus contain all command-line options.
479 *
480 * Each option in this array has four elements:
481 *
482 * 1. the long option string
483 * 2. argument behavior for the option:
484 * no_argument - no argument permitted
485 * required_argument - an argument is expected
486 * optional_argument - an argument is permitted but not required
487 * 3. this is a pointer to an int which is set to the 4th entry of the
488 * array if the option is present; or NULL, in which case
489 * getopt_long() returns the 4th entry
490 * 4. the return value for getopt_long() when this long option (or the
491 * value to set the 3rd entry to; see #3)
492 *
493 * If you add something here, you should add it in src/main/usage.h
494 * also, to document it.
495 *
496 * If you add something that has a short option equivalent, you should
497 * add it to the getopt_long() call in parseOptions().
498 */
499 static struct option cmdlineOptions[] = {
500 // name, has_arg, *flag, val
501 { "verbose" , no_argument , NULL, 'v' },
502 { "quiet" , no_argument , NULL, 'q' },
503 { "debug" , required_argument, NULL, 'd' },
504 { "trace" , required_argument, NULL, 't' },
505 { "stats" , no_argument , NULL, STATS },
506 { "no-checking", no_argument , NULL, NO_CHECKING },
507 { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
508 { "show-debug-tags", no_argument , NULL, SHOW_DEBUG_TAGS },
509 { "show-trace-tags", no_argument , NULL, SHOW_TRACE_TAGS },
510 { "show-sat-solvers", no_argument , NULL, SHOW_SAT_SOLVERS },
511 { "show-config", no_argument , NULL, SHOW_CONFIG },
512 { "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
513 { "help" , no_argument , NULL, 'h' },
514 { "version" , no_argument , NULL, 'V' },
515 { "about" , no_argument , NULL, 'V' },
516 { "lang" , required_argument, NULL, 'L' },
517 { "output-lang", required_argument, NULL, OUTPUT_LANGUAGE },
518 { "parse-only" , no_argument , NULL, PARSE_ONLY },
519 { "preprocess-only", no_argument , NULL, PREPROCESS_ONLY },
520 { "dump" , required_argument, NULL, DUMP },
521 { "dump-to" , required_argument, NULL, DUMP_TO },
522 { "mmap" , no_argument , NULL, USE_MMAP },
523 { "strict-parsing", no_argument , NULL, STRICT_PARSING },
524 { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
525 { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
526 { "uf" , required_argument, NULL, UF_THEORY },
527 { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
528 { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
529 { "decision", required_argument, NULL, DECISION_MODE },
530 { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
531 { "ite-simp", no_argument, NULL, ITE_SIMP },
532 { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
533 { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
534 { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
535 { "interactive", no_argument , NULL, INTERACTIVE },
536 { "no-interactive", no_argument , NULL, NO_INTERACTIVE },
537 { "produce-models", no_argument , NULL, 'm' },
538 { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
539 { "print-success", no_argument, NULL, PRINT_SUCCESS },
540 { "smtlib2", no_argument, NULL, SMTLIB2 },
541 { "proof", no_argument, NULL, PROOF },
542 { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
543 { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
544 { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
545 { "incremental", no_argument , NULL, 'i' },
546 { "replay" , required_argument, NULL, REPLAY },
547 { "replay-log" , required_argument, NULL, REPLAY_LOG },
548 { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY },
549 { "random-seed" , required_argument, NULL, RANDOM_SEED },
550 { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
551 { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
552 { "print-winner", no_argument , NULL, PRINT_WINNER },
553 { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE },
554 { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE },
555 { "pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE },
556 { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD },
557 { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH },
558 { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
559 { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES },
560 { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
561 { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
562 { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
563 { "threads", required_argument, NULL, PARALLEL_THREADS },
564 { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
565 { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
566 { "tlimit" , required_argument, NULL, TIME_LIMIT },
567 { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
568 { "rlimit" , required_argument, NULL, RESOURCE_LIMIT },
569 { "rlimit-per" , required_argument, NULL, RESOURCE_LIMIT_PER },
570 { "bitblast-eager", no_argument, NULL, BITVECTOR_EAGER_BITBLAST },
571 { "bitblast-share-lemmas", no_argument, NULL, BITVECTOR_SHARE_LEMMAS },
572 { "bitblast-eager-fullcheck", no_argument, NULL, BITVECTOR_EAGER_FULLCHECK },
573 { "refine-conflicts", no_argument, NULL, SAT_REFINE_CONFLICTS },
574 { NULL , no_argument , NULL, '\0' }
575 };/* if you add things to the above, please remember to update usage.h! */
576
577
578 /** Parse argc/argv and put the result into a CVC4::Options struct. */
579 int Options::parseOptions(int argc, char* argv[])
580 throw(OptionException) {
581 const char *progName = argv[0];
582 int c;
583
584 // Reset getopt(), in the case of multiple calls.
585 // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
586 optind = 0;
587 #if HAVE_DECL_OPTRESET
588 optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
589 #endif /* HAVE_DECL_OPTRESET */
590
591 // find the base name of the program
592 const char *x = strrchr(progName, '/');
593 if(x != NULL) {
594 progName = x + 1;
595 }
596 binary_name = string(progName);
597
598 // The strange string in this call is the short option string. An
599 // initial '+' means that option processing stops as soon as a
600 // non-option argument is encountered (it is not present, by design).
601 // The initial ':' indicates that getopt_long() should return ':'
602 // instead of '?' for a missing option argument. Then, each letter
603 // is a valid short option for getopt_long(), and if it's encountered,
604 // getopt_long() returns that character. A ':' after an option
605 // character means an argument is required; two colons indicates an
606 // argument is optional; no colons indicate an argument is not
607 // permitted. cmdlineOptions specifies all the long-options and the
608 // return value for getopt_long() should they be encountered.
609 while((c = getopt_long(argc, argv,
610 ":himVvqL:d:t:",
611 cmdlineOptions, NULL)) != -1) {
612 switch(c) {
613
614 case 'h':
615 help = true;
616 break;
617
618 case 'V':
619 version = true;
620 break;
621
622 case 'v':
623 ++verbosity;
624 break;
625
626 case 'q':
627 --verbosity;
628 break;
629
630 case 'L':
631 setInputLanguage(optarg);
632 break;
633
634 case OUTPUT_LANGUAGE:
635 setOutputLanguage(optarg);
636 break;
637
638 case 't':
639 if(Configuration::isTracingBuild()) {
640 if(!Configuration::isTraceTag(optarg))
641 throw OptionException(string("trace tag ") + optarg +
642 string(" not available"));
643 } else {
644 throw OptionException("trace tags not available in non-tracing builds");
645 }
646 Trace.on(optarg);
647 break;
648
649 case 'd':
650 if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
651 if(!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg)) {
652 throw OptionException(string("debug tag ") + optarg +
653 string(" not available"));
654 }
655 } else if(! Configuration::isDebugBuild()) {
656 throw OptionException("debug tags not available in non-debug builds");
657 } else {
658 throw OptionException("debug tags not available in non-tracing builds");
659 }
660 Debug.on(optarg);
661 Trace.on(optarg);
662 break;
663
664 case STATS:
665 statistics = true;
666 break;
667
668 case SEGV_NOSPIN:
669 segvNoSpin = true;
670 break;
671
672 case PARSE_ONLY:
673 parseOnly = true;
674 break;
675
676 case PREPROCESS_ONLY:
677 preprocessOnly = true;
678 break;
679
680 case DUMP: {
681 #ifdef CVC4_DUMPING
682 char* tokstr = optarg;
683 char* toksave;
684 while((optarg = strtok_r(tokstr, ",", &toksave)) != NULL) {
685 tokstr = NULL;
686 if(!strcmp(optarg, "benchmark")) {
687 } else if(!strcmp(optarg, "declarations")) {
688 } else if(!strcmp(optarg, "assertions")) {
689 } else if(!strcmp(optarg, "learned")) {
690 } else if(!strcmp(optarg, "clauses")) {
691 } else if(!strcmp(optarg, "t-conflicts") ||
692 !strcmp(optarg, "t-lemmas") ||
693 !strcmp(optarg, "t-explanations") ||
694 !strcmp(optarg, "bv-rewrites")) {
695 // These are "non-state-dumping" modes. If state (SAT decisions,
696 // propagations, etc.) is dumped, it will interfere with the validity
697 // of these generated queries.
698 if(Dump.isOn("state")) {
699 throw OptionException(string("dump option `") + optarg +
700 "' conflicts with a previous, "
701 "state-dumping dump option. You cannot "
702 "mix stateful and non-stateful dumping modes; "
703 "see --dump help.");
704 } else {
705 Dump.on("no-permit-state");
706 }
707 } else if(!strcmp(optarg, "state") ||
708 !strcmp(optarg, "missed-t-conflicts") ||
709 !strcmp(optarg, "t-propagations") ||
710 !strcmp(optarg, "missed-t-propagations")) {
711 // These are "state-dumping" modes. If state (SAT decisions,
712 // propagations, etc.) is not dumped, it will interfere with the
713 // validity of these generated queries.
714 if(Dump.isOn("no-permit-state")) {
715 throw OptionException(string("dump option `") + optarg +
716 "' conflicts with a previous, "
717 "non-state-dumping dump option. You cannot "
718 "mix stateful and non-stateful dumping modes; "
719 "see --dump help.");
720 } else {
721 Dump.on("state");
722 }
723 } else if(!strcmp(optarg, "help")) {
724 puts(dumpHelp.c_str());
725 exit(1);
726 } else {
727 throw OptionException(string("unknown option for --dump: `") +
728 optarg + "'. Try --dump help.");
729 }
730
731 Dump.on(optarg);
732 Dump.on("benchmark");
733 if(strcmp(optarg, "benchmark")) {
734 Dump.on("declarations");
735 }
736 }
737 #else /* CVC4_DUMPING */
738 throw OptionException("The dumping feature was disabled in this build of CVC4.");
739 #endif /* CVC4_DUMPING */
740 break;
741 }
742
743 case DUMP_TO: {
744 #ifdef CVC4_DUMPING
745 if(optarg == NULL || *optarg == '\0') {
746 throw OptionException(string("Bad file name for --dump-to"));
747 } else if(!strcmp(optarg, "-")) {
748 Dump.setStream(DumpOutC::dump_cout);
749 } else {
750 ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc);
751 if(!*dumpTo) {
752 throw OptionException(string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
753 }
754 Dump.setStream(*dumpTo);
755 }
756 #else /* CVC4_DUMPING */
757 throw OptionException("The dumping feature was disabled in this build of CVC4.");
758 #endif /* CVC4_DUMPING */
759 }
760 break;
761
762 case NO_THEORY_REGISTRATION:
763 theoryRegistration = false;
764 break;
765
766 case NO_CHECKING:
767 semanticChecks = false;
768 typeChecking = false;
769 earlyTypeChecking = false;
770 break;
771
772 case USE_MMAP:
773 memoryMap = true;
774 break;
775
776 case PRINT_WINNER:
777 printWinner = true;
778 break;
779
780 case STRICT_PARSING:
781 strictParsing = true;
782 break;
783
784 case DEFAULT_EXPR_DEPTH:
785 {
786 int depth = atoi(optarg);
787 Debug.getStream() << Expr::setdepth(depth);
788 Trace.getStream() << Expr::setdepth(depth);
789 Notice.getStream() << Expr::setdepth(depth);
790 Chat.getStream() << Expr::setdepth(depth);
791 Message.getStream() << Expr::setdepth(depth);
792 Warning.getStream() << Expr::setdepth(depth);
793 }
794 break;
795
796 case PRINT_EXPR_TYPES:
797 Debug.getStream() << Expr::printtypes(true);
798 Trace.getStream() << Expr::printtypes(true);
799 Notice.getStream() << Expr::printtypes(true);
800 Chat.getStream() << Expr::printtypes(true);
801 Message.getStream() << Expr::printtypes(true);
802 Warning.getStream() << Expr::printtypes(true);
803 break;
804
805 case LAZY_DEFINITION_EXPANSION:
806 lazyDefinitionExpansion = true;
807 break;
808
809 case SIMPLIFICATION_MODE:
810 if(!strcmp(optarg, "batch")) {
811 simplificationMode = SIMPLIFICATION_MODE_BATCH;
812 simplificationModeSetByUser = true;
813 } else if(!strcmp(optarg, "incremental")) {
814 simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
815 simplificationModeSetByUser = true;
816 } else if(!strcmp(optarg, "none")) {
817 simplificationMode = SIMPLIFICATION_MODE_NONE;
818 simplificationModeSetByUser = true;
819 } else if(!strcmp(optarg, "help")) {
820 puts(simplificationHelp.c_str());
821 exit(1);
822 } else {
823 throw OptionException(string("unknown option for --simplification: `") +
824 optarg + "'. Try --simplification help.");
825 }
826 break;
827
828 case DECISION_MODE:
829 if(!strcmp(optarg, "internal")) {
830 decisionMode = DECISION_STRATEGY_INTERNAL;
831 decisionModeSetByUser = true;
832 } else if(!strcmp(optarg, "justification")) {
833 decisionMode = DECISION_STRATEGY_JUSTIFICATION;
834 decisionModeSetByUser = true;
835 } else if(!strcmp(optarg, "help")) {
836 puts(decisionHelp.c_str());
837 exit(1);
838 } else {
839 throw OptionException(string("unknown option for --decision: `") +
840 optarg + "'. Try --decision help.");
841 }
842 break;
843
844 case NO_STATIC_LEARNING:
845 doStaticLearning = false;
846 break;
847
848 case ITE_SIMP:
849 doITESimp = true;
850 doITESimpSetByUser = true;
851 break;
852
853 case NO_ITE_SIMP:
854 doITESimp = false;
855 doITESimpSetByUser = true;
856 break;
857
858 case REPEAT_SIMP:
859 repeatSimp = true;
860 repeatSimpSetByUser = true;
861 break;
862
863 case NO_REPEAT_SIMP:
864 repeatSimp = false;
865 repeatSimpSetByUser = true;
866 break;
867
868 case INTERACTIVE:
869 interactive = true;
870 interactiveSetByUser = true;
871 break;
872
873 case NO_INTERACTIVE:
874 interactive = false;
875 interactiveSetByUser = true;
876 break;
877
878 case 'm':
879 produceModels = true;
880 break;
881
882 case PRODUCE_ASSIGNMENTS:
883 produceAssignments = true;
884 break;
885
886 case SMTLIB2: // smtlib v2 compliance mode
887 inputLanguage = language::input::LANG_SMTLIB_V2;
888 outputLanguage = language::output::LANG_SMTLIB_V2;
889 strictParsing = true;
890 // make sure entire expressions are printed on all the non-debug, non-trace streams
891 Notice.getStream() << Expr::setdepth(-1);
892 Chat.getStream() << Expr::setdepth(-1);
893 Message.getStream() << Expr::setdepth(-1);
894 Warning.getStream() << Expr::setdepth(-1);
895 /* intentionally fall through */
896
897 case PRINT_SUCCESS:
898 Debug.getStream() << Command::printsuccess(true);
899 Trace.getStream() << Command::printsuccess(true);
900 Notice.getStream() << Command::printsuccess(true);
901 Chat.getStream() << Command::printsuccess(true);
902 Message.getStream() << Command::printsuccess(true);
903 Warning.getStream() << Command::printsuccess(true);
904 break;
905
906 case PROOF:
907 #ifdef CVC4_PROOF
908 proof = true;
909 #else /* CVC4_PROOF */
910 throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used");
911 #endif /* CVC4_PROOF */
912 break;
913
914 case NO_TYPE_CHECKING:
915 typeChecking = false;
916 earlyTypeChecking = false;
917 break;
918
919 case LAZY_TYPE_CHECKING:
920 typeChecking = true;
921 earlyTypeChecking = false;
922 break;
923
924 case EAGER_TYPE_CHECKING:
925 typeChecking = true;
926 earlyTypeChecking = true;
927 break;
928
929 case 'i':
930 incrementalSolving = true;
931 break;
932
933 case REPLAY:
934 #ifdef CVC4_REPLAY
935 if(optarg == NULL || *optarg == '\0') {
936 throw OptionException(string("Bad file name for --replay"));
937 } else {
938 replayFilename = optarg;
939 }
940 #else /* CVC4_REPLAY */
941 throw OptionException("The replay feature was disabled in this build of CVC4.");
942 #endif /* CVC4_REPLAY */
943 break;
944
945 case REPLAY_LOG:
946 #ifdef CVC4_REPLAY
947 if(optarg == NULL || *optarg == '\0') {
948 throw OptionException(string("Bad file name for --replay-log"));
949 } else if(!strcmp(optarg, "-")) {
950 replayLog = &cout;
951 } else {
952 replayLog = new ofstream(optarg, ofstream::out | ofstream::trunc);
953 if(!*replayLog) {
954 throw OptionException(string("Cannot open replay-log file: `") + optarg + "'");
955 }
956 }
957 #else /* CVC4_REPLAY */
958 throw OptionException("The replay feature was disabled in this build of CVC4.");
959 #endif /* CVC4_REPLAY */
960 break;
961
962 case ENABLE_SYMMETRY_BREAKER:
963 ufSymmetryBreaker = true;
964 ufSymmetryBreakerSetByUser = true;
965 break;
966 case DISABLE_SYMMETRY_BREAKER:
967 ufSymmetryBreaker = false;
968 ufSymmetryBreakerSetByUser = true;
969 break;
970
971 case TIME_LIMIT:
972 {
973 int i = atoi(optarg);
974 if(i < 0) {
975 throw OptionException("--time-limit requires a nonnegative argument.");
976 }
977 cumulativeMillisecondLimit = (unsigned long) i;
978 }
979 break;
980 case TIME_LIMIT_PER:
981 {
982 int i = atoi(optarg);
983 if(i < 0) {
984 throw OptionException("--time-limit-per requires a nonnegative argument.");
985 }
986 perCallMillisecondLimit = (unsigned long) i;
987 }
988 break;
989 case RESOURCE_LIMIT:
990 {
991 int i = atoi(optarg);
992 if(i < 0) {
993 throw OptionException("--limit requires a nonnegative argument.");
994 }
995 cumulativeResourceLimit = (unsigned long) i;
996 }
997 break;
998 case RESOURCE_LIMIT_PER:
999 {
1000 int i = atoi(optarg);
1001 if(i < 0) {
1002 throw OptionException("--limit-per requires a nonnegative argument.");
1003 }
1004 perCallResourceLimit = (unsigned long) i;
1005 break;
1006 }
1007 case BITVECTOR_EAGER_BITBLAST:
1008 {
1009 bitvectorEagerBitblast = true;
1010 break;
1011 }
1012 case BITVECTOR_EAGER_FULLCHECK:
1013 {
1014 bitvectorEagerFullcheck = true;
1015 break;
1016 }
1017 case BITVECTOR_SHARE_LEMMAS:
1018 {
1019 bitvectorShareLemmas = true;
1020 break;
1021 }
1022 case SAT_REFINE_CONFLICTS:
1023 {
1024 sat_refine_conflicts = true;
1025 break;
1026 }
1027 case RANDOM_SEED:
1028 satRandomSeed = atof(optarg);
1029 break;
1030
1031 case RANDOM_FREQUENCY:
1032 satRandomFreq = atof(optarg);
1033 if(! (0.0 <= satRandomFreq && satRandomFreq <= 1.0)){
1034 throw OptionException(string("--random-freq: `") +
1035 optarg + "' is not between 0.0 and 1.0.");
1036 }
1037 break;
1038
1039 case SAT_RESTART_FIRST:
1040 {
1041 int i = atoi(optarg);
1042 if(i < 1) {
1043 throw OptionException("--restart-int-base requires a number bigger than 1");
1044 }
1045 satRestartFirst = i;
1046 break;
1047 }
1048
1049 case SAT_RESTART_INC:
1050 {
1051 int i = atoi(optarg);
1052 if(i < 1) {
1053 throw OptionException("--restart-int-inc requires a number bigger than 1.0");
1054 }
1055 satRestartInc = i;
1056 }
1057 break;
1058
1059 case ARITHMETIC_UNATE_LEMMA_MODE:
1060 if(!strcmp(optarg, "all")) {
1061 arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS;
1062 break;
1063 } else if(!strcmp(optarg, "none")) {
1064 arithUnateLemmaMode = NO_PRESOLVE_LEMMAS;
1065 break;
1066 } else if(!strcmp(optarg, "ineqs")) {
1067 arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS;
1068 break;
1069 } else if(!strcmp(optarg, "eqs")) {
1070 arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS;
1071 break;
1072 } else if(!strcmp(optarg, "help")) {
1073 puts(arithPresolveLemmasHelp.c_str());
1074 exit(1);
1075 } else {
1076 throw OptionException(string("unknown option for --arith-presolve-lemmas: `") +
1077 optarg + "'. Try --arith-presolve-lemmas=help.");
1078 }
1079 break;
1080
1081 case ARITHMETIC_PROPAGATION_MODE:
1082 if(!strcmp(optarg, "none")) {
1083 arithPropagationMode = NO_PROP;
1084 break;
1085 } else if(!strcmp(optarg, "unate")) {
1086 arithPropagationMode = UNATE_PROP;
1087 break;
1088 } else if(!strcmp(optarg, "bi")) {
1089 arithPropagationMode = BOUND_INFERENCE_PROP;
1090 break;
1091 } else if(!strcmp(optarg, "both")) {
1092 arithPropagationMode = BOTH_PROP;
1093 break;
1094 } else if(!strcmp(optarg, "help")) {
1095 puts(propagationModeHelp.c_str());
1096 exit(1);
1097 } else {
1098 throw OptionException(string("unknown option for --arith-prop: `") +
1099 optarg + "'. Try --arith-prop help.");
1100 }
1101 break;
1102
1103 case ARITHMETIC_PIVOT_RULE:
1104 if(!strcmp(optarg, "min")) {
1105 arithPivotRule = MINIMUM;
1106 break;
1107 } else if(!strcmp(optarg, "min-break-ties")) {
1108 arithPivotRule = BREAK_TIES;
1109 break;
1110 } else if(!strcmp(optarg, "max")) {
1111 arithPivotRule = MAXIMUM;
1112 break;
1113 } else if(!strcmp(optarg, "help")) {
1114 puts(pivotRulesHelp.c_str());
1115 exit(1);
1116 } else {
1117 throw OptionException(string("unknown option for --pivot-rule: `") +
1118 optarg + "'. Try --pivot-rule help.");
1119 }
1120 break;
1121
1122 case ARITHMETIC_PIVOT_THRESHOLD:
1123 arithPivotThreshold = atoi(optarg);
1124 break;
1125
1126 case ARITHMETIC_PROP_MAX_LENGTH:
1127 arithPropagateMaxLength = atoi(optarg);
1128 break;
1129
1130 case ARITHMETIC_DIO_SOLVER:
1131 arithDioSolver = false;
1132 break;
1133
1134 case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
1135 arithRewriteEq = true;
1136 arithRewriteEqSetByUser = true;
1137 break;
1138
1139 case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
1140 arithRewriteEq = false;
1141 arithRewriteEqSetByUser = true;
1142 break;
1143
1144 case SHOW_DEBUG_TAGS:
1145 if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
1146 printf("available tags:");
1147 unsigned ntags = Configuration::getNumDebugTags();
1148 char const* const* tags = Configuration::getDebugTags();
1149 for(unsigned i = 0; i < ntags; ++ i) {
1150 printf(" %s", tags[i]);
1151 }
1152 printf("\n");
1153 } else if(! Configuration::isDebugBuild()) {
1154 throw OptionException("debug tags not available in non-debug builds");
1155 } else {
1156 throw OptionException("debug tags not available in non-tracing builds");
1157 }
1158 exit(0);
1159 break;
1160
1161 case SHOW_TRACE_TAGS:
1162 if(Configuration::isTracingBuild()) {
1163 printf("available tags:");
1164 unsigned ntags = Configuration::getNumTraceTags();
1165 char const* const* tags = Configuration::getTraceTags();
1166 for (unsigned i = 0; i < ntags; ++ i) {
1167 printf(" %s", tags[i]);
1168 }
1169 printf("\n");
1170 } else {
1171 throw OptionException("trace tags not available in non-tracing builds");
1172 }
1173 exit(0);
1174 break;
1175
1176 case SHOW_SAT_SOLVERS:
1177 {
1178 vector<string> solvers;
1179 prop::SatSolverFactory::getSolverIds(solvers);
1180 printf("Available SAT solvers: ");
1181 for (unsigned i = 0; i < solvers.size(); ++ i) {
1182 if (i > 0) {
1183 printf(", ");
1184 }
1185 printf("%s", solvers[i].c_str());
1186 }
1187 printf("\n");
1188 exit(0);
1189 break;
1190 }
1191 case SHOW_CONFIG:
1192 fputs(Configuration::about().c_str(), stdout);
1193 printf("\n");
1194 printf("version : %s\n", Configuration::getVersionString().c_str());
1195 if(Configuration::isSubversionBuild()) {
1196 printf("subversion : yes [%s r%u%s]\n",
1197 Configuration::getSubversionBranchName(),
1198 Configuration::getSubversionRevision(),
1199 Configuration::hasSubversionModifications() ?
1200 " (with modifications)" : "");
1201 } else {
1202 printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
1203 }
1204 printf("\n");
1205 printf("library : %u.%u.%u\n",
1206 Configuration::getVersionMajor(),
1207 Configuration::getVersionMinor(),
1208 Configuration::getVersionRelease());
1209 printf("\n");
1210 printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
1211 printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
1212 printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
1213 printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
1214 printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
1215 printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
1216 printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
1217 printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no");
1218 printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
1219 printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
1220 printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
1221 printf("\n");
1222 printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
1223 printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
1224 printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
1225 printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
1226 exit(0);
1227
1228 case PARALLEL_THREADS:
1229 threads = atoi(optarg);
1230 break;
1231
1232 case PARALLEL_SEPARATE_OUTPUT:
1233 separateOutput = true;
1234 break;
1235
1236 case PORTFOLIO_FILTER_LENGTH:
1237 sharingFilterByLength = atoi(optarg);
1238 break;
1239
1240 case ':':
1241 // This can be a long or short option, and the way to get at the name of it is different.
1242 if(optopt == 0 || // was a long option
1243 (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option
1244 throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
1245 } else { // was a short option
1246 throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
1247 }
1248
1249 case '?':
1250 default:
1251 if(optopt == 0 &&
1252 !strncmp(argv[optind - 1], "--thread", 8) &&
1253 strlen(argv[optind - 1]) > 8 &&
1254 isdigit(argv[optind - 1][8])) {
1255 int tnum = atoi(argv[optind - 1] + 8);
1256 threadArgv.resize(tnum + 1);
1257 if(threadArgv[tnum] != "") {
1258 threadArgv[tnum] += " ";
1259 }
1260 const char* p = strchr(argv[optind - 1] + 9, '=');
1261 if(p == NULL) { // e.g., we have --thread0 "foo"
1262 threadArgv[tnum] += argv[optind++];
1263 } else { // e.g., we have --thread0="foo"
1264 threadArgv[tnum] += p + 1;
1265 }
1266 break;
1267 }
1268
1269 // This can be a long or short option, and the way to get at the name of it is different.
1270 if(optopt == 0) { // was a long option
1271 throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
1272 } else { // was a short option
1273 throw OptionException(string("can't understand option `-") + char(optopt) + "'");
1274 }
1275 }
1276 }
1277
1278 if(incrementalSolving && proof) {
1279 throw OptionException(string("The use of --incremental with --proof is not yet supported"));
1280 }
1281
1282 return optind;
1283 }
1284
1285 void Options::setOutputLanguage(const char* str) throw(OptionException) {
1286 if(!strcmp(str, "cvc4") || !strcmp(str, "pl")) {
1287 outputLanguage = language::output::LANG_CVC4;
1288 return;
1289 } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
1290 outputLanguage = language::output::LANG_SMTLIB;
1291 return;
1292 } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
1293 outputLanguage = language::output::LANG_SMTLIB_V2;
1294 return;
1295 } else if(!strcmp(str, "ast")) {
1296 outputLanguage = language::output::LANG_AST;
1297 return;
1298 } else if(!strcmp(str, "auto")) {
1299 outputLanguage = language::output::LANG_AUTO;
1300 return;
1301 }
1302
1303 if(strcmp(str, "help")) {
1304 throw OptionException(string("unknown language for --output-lang: `") +
1305 str + "'. Try --output-lang help.");
1306 }
1307
1308 languageHelp = true;
1309 }
1310
1311 void Options::setInputLanguage(const char* str) throw(OptionException) {
1312 if(!strcmp(str, "cvc4") || !strcmp(str, "pl") || !strcmp(str, "presentation")) {
1313 inputLanguage = language::input::LANG_CVC4;
1314 return;
1315 } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
1316 inputLanguage = language::input::LANG_SMTLIB;
1317 return;
1318 } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
1319 inputLanguage = language::input::LANG_SMTLIB_V2;
1320 return;
1321 } else if(!strcmp(str, "auto")) {
1322 inputLanguage = language::input::LANG_AUTO;
1323 return;
1324 }
1325
1326 if(strcmp(str, "help")) {
1327 throw OptionException(string("unknown language for --lang: `") +
1328 str + "'. Try --lang help.");
1329 }
1330
1331 languageHelp = true;
1332 }
1333
1334 std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) {
1335 switch(rule) {
1336 case Options::MINIMUM:
1337 out << "MINIMUM";
1338 break;
1339 case Options::BREAK_TIES:
1340 out << "BREAK_TIES";
1341 break;
1342 case Options::MAXIMUM:
1343 out << "MAXIMUM";
1344 break;
1345 default:
1346 out << "ArithPivotRule!UNKNOWN";
1347 }
1348
1349 return out;
1350 }
1351
1352 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
1353 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
1354
1355 }/* CVC4 namespace */