src/options/main_options

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