Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.

3 files changed, 18 insertions, 8 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f91f951c6..b89d43cc9 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -98,7 +98,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   progPath = argv[0];
 
   // Parse the options
-  int firstArgIndex = opts.parseOptions(argc, argv);
+  vector<string> filenames = opts.parseOptions(argc, argv);
+
+# ifndef PORTFOLIO_BUILD
+  if( opts.wasSetByUser(options::threads) ||
+      ! opts[options::threadArgv].empty() ) {
+    throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
+  }
+# endif
 
   progName = opts[options::binary_name].c_str();
 
@@ -121,13 +128,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 #endif /* CVC4_COMPETITION_MODE */
 
   // We only accept one input file
-  if(argc > firstArgIndex + 1) {
+  if(filenames.size() > 1) {
     throw Exception("Too many input files specified.");
   }
 
   // If no file supplied we will read from standard input
-  const bool inputFromStdin =
-    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+  const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 
   // if we're reading from stdin on a TTY, default to interactive mode
   if(!opts.wasSetByUser(options::interactive)) {
@@ -157,7 +163,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   }
 
   // Auto-detect input language by filename extension
-  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+  const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
 
   if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
     if( inputFromStdin ) {
diff --git a/src/main/options b/src/main/options
index 47e397d11..47d8da598 100644
--- a/src/main/options
+++ b/src/main/options
@@ -22,10 +22,11 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl
 # portfolio options
 option printWinner bool
  enable printing the winning thread (pcvc4 only)
-option - --threadN=string void
+option threads --threads=N unsigned :default 2 :predicate greater(0)
+ Total number of threads
+option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h"
  configures thread N (0..#threads-1)
-option threadArgv std::vector<std::string>
-#:includes <vector> <string>
+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
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index e607e13ce..7d5d35e08 100644
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -94,6 +94,9 @@ inline void showTraceTags(std::string option, SmtEngine* smt) {
   exit(0);
 }
 
+inline void threadN(std::string option, SmtEngine* smt) {
+  throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
+}
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */