diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 16 | ||||
-rw-r--r-- | src/main/options | 7 | ||||
-rw-r--r-- | src/main/options_handlers.h | 3 |
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 */ |