blob: 0fa799df2f9733db998c5310729bdd513fd210d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#
module DRIVER "options/main_options.h" Driver
common-option version -V --version/ bool
identify this CVC4 binary
undocumented-alias --license = --version
common-option help -h --help/ bool
full command line reference
common-option - --show-config void :handler showConfiguration
show CVC4 static configuration
option - --show-debug-tags void :handler showDebugTags
show all available tags for debugging
option - --show-trace-tags void :handler showTraceTags
show all available tags for tracing
expert-option earlyExit --early-exit bool :default true
do not run destructors at exit; default on except in debug builds
# portfolio options
option threads --threads=N unsigned :default 2 :predicate unsignedGreater0
Total number of threads for portfolio
option - --threadN=string void :handler threadN
configures portfolio thread N (0..#threads-1)
option threadStackSize --thread-stack=N unsigned :default 0
stack size for worker threads in MB (0 means use Boost/thread lib default)
option threadArgv std::vector<std::string> :include <vector> <string>
Thread configuration (a string to be passed to parseOptions)
option thread_id int :default -1
Thread ID, for internal use in case of multi-threaded run
option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
don't share (among portfolio threads) lemmas strictly longer than N
option fallbackSequential --fallback-sequential bool :default false
Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode
option incrementalParallel --incremental-parallel bool :default false :link --incremental :link-smt incremental
Use parallel solver even in incremental mode (may print 'unknown's at times)
option interactive : --interactive bool :read-write
force interactive/non-interactive mode
undocumented-option interactivePrompt --interactive-prompt bool :default true
interactive prompting while in interactive mode
# error behaviors (--immediate-exit is default in cases we support, thus no options)
option continuedExecution --continued-execution/ bool :default false :link "--interactive --no-interactive-prompt"/ :link-smt interactive :link-smt interactivePrompt \"false\"
continue executing commands, even on error
option segvSpin --segv-spin bool :default false
spin on segfault/other crash waiting for gdb
undocumented-alias --segv-nospin = --no-segv-spin
expert-option tearDownIncremental : --tear-down-incremental=N int :default 0
implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries
expert-option waitToJoin --wait-to-join bool :default true
wait for other threads to join before quitting
endmodule
|
