diff options
Diffstat (limited to 'src/main/driver.cpp')
-rw-r--r-- | src/main/driver.cpp | 144 |
1 files changed, 75 insertions, 69 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index f24526e6c..ca5dfad93 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -36,7 +36,10 @@ #include "expr/command.h" #include "util/Assert.h" #include "util/configuration.h" -#include "util/options.h" +#include "options/options.h" +#include "main/options.h" +#include "smt/options.h" +#include "theory/uf/options.h" #include "util/output.h" #include "util/dump.h" #include "util/result.h" @@ -66,28 +69,28 @@ namespace CVC4 { } -void printUsage(Options& options, bool full) { +void printUsage(Options& opts, bool full) { stringstream ss; - ss << "usage: " << options.binary_name << " [options] [input-file]" << endl + ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl << endl << "Without an input file, or with `-', CVC4 reads from standard input." << endl << endl << "CVC4 options:" << endl; if(full) { - Options::printUsage( ss.str(), *options.out ); + Options::printUsage( ss.str(), *opts[options::out] ); } else { - Options::printShortUsage( ss.str(), *options.out ); + Options::printShortUsage( ss.str(), *opts[options::out] ); } } -int runCvc4(int argc, char* argv[], Options& options) { +int runCvc4(int argc, char* argv[], Options& opts) { // Timer statistic TimerStat s_totalTime("totalTime"); s_totalTime.start(); // For the signal handlers' benefit - pOptions = &options; + pOptions = &opts; // Initialize the signal handlers cvc4_init(); @@ -95,26 +98,26 @@ int runCvc4(int argc, char* argv[], Options& options) { progPath = argv[0]; // Parse the options - int firstArgIndex = options.parseOptions(argc, argv); + int firstArgIndex = opts.parseOptions(argc, argv); - progName = options.binary_name.c_str(); + progName = opts[options::binary_name].c_str(); - if( options.help ) { - printUsage(options, true); + if( opts[options::help] ) { + printUsage(opts, true); exit(1); - } else if( options.languageHelp ) { - Options::printLanguageHelp(*options.out); + } else if( opts[options::languageHelp] ) { + Options::printLanguageHelp(*opts[options::out]); exit(1); - } else if( options.version ) { - *options.out << Configuration::about().c_str() << flush; + } else if( opts[options::version] ) { + *opts[options::out] << Configuration::about().c_str() << flush; exit(0); } - segvNoSpin = options.segvNoSpin; + segvNoSpin = opts[options::segvNoSpin]; // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE - *options.out << unitbuf; + *opts[options::out] << unitbuf; #endif /* CVC4_COMPETITION_MODE */ // We only accept one input file @@ -127,8 +130,8 @@ int runCvc4(int argc, char* argv[], Options& options) { firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); // if we're reading from stdin on a TTY, default to interactive mode - if(!options.interactiveSetByUser) { - options.interactive = inputFromStdin && isatty(fileno(stdin)); + if(!opts.wasSetByUser(options::interactive)) { + opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin))); } // Determine which messages to show based on smtcomp_mode and verbosity @@ -141,13 +144,13 @@ int runCvc4(int argc, char* argv[], Options& options) { Warning.setStream(CVC4::null_os); Dump.setStream(CVC4::null_os); } else { - if(options.verbosity < 2) { + if(opts[options::verbosity] < 2) { Chat.setStream(CVC4::null_os); } - if(options.verbosity < 1) { + if(opts[options::verbosity] < 1) { Notice.setStream(CVC4::null_os); } - if(options.verbosity < 0) { + if(opts[options::verbosity] < 0) { Message.setStream(CVC4::null_os); Warning.setStream(CVC4::null_os); } @@ -156,28 +159,28 @@ int runCvc4(int argc, char* argv[], Options& options) { // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; - if(options.inputLanguage == language::input::LANG_AUTO) { + if(opts[options::inputLanguage] == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - options.inputLanguage = language::input::LANG_CVC4; + opts.set(options::inputLanguage, language::input::LANG_CVC4); } else { unsigned len = strlen(filename); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options.inputLanguage = language::input::LANG_SMTLIB_V2; + opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2); } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - options.inputLanguage = language::input::LANG_SMTLIB; + opts.set(options::inputLanguage, language::input::LANG_SMTLIB); } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - options.inputLanguage = language::input::LANG_TPTP; + opts.set(options::inputLanguage, language::input::LANG_TPTP); } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options.inputLanguage = language::input::LANG_CVC4; + opts.set(options::inputLanguage, language::input::LANG_CVC4); } } } - if(options.outputLanguage == language::output::LANG_AUTO) { - options.outputLanguage = language::toOutputLanguage(options.inputLanguage); + if(opts[options::outputLanguage] == language::output::LANG_AUTO) { + opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage])); } // Determine which messages to show based on smtcomp_mode and verbosity @@ -190,70 +193,73 @@ int runCvc4(int argc, char* argv[], Options& options) { Warning.setStream(CVC4::null_os); Dump.setStream(CVC4::null_os); } else { - if(options.verbosity < 2) { + if(opts[options::verbosity] < 2) { Chat.setStream(CVC4::null_os); } - if(options.verbosity < 1) { + if(opts[options::verbosity] < 1) { Notice.setStream(CVC4::null_os); } - if(options.verbosity < 0) { + if(opts[options::verbosity] < 0) { Message.setStream(CVC4::null_os); Warning.setStream(CVC4::null_os); } - Debug.getStream() << Expr::setlanguage(options.outputLanguage); - Trace.getStream() << Expr::setlanguage(options.outputLanguage); - Notice.getStream() << Expr::setlanguage(options.outputLanguage); - Chat.getStream() << Expr::setlanguage(options.outputLanguage); - Message.getStream() << Expr::setlanguage(options.outputLanguage); - Warning.getStream() << Expr::setlanguage(options.outputLanguage); - Dump.getStream() << Expr::setlanguage(options.outputLanguage) + Debug.getStream() << Expr::setlanguage(opts[options::outputLanguage]); + Trace.getStream() << Expr::setlanguage(opts[options::outputLanguage]); + Notice.getStream() << Expr::setlanguage(opts[options::outputLanguage]); + Chat.getStream() << Expr::setlanguage(opts[options::outputLanguage]); + Message.getStream() << Expr::setlanguage(opts[options::outputLanguage]); + Warning.getStream() << Expr::setlanguage(opts[options::outputLanguage]); + Dump.getStream() << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1) << Expr::printtypes(false); } // important even for muzzled builds (to get result output right) - *options.out << Expr::setlanguage(options.outputLanguage); + *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]); // Create the expression manager - ExprManager exprMgr(options); + ExprManager exprMgr(opts); // Create the SmtEngine + StatisticsRegistry driverStats("driver"); SmtEngine smt(&exprMgr); Parser* replayParser = NULL; - if( options.replayFilename != "" ) { - ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options); + if( opts[options::replayFilename] != "" ) { + ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts); - if( options.replayFilename == "-") { + if( opts[options::replayFilename] == "-") { if( inputFromStdin ) { throw OptionException("Replay file and input file can't both be stdin."); } replayParserBuilder.withStreamInput(cin); } replayParser = replayParserBuilder.build(); - options.replayStream = new Parser::ExprStream(replayParser); + opts.set(options::replayStream, new Parser::ExprStream(replayParser)); } - if( options.replayLog != NULL ) { - *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1); + if( opts[options::replayLog] != NULL ) { + *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1); } // signal handlers need access pStatistics = smt.getStatisticsRegistry(); + exprMgr.getStatisticsRegistry()->setName("ExprManager"); pStatistics->registerStat_(exprMgr.getStatisticsRegistry()); + pStatistics->registerStat_(&driverStats); // Timer statistic - RegisterStatistic statTotalTime(exprMgr, &s_totalTime); + RegisterStatistic statTotalTime(&driverStats, &s_totalTime); // Filename statistics ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(exprMgr, &s_statFilename); + RegisterStatistic statFilenameReg(&driverStats, &s_statFilename); // Parse and execute commands until we are done Command* cmd; bool status = true; - if( options.interactive ) { - InteractiveShell shell(exprMgr, options); + if( opts[options::interactive] ) { + InteractiveShell shell(exprMgr, opts); Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); if(Configuration::isSubversionBuild()) { @@ -268,11 +274,11 @@ int runCvc4(int argc, char* argv[], Options& options) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - status = doCommand(smt,cmd, options) && status; + status = doCommand(smt,cmd, opts) && status; delete cmd; } } else { - ParserBuilder parserBuilder(&exprMgr, filename, options); + ParserBuilder parserBuilder(&exprMgr, filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -292,23 +298,23 @@ int runCvc4(int argc, char* argv[], Options& options) { delete cmd; break; } - status = doCommand(smt, cmd, options) && status; + status = doCommand(smt, cmd, opts) && status; delete cmd; } // Remove the parser delete parser; } - if( options.replayStream != NULL ) { + if( opts[options::replayStream] != NULL ) { // this deletes the expression parser too - delete options.replayStream; - options.replayStream = NULL; + delete opts[options::replayStream]; + opts.set(options::replayStream, NULL); } int returnValue; string result = "unknown"; if(status) { - result = smt.getInfo(":status").getValue(); + result = smt.getInfo("status").getValue(); if(result == "sat") { returnValue = 10; @@ -329,20 +335,20 @@ int runCvc4(int argc, char* argv[], Options& options) { #endif /* CVC4_COMPETITION_MODE */ ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult); + RegisterStatistic statSatResultReg(&driverStats, &s_statSatResult); s_totalTime.stop(); - if(options.statistics) { - pStatistics->flushInformation(*options.err); + if(opts[options::statistics]) { + pStatistics->flushInformation(*opts[options::err]); } return returnValue; } /** Executes a command. Deletes the command after execution. */ -static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { - if( options.parseOnly ) { +static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) { + if( opts[options::parseOnly] ) { return true; } @@ -354,15 +360,15 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { for(CommandSequence::iterator subcmd = seq->begin(); subcmd != seq->end(); ++subcmd) { - status = doCommand(smt, *subcmd, options) && status; + status = doCommand(smt, *subcmd, opts) && status; } } else { - if(options.verbosity > 0) { - *options.out << "Invoking: " << *cmd << endl; + if(opts[options::verbosity] > 0) { + *opts[options::out] << "Invoking: " << *cmd << endl; } - if(options.verbosity >= 0) { - cmd->invoke(&smt, *options.out); + if(opts[options::verbosity] >= 0) { + cmd->invoke(&smt, *opts[options::out]); } else { cmd->invoke(&smt); } |