diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/cvc4.1_template.in (renamed from doc/cvc4.1.in) | 89 |
1 files changed, 4 insertions, 85 deletions
diff --git a/doc/cvc4.1.in b/doc/cvc4.1_template.in index 6c6a9768c..23eff6110 100644 --- a/doc/cvc4.1.in +++ b/doc/cvc4.1_template.in @@ -44,91 +44,10 @@ is unspecified and .B CVC4 is connected to a terminal, interactive mode is assumed. -.SH OPTIONS -.IP "\-\-lang=LANG | \-L LANG" -force input language (default is \(lqauto\(rq; see \-\-lang help) -.IP \-\-output\-lang=LANG -force output language (default is \(lqauto\(rq; see \-\-output\-lang help) -.IP "\-\-version | \-V" -identify this CVC4 binary -.IP "\-\-help | \-h" -this command line reference -.IP \-\-parse\-only -exit after parsing input -.IP \-\-preprocess\-only -exit after preprocessing (useful with \-\-stats or \-\-dump) -.IP \-\-dump=MODE -dump preprocessed assertions, T\-propagations, etc., see \-\-dump=help -.IP \-\-dump\-to=FILE -all dumping goes to FILE (instead of stdout) -.IP \-\-mmap -memory map file input -.IP \-\-show\-config -show CVC4 static configuration -.IP \-\-segv\-nospin -don't spin on segfault waiting for gdb -.IP \-\-lazy\-type\-checking -type check expressions only when necessary (default) -.IP \-\-eager\-type\-checking -type check expressions immediately on creation (debug builds only) -.IP \-\-no\-type\-checking -never type check expressions -.IP \-\-no\-checking -disable ALL semantic checks, including type checks -.IP \-\-no\-theory\-registration -disable theory reg (not safe for some theories) -.IP \-\-strict\-parsing -fail on non\-conformant inputs (SMT2 only) -.IP "\-\-verbose | \-v" -increase verbosity (may be repeated) -.IP "\-\-quiet | \-q" -decrease verbosity (may be repeated) -.IP "\-\-trace=FLAG | \-t FLAG" -trace something (e.g. \-t pushpop), can repeat -.IP "\-\-debug=FLAG | \-d FLAG" -debug something (e.g. \-d arith), can repeat -.IP \-\-stats -give statistics on exit -.IP \-\-default\-expr\-depth=N -print exprs to depth N (0 == default, \-1 == no limit) -.IP \-\-print\-expr\-types -print types with variables when printing exprs -.IP \-\-interactive -run interactively -.IP \-\-no\-interactive -do not run interactively -.IP \-\-produce\-models -support the get\-value command -.IP \-\-produce\-assignments -support the get\-assignment command -.IP \-\-lazy\-definition\-expansion -expand define\-fun lazily -.IP \-\-simplification=MODE -choose simplification mode, see \-\-simplification=help -.IP \-\-no\-static\-learning -turn off static learning (e.g. diamond\-breaking) -.IP \-\-replay=file -replay decisions from file -.IP \-\-replay\-log=file -log decisions and propagations to file -.IP \-\-pivot\-rule=RULE -change the pivot rule (see \-\-pivot\-rule help) -.IP \-\-pivot\-threshold=N -sets the number of heuristic pivots per variable per simplex instance -.IP \-\-prop\-row\-length=N -sets the maximum row length to be used in propagation -.IP \-\-random\-freq=P -sets the frequency of random decisions in the sat solver(P=0.0 by default) -.IP \-\-random\-seed=S -sets the random seed for the sat solver -.IP \-\-disable\-variable\-removal -enable permanent removal of variables in arithmetic (UNSAFE! experts only) -.IP \-\-disable\-arithmetic\-propagation -turns on arithmetic propagation -.IP \-\-disable\-symmetry\-breaker -turns off UF symmetry breaker (Deharbe et al., CADE 2011) -.IP \-\-incremental -enable incremental solving +.SH COMMON OPTIONS +${common_manpage_documentation} + +${remaining_manpage_documentation} .\".SH FILES .\".SH ENVIRONMENT |