From b5fd5b61a9f0f993703497fb1c8d678cf2d8bb01 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 2 Nov 2011 13:55:48 +0000 Subject: [PATCH] Only print a shortlist of most-commonly-used options on option processing errors; reduces clutter, increases usability --- src/main/main.cpp | 33 +++++++++++---------------- src/util/options.cpp | 54 +++++++++++++++++++++++++++----------------- src/util/options.h | 8 +++++++ 3 files changed, 54 insertions(+), 41 deletions(-) diff --git a/src/main/main.cpp b/src/main/main.cpp index ec0a00ff8..ba5d06672 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -46,9 +46,9 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -int runCvc4(int argc, char* argv[]); -void doCommand(SmtEngine&, Command*); -void printUsage(); +static int runCvc4(int argc, char* argv[]); +static void doCommand(SmtEngine&, Command*); +static void printUsage(bool full = false); namespace CVC4 { namespace main { @@ -66,24 +66,17 @@ namespace CVC4 { } } - -// no more % chars in here without being escaped; it's used as a -// printf() format string -const string usageMessage = "\ -usage: %s [options] [input-file]\n\ -\n\ -Without an input file, or with `-', CVC4 reads from standard input.\n\ -\n\ -CVC4 options:\n"; - -void printUsage() { +static void printUsage(bool full) { stringstream ss; ss << "usage: " << options.binary_name << " [options] [input-file]" << endl << endl << "Without an input file, or with `-', CVC4 reads from standard input." << endl - << endl - << "CVC4 options:" << endl; - Options::printUsage( ss.str(), *options.out ); + << endl; + if(full) { + Options::printUsage( ss.str(), *options.out ); + } else { + Options::printShortUsage( ss.str(), *options.out ); + } } /** @@ -131,7 +124,7 @@ int main(int argc, char* argv[]) { } -int runCvc4(int argc, char* argv[]) { +static int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers cvc4_init(); @@ -144,7 +137,7 @@ int runCvc4(int argc, char* argv[]) { progName = options.binary_name.c_str(); if( options.help ) { - printUsage(); + printUsage(true); exit(1); } else if( options.languageHelp ) { Options::printLanguageHelp(*options.out); @@ -357,7 +350,7 @@ int runCvc4(int argc, char* argv[]) { } /** Executes a command. Deletes the command after execution. */ -void doCommand(SmtEngine& smt, Command* cmd) { +static void doCommand(SmtEngine& smt, Command* cmd) { if( options.parseOnly ) { return; } 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); -- 2.30.2