diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:33 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-22 22:50:33 +0000 |
commit | a486cdde94366aa6b4a1f558eecc0130ba25ad5e (patch) | |
tree | 8931708b9046ec62c7bdd513de9de1e5a507aa53 /src/main/main.cpp | |
parent | 6dee1d9817d8e9209f0a681b7c601ec6b4b5014d (diff) |
Merging main/getopt.cpp, main/usage.h, and smt/options.h in
util/options.h,cpp
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 91 |
1 files changed, 67 insertions, 24 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 8ed938351..544c6fd29 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -28,7 +28,6 @@ #include "cvc4autoconfig.h" #include "main.h" #include "interactive_shell.h" -#include "usage.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -37,8 +36,8 @@ #include "expr/command.h" #include "util/Assert.h" #include "util/configuration.h" +#include "util/options.h" #include "util/output.h" -#include "smt/options.h" #include "util/result.h" #include "util/stats.h" @@ -47,14 +46,41 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -namespace CVC4 { - namespace main { - struct Options options; - }/* CVC4::main namespace */ -}/* CVC4 namespace */ - int runCvc4(int argc, char* argv[]); void doCommand(SmtEngine&, Command*); +void printUsage(); + +namespace CVC4 { + namespace main {/* Global options variable */ + Options options; + + /** Full argv[0] */ + const char *progPath; + + /** Just the basename component of argv[0] */ + const char *progName; + } +} + + +// 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() { + 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 ); +} /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. @@ -68,34 +94,34 @@ int main(int argc, char* argv[]) { return runCvc4(argc, argv); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; - printf(usage, options.binary_name.c_str()); + printUsage(); exit(1); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 Error:" << endl << e << endl; + options.err << "CVC4 Error:" << endl << e << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } exit(1); } catch(bad_alloc) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 ran out of memory." << endl; + options.err << "CVC4 ran out of memory." << endl; if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } exit(1); } catch(...) { #ifdef CVC4_COMPETITION_MODE - cout << "unknown" << endl; + options.out << "unknown" << endl; #endif - cerr << "CVC4 threw an exception of unknown type." << endl; + options.err << "CVC4 threw an exception of unknown type." << endl; exit(1); } } @@ -106,12 +132,29 @@ int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers cvc4_init(); + progPath = argv[0]; + // Parse the options - int firstArgIndex = parseOptions(argc, argv, &options); + int firstArgIndex = options.parseOptions(argc, argv); + + progName = options.binary_name.c_str(); + + if( options.help ) { + printUsage(); + exit(1); + } else if( options.languageHelp ) { + Options::printLanguageHelp(options.out); + exit(1); + } else if( options.version ) { + options.out << Configuration::about().c_str() << flush; + exit(0); + } + + segvNoSpin = options.segvNoSpin; // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE - cout << unitbuf; + options.out << unitbuf; #endif // We only accept one input file @@ -201,7 +244,7 @@ int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; if( options.interactive ) { - InteractiveShell shell(cin,cout,parserBuilder); + InteractiveShell shell(options.in,options.out,parserBuilder); while((cmd = shell.readCommand())) { doCommand(smt,cmd); delete cmd; @@ -237,7 +280,7 @@ int runCvc4(int argc, char* argv[]) { StatisticsRegistry::registerStat(&s_statSatResult); if(options.statistics) { - StatisticsRegistry::flushStatistics(cerr); + StatisticsRegistry::flushStatistics(options.err); } StatisticsRegistry::unregisterStat(&s_statSatResult); @@ -261,11 +304,11 @@ void doCommand(SmtEngine& smt, Command* cmd) { } } else { if(options.verbosity > 0) { - cout << "Invoking: " << *cmd << endl; + options.out << "Invoking: " << *cmd << endl; } if(options.verbosity >= 0) { - cmd->invoke(&smt, cout); + cmd->invoke(&smt, options.out); } else { cmd->invoke(&smt); } |