diff options
Diffstat (limited to 'src/options/main_options')
| -rw-r--r-- | src/options/main_options | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/src/options/main_options b/src/options/main_options new file mode 100644 index 000000000..b468c9284 --- /dev/null +++ b/src/options/main_options @@ -0,0 +1,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 CVC4::options::showConfiguration :handler-include "options/options_handler_interface.h" + show CVC4 static configuration + +option - --show-debug-tags void :handler CVC4::options::showDebugTags :handler-include "options/options_handler_interface.h" + show all available tags for debugging +option - --show-trace-tags void :handler CVC4::options::showTraceTags :handler-include "options/options_handler_interface.h" + 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 options::greater(0) + Total number of threads for portfolio +option - --threadN=string void :handler CVC4::options::threadN :handler-include "options/options_handler_interface.h" + 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 + 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 /--no-interactive-prompt bool :default true + turn off 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"/ + 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 bool :default false + implement PUSH/POP/multi-query by destroying and recreating SmtEngine + +expert-option waitToJoin --wait-to-join bool :default true + wait for other threads to join before quitting + +endmodule |