diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 54 | ||||
-rw-r--r-- | src/util/options.h | 8 |
2 files changed, 41 insertions, 21 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index 3b7b7b08c..7decc693b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -99,39 +99,50 @@ Options::Options() : { } -static const string optionsDescription = "\ - --lang | -L force input language (default is `auto'; see --lang help)\n\ - --output-lang force output language (default is `auto'; see --lang help)\n\ +static const string mostCommonOptionsDescription = "\ +Most commonly-used CVC4 options:\n\ --version | -V identify this CVC4 binary\n\ --help | -h this command line reference\n\ + --lang | -L force input language (default is `auto'; see --lang help)\n\ + --output-lang force output language (default is `auto'; see --lang help)\n\ + --verbose | -v increase verbosity (may be repeated)\n\ + --quiet | -q decrease verbosity (may be repeated)\n\ + --stats give statistics on exit\n\ --parse-only exit after parsing input\n\ - --preprocess-only exit after preprocessing (useful with --stats or --dump)\n\ - --dump=MODE dump preprocessed assertions, T-propagations, etc., see --dump=help\n\ + --preprocess-only exit after preproc (useful with --stats or --dump)\n\ + --dump=MODE dump preprocessed assertions, etc., see --dump=help\n\ --dump-to=FILE all dumping goes to FILE (instead of stdout)\n\ - --mmap memory map file input\n\ --show-config show CVC4 static configuration\n\ + --strict-parsing be less tolerant of non-conforming inputs\n\ + --interactive force interactive mode\n\ + --no-interactive force non-interactive mode\n\ + --produce-models | -m support the get-value command\n\ + --produce-assignments support the get-assignment command\n\ + --proof turn on proof generation\n\ + --incremental | -i enable incremental solving\n\ + --tlimit=MS enable time limiting (give milliseconds)\n\ + --tlimit-per=MS enable time limiting per query (give milliseconds)\n\ + --rlimit=N enable resource limiting\n\ + --rlimit-per=N enable resource limiting per query\n\ +"; + +static const string optionsDescription = mostCommonOptionsDescription + "\ +\n\ +Additional CVC4 options:\n\ + --mmap memory map file input\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ --lazy-type-checking type check expressions only when necessary (default)\n\ --eager-type-checking type check expressions immediately on creation (debug builds only)\n\ --no-type-checking never type check expressions\n\ --no-checking disable ALL semantic checks, including type checks\n\ --no-theory-registration disable theory reg (not safe for some theories)\n\ - --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ - --verbose | -v increase verbosity (may be repeated)\n\ - --quiet | -q decrease verbosity (may be repeated)\n\ --trace | -t trace something (e.g. -t pushpop), can repeat\n\ --debug | -d debug something (e.g. -d arith), can repeat\n\ --show-debug-tags show all avalable tags for debugging\n\ --show-trace-tags show all avalable tags for tracing\n\ - --stats give statistics on exit\n\ --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ --print-expr-types print types with variables when printing exprs\n\ - --interactive run interactively\n\ - --no-interactive do not run interactively\n\ - --produce-models | -m support the get-value command\n\ - --produce-assignments support the get-assignment command\n\ - --proof turn proof generation on\n\ - --lazy-definition-expansion expand define-fun lazily\n\ + --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --replay=file replay decisions from file\n\ @@ -144,11 +155,7 @@ static const string optionsDescription = "\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\ - --incremental | -i enable incremental solving\n\ - --tlimit=MS enable time limiting (give milliseconds)\n\ - --tlimit-per=MS enable time limiting per query (give milliseconds)\n\ - --rlimit=N enable resource limiting\n\ - --rlimit-per=N enable resource limiting per query\n"; +"; #warning "Change CL options as --disable-variable-removal cannot do anything currently." @@ -257,6 +264,11 @@ void Options::printUsage(const std::string msg, std::ostream& out) { out << msg << optionsDescription << endl << flush; } +void Options::printShortUsage(const std::string msg, std::ostream& out) { + out << msg << mostCommonOptionsDescription << endl + << "For full usage, please use --help." << endl << flush; +} + void Options::printLanguageHelp(std::ostream& out) { out << languageDescription << flush; } diff --git a/src/util/options.h b/src/util/options.h index 699895c47..1e392e87d 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -223,6 +223,14 @@ struct CVC4_PUBLIC Options { */ static void printUsage(const std::string msg, std::ostream& out); + /** + * Print command-line option usage message for only the most-commonly + * used options. The message is prefixed by "msg"---which could be + * an error message causing the usage output in the first place, e.g. + * "no such option --foo" + */ + static void printShortUsage(const std::string msg, std::ostream& out); + /** Print help for the --lang command line option */ static void printLanguageHelp(std::ostream& out); |