Only print a shortlist of most-commonly-used options on option processing errors; reduces clutter, increases usability

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);