projects / cvc5.git / blob
? search:


c912023ad35eb63250fe252d2cf4d116443f402e
[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 /** default decision options */
62 const Options::DecisionOptions defaultDecOpt = {
63 false, // relevancyLeaves
64 1000, // maxRelTimeAsPermille
65 true, // computeRelevancy
66 false, // mustRelevancy
67 };
68
69 Options::Options() :
70 binary_name(),
71 statistics(false),
72 in(&std::cin),
73 out(&std::cout),
74 err(&std::cerr),
75 verbosity(0),
76 inputLanguage(language::input::LANG_AUTO),
77 outputLanguage(language::output::LANG_AUTO),
78 help(false),
79 version(false),
80 languageHelp(false),
81 parseOnly(false),
82 preprocessOnly(false),
83 semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
84 theoryRegistration(true),
85 memoryMap(false),
86 strictParsing(false),
87 lazyDefinitionExpansion(false),
88 printWinner(false),
89 simplificationMode(SIMPLIFICATION_MODE_BATCH),
90 simplificationModeSetByUser(false),
91 decisionMode(DECISION_STRATEGY_INTERNAL),
92 decisionModeSetByUser(false),
93 decisionOptions(DecisionOptions(defaultDecOpt)),
94 doStaticLearning(true),
95 doITESimp(false),
96 doITESimpSetByUser(false),
97 unconstrainedSimp(false),
98 unconstrainedSimpSetByUser(false),
99 repeatSimp(false),
100 repeatSimpSetByUser(false),
101 interactive(false),
102 interactiveSetByUser(false),
103 perCallResourceLimit(0),
104 cumulativeResourceLimit(0),
105 perCallMillisecondLimit(0),
106 cumulativeMillisecondLimit(0),
107 segvNoSpin(false),
108 produceModels(false),
109 proof(false),
110 produceAssignments(false),
111 typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
112 earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
113 incrementalSolving(false),
114 replayFilename(""),
115 replayStream(NULL),
116 replayLog(NULL),
117 satRandomFreq(0.0),
118 satRandomSeed(91648253),// Minisat's default value
119 satVarDecay(0.95),
120 satClauseDecay(0.999),
121 satRestartFirst(25),
122 satRestartInc(3.0),
123 arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
124 arithPropagationMode(BOTH_PROP),
125 arithHeuristicPivots(0),
126 arithHeuristicPivotsSetByUser(false),
127 arithStandardCheckVarOrderPivots(-1),
128 arithStandardCheckVarOrderPivotsSetByUser(false),
129 arithHeuristicPivotRule(MINIMUM),
130 arithSimplexCheckPeriod(200),
131 arithPivotThreshold(2),
132 arithPivotThresholdSetByUser(false),
133 arithPropagateMaxLength(16),
134 arithDioSolver(true),
135 arithRewriteEq(false),
136 arithRewriteEqSetByUser(false),
137 ufSymmetryBreaker(false),
138 ufSymmetryBreakerSetByUser(false),
139 miniscopeQuant(true),
140 miniscopeQuantFreeVar(true),
141 prenexQuant(true),
142 varElimQuant(false),
143 cnfQuant(false),
144 preSkolemQuant(false),
145 smartTriggers(true),
146 registerQuantBodyTerms(false),
147 instWhenMode(INST_WHEN_FULL_LAST_CALL),
148 eagerInstQuant(false),
149 finiteModelFind(false),
150 fmfRegionSat(false),
151 fmfModelBasedInst(true),
152 efficientEMatching(false),
153 literalMatchMode(LITERAL_MATCH_NONE),
154 cbqi(false),
155 cbqiSetByUser(false),
156 userPatternsQuant(true),
157 flipDecision(false),
158 lemmaOutputChannel(NULL),
159 lemmaInputChannel(NULL),
160 threads(2),// default should be 1 probably, but say 2 for now
161 threadArgv(),
162 thread_id(-1),
163 separateOutput(false),
164 sharingFilterByLength(-1),
165 bitvectorEagerBitblast(false),
166 bitvectorEagerFullcheck(false),
167 bitvectorShareLemmas(false),
168 sat_refine_conflicts(false),
169 theoryOfModeSetByUser(false),
170 theoryOfMode(theory::THEORY_OF_TYPE_BASED)
171 {
172 }
173
174
175 static const string mostCommonOptionsDescription = "\
176 Most commonly-used CVC4 options:\n\
177 --version | -V identify this CVC4 binary\n\
178 --help | -h full command line reference\n\
179 --lang | -L force input language\n\
180 (default is `auto'; see --lang help)\n\
181 --output-lang force output language\n\
182 (default is `auto'; see --lang help)\n\
183 --verbose | -v increase verbosity (may be repeated)\n\
184 --quiet | -q decrease verbosity (may be repeated)\n\
185 --stats give statistics on exit\n\
186 --parse-only exit after parsing input\n\
187 --preprocess-only exit after preproc (useful with --stats or --dump)\n\
188 --dump=MODE dump preprocessed assertions, etc., see --dump=help\n\
189 --dump-to=FILE all dumping goes to FILE (instead of stdout)\n\
190 --show-config show CVC4 static configuration\n\
191 --strict-parsing be less tolerant of non-conforming inputs\n\
192 --interactive force interactive mode\n\
193 --no-interactive force non-interactive mode\n\
194 --produce-models | -m support the get-value command\n\
195 --produce-assignments support the get-assignment command\n\
196 --print-success print the \"success\" output required of SMT-LIBv2\n\
197 --smtlib2 SMT-LIBv2 conformance mode (implies other options)\n\
198 --proof turn on proof generation\n\
199 --incremental | -i enable incremental solving\n\
200 --tlimit=MS enable time limiting (give milliseconds)\n\
201 --tlimit-per=MS enable time limiting per query (give milliseconds)\n\
202 --rlimit=N enable resource limiting\n\
203 --rlimit-per=N enable resource limiting per query\n\
204 ";
205
206 static const string optionsDescription = mostCommonOptionsDescription + "\
207 \n\
208 Additional CVC4 options:\n\
209 --mmap memory map file input\n\
210 --segv-nospin don't spin on segfault waiting for gdb\n\
211 --lazy-type-checking type check expressions only when necessary (default)\n\
212 --eager-type-checking type check expressions immediately on creation\n\
213 (debug builds only)\n\
214 --no-type-checking never type check expressions\n\
215 --no-checking disable ALL semantic checks, including type checks\n\
216 --no-theory-registration disable theory reg (not safe for some theories)\n\
217 --print-winner enable printing the winning thread (pcvc4 only)\n\
218 --trace | -t trace something (e.g. -t pushpop), can repeat\n\
219 --debug | -d debug something (e.g. -d arith), can repeat\n\
220 --show-debug-tags show all avalable tags for debugging\n\
221 --show-trace-tags show all avalable tags for tracing\n\
222 --show-sat-solvers show all available SAT solvers\n\
223 --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
224 --default-dag-thresh=N dagify common subexprs appearing > N times\n\
225 (1 == default, 0 == don't dagify)\n\
226 --print-expr-types print types with variables when printing exprs\n\
227 --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
228 --simplification=MODE choose simplification mode, see --simplification=help\n\
229 --decision=MODE choose decision mode, see --decision=help\n\
230 --decision-budget=N impose a budget for relevancy hueristic which increases linearly with\n\
231 each decision. N between 0 and 1000. (default: 1000, no budget)\n\
232 --no-static-learning turn off static learning (e.g. diamond-breaking)\n\
233 --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
234 --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
235 --unconstrained-simp turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
236 --no-unconstrained-simp turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
237 --repeat-simp make multiple passes with nonclausal simplifier\n\
238 --no-repeat-simp do not make multiple passes with nonclausal simplifier\n\
239 --replay=file replay decisions from file\n\
240 --replay-log=file log decisions and propagations to file\n\
241 --theoryof-mode=mode mode for theoryof\n\
242 SAT:\n\
243 --random-freq=P frequency of random decisions in the sat solver\n\
244 (P=0.0 by default)\n\
245 --random-seed=S sets the random seed for the sat solver\n\
246 --restart-int-base=I sets the base restart interval for the sat solver\n\
247 (I=25 by default)\n\
248 --restart-int-inc=F restart interval increase factor for the sat solver\n\
249 (F=3.0 by default)\n\
250 ARITHMETIC:\n\
251 --unate-lemmas=MODE determines which lemmas to add before solving\n\
252 (default is 'all', see --unate-lemmas=help)\n\
253 --arith-prop=MODE turns on arithmetic propagation\n\
254 (default is 'old', see --arith-prop=help)\n\
255 --heuristic-pivot-rule=RULE change the pivot rule for the basic variable\n\
256 (default is 'min', see --heuristic-pivot-rule help)\n\
257 --heuristic-pivots=N the number of times to apply the heuristic pivot rule.\n\
258 If N < 0, this defaults to the number of variables\n\
259 If this is unset, this is tuned by the logic selection.\n\
260 --simplex-check-period=N The number of pivots to do in simplex before rechecking for\n\
261 a conflict on all variables.\n\
262 --pivot-threshold=N sets the number of pivots using --pivot-rule\n\
263 per basic variable per simplex instance before\n\
264 using variable order\n\
265 --prop-row-length=N sets the maximum row length to be used in propagation\n\
266 --disable-dio-solver turns off Linear Diophantine Equation solver \n\
267 (Griggio, JSAT 2012)\n\
268 --enable-arith-rewrite-equalities turns on the preprocessing rewrite\n\
269 turning equalities into a conjunction of inequalities.\n \
270 --disable-arith-rewrite-equalities turns off the preprocessing rewrite\n\
271 turning equalities into a conjunction of inequalities.\n \
272 UF:\n\
273 --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
274 CADE 2011) [on by default only for QF_UF]\n\
275 --disable-symmetry-breaker turns off UF symmetry breaker\n\
276 --disable-miniscope-quant disable miniscope quantifiers\n\
277 --disable-miniscope-quant-fv disable miniscope quantifiers for ground subformulas\n\
278 --disable-prenex-quant disable prenexing of quantified formulas\n\
279 --var-elim-quant enable variable elimination of quantified formulas\n\
280 --cnf-quant apply CNF conversion to quantified formulas\n\
281 --pre-skolem-quant apply skolemization eagerly to bodies of quantified formulas\n\
282 --disable-smart-triggers disable smart triggers\n\
283 --register-quant-body-terms consider terms within bodies of quantified formulas for matching\n\
284 --inst-when=MODE when to apply instantiation\n\
285 --eager-inst-quant apply quantifier instantiation eagerly\n\
286 --finite-model-find use finite model finding heuristic for quantifier instantiation\n\
287 --use-fmf-region-sat use region-based SAT heuristic for finite model finding\n\
288 --disable-fmf-model-inst disable model-based instantiation for finite model finding\n\
289 --efficient-e-matching use efficient E-matching\n\
290 --literal-matching=MODE choose literal matching mode\n\
291 --enable-cbqi turns on counterexample-based quantifier instantiation [off by default]\n\
292 --disable-cbqi turns off counterexample-based quantifier instantiation\n\
293 --ignore-user-patterns ignore user-provided patterns for quantifier instantiation\n\
294 --enable-flip-decision turns on flip decision heuristic\n\
295 --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
296 --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
297 --threads=N sets the number of solver threads\n\
298 --threadN=string configures thread N (0..#threads-1)\n\
299 --filter-lemma-length=N don't share lemmas strictly longer than N\n\
300 --bitblast-eager eagerly bitblast the bitvectors to the main SAT solver\n\
301 --bitblast-share-lemmas share lemmas from the bitblsting solver with the main solver\n\
302 --bitblast-eager-fullcheck check the bitblasting eagerly\n\
303 --refine-conflicts refine theory conflict clauses\n\
304 ";
305
306
307
308 static const string languageDescription = "\
309 Languages currently supported as arguments to the -L / --lang option:\n\
310 auto attempt to automatically determine the input language\n\
311 pl | cvc4 CVC4 presentation language\n\
312 smt | smtlib SMT-LIB format 1.2\n\
313 smt2 | smtlib2 SMT-LIB format 2.0\n\
314 \n\
315 Languages currently supported as arguments to the --output-lang option:\n\
316 auto match the output language to the input language\n\
317 pl | cvc4 CVC4 presentation language\n\
318 smt | smtlib SMT-LIB format 1.2\n\
319 smt2 | smtlib2 SMT-LIB format 2.0\n\
320 ast internal format (simple syntax-tree language)\n\
321 ";
322
323 static const string simplificationHelp = "\
324 Simplification modes currently supported by the --simplification option:\n\
325 \n\
326 batch (default) \n\
327 + save up all ASSERTions; run nonclausal simplification and clausal\n\
328 (MiniSat) propagation for all of them only after reaching a querying command\n\
329 (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
330 \n\
331 incremental\n\
332 + run nonclausal simplification and clausal propagation at each ASSERT\n\
333 (and at CHECKSAT/QUERY/SUBTYPE)\n\
334 \n\
335 none\n\
336 + do not perform nonclausal simplification\n\
337 ";
338
339 static const string theoryofHelp = "\
340 TheoryOf modes currently supported by the --theoryof-mode option:\n\
341 \n\
342 type (default) \n\
343 + type variables, constants and equalities by type\n\
344 \n\
345 term \n\
346 + type variables as uninterpreted, equalities by the parametric theory\n\
347 ";
348
349 static const string decisionHelp = "\
350 Decision modes currently supported by the --decision option:\n\
351 \n\
352 internal (default)\n\
353 + Use the internal decision hueristics of the SAT solver\n\
354 \n\
355 justification\n\
356 + An ATGP-inspired justification heuristic\n\
357 \n\
358 relevancy\n\
359 + Under development may-relevancy\n\
360 \n\
361 relevancy-leaves\n\
362 + May-relevancy, but decide only on leaves\n\
363 \n\
364 Developer modes:\n\
365 \n\
366 justification-rel\n\
367 + Use the relevancy code to do the justification stuff\n\
368 + (This should do exact same thing as justification)\n\
369 \n\
370 justification-must\n\
371 + Start deciding on literals close to root instead of those\n\
372 + near leaves (don't expect it to work well) [Unimplemented]\n\
373 ";
374
375 static const string dumpHelp = "\
376 Dump modes currently supported by the --dump option:\n\
377 \n\
378 benchmark\n\
379 + Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
380 does not include any declarations or assertions. Implied by all following\n\
381 modes.\n\
382 \n\
383 declarations\n\
384 + Dump declarations. Implied by all following modes.\n\
385 \n\
386 assertions\n\
387 + Output the assertions after non-clausal simplification and static\n\
388 learning phases, but before presolve-time T-lemmas arrive. If\n\
389 non-clausal simplification and static learning are off\n\
390 (--simplification=none --no-static-learning), the output\n\
391 will closely resemble the input (with term-level ITEs removed).\n\
392 \n\
393 learned\n\
394 + Output the assertions after non-clausal simplification, static\n\
395 learning, and presolve-time T-lemmas. This should include all eager\n\
396 T-lemmas (in the form provided by the theory, which my or may not be\n\
397 clausal). Also includes level-0 BCP done by Minisat.\n\
398 \n\
399 clauses\n\
400 + Do all the preprocessing outlined above, and dump the CNF-converted\n\
401 output\n\
402 \n\
403 state\n\
404 + Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
405 Implied by all \"stateful\" modes below and conflicts with all\n\
406 non-stateful modes below.\n\
407 \n\
408 t-conflicts [non-stateful]\n\
409 + Output correctness queries for all theory conflicts\n\
410 \n\
411 missed-t-conflicts [stateful]\n\
412 + Output completeness queries for theory conflicts\n\
413 \n\
414 t-propagations [stateful]\n\
415 + Output correctness queries for all theory propagations\n\
416 \n\
417 missed-t-propagations [stateful]\n\
418 + Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
419 \n\
420 t-lemmas [non-stateful]\n\
421 + Output correctness queries for all theory lemmas\n\
422 \n\
423 t-explanations [non-stateful]\n\
424 + Output correctness queries for all theory explanations\n\
425 \n\
426 Dump modes can be combined with multiple uses of --dump. Generally you want\n\
427 one from the assertions category (either asertions, learned, or clauses), and\n\
428 perhaps one or more stateful or non-stateful modes for checking correctness\n\
429 and completeness of decision procedure implementations. Stateful modes dump\n\
430 the contextual assertions made by the core solver (all decisions and\n\
431 propagations as assertions; that affects the validity of the resulting\n\
432 correctness and completeness queries, so of course stateful and non-stateful\n\
433 modes cannot be mixed in the same run.\n\
434 \n\
435 The --output-language option controls the language used for dumping, and\n\
436 this allows you to connect CVC4 to another solver implementation via a UNIX\n\
437 pipe to perform on-line checking. The --dump-to option can be used to dump\n\
438 to a file.\n\
439 ";
440
441 static const string arithUnateLemmasHelp = "\
442 Presolve lemmas are generated before SAT search begins using the relationship\n\
443 of constant terms and polynomials.\n\
444 Modes currently supported by the --unate-lemmas option:\n\
445 + none \n\
446 + ineqs \n\
447 Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
448 + eqs \n\
449 Outputs lemmas of the general forms\n\
450 (= p c) implies (<= p d) for c < d, or\n\
451 (= p c) implies (not (= p d)) for c != d.\n\
452 + all \n\
453 A combination of inequalities and equalities.\n\
454 ";
455
456 static const string propagationModeHelp = "\
457 This decides on kind of propagation arithmetic attempts to do during the search.\n\
458 + none\n\
459 + unate\n\
460 use constraints to do unate propagation\n\
461 + bi (Bounds Inference)\n\
462 infers bounds on basic variables using the upper and lower bounds of the\n\
463 non-basic variables in the tableau.\n\
464 +both\n\
465 ";
466
467 static const string pivotRulesHelp = "\
468 This decides on the rule used by simplex during hueristic rounds\n\
469 for deciding the next basic variable to select.\n\
470 Pivot rules available:\n\
471 +min\n\
472 The minimum abs() value of the variable's violation of its bound. (default)\n\
473 +min-break-ties\n\
474 The minimum violation with ties broken by variable order (total)\n\
475 +max\n\
476 The maximum violation the bound\n\
477 ";
478
479 string Options::getDescription() const {
480 return optionsDescription;
481 }
482
483 void Options::printUsage(const std::string msg, std::ostream& out) {
484 out << msg << optionsDescription << endl << flush;
485 }
486
487 void Options::printShortUsage(const std::string msg, std::ostream& out) {
488 out << msg << mostCommonOptionsDescription << endl
489 << "For full usage, please use --help." << endl << flush;
490 }
491
492 void Options::printLanguageHelp(std::ostream& out) {
493 out << languageDescription << flush;
494 }
495
496 /**
497 * For the main getopt() routine, we need ways to switch on long
498 * options without clashing with short option characters. This is an
499 * enum of those long options. For long options (e.g. "--verbose")
500 * with a short option equivalent ("-v"), we use the single-letter
501 * short option; therefore, this enumeration starts at 256 to avoid
502 * any collision.
503 */
504 enum OptionValue {
505 OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */
506 SMTCOMP,
507 STATS,
508 SEGV_NOSPIN,
509 OUTPUT_LANGUAGE,
510 PARSE_ONLY,
511 PREPROCESS_ONLY,
512 DUMP,
513 DUMP_TO,
514 NO_CHECKING,
515 NO_THEORY_REGISTRATION,
516 USE_MMAP,
517 SHOW_DEBUG_TAGS,
518 SHOW_TRACE_TAGS,
519 SHOW_SAT_SOLVERS,
520 SHOW_CONFIG,
521 STRICT_PARSING,
522 DEFAULT_EXPR_DEPTH,
523 DEFAULT_DAG_THRESH,
524 PRINT_EXPR_TYPES,
525 UF_THEORY,
526 LAZY_DEFINITION_EXPANSION,
527 SIMPLIFICATION_MODE,
528 DECISION_MODE,
529 DECISION_BUDGET,
530 NO_STATIC_LEARNING,
531 ITE_SIMP,
532 NO_ITE_SIMP,
533 UNCONSTRAINED_SIMP,
534 NO_UNCONSTRAINED_SIMP,
535 REPEAT_SIMP,
536 NO_REPEAT_SIMP,
537 INTERACTIVE,
538 NO_INTERACTIVE,
539 PRODUCE_ASSIGNMENTS,
540 PRINT_SUCCESS,
541 SMTLIB2,
542 PROOF,
543 NO_TYPE_CHECKING,
544 LAZY_TYPE_CHECKING,
545 EAGER_TYPE_CHECKING,
546 REPLAY,
547 REPLAY_LOG,
548 PRINT_WINNER,
549 RANDOM_FREQUENCY,
550 RANDOM_SEED,
551 SAT_RESTART_FIRST,
552 SAT_RESTART_INC,
553 ARITHMETIC_UNATE_LEMMA_MODE,
554 ARITHMETIC_PROPAGATION_MODE,
555 ARITHMETIC_HEURISTIC_PIVOTS,
556 ARITHMETIC_VAR_ORDER_PIVOTS,
557 ARITHMETIC_PIVOT_RULE,
558 ARITHMETIC_CHECK_PERIOD,
559 ARITHMETIC_PIVOT_THRESHOLD,
560 ARITHMETIC_PROP_MAX_LENGTH,
561 ARITHMETIC_DIO_SOLVER,
562 ENABLE_ARITHMETIC_REWRITE_EQUALITIES,
563 DISABLE_ARITHMETIC_REWRITE_EQUALITIES,
564 ENABLE_SYMMETRY_BREAKER,
565 DISABLE_SYMMETRY_BREAKER,
566 DISABLE_MINISCOPE_QUANT,
567 DISABLE_MINISCOPE_QUANT_FV,
568 DISABLE_PRENEX_QUANT,
569 VAR_ELIM_QUANT,
570 CNF_QUANT,
571 PRE_SKOLEM_QUANT,
572 DISABLE_SMART_TRIGGERS,
573 REGISTER_QUANT_BODY_TERMS,
574 INST_WHEN,
575 EAGER_INST_QUANT,
576 FINITE_MODEL_FIND,
577 FMF_REGION_SAT,
578 DISABLE_FMF_MODEL_BASED_INST,
579 EFFICIENT_E_MATCHING,
580 LITERAL_MATCHING,
581 ENABLE_CBQI,
582 DISABLE_CBQI,
583 IGNORE_USER_PATTERNS,
584 ENABLE_FLIP_DECISION,
585 PARALLEL_THREADS,
586 PARALLEL_SEPARATE_OUTPUT,
587 PORTFOLIO_FILTER_LENGTH,
588 TIME_LIMIT,
589 TIME_LIMIT_PER,
590 RESOURCE_LIMIT,
591 RESOURCE_LIMIT_PER,
592 BITVECTOR_EAGER_BITBLAST,
593 BITVECTOR_SHARE_LEMMAS,
594 BITVECTOR_EAGER_FULLCHECK,
595 SAT_REFINE_CONFLICTS,
596 THEORYOF_MODE,
597 OPTION_VALUE_END
598 };/* enum OptionValue */
599
600 /**
601 * This is a table of long options. By policy, each short option
602 * should have an equivalent long option (but the reverse isn't the
603 * case), so this table should thus contain all command-line options.
604 *
605 * Each option in this array has four elements:
606 *
607 * 1. the long option string
608 * 2. argument behavior for the option:
609 * no_argument - no argument permitted
610 * required_argument - an argument is expected
611 * optional_argument - an argument is permitted but not required
612 * 3. this is a pointer to an int which is set to the 4th entry of the
613 * array if the option is present; or NULL, in which case
614 * getopt_long() returns the 4th entry
615 * 4. the return value for getopt_long() when this long option (or the
616 * value to set the 3rd entry to; see #3)
617 *
618 * If you add something here, you should add it in src/main/usage.h
619 * also, to document it.
620 *
621 * If you add something that has a short option equivalent, you should
622 * add it to the getopt_long() call in parseOptions().
623 */
624 static struct option cmdlineOptions[] = {
625 // name, has_arg, *flag, val
626 { "verbose" , no_argument , NULL, 'v' },
627 { "quiet" , no_argument , NULL, 'q' },
628 { "debug" , required_argument, NULL, 'd' },
629 { "trace" , required_argument, NULL, 't' },
630 { "stats" , no_argument , NULL, STATS },
631 { "no-checking", no_argument , NULL, NO_CHECKING },
632 { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
633 { "show-debug-tags", no_argument , NULL, SHOW_DEBUG_TAGS },
634 { "show-trace-tags", no_argument , NULL, SHOW_TRACE_TAGS },
635 { "show-sat-solvers", no_argument , NULL, SHOW_SAT_SOLVERS },
636 { "show-config", no_argument , NULL, SHOW_CONFIG },
637 { "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
638 { "help" , no_argument , NULL, 'h' },
639 { "version" , no_argument , NULL, 'V' },
640 { "about" , no_argument , NULL, 'V' },
641 { "lang" , required_argument, NULL, 'L' },
642 { "output-lang", required_argument, NULL, OUTPUT_LANGUAGE },
643 { "parse-only" , no_argument , NULL, PARSE_ONLY },
644 { "preprocess-only", no_argument , NULL, PREPROCESS_ONLY },
645 { "dump" , required_argument, NULL, DUMP },
646 { "dump-to" , required_argument, NULL, DUMP_TO },
647 { "mmap" , no_argument , NULL, USE_MMAP },
648 { "strict-parsing", no_argument , NULL, STRICT_PARSING },
649 { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
650 { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
651 { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
652 { "uf" , required_argument, NULL, UF_THEORY },
653 { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
654 { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
655 { "decision", required_argument, NULL, DECISION_MODE },
656 { "decision-budget", required_argument, NULL, DECISION_BUDGET },
657 { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
658 { "ite-simp", no_argument, NULL, ITE_SIMP },
659 { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
660 { "unconstrained-simp", no_argument, NULL, UNCONSTRAINED_SIMP },
661 { "no-unconstrained-simp", no_argument, NULL, NO_UNCONSTRAINED_SIMP },
662 { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
663 { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
664 { "interactive", no_argument , NULL, INTERACTIVE },
665 { "no-interactive", no_argument , NULL, NO_INTERACTIVE },
666 { "produce-models", no_argument , NULL, 'm' },
667 { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
668 { "print-success", no_argument, NULL, PRINT_SUCCESS },
669 { "smtlib2", no_argument, NULL, SMTLIB2 },
670 { "proof", no_argument, NULL, PROOF },
671 { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
672 { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
673 { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
674 { "incremental", no_argument , NULL, 'i' },
675 { "replay" , required_argument, NULL, REPLAY },
676 { "replay-log" , required_argument, NULL, REPLAY_LOG },
677 { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY },
678 { "random-seed" , required_argument, NULL, RANDOM_SEED },
679 { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
680 { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
681 { "print-winner", no_argument , NULL, PRINT_WINNER },
682 { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE },
683 { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE },
684 { "heuristic-pivots", required_argument, NULL, ARITHMETIC_HEURISTIC_PIVOTS },
685 { "heuristic-pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE },
686 { "standard-effort-variable-order-pivots", required_argument, NULL, ARITHMETIC_VAR_ORDER_PIVOTS },
687 { "simplex-check-period" , required_argument, NULL, ARITHMETIC_CHECK_PERIOD },
688 { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD },
689 { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH },
690 { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
691 { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES },
692 { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
693 { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER },
694 { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
695 { "disable-miniscope-quant", no_argument, NULL, DISABLE_MINISCOPE_QUANT },
696 { "disable-miniscope-quant-fv", no_argument, NULL, DISABLE_MINISCOPE_QUANT_FV },
697 { "disable-prenex-quant", no_argument, NULL, DISABLE_PRENEX_QUANT },
698 { "var-elim-quant", no_argument, NULL, VAR_ELIM_QUANT },
699 { "cnf-quant", no_argument, NULL, CNF_QUANT },
700 { "pre-skolem-quant", no_argument, NULL, PRE_SKOLEM_QUANT },
701 { "disable-smart-triggers", no_argument, NULL, DISABLE_SMART_TRIGGERS },
702 { "register-quant-body-terms", no_argument, NULL, REGISTER_QUANT_BODY_TERMS },
703 { "inst-when", required_argument, NULL, INST_WHEN },
704 { "eager-inst-quant", no_argument, NULL, EAGER_INST_QUANT },
705 { "finite-model-find", no_argument, NULL, FINITE_MODEL_FIND },
706 { "use-fmf-region-sat", no_argument, NULL, FMF_REGION_SAT },
707 { "disable-fmf-model-inst", no_argument, NULL, DISABLE_FMF_MODEL_BASED_INST },
708 { "efficient-e-matching", no_argument, NULL, EFFICIENT_E_MATCHING },
709 { "literal-matching", required_argument, NULL, LITERAL_MATCHING },
710 { "enable-cbqi", no_argument, NULL, ENABLE_CBQI },
711 { "disable-cbqi", no_argument, NULL, DISABLE_CBQI },
712 { "ignore-user-patterns", no_argument, NULL, IGNORE_USER_PATTERNS },
713 { "enable-flip-decision", no_argument, NULL, ENABLE_FLIP_DECISION },
714 { "threads", required_argument, NULL, PARALLEL_THREADS },
715 { "separate-output", no_argument, NULL, PARALLEL_SEPARATE_OUTPUT },
716 { "filter-lemma-length", required_argument, NULL, PORTFOLIO_FILTER_LENGTH },
717 { "tlimit" , required_argument, NULL, TIME_LIMIT },
718 { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
719 { "rlimit" , required_argument, NULL, RESOURCE_LIMIT },
720 { "rlimit-per" , required_argument, NULL, RESOURCE_LIMIT_PER },
721 { "bitblast-eager", no_argument, NULL, BITVECTOR_EAGER_BITBLAST },
722 { "bitblast-share-lemmas", no_argument, NULL, BITVECTOR_SHARE_LEMMAS },
723 { "bitblast-eager-fullcheck", no_argument, NULL, BITVECTOR_EAGER_FULLCHECK },
724 { "refine-conflicts", no_argument, NULL, SAT_REFINE_CONFLICTS },
725 { "theoryof-mode", required_argument, NULL, THEORYOF_MODE },
726 { NULL , no_argument , NULL, '\0' }
727 };/* if you add things to the above, please remember to update usage.h! */
728
729
730 /** Parse argc/argv and put the result into a CVC4::Options struct. */
731 int Options::parseOptions(int argc, char* argv[])
732 throw(OptionException) {
733 const char *progName = argv[0];
734 int c;
735
736 // Reset getopt(), in the case of multiple calls.
737 // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
738 optind = 0;
739 #if HAVE_DECL_OPTRESET
740 optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
741 #endif /* HAVE_DECL_OPTRESET */
742
743 // find the base name of the program
744 const char *x = strrchr(progName, '/');
745 if(x != NULL) {
746 progName = x + 1;
747 }
748 binary_name = string(progName);
749
750 // The strange string in this call is the short option string. An
751 // initial '+' means that option processing stops as soon as a
752 // non-option argument is encountered (it is not present, by design).
753 // The initial ':' indicates that getopt_long() should return ':'
754 // instead of '?' for a missing option argument. Then, each letter
755 // is a valid short option for getopt_long(), and if it's encountered,
756 // getopt_long() returns that character. A ':' after an option
757 // character means an argument is required; two colons indicates an
758 // argument is optional; no colons indicate an argument is not
759 // permitted. cmdlineOptions specifies all the long-options and the
760 // return value for getopt_long() should they be encountered.
761 while((c = getopt_long(argc, argv,
762 ":himVvqL:d:t:",
763 cmdlineOptions, NULL)) != -1) {
764 switch(c) {
765
766 case 'h':
767 help = true;
768 break;
769
770 case 'V':
771 version = true;
772 break;
773
774 case 'v':
775 ++verbosity;
776 break;
777
778 case 'q':
779 --verbosity;
780 break;
781
782 case 'L':
783 setInputLanguage(optarg);
784 break;
785
786 case OUTPUT_LANGUAGE:
787 setOutputLanguage(optarg);
788 break;
789
790 case 't':
791 if(Configuration::isTracingBuild()) {
792 if(!Configuration::isTraceTag(optarg))
793 throw OptionException(string("trace tag ") + optarg +
794 string(" not available"));
795 } else {
796 throw OptionException("trace tags not available in non-tracing builds");
797 }
798 Trace.on(optarg);
799 break;
800
801 case 'd':
802 if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
803 if(!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg)) {
804 throw OptionException(string("debug tag ") + optarg +
805 string(" not available"));
806 }
807 } else if(! Configuration::isDebugBuild()) {
808 throw OptionException("debug tags not available in non-debug builds");
809 } else {
810 throw OptionException("debug tags not available in non-tracing builds");
811 }
812 Debug.on(optarg);
813 Trace.on(optarg);
814 break;
815
816 case STATS:
817 statistics = true;
818 break;
819
820 case SEGV_NOSPIN:
821 segvNoSpin = true;
822 break;
823
824 case PARSE_ONLY:
825 parseOnly = true;
826 break;
827
828 case PREPROCESS_ONLY:
829 preprocessOnly = true;
830 break;
831
832 case DUMP: {
833 #ifdef CVC4_DUMPING
834 char* tokstr = optarg;
835 char* toksave;
836 while((optarg = strtok_r(tokstr, ",", &toksave)) != NULL) {
837 tokstr = NULL;
838 if(!strcmp(optarg, "benchmark")) {
839 } else if(!strcmp(optarg, "declarations")) {
840 } else if(!strcmp(optarg, "assertions")) {
841 } else if(!strcmp(optarg, "learned")) {
842 } else if(!strcmp(optarg, "clauses")) {
843 } else if(!strcmp(optarg, "t-conflicts") ||
844 !strcmp(optarg, "t-lemmas") ||
845 !strcmp(optarg, "t-explanations") ||
846 !strcmp(optarg, "bv-rewrites") ||
847 !strcmp(optarg, "theory::fullcheck")) {
848 // These are "non-state-dumping" modes. If state (SAT decisions,
849 // propagations, etc.) is dumped, it will interfere with the validity
850 // of these generated queries.
851 if(Dump.isOn("state")) {
852 throw OptionException(string("dump option `") + optarg +
853 "' conflicts with a previous, "
854 "state-dumping dump option. You cannot "
855 "mix stateful and non-stateful dumping modes; "
856 "see --dump help.");
857 } else {
858 Dump.on("no-permit-state");
859 }
860 } else if(!strcmp(optarg, "state") ||
861 !strcmp(optarg, "missed-t-conflicts") ||
862 !strcmp(optarg, "t-propagations") ||
863 !strcmp(optarg, "missed-t-propagations")) {
864 // These are "state-dumping" modes. If state (SAT decisions,
865 // propagations, etc.) is not dumped, it will interfere with the
866 // validity of these generated queries.
867 if(Dump.isOn("no-permit-state")) {
868 throw OptionException(string("dump option `") + optarg +
869 "' conflicts with a previous, "
870 "non-state-dumping dump option. You cannot "
871 "mix stateful and non-stateful dumping modes; "
872 "see --dump help.");
873 } else {
874 Dump.on("state");
875 }
876 } else if(!strcmp(optarg, "help")) {
877 puts(dumpHelp.c_str());
878 exit(1);
879 } else {
880 throw OptionException(string("unknown option for --dump: `") +
881 optarg + "'. Try --dump help.");
882 }
883
884 Dump.on(optarg);
885 Dump.on("benchmark");
886 if(strcmp(optarg, "benchmark")) {
887 Dump.on("declarations");
888 }
889 }
890 #else /* CVC4_DUMPING */
891 throw OptionException("The dumping feature was disabled in this build of CVC4.");
892 #endif /* CVC4_DUMPING */
893 break;
894 }
895
896 case DUMP_TO: {
897 #ifdef CVC4_DUMPING
898 size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
899 if(optarg == NULL || *optarg == '\0') {
900 throw OptionException(string("Bad file name for --dump-to"));
901 } else if(!strcmp(optarg, "-")) {
902 Dump.setStream(DumpOutC::dump_cout);
903 } else {
904 ostream* dumpTo = new ofstream(optarg, ofstream::out | ofstream::trunc);
905 if(!*dumpTo) {
906 throw OptionException(string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
907 }
908 Dump.setStream(*dumpTo);
909 }
910 expr::ExprDag::setDag(Dump.getStream(), dagSetting);
911 #else /* CVC4_DUMPING */
912 throw OptionException("The dumping feature was disabled in this build of CVC4.");
913 #endif /* CVC4_DUMPING */
914 }
915 break;
916
917 case NO_THEORY_REGISTRATION:
918 theoryRegistration = false;
919 break;
920
921 case NO_CHECKING:
922 semanticChecks = false;
923 typeChecking = false;
924 earlyTypeChecking = false;
925 break;
926
927 case USE_MMAP:
928 memoryMap = true;
929 break;
930
931 case PRINT_WINNER:
932 printWinner = true;
933 break;
934
935 case STRICT_PARSING:
936 strictParsing = true;
937 break;
938
939 case DEFAULT_EXPR_DEPTH:
940 {
941 int depth = atoi(optarg);
942 Debug.getStream() << Expr::setdepth(depth);
943 Trace.getStream() << Expr::setdepth(depth);
944 Notice.getStream() << Expr::setdepth(depth);
945 Chat.getStream() << Expr::setdepth(depth);
946 Message.getStream() << Expr::setdepth(depth);
947 Warning.getStream() << Expr::setdepth(depth);
948 }
949 break;
950
951 case DEFAULT_DAG_THRESH:
952 {
953 int dag = atoi(optarg);
954 if(dag < 0) {
955 throw OptionException("--default-dag-thresh requires a nonnegative argument.");
956 }
957 Debug.getStream() << Expr::dag(dag);
958 Trace.getStream() << Expr::dag(dag);
959 Notice.getStream() << Expr::dag(dag);
960 Chat.getStream() << Expr::dag(dag);
961 Message.getStream() << Expr::dag(dag);
962 Warning.getStream() << Expr::dag(dag);
963 Dump.getStream() << Expr::dag(dag);
964 }
965 break;
966
967 case PRINT_EXPR_TYPES:
968 Debug.getStream() << Expr::printtypes(true);
969 Trace.getStream() << Expr::printtypes(true);
970 Notice.getStream() << Expr::printtypes(true);
971 Chat.getStream() << Expr::printtypes(true);
972 Message.getStream() << Expr::printtypes(true);
973 Warning.getStream() << Expr::printtypes(true);
974 break;
975
976 case LAZY_DEFINITION_EXPANSION:
977 lazyDefinitionExpansion = true;
978 break;
979
980 case SIMPLIFICATION_MODE:
981 if(!strcmp(optarg, "batch")) {
982 simplificationMode = SIMPLIFICATION_MODE_BATCH;
983 simplificationModeSetByUser = true;
984 } else if(!strcmp(optarg, "incremental")) {
985 simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL;
986 simplificationModeSetByUser = true;
987 } else if(!strcmp(optarg, "none")) {
988 simplificationMode = SIMPLIFICATION_MODE_NONE;
989 simplificationModeSetByUser = true;
990 } else if(!strcmp(optarg, "help")) {
991 puts(simplificationHelp.c_str());
992 exit(1);
993 } else {
994 throw OptionException(string("unknown option for --simplification: `") +
995 optarg + "'. Try --simplification help.");
996 }
997 break;
998
999 case THEORYOF_MODE:
1000 if (!strcmp(optarg, "type")) {
1001 theoryOfModeSetByUser = true;
1002 theoryOfMode = theory::THEORY_OF_TYPE_BASED;
1003 } else if (!strcmp(optarg, "term")) {
1004 theoryOfModeSetByUser = true;
1005 theoryOfMode = theory::THEORY_OF_TERM_BASED;
1006 } else if (!strcmp(optarg, "help")) {
1007 puts(theoryofHelp.c_str());
1008 exit(1);
1009 } else {
1010 throw OptionException(string("unknown option for --theoryof-mode: `") +
1011 optarg + "'. Try --theoryof-mode help.");
1012 }
1013 break;
1014 case DECISION_MODE:
1015 if(!strcmp(optarg, "internal")) {
1016 decisionMode = DECISION_STRATEGY_INTERNAL;
1017 decisionModeSetByUser = true;
1018 } else if(!strcmp(optarg, "justification")) {
1019 decisionMode = DECISION_STRATEGY_JUSTIFICATION;
1020 decisionModeSetByUser = true;
1021 } else if(!strcmp(optarg, "relevancy")) {
1022 decisionMode = DECISION_STRATEGY_RELEVANCY;
1023 decisionModeSetByUser = true;
1024 decisionOptions.relevancyLeaves = false;
1025 } else if(!strcmp(optarg, "relevancy-leaves")) {
1026 decisionMode = DECISION_STRATEGY_RELEVANCY;
1027 decisionModeSetByUser = true;
1028 decisionOptions.relevancyLeaves = true;
1029 } else if(!strcmp(optarg, "justification-rel")) {
1030 decisionMode = DECISION_STRATEGY_RELEVANCY;
1031 decisionModeSetByUser = true;
1032 // relevancyLeaves : irrelevant
1033 // maxRelTimeAsPermille : irrelevant
1034 decisionOptions.computeRelevancy = false;
1035 decisionOptions.mustRelevancy = false;
1036 } else if(!strcmp(optarg, "justification-must")) {
1037 decisionMode = DECISION_STRATEGY_RELEVANCY;
1038 decisionModeSetByUser = true;
1039 // relevancyLeaves : irrelevant
1040 // maxRelTimeAsPermille : irrelevant
1041 decisionOptions.computeRelevancy = false;
1042 decisionOptions.mustRelevancy = true;
1043 } else if(!strcmp(optarg, "help")) {
1044 puts(decisionHelp.c_str());
1045 exit(1);
1046 } else {
1047 throw OptionException(string("unknown option for --decision: `") +
1048 optarg + "'. Try --decision help.");
1049 }
1050 break;
1051
1052 case DECISION_BUDGET: {
1053 int i = atoi(optarg);
1054 if(i < 0 || i > 1000) {
1055 throw OptionException(string("invalid value for --decision-budget: `") +
1056 optarg + "'. Must be between 0 and 1000.");
1057 }
1058 if(i == 0) {
1059 Warning() << "Decision budget is 0. Consider using internal decision hueristic and "
1060 << std::endl << " removing this option." << std::endl;
1061
1062 }
1063 decisionOptions.maxRelTimeAsPermille = (unsigned short)i;
1064 }
1065 break;
1066
1067 case NO_STATIC_LEARNING:
1068 doStaticLearning = false;
1069 break;
1070
1071 case ITE_SIMP:
1072 doITESimp = true;
1073 doITESimpSetByUser = true;
1074 break;
1075
1076 case NO_ITE_SIMP:
1077 doITESimp = false;
1078 doITESimpSetByUser = true;
1079 break;
1080
1081 case UNCONSTRAINED_SIMP:
1082 unconstrainedSimp = true;
1083 unconstrainedSimpSetByUser = true;
1084 break;
1085
1086 case NO_UNCONSTRAINED_SIMP:
1087 unconstrainedSimp = false;
1088 unconstrainedSimpSetByUser = true;
1089 break;
1090
1091 case REPEAT_SIMP:
1092 repeatSimp = true;
1093 repeatSimpSetByUser = true;
1094 break;
1095
1096 case NO_REPEAT_SIMP:
1097 repeatSimp = false;
1098 repeatSimpSetByUser = true;
1099 break;
1100
1101 case INTERACTIVE:
1102 interactive = true;
1103 interactiveSetByUser = true;
1104 break;
1105
1106 case NO_INTERACTIVE:
1107 interactive = false;
1108 interactiveSetByUser = true;
1109 break;
1110
1111 case 'm':
1112 produceModels = true;
1113 break;
1114
1115 case PRODUCE_ASSIGNMENTS:
1116 produceAssignments = true;
1117 break;
1118
1119 case SMTLIB2: // smtlib v2 compliance mode
1120 inputLanguage = language::input::LANG_SMTLIB_V2;
1121 outputLanguage = language::output::LANG_SMTLIB_V2;
1122 strictParsing = true;
1123 // make sure entire expressions are printed on all the non-debug, non-trace streams
1124 Notice.getStream() << Expr::setdepth(-1);
1125 Chat.getStream() << Expr::setdepth(-1);
1126 Message.getStream() << Expr::setdepth(-1);
1127 Warning.getStream() << Expr::setdepth(-1);
1128 /* intentionally fall through */
1129
1130 case PRINT_SUCCESS:
1131 Debug.getStream() << Command::printsuccess(true);
1132 Trace.getStream() << Command::printsuccess(true);
1133 Notice.getStream() << Command::printsuccess(true);
1134 Chat.getStream() << Command::printsuccess(true);
1135 Message.getStream() << Command::printsuccess(true);
1136 Warning.getStream() << Command::printsuccess(true);
1137 break;
1138
1139 case PROOF:
1140 #ifdef CVC4_PROOF
1141 proof = true;
1142 #else /* CVC4_PROOF */
1143 throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used");
1144 #endif /* CVC4_PROOF */
1145 break;
1146
1147 case NO_TYPE_CHECKING:
1148 typeChecking = false;
1149 earlyTypeChecking = false;
1150 break;
1151
1152 case LAZY_TYPE_CHECKING:
1153 typeChecking = true;
1154 earlyTypeChecking = false;
1155 break;
1156
1157 case EAGER_TYPE_CHECKING:
1158 typeChecking = true;
1159 earlyTypeChecking = true;
1160 break;
1161
1162 case 'i':
1163 incrementalSolving = true;
1164 break;
1165
1166 case REPLAY:
1167 #ifdef CVC4_REPLAY
1168 if(optarg == NULL || *optarg == '\0') {
1169 throw OptionException(string("Bad file name for --replay"));
1170 } else {
1171 replayFilename = optarg;
1172 }
1173 #else /* CVC4_REPLAY */
1174 throw OptionException("The replay feature was disabled in this build of CVC4.");
1175 #endif /* CVC4_REPLAY */
1176 break;
1177
1178 case REPLAY_LOG:
1179 #ifdef CVC4_REPLAY
1180 if(optarg == NULL || *optarg == '\0') {
1181 throw OptionException(string("Bad file name for --replay-log"));
1182 } else if(!strcmp(optarg, "-")) {
1183 replayLog = &cout;
1184 } else {
1185 replayLog = new ofstream(optarg, ofstream::out | ofstream::trunc);
1186 if(!*replayLog) {
1187 throw OptionException(string("Cannot open replay-log file: `") + optarg + "'");
1188 }
1189 }
1190 #else /* CVC4_REPLAY */
1191 throw OptionException("The replay feature was disabled in this build of CVC4.");
1192 #endif /* CVC4_REPLAY */
1193 break;
1194
1195 case ENABLE_SYMMETRY_BREAKER:
1196 ufSymmetryBreaker = true;
1197 ufSymmetryBreakerSetByUser = true;
1198 break;
1199 case DISABLE_SYMMETRY_BREAKER:
1200 ufSymmetryBreaker = false;
1201 ufSymmetryBreakerSetByUser = true;
1202 break;
1203 case DISABLE_MINISCOPE_QUANT:
1204 miniscopeQuant = false;
1205 break;
1206 case DISABLE_MINISCOPE_QUANT_FV:
1207 miniscopeQuantFreeVar = false;
1208 break;
1209 case DISABLE_PRENEX_QUANT:
1210 prenexQuant = false;
1211 break;
1212 case VAR_ELIM_QUANT:
1213 varElimQuant = true;
1214 break;
1215 case CNF_QUANT:
1216 cnfQuant = true;
1217 break;
1218 case PRE_SKOLEM_QUANT:
1219 preSkolemQuant = true;
1220 break;
1221 case DISABLE_SMART_TRIGGERS:
1222 smartTriggers = false;
1223 break;
1224 case REGISTER_QUANT_BODY_TERMS:
1225 registerQuantBodyTerms = true;
1226 break;
1227 case INST_WHEN:
1228 if(!strcmp(optarg, "pre-full")) {
1229 instWhenMode = INST_WHEN_PRE_FULL;
1230 } else if(!strcmp(optarg, "full")) {
1231 instWhenMode = INST_WHEN_FULL;
1232 } else if(!strcmp(optarg, "full-last-call")) {
1233 instWhenMode = INST_WHEN_FULL_LAST_CALL;
1234 } else if(!strcmp(optarg, "last-call")) {
1235 instWhenMode = INST_WHEN_LAST_CALL;
1236 } else if(!strcmp(optarg, "help")) {
1237 //puts(instWhenHelp.c_str());
1238 exit(1);
1239 } else {
1240 throw OptionException(string("unknown option for --inst-when: `") +
1241 optarg + "'. Try --inst-when help.");
1242 }
1243 break;
1244 case EAGER_INST_QUANT:
1245 eagerInstQuant = true;
1246 break;
1247 case FINITE_MODEL_FIND:
1248 finiteModelFind = true;
1249 break;
1250 case FMF_REGION_SAT:
1251 fmfRegionSat = true;
1252 break;
1253 case DISABLE_FMF_MODEL_BASED_INST:
1254 fmfModelBasedInst = false;
1255 break;
1256 case EFFICIENT_E_MATCHING:
1257 efficientEMatching = true;
1258 break;
1259 case LITERAL_MATCHING:
1260 if(!strcmp(optarg, "none")) {
1261 literalMatchMode = LITERAL_MATCH_NONE;
1262 } else if(!strcmp(optarg, "predicate")) {
1263 literalMatchMode = LITERAL_MATCH_PREDICATE;
1264 } else if(!strcmp(optarg, "equality")) {
1265 literalMatchMode = LITERAL_MATCH_EQUALITY;
1266 } else if(!strcmp(optarg, "help")) {
1267 //puts(literalMatchHelp.c_str());
1268 exit(1);
1269 } else {
1270 throw OptionException(string("unknown option for --literal-matching: `") +
1271 optarg + "'. Try --literal-matching help.");
1272 }
1273 break;
1274 case ENABLE_CBQI:
1275 cbqi = true;
1276 cbqiSetByUser = true;
1277 break;
1278 case DISABLE_CBQI:
1279 cbqi = false;
1280 cbqiSetByUser = true;
1281 break;
1282 case IGNORE_USER_PATTERNS:
1283 userPatternsQuant = false;
1284 break;
1285 case ENABLE_FLIP_DECISION:
1286 flipDecision = true;
1287 break;
1288 case TIME_LIMIT:
1289 {
1290 int i = atoi(optarg);
1291 if(i < 0) {
1292 throw OptionException("--time-limit requires a nonnegative argument.");
1293 }
1294 cumulativeMillisecondLimit = (unsigned long) i;
1295 }
1296 break;
1297 case TIME_LIMIT_PER:
1298 {
1299 int i = atoi(optarg);
1300 if(i < 0) {
1301 throw OptionException("--time-limit-per requires a nonnegative argument.");
1302 }
1303 perCallMillisecondLimit = (unsigned long) i;
1304 }
1305 break;
1306 case RESOURCE_LIMIT:
1307 {
1308 int i = atoi(optarg);
1309 if(i < 0) {
1310 throw OptionException("--limit requires a nonnegative argument.");
1311 }
1312 cumulativeResourceLimit = (unsigned long) i;
1313 }
1314 break;
1315 case RESOURCE_LIMIT_PER:
1316 {
1317 int i = atoi(optarg);
1318 if(i < 0) {
1319 throw OptionException("--limit-per requires a nonnegative argument.");
1320 }
1321 perCallResourceLimit = (unsigned long) i;
1322 break;
1323 }
1324 case BITVECTOR_EAGER_BITBLAST:
1325 {
1326 bitvectorEagerBitblast = true;
1327 break;
1328 }
1329 case BITVECTOR_EAGER_FULLCHECK:
1330 {
1331 bitvectorEagerFullcheck = true;
1332 break;
1333 }
1334 case BITVECTOR_SHARE_LEMMAS:
1335 {
1336 bitvectorShareLemmas = true;
1337 break;
1338 }
1339 case SAT_REFINE_CONFLICTS:
1340 {
1341 sat_refine_conflicts = true;
1342 break;
1343 }
1344 case RANDOM_SEED:
1345 satRandomSeed = atof(optarg);
1346 break;
1347
1348 case RANDOM_FREQUENCY:
1349 satRandomFreq = atof(optarg);
1350 if(! (0.0 <= satRandomFreq && satRandomFreq <= 1.0)){
1351 throw OptionException(string("--random-freq: `") +
1352 optarg + "' is not between 0.0 and 1.0.");
1353 }
1354 break;
1355
1356 case SAT_RESTART_FIRST:
1357 {
1358 int i = atoi(optarg);
1359 if(i < 1) {
1360 throw OptionException("--restart-int-base requires a number bigger than 1");
1361 }
1362 satRestartFirst = i;
1363 break;
1364 }
1365
1366 case SAT_RESTART_INC:
1367 {
1368 int i = atoi(optarg);
1369 if(i < 1) {
1370 throw OptionException("--restart-int-inc requires a number bigger than 1.0");
1371 }
1372 satRestartInc = i;
1373 }
1374 break;
1375
1376 case ARITHMETIC_UNATE_LEMMA_MODE:
1377 if(!strcmp(optarg, "all")) {
1378 arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS;
1379 break;
1380 } else if(!strcmp(optarg, "none")) {
1381 arithUnateLemmaMode = NO_PRESOLVE_LEMMAS;
1382 break;
1383 } else if(!strcmp(optarg, "ineqs")) {
1384 arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS;
1385 break;
1386 } else if(!strcmp(optarg, "eqs")) {
1387 arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS;
1388 break;
1389 } else if(!strcmp(optarg, "help")) {
1390 puts(arithUnateLemmasHelp.c_str());
1391 exit(1);
1392 } else {
1393 throw OptionException(string("unknown option for --unate-lemmas: `") +
1394 optarg + "'. Try --unate-lemmas=help.");
1395 }
1396 break;
1397
1398 case ARITHMETIC_PROPAGATION_MODE:
1399 if(!strcmp(optarg, "none")) {
1400 arithPropagationMode = NO_PROP;
1401 break;
1402 } else if(!strcmp(optarg, "unate")) {
1403 arithPropagationMode = UNATE_PROP;
1404 break;
1405 } else if(!strcmp(optarg, "bi")) {
1406 arithPropagationMode = BOUND_INFERENCE_PROP;
1407 break;
1408 } else if(!strcmp(optarg, "both")) {
1409 arithPropagationMode = BOTH_PROP;
1410 break;
1411 } else if(!strcmp(optarg, "help")) {
1412 puts(propagationModeHelp.c_str());
1413 exit(1);
1414 } else {
1415 throw OptionException(string("unknown option for --arith-prop: `") +
1416 optarg + "'. Try --arith-prop help.");
1417 }
1418 break;
1419
1420 case ARITHMETIC_HEURISTIC_PIVOTS:
1421 arithHeuristicPivots = atoi(optarg);
1422 arithHeuristicPivotsSetByUser = true;
1423 break;
1424
1425 case ARITHMETIC_VAR_ORDER_PIVOTS:
1426 arithStandardCheckVarOrderPivots = atoi(optarg);
1427 arithStandardCheckVarOrderPivotsSetByUser = true;
1428 break;
1429
1430 case ARITHMETIC_PIVOT_RULE:
1431 if(!strcmp(optarg, "min")) {
1432 arithHeuristicPivotRule = MINIMUM;
1433 break;
1434 } else if(!strcmp(optarg, "min-break-ties")) {
1435 arithHeuristicPivotRule = BREAK_TIES;
1436 break;
1437 } else if(!strcmp(optarg, "max")) {
1438 arithHeuristicPivotRule = MAXIMUM;
1439 break;
1440 } else if(!strcmp(optarg, "help")) {
1441 puts(pivotRulesHelp.c_str());
1442 exit(1);
1443 } else {
1444 throw OptionException(string("unknown option for --heuristic-pivot-rule: `") +
1445 optarg + "'. Try --heuristic-pivot-rule help.");
1446 }
1447 break;
1448
1449 case ARITHMETIC_CHECK_PERIOD:
1450 arithSimplexCheckPeriod = atoi(optarg);
1451 break;
1452
1453 case ARITHMETIC_PIVOT_THRESHOLD:
1454 arithPivotThreshold = atoi(optarg);
1455 arithPivotThresholdSetByUser = true;
1456 break;
1457
1458 case ARITHMETIC_PROP_MAX_LENGTH:
1459 arithPropagateMaxLength = atoi(optarg);
1460 break;
1461
1462 case ARITHMETIC_DIO_SOLVER:
1463 arithDioSolver = false;
1464 break;
1465
1466 case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
1467 arithRewriteEq = true;
1468 arithRewriteEqSetByUser = true;
1469 break;
1470
1471 case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
1472 arithRewriteEq = false;
1473 arithRewriteEqSetByUser = true;
1474 break;
1475
1476 case SHOW_DEBUG_TAGS:
1477 if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
1478 printf("available tags:");
1479 unsigned ntags = Configuration::getNumDebugTags();
1480 char const* const* tags = Configuration::getDebugTags();
1481 for(unsigned i = 0; i < ntags; ++ i) {
1482 printf(" %s", tags[i]);
1483 }
1484 printf("\n");
1485 } else if(! Configuration::isDebugBuild()) {
1486 throw OptionException("debug tags not available in non-debug builds");
1487 } else {
1488 throw OptionException("debug tags not available in non-tracing builds");
1489 }
1490 exit(0);
1491 break;
1492
1493 case SHOW_TRACE_TAGS:
1494 if(Configuration::isTracingBuild()) {
1495 printf("available tags:");
1496 unsigned ntags = Configuration::getNumTraceTags();
1497 char const* const* tags = Configuration::getTraceTags();
1498 for (unsigned i = 0; i < ntags; ++ i) {
1499 printf(" %s", tags[i]);
1500 }
1501 printf("\n");
1502 } else {
1503 throw OptionException("trace tags not available in non-tracing builds");
1504 }
1505 exit(0);
1506 break;
1507
1508 case SHOW_SAT_SOLVERS:
1509 {
1510 vector<string> solvers;
1511 prop::SatSolverFactory::getSolverIds(solvers);
1512 printf("Available SAT solvers: ");
1513 for (unsigned i = 0; i < solvers.size(); ++ i) {
1514 if (i > 0) {
1515 printf(", ");
1516 }
1517 printf("%s", solvers[i].c_str());
1518 }
1519 printf("\n");
1520 exit(0);
1521 break;
1522 }
1523 case SHOW_CONFIG:
1524 fputs(Configuration::about().c_str(), stdout);
1525 printf("\n");
1526 printf("version : %s\n", Configuration::getVersionString().c_str());
1527 if(Configuration::isSubversionBuild()) {
1528 printf("subversion : yes [%s r%u%s]\n",
1529 Configuration::getSubversionBranchName(),
1530 Configuration::getSubversionRevision(),
1531 Configuration::hasSubversionModifications() ?
1532 " (with modifications)" : "");
1533 } else {
1534 printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
1535 }
1536 printf("\n");
1537 printf("library : %u.%u.%u\n",
1538 Configuration::getVersionMajor(),
1539 Configuration::getVersionMinor(),
1540 Configuration::getVersionRelease());
1541 printf("\n");
1542 printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
1543 printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
1544 printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
1545 printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
1546 printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
1547 printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
1548 printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
1549 printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no");
1550 printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
1551 printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
1552 printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
1553 printf("\n");
1554 printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
1555 printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
1556 printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
1557 printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
1558 exit(0);
1559
1560 case PARALLEL_THREADS:
1561 threads = atoi(optarg);
1562 break;
1563
1564 case PARALLEL_SEPARATE_OUTPUT:
1565 separateOutput = true;
1566 break;
1567
1568 case PORTFOLIO_FILTER_LENGTH:
1569 sharingFilterByLength = atoi(optarg);
1570 break;
1571
1572 case ':':
1573 // This can be a long or short option, and the way to get at the name of it is different.
1574 if(optopt == 0 || // was a long option
1575 (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option
1576 throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
1577 } else { // was a short option
1578 throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
1579 }
1580
1581 case '?':
1582 default:
1583 if(optopt == 0 &&
1584 !strncmp(argv[optind - 1], "--thread", 8) &&
1585 strlen(argv[optind - 1]) > 8 &&
1586 isdigit(argv[optind - 1][8])) {
1587 int tnum = atoi(argv[optind - 1] + 8);
1588 threadArgv.resize(tnum + 1);
1589 if(threadArgv[tnum] != "") {
1590 threadArgv[tnum] += " ";
1591 }
1592 const char* p = strchr(argv[optind - 1] + 9, '=');
1593 if(p == NULL) { // e.g., we have --thread0 "foo"
1594 threadArgv[tnum] += argv[optind++];
1595 } else { // e.g., we have --thread0="foo"
1596 threadArgv[tnum] += p + 1;
1597 }
1598 break;
1599 }
1600
1601 // This can be a long or short option, and the way to get at the name of it is different.
1602 if(optopt == 0) { // was a long option
1603 throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
1604 } else { // was a short option
1605 throw OptionException(string("can't understand option `-") + char(optopt) + "'");
1606 }
1607 }
1608 }
1609
1610 if(incrementalSolving && proof) {
1611 throw OptionException(string("The use of --incremental with --proof is not yet supported"));
1612 }
1613
1614 return optind;
1615 }
1616
1617 void Options::setOutputLanguage(const char* str) throw(OptionException) {
1618 if(!strcmp(str, "cvc4") || !strcmp(str, "pl")) {
1619 outputLanguage = language::output::LANG_CVC4;
1620 return;
1621 } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
1622 outputLanguage = language::output::LANG_SMTLIB;
1623 return;
1624 } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
1625 outputLanguage = language::output::LANG_SMTLIB_V2;
1626 return;
1627 } else if(!strcmp(str, "ast")) {
1628 outputLanguage = language::output::LANG_AST;
1629 return;
1630 } else if(!strcmp(str, "auto")) {
1631 outputLanguage = language::output::LANG_AUTO;
1632 return;
1633 }
1634
1635 if(strcmp(str, "help")) {
1636 throw OptionException(string("unknown language for --output-lang: `") +
1637 str + "'. Try --output-lang help.");
1638 }
1639
1640 languageHelp = true;
1641 }
1642
1643 void Options::setInputLanguage(const char* str) throw(OptionException) {
1644 if(!strcmp(str, "cvc4") || !strcmp(str, "pl") || !strcmp(str, "presentation")) {
1645 inputLanguage = language::input::LANG_CVC4;
1646 return;
1647 } else if(!strcmp(str, "smtlib") || !strcmp(str, "smt")) {
1648 inputLanguage = language::input::LANG_SMTLIB;
1649 return;
1650 } else if(!strcmp(str, "smtlib2") || !strcmp(str, "smt2")) {
1651 inputLanguage = language::input::LANG_SMTLIB_V2;
1652 return;
1653 } else if(!strcmp(str, "auto")) {
1654 inputLanguage = language::input::LANG_AUTO;
1655 return;
1656 }
1657
1658 if(strcmp(str, "help")) {
1659 throw OptionException(string("unknown language for --lang: `") +
1660 str + "'. Try --lang help.");
1661 }
1662
1663 languageHelp = true;
1664 }
1665
1666 std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) {
1667 switch(rule) {
1668 case Options::MINIMUM:
1669 out << "MINIMUM";
1670 break;
1671 case Options::BREAK_TIES:
1672 out << "BREAK_TIES";
1673 break;
1674 case Options::MAXIMUM:
1675 out << "MAXIMUM";
1676 break;
1677 default:
1678 out << "ArithPivotRule!UNKNOWN";
1679 }
1680
1681 return out;
1682 }
1683
1684 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
1685 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
1686
1687 }/* CVC4 namespace */