1 /********************* */
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
14 ** \brief Contains code for handling command-line options.
16 ** Contains code for handling command-line options
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"
40 #include "cvc4autoconfig.h"
47 CVC4_THREADLOCAL(const Options
*) Options::s_current
= NULL
;
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 */
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 */
68 inputLanguage(language::input::LANG_AUTO
),
69 outputLanguage(language::output::LANG_AUTO
),
74 preprocessOnly(false),
75 semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT
),
76 theoryRegistration(true),
79 lazyDefinitionExpansion(false),
81 simplificationMode(SIMPLIFICATION_MODE_BATCH
),
82 simplificationModeSetByUser(false),
83 decisionMode(DECISION_STRATEGY_INTERNAL
),
84 decisionModeSetByUser(false),
85 doStaticLearning(true),
87 doITESimpSetByUser(false),
89 repeatSimpSetByUser(false),
91 interactiveSetByUser(false),
92 perCallResourceLimit(0),
93 cumulativeResourceLimit(0),
94 perCallMillisecondLimit(0),
95 cumulativeMillisecondLimit(0),
99 produceAssignments(false),
100 typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT
),
101 earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT
),
102 incrementalSolving(false),
107 satRandomSeed(91648253),// Minisat's default value
109 satClauseDecay(0.999),
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
127 separateOutput(false),
128 sharingFilterByLength(-1),
129 bitvectorEagerBitblast(false),
130 bitvectorEagerFullcheck(false),
131 bitvectorShareLemmas(false),
132 sat_refine_conflicts(false)
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\
167 static const string optionsDescription
= mostCommonOptionsDescription
+ "\
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\
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\
202 --restart-int-inc=F restart interval increase factor for the sat solver\n\
203 (F=3.0 by default)\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 \
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\
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\
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\
251 static const string simplificationHelp
= "\
252 Simplification modes currently supported by the --simplification option:\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\
260 + run nonclausal simplification and clausal propagation at each ASSERT\n\
261 (and at CHECKSAT/QUERY/SUBTYPE)\n\
264 + do not perform nonclausal simplification\n\
267 static const string decisionHelp
= "\
268 Decision modes currently supported by the --decision option:\n\
270 internal (default)\n\
271 + Use the internal decision hueristics of the SAT solver\n\
274 + An ATGP-inspired justification heuristic\n\
277 static const string dumpHelp
= "\
278 Dump modes currently supported by the --dump option:\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\
286 + Dump declarations. Implied by all following modes.\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\
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\
302 + Do all the preprocessing outlined above, and dump the CNF-converted\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\
310 t-conflicts [non-stateful]\n\
311 + Output correctness queries for all theory conflicts\n\
313 missed-t-conflicts [stateful]\n\
314 + Output completeness queries for theory conflicts\n\
316 t-propagations [stateful]\n\
317 + Output correctness queries for all theory propagations\n\
319 missed-t-propagations [stateful]\n\
320 + Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
322 t-lemmas [non-stateful]\n\
323 + Output correctness queries for all theory lemmas\n\
325 t-explanations [non-stateful]\n\
326 + Output correctness queries for all theory explanations\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\
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\
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\
349 Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\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\
355 A combination of inequalities and equalities.\n\
358 static const string propagationModeHelp
= "\
359 This decides on kind of propagation arithmetic attempts to do during the search.\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\
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\
374 The minimum abs() value of the variable's violation of its bound. (default)\n\
376 The minimum violation with ties broken by variable order (total)\n\
378 The maximum violation the bound\n\
381 string
Options::getDescription() const {
382 return optionsDescription
;
385 void Options::printUsage(const std::string msg
, std::ostream
& out
) {
386 out
<< msg
<< optionsDescription
<< endl
<< flush
;
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
;
394 void Options::printLanguageHelp(std::ostream
& out
) {
395 out
<< languageDescription
<< flush
;
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
407 OPTION_VALUE_BEGIN
= 256, /* avoid clashing with char options */
417 NO_THEORY_REGISTRATION
,
427 LAZY_DEFINITION_EXPANSION
,
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
,
462 PARALLEL_SEPARATE_OUTPUT
,
463 PORTFOLIO_FILTER_LENGTH
,
468 BITVECTOR_EAGER_BITBLAST
,
469 BITVECTOR_SHARE_LEMMAS
,
470 BITVECTOR_EAGER_FULLCHECK
,
471 SAT_REFINE_CONFLICTS
,
473 };/* enum OptionValue */
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.
480 * Each option in this array has four elements:
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)
493 * If you add something here, you should add it in src/main/usage.h
494 * also, to document it.
496 * If you add something that has a short option equivalent, you should
497 * add it to the getopt_long() call in parseOptions().
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! */
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];
584 // Reset getopt(), in the case of multiple calls.
585 // This can be = 1 in newer GNU getopt, but older (< 2007) require = 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 */
591 // find the base name of the program
592 const char *x
= strrchr(progName
, '/');
596 binary_name
= string(progName
);
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
,
611 cmdlineOptions
, NULL
)) != -1) {
631 setInputLanguage(optarg
);
634 case OUTPUT_LANGUAGE
:
635 setOutputLanguage(optarg
);
639 if(Configuration::isTracingBuild()) {
640 if(!Configuration::isTraceTag(optarg
))
641 throw OptionException(string("trace tag ") + optarg
+
642 string(" not available"));
644 throw OptionException("trace tags not available in non-tracing builds");
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"));
655 } else if(! Configuration::isDebugBuild()) {
656 throw OptionException("debug tags not available in non-debug builds");
658 throw OptionException("debug tags not available in non-tracing builds");
676 case PREPROCESS_ONLY
:
677 preprocessOnly
= true;
682 char* tokstr
= optarg
;
684 while((optarg
= strtok_r(tokstr
, ",", &toksave
)) != 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; "
705 Dump
.on("no-permit-state");
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; "
723 } else if(!strcmp(optarg
, "help")) {
724 puts(dumpHelp
.c_str());
727 throw OptionException(string("unknown option for --dump: `") +
728 optarg
+ "'. Try --dump help.");
732 Dump
.on("benchmark");
733 if(strcmp(optarg
, "benchmark")) {
734 Dump
.on("declarations");
737 #else /* CVC4_DUMPING */
738 throw OptionException("The dumping feature was disabled in this build of CVC4.");
739 #endif /* 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
);
750 ostream
* dumpTo
= new ofstream(optarg
, ofstream::out
| ofstream::trunc
);
752 throw OptionException(string("Cannot open dump-to file (maybe it exists): `") + optarg
+ "'");
754 Dump
.setStream(*dumpTo
);
756 #else /* CVC4_DUMPING */
757 throw OptionException("The dumping feature was disabled in this build of CVC4.");
758 #endif /* CVC4_DUMPING */
762 case NO_THEORY_REGISTRATION
:
763 theoryRegistration
= false;
767 semanticChecks
= false;
768 typeChecking
= false;
769 earlyTypeChecking
= false;
781 strictParsing
= true;
784 case DEFAULT_EXPR_DEPTH
:
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
);
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);
805 case LAZY_DEFINITION_EXPANSION
:
806 lazyDefinitionExpansion
= true;
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());
823 throw OptionException(string("unknown option for --simplification: `") +
824 optarg
+ "'. Try --simplification help.");
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());
839 throw OptionException(string("unknown option for --decision: `") +
840 optarg
+ "'. Try --decision help.");
844 case NO_STATIC_LEARNING
:
845 doStaticLearning
= false;
850 doITESimpSetByUser
= true;
855 doITESimpSetByUser
= true;
860 repeatSimpSetByUser
= true;
865 repeatSimpSetByUser
= true;
870 interactiveSetByUser
= true;
875 interactiveSetByUser
= true;
879 produceModels
= true;
882 case PRODUCE_ASSIGNMENTS
:
883 produceAssignments
= true;
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 */
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);
909 #else /* CVC4_PROOF */
910 throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used");
911 #endif /* CVC4_PROOF */
914 case NO_TYPE_CHECKING
:
915 typeChecking
= false;
916 earlyTypeChecking
= false;
919 case LAZY_TYPE_CHECKING
:
921 earlyTypeChecking
= false;
924 case EAGER_TYPE_CHECKING
:
926 earlyTypeChecking
= true;
930 incrementalSolving
= true;
935 if(optarg
== NULL
|| *optarg
== '\0') {
936 throw OptionException(string("Bad file name for --replay"));
938 replayFilename
= optarg
;
940 #else /* CVC4_REPLAY */
941 throw OptionException("The replay feature was disabled in this build of CVC4.");
942 #endif /* CVC4_REPLAY */
947 if(optarg
== NULL
|| *optarg
== '\0') {
948 throw OptionException(string("Bad file name for --replay-log"));
949 } else if(!strcmp(optarg
, "-")) {
952 replayLog
= new ofstream(optarg
, ofstream::out
| ofstream::trunc
);
954 throw OptionException(string("Cannot open replay-log file: `") + optarg
+ "'");
957 #else /* CVC4_REPLAY */
958 throw OptionException("The replay feature was disabled in this build of CVC4.");
959 #endif /* CVC4_REPLAY */
962 case ENABLE_SYMMETRY_BREAKER
:
963 ufSymmetryBreaker
= true;
964 ufSymmetryBreakerSetByUser
= true;
966 case DISABLE_SYMMETRY_BREAKER
:
967 ufSymmetryBreaker
= false;
968 ufSymmetryBreakerSetByUser
= true;
973 int i
= atoi(optarg
);
975 throw OptionException("--time-limit requires a nonnegative argument.");
977 cumulativeMillisecondLimit
= (unsigned long) i
;
982 int i
= atoi(optarg
);
984 throw OptionException("--time-limit-per requires a nonnegative argument.");
986 perCallMillisecondLimit
= (unsigned long) i
;
991 int i
= atoi(optarg
);
993 throw OptionException("--limit requires a nonnegative argument.");
995 cumulativeResourceLimit
= (unsigned long) i
;
998 case RESOURCE_LIMIT_PER
:
1000 int i
= atoi(optarg
);
1002 throw OptionException("--limit-per requires a nonnegative argument.");
1004 perCallResourceLimit
= (unsigned long) i
;
1007 case BITVECTOR_EAGER_BITBLAST
:
1009 bitvectorEagerBitblast
= true;
1012 case BITVECTOR_EAGER_FULLCHECK
:
1014 bitvectorEagerFullcheck
= true;
1017 case BITVECTOR_SHARE_LEMMAS
:
1019 bitvectorShareLemmas
= true;
1022 case SAT_REFINE_CONFLICTS
:
1024 sat_refine_conflicts
= true;
1028 satRandomSeed
= atof(optarg
);
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.");
1039 case SAT_RESTART_FIRST
:
1041 int i
= atoi(optarg
);
1043 throw OptionException("--restart-int-base requires a number bigger than 1");
1045 satRestartFirst
= i
;
1049 case SAT_RESTART_INC
:
1051 int i
= atoi(optarg
);
1053 throw OptionException("--restart-int-inc requires a number bigger than 1.0");
1059 case ARITHMETIC_UNATE_LEMMA_MODE
:
1060 if(!strcmp(optarg
, "all")) {
1061 arithUnateLemmaMode
= ALL_PRESOLVE_LEMMAS
;
1063 } else if(!strcmp(optarg
, "none")) {
1064 arithUnateLemmaMode
= NO_PRESOLVE_LEMMAS
;
1066 } else if(!strcmp(optarg
, "ineqs")) {
1067 arithUnateLemmaMode
= INEQUALITY_PRESOLVE_LEMMAS
;
1069 } else if(!strcmp(optarg
, "eqs")) {
1070 arithUnateLemmaMode
= EQUALITY_PRESOLVE_LEMMAS
;
1072 } else if(!strcmp(optarg
, "help")) {
1073 puts(arithPresolveLemmasHelp
.c_str());
1076 throw OptionException(string("unknown option for --arith-presolve-lemmas: `") +
1077 optarg
+ "'. Try --arith-presolve-lemmas=help.");
1081 case ARITHMETIC_PROPAGATION_MODE
:
1082 if(!strcmp(optarg
, "none")) {
1083 arithPropagationMode
= NO_PROP
;
1085 } else if(!strcmp(optarg
, "unate")) {
1086 arithPropagationMode
= UNATE_PROP
;
1088 } else if(!strcmp(optarg
, "bi")) {
1089 arithPropagationMode
= BOUND_INFERENCE_PROP
;
1091 } else if(!strcmp(optarg
, "both")) {
1092 arithPropagationMode
= BOTH_PROP
;
1094 } else if(!strcmp(optarg
, "help")) {
1095 puts(propagationModeHelp
.c_str());
1098 throw OptionException(string("unknown option for --arith-prop: `") +
1099 optarg
+ "'. Try --arith-prop help.");
1103 case ARITHMETIC_PIVOT_RULE
:
1104 if(!strcmp(optarg
, "min")) {
1105 arithPivotRule
= MINIMUM
;
1107 } else if(!strcmp(optarg
, "min-break-ties")) {
1108 arithPivotRule
= BREAK_TIES
;
1110 } else if(!strcmp(optarg
, "max")) {
1111 arithPivotRule
= MAXIMUM
;
1113 } else if(!strcmp(optarg
, "help")) {
1114 puts(pivotRulesHelp
.c_str());
1117 throw OptionException(string("unknown option for --pivot-rule: `") +
1118 optarg
+ "'. Try --pivot-rule help.");
1122 case ARITHMETIC_PIVOT_THRESHOLD
:
1123 arithPivotThreshold
= atoi(optarg
);
1126 case ARITHMETIC_PROP_MAX_LENGTH
:
1127 arithPropagateMaxLength
= atoi(optarg
);
1130 case ARITHMETIC_DIO_SOLVER
:
1131 arithDioSolver
= false;
1134 case ENABLE_ARITHMETIC_REWRITE_EQUALITIES
:
1135 arithRewriteEq
= true;
1136 arithRewriteEqSetByUser
= true;
1139 case DISABLE_ARITHMETIC_REWRITE_EQUALITIES
:
1140 arithRewriteEq
= false;
1141 arithRewriteEqSetByUser
= true;
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
]);
1153 } else if(! Configuration::isDebugBuild()) {
1154 throw OptionException("debug tags not available in non-debug builds");
1156 throw OptionException("debug tags not available in non-tracing builds");
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
]);
1171 throw OptionException("trace tags not available in non-tracing builds");
1176 case SHOW_SAT_SOLVERS
:
1178 vector
<string
> solvers
;
1179 prop::SatSolverFactory::getSolverIds(solvers
);
1180 printf("Available SAT solvers: ");
1181 for (unsigned i
= 0; i
< solvers
.size(); ++ i
) {
1185 printf("%s", solvers
[i
].c_str());
1192 fputs(Configuration::about().c_str(), stdout
);
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)" : "");
1202 printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
1205 printf("library : %u.%u.%u\n",
1206 Configuration::getVersionMajor(),
1207 Configuration::getVersionMinor(),
1208 Configuration::getVersionRelease());
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");
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");
1228 case PARALLEL_THREADS
:
1229 threads
= atoi(optarg
);
1232 case PARALLEL_SEPARATE_OUTPUT
:
1233 separateOutput
= true;
1236 case PORTFOLIO_FILTER_LENGTH
:
1237 sharingFilterByLength
= atoi(optarg
);
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");
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
] += " ";
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;
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
) + "'");
1278 if(incrementalSolving
&& proof
) {
1279 throw OptionException(string("The use of --incremental with --proof is not yet supported"));
1285 void Options::setOutputLanguage(const char* str
) throw(OptionException
) {
1286 if(!strcmp(str
, "cvc4") || !strcmp(str
, "pl")) {
1287 outputLanguage
= language::output::LANG_CVC4
;
1289 } else if(!strcmp(str
, "smtlib") || !strcmp(str
, "smt")) {
1290 outputLanguage
= language::output::LANG_SMTLIB
;
1292 } else if(!strcmp(str
, "smtlib2") || !strcmp(str
, "smt2")) {
1293 outputLanguage
= language::output::LANG_SMTLIB_V2
;
1295 } else if(!strcmp(str
, "ast")) {
1296 outputLanguage
= language::output::LANG_AST
;
1298 } else if(!strcmp(str
, "auto")) {
1299 outputLanguage
= language::output::LANG_AUTO
;
1303 if(strcmp(str
, "help")) {
1304 throw OptionException(string("unknown language for --output-lang: `") +
1305 str
+ "'. Try --output-lang help.");
1308 languageHelp
= true;
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
;
1315 } else if(!strcmp(str
, "smtlib") || !strcmp(str
, "smt")) {
1316 inputLanguage
= language::input::LANG_SMTLIB
;
1318 } else if(!strcmp(str
, "smtlib2") || !strcmp(str
, "smt2")) {
1319 inputLanguage
= language::input::LANG_SMTLIB_V2
;
1321 } else if(!strcmp(str
, "auto")) {
1322 inputLanguage
= language::input::LANG_AUTO
;
1326 if(strcmp(str
, "help")) {
1327 throw OptionException(string("unknown language for --lang: `") +
1328 str
+ "'. Try --lang help.");
1331 languageHelp
= true;
1334 std::ostream
& operator<<(std::ostream
& out
, Options::ArithPivotRule rule
) {
1336 case Options::MINIMUM
:
1339 case Options::BREAK_TIES
:
1340 out
<< "BREAK_TIES";
1342 case Options::MAXIMUM
:
1346 out
<< "ArithPivotRule!UNKNOWN";
1352 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
1353 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
1355 }/* CVC4 namespace */