diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/Makefile.am | 3 | ||||
-rw-r--r-- | src/main/driver.cpp | 144 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 262 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 18 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 1 | ||||
-rw-r--r-- | src/main/main.cpp | 19 | ||||
-rw-r--r-- | src/main/main.h | 2 | ||||
-rw-r--r-- | src/main/options | 38 | ||||
-rw-r--r-- | src/main/options_handlers.h | 101 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 2 | ||||
-rw-r--r-- | src/main/portfolio.h | 2 | ||||
-rw-r--r-- | src/main/util.cpp | 22 |
12 files changed, 387 insertions, 227 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 594751358..730afa32d 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -65,6 +65,9 @@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ +EXTRA_DIST = \ + options_handlers.h + clean-local: rm -f $(BUILT_SOURCES) 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); } diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index d93e9f872..648c6c9f9 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -40,7 +40,11 @@ #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 "prop/options.h" +#include "theory/uf/options.h" #include "util/output.h" #include "util/dump.h" #include "util/result.h" @@ -78,7 +82,7 @@ static bool doCommand(SmtEngine&, Command*, Options&); Result doSmt(SmtEngine &smt, Command *cmd, Options &options); template<typename T> -void sharingManager(int numThreads, +void sharingManager(unsigned numThreads, SharedChannel<T>* channelsOut[], SharedChannel<T>* channelsIn[], SmtEngine* smts[]); @@ -122,23 +126,25 @@ public: {} void notifyNewLemma(Expr lemma) { - if(Debug.isOn("disable-lemma-sharing")) return; - const Options *options = Options::current(); - if(options->sharingFilterByLength >= 0) { // 0 would mean no-sharing effectively - if( int(lemma.getNumChildren()) > options->sharingFilterByLength) + if(Debug.isOn("disable-lemma-sharing")) { + return; + } + if(options::sharingFilterByLength() >= 0) { // 0 would mean no-sharing effectively + if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { return; + } } ++cnt; - Trace("sharing") << d_tag << ": " << lemma << std::endl; + Trace("sharing") << d_tag << ": " << lemma << endl; expr::pickle::Pickle pkl; - try{ + try { d_pickler.toPickle(lemma, pkl); d_sharedChannel->push(pkl); - if(Trace.isOn("showSharing") and options->thread_id == 0) { - *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl; + if(Trace.isOn("showSharing") && options::thread_id() == 0) { + *options::out() << "thread #0: notifyNewLemma: " << lemma << endl; } - }catch(expr::pickle::PicklingException& p){ - Trace("sharing::blocked") << lemma << std::endl; + } catch(expr::pickle::PicklingException& p){ + Trace("sharing::blocked") << lemma << endl; } } @@ -172,8 +178,8 @@ public: expr::pickle::Pickle pkl = d_sharedChannel->pop(); Expr e = d_pickler.fromPickle(pkl); - if(Trace.isOn("showSharing") and Options::current()->thread_id == 0) { - *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl; + if(Trace.isOn("showSharing") && options::thread_id() == 0) { + *options::out() << "thread #0: getNewLemma: " << e << endl; } return e; } @@ -182,7 +188,7 @@ public: -int runCvc4(int argc, char *argv[], Options& options) { +int runCvc4(int argc, char *argv[], Options& opts) { #ifdef CVC4_CLN_IMP Warning() << "WARNING:" << endl @@ -211,7 +217,7 @@ int runCvc4(int argc, char *argv[], Options& options) { s_beforePortfolioTime.start(); // For the signal handlers' benefit - pOptions = &options; + pOptions = &opts; // Initialize the signal handlers cvc4_init(); @@ -222,36 +228,36 @@ int runCvc4(int argc, char *argv[], Options& options) { /****************************** Options Processing ************************/ // 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); } - int numThreads = options.threads; + unsigned numThreads = opts[options::threads]; - if(options.threadArgv.size() > size_t(numThreads)) { + if(opts[options::threadArgv].size() > size_t(numThreads)) { stringstream ss; - ss << "--thread" << (options.threadArgv.size() - 1) + ss << "--thread" << (opts[options::threadArgv].size() - 1) << " configuration string seen but this portfolio will only contain " << numThreads << " thread(s)!"; throw OptionException(ss.str()); } - 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 @@ -264,29 +270,29 @@ 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))); } // 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); } } } @@ -301,54 +307,55 @@ 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); } - OutputLanguage language = language::toOutputLanguage(options.inputLanguage); + OutputLanguage language = language::toOutputLanguage(opts[options::inputLanguage]); Debug.getStream() << Expr::setlanguage(language); Trace.getStream() << Expr::setlanguage(language); Notice.getStream() << Expr::setlanguage(language); Chat.getStream() << Expr::setlanguage(language); Message.getStream() << Expr::setlanguage(language); Warning.getStream() << Expr::setlanguage(language); - Dump.getStream() << Expr::setlanguage(options.outputLanguage) + Dump.getStream() << Expr::setlanguage(language) << 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]); vector<Options> threadOptions; - for(int i = 0; i < numThreads; ++i) { - threadOptions.push_back(options); - Options& opts = threadOptions.back(); + for(unsigned i = 0; i < numThreads; ++i) { + threadOptions.push_back(opts); + Options& tOpts = threadOptions.back(); // Set thread identifier - opts.thread_id = i; + tOpts.set(options::thread_id, i); // If the random-seed is negative, pick a random seed randomly - if(options.satRandomSeed < 0) - opts.satRandomSeed = (double)rand(); + if(opts[options::satRandomSeed] < 0) { + tOpts.set(options::satRandomSeed, (double)rand()); + } - if(i < (int)options.threadArgv.size() && !options.threadArgv[i].empty()) { + if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) { // separate out the thread's individual configuration string stringstream optidss; optidss << "--thread" << i; string optid = optidss.str(); int targc = 1; - char* tbuf = strdup(options.threadArgv[i].c_str()); + char* tbuf = strdup(opts[options::threadArgv][i].c_str()); char* p = tbuf; // string length is certainly an upper bound on size needed - char** targv = new char*[options.threadArgv[i].size()]; + char** targv = new char*[opts[options::threadArgv][i].size()]; char** vp = targv; *vp++ = strdup(optid.c_str()); p = strtok(p, " "); @@ -360,7 +367,7 @@ int runCvc4(int argc, char *argv[], Options& options) { *vp++ = NULL; if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " try { - opts.parseOptions(targc, targv); + tOpts.parseOptions(targc, targv); } catch(OptionException& e) { stringstream ss; ss << optid << ": " << e.getMessage(); @@ -372,7 +379,7 @@ int runCvc4(int argc, char *argv[], Options& options) { << "' in thread configuration " << optid << " !"; throw OptionException(ss.str()); } - if(opts.threads != numThreads || opts.threadArgv != options.threadArgv) { + if(tOpts[options::threads] != numThreads || tOpts[options::threadArgv] != opts[options::threadArgv]) { stringstream ss; ss << "not allowed to set thread options in " << optid << " !"; throw OptionException(ss.str()); @@ -387,16 +394,16 @@ int runCvc4(int argc, char *argv[], Options& options) { // Some more options related stuff /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */ - srand((unsigned int)(-options.satRandomSeed)); + srand((unsigned int)(-opts[options::satRandomSeed])); assert(numThreads >= 1); //do we need this? /* Output to string stream */ vector<stringstream*> ss_out(numThreads); - if(options.verbosity == 0 or options.separateOutput) { - for(int i = 0;i <numThreads; ++i) { + if(opts[options::verbosity] == 0 || opts[options::separateOutput]) { + for(unsigned i = 0; i < numThreads; ++i) { ss_out[i] = new stringstream; - threadOptions[i].out = ss_out[i]; + threadOptions[i].set(options::out, ss_out[i]); } } @@ -431,8 +438,8 @@ int runCvc4(int argc, char *argv[], Options& options) { Command* cmd; // bool status = true; // Doesn't seem to be use right now: commenting it out CommandSequence* seq = new CommandSequence(); - if( options.interactive ) { - InteractiveShell shell(*exprMgr, options); + if( opts[options::interactive] ) { + InteractiveShell shell(*exprMgr, opts); Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); if(Configuration::isSubversionBuild()) { @@ -452,7 +459,7 @@ int runCvc4(int argc, char *argv[], Options& options) { } else { ParserBuilder parserBuilder = ParserBuilder(exprMgr, filename). - withOptions(options); + withOptions(opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -465,15 +472,16 @@ int runCvc4(int argc, char *argv[], Options& options) { Parser *parser = parserBuilder.build(); while((cmd = parser->nextCommand())) { seq->addCommand(cmd); - // doCommand(smt, cmd, options); + // doCommand(smt, cmd, opts); // delete cmd; } // Remove the parser delete parser; } - if(options.parseOnly) + if(opts[options::parseOnly]) { return 0; + } exprMgr = NULL; // don't want to use that variable // after this point @@ -482,7 +490,7 @@ int runCvc4(int argc, char *argv[], Options& options) { ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty Command *seqs[numThreads]; seqs[0] = seq; seq = NULL; - for(int i = 1; i < numThreads; ++i) { + for(unsigned i = 1; i < numThreads; ++i) { vmaps[i] = new ExprManagerMapCollection(); exprMgrs[i] = new ExprManager(threadOptions[i]); seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) ); @@ -515,14 +523,16 @@ int runCvc4(int argc, char *argv[], Options& options) { // Create the SmtEngine(s) SmtEngine *smts[numThreads]; - for(int i = 0; i < numThreads; ++i) { + for(unsigned i = 0; i < numThreads; ++i) { smts[i] = new SmtEngine(exprMgrs[i]); // Register the statistics registry of the thread - string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id); - smts[i]->getStatisticsRegistry()->setName(tag); - theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() ); + string emTag = "ExprManager thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]); + string smtTag = "SmtEngine thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]); + exprMgrs[i]->getStatisticsRegistry()->setName(emTag); + smts[i]->getStatisticsRegistry()->setName(smtTag); theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() ); + theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() ); } /************************* Lemma sharing init ************************/ @@ -532,12 +542,12 @@ int runCvc4(int argc, char *argv[], Options& options) { if(numThreads == 1) { // Disable sharing - threadOptions[0].sharingFilterByLength = 0; + threadOptions[0].set(options::sharingFilterByLength, 0); } else { // Setup sharing channels const unsigned int sharingChannelSize = 1000000; - for(int i = 0; i<numThreads; ++i){ + for(unsigned i = 0; i < numThreads; ++i){ if(Debug.isOn("channel-empty")) { channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize); channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize); @@ -548,14 +558,14 @@ int runCvc4(int argc, char *argv[], Options& options) { } /* Lemma output channel */ - for(int i = 0; i<numThreads; ++i) { - string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id); - threadOptions[i].lemmaOutputChannel = + for(unsigned i = 0; i < numThreads; ++i) { + string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]); + threadOptions[i].set(options::lemmaOutputChannel, new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i], - vmaps[i]->d_from, vmaps[i]->d_to); - threadOptions[i].lemmaInputChannel = + vmaps[i]->d_from, vmaps[i]->d_to)); + threadOptions[i].set(options::lemmaInputChannel, new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i], - vmaps[i]->d_from, vmaps[i]->d_to); + vmaps[i]->d_from, vmaps[i]->d_to)); } } @@ -564,7 +574,7 @@ int runCvc4(int argc, char *argv[], Options& options) { /* Portfolio */ boost::function<Result()> fns[numThreads]; - for(int i = 0; i < numThreads; ++i) { + for(unsigned i = 0; i < numThreads; ++i) { fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i])); } @@ -580,7 +590,7 @@ int runCvc4(int argc, char *argv[], Options& options) { /************************* Post printing answer ***********************/ - if(options.printWinner){ + if(opts[options::printWinner]){ cout << "The winner is #" << winner << endl; } @@ -606,29 +616,29 @@ int runCvc4(int argc, char *argv[], Options& options) { // Stop timers, enough work done s_totalTime.stop(); - if(options.statistics) { - pStatistics->flushInformation(*options.err); + if(opts[options::statistics]) { + pStatistics->flushInformation(*opts[options::err]); } - if(options.separateOutput) { - for(int i = 0; i < numThreads; ++i) { - *options.out << "--- Output from thread #" << i << " ---" << endl; - *options.out << ss_out[i]->str(); + if(opts[options::separateOutput]) { + for(unsigned i = 0; i < numThreads; ++i) { + *opts[options::out] << "--- Output from thread #" << i << " ---" << endl; + *opts[options::out] << ss_out[i]->str(); } } - /*if(options.statistics) { + /*if(opts[options::statistics]) { double totalTime = double(s_totalTime.getData().tv_sec) + double(s_totalTime.getData().tv_nsec)/1000000000.0; cout.precision(6); - *options.err << "real time: " << totalTime << "s\n"; - int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt; + *opts[options::err] << "real time: " << totalTime << "s\n"; + int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(opts[options::lemmaOutputChannel])).cnt; int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt; - *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl; - *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl; - *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime) + *opts[options::err] << "lemmas shared by thread #0: " << th0_lemcnt << endl; + *opts[options::err] << "lemmas shared by thread #1: " << th1_lemcnt << endl; + *opts[options::err] << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime) << " lem/sec" << endl; - *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl; + *opts[options::err] << "winner: #" << (winner == 0 ? 0 : 1) << endl; }*/ // destruction is causing segfaults, let us just exit @@ -663,23 +673,23 @@ 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] ); } } /** 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; } @@ -691,15 +701,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); } @@ -712,48 +722,48 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { /**** End of code shared with driver.cpp ****/ /** Create the SMT engine and execute the commands */ -Result doSmt(SmtEngine &smt, Command *cmd, Options &options) { +Result doSmt(SmtEngine &smt, Command *cmd, Options &opts) { try { // For the signal handlers' benefit - pOptions = &options; + pOptions = &opts; // Execute the commands - bool status = doCommand(smt, cmd, options); + bool status = doCommand(smt, cmd, opts); - // if(options.statistics) { - // smt.getStatisticsRegistry()->flushInformation(*options.err); - // *options.err << "Statistics printing of my thread complete " << endl; + // if(opts[options::statistics]) { + // smt.getStatisticsRegistry()->flushInformation(*opts[options::err]); + // *opts[options::err] << "Statistics printing of my thread complete " << endl; // } return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN; } catch(OptionException& e) { - *pOptions->out << "unknown" << endl; + *(*pOptions)[options::out] << "unknown" << endl; cerr << "CVC4 Error:" << endl << e << endl; printUsage(*pOptions); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - *pOptions->out << "unknown" << endl; + *(*pOptions)[options::out] << "unknown" << endl; #endif - *pOptions->err << "CVC4 Error:" << endl << e << endl; - if(pOptions->statistics) { - pStatistics->flushInformation(*pOptions->err); + *(*pOptions)[options::err] << "CVC4 Error:" << endl << e << endl; + if((*pOptions)[options::statistics]) { + pStatistics->flushInformation(*(*pOptions)[options::err]); } } return Result::SAT_UNKNOWN; } template<typename T> -void sharingManager(int numThreads, +void sharingManager(unsigned numThreads, SharedChannel<T> *channelsOut[], // out and in with respect SharedChannel<T> *channelsIn[], SmtEngine *smts[]) // to smt engines { - Trace("sharing") << "sharing: thread started " << std::endl; + Trace("sharing") << "sharing: thread started " << endl; vector <int> cnt(numThreads); // Debug("sharing") vector< queue<T> > queues; - for(int i = 0; i < numThreads; ++i){ + for(unsigned i = 0; i < numThreads; ++i){ queues.push_back(queue<T>()); } @@ -768,7 +778,7 @@ void sharingManager(int numThreads, boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval)); - for(int t = 0; t < numThreads; ++t) { + for(unsigned t = 0; t < numThreads; ++t) { if(channelsOut[t]->empty()) continue; /* No activity on this channel */ @@ -784,22 +794,22 @@ void sharingManager(int numThreads, << ". Chunk " << cnt[t] << std :: endl; } - for(int u = 0; u < numThreads; ++u) { + for(unsigned u = 0; u < numThreads; ++u) { if(u != t){ - Trace("sharing") << "sharing: adding to queue " << u << std::endl; + Trace("sharing") << "sharing: adding to queue " << u << endl; queues[u].push(data); } }/* end of inner for: broadcast activity */ } /* end of outer for: look for activity */ - for(int t = 0; t < numThreads; ++t){ + for(unsigned t = 0; t < numThreads; ++t){ /* Alert if channel full, so that we increase sharingChannelSize or decrease sharingBroadcastInterval */ Assert(not channelsIn[t]->full()); while(!queues[t].empty() && !channelsIn[t]->full()){ - Trace("sharing") << "sharing: pushing on channel " << t << std::endl; + Trace("sharing") << "sharing: pushing on channel " << t << endl; T data = queues[t].front(); channelsIn[t]->push(data); queues[t].pop(); @@ -807,17 +817,17 @@ void sharingManager(int numThreads, } } /* end of infinite while */ - Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << std::endl; + Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << endl; - for(int t = 0; t < numThreads; ++t) { - Trace("interrupt") << "Interrupting thread #" << t << std::endl; + for(unsigned t = 0; t < numThreads; ++t) { + Trace("interrupt") << "Interrupting thread #" << t << endl; try{ smts[t]->interrupt(); }catch(ModalException &e){ // It's fine, the thread is probably not there. - Trace("interrupt") << "Could not interrupt thread #" << t << std::endl; + Trace("interrupt") << "Could not interrupt thread #" << t << endl; } } - Trace("sharing") << "sharing: Interrupted, exiting." << std::endl; + Trace("sharing") << "sharing: Interrupted, exiting." << endl; } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 03a3a0ae3..443404384 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -33,7 +33,7 @@ #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "util/options.h" +#include "options/options.h" #include "util/language.h" #include <string.h> @@ -85,8 +85,8 @@ static set<string> s_declarations; InteractiveShell::InteractiveShell(ExprManager& exprManager, const Options& options) : - d_in(*options.in), - d_out(*options.out), + d_in(*options[options::in]), + d_out(*options[options::out]), d_options(options), d_quit(false) { ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); @@ -99,7 +99,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, ::rl_completion_entry_function = commandGenerator; ::using_history(); - switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) { + switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) { case output::LANG_CVC4: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; commandsBegin = cvc_commands; @@ -174,7 +174,7 @@ Command* InteractiveShell::readCommand() { /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : ""); + lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "CVC4> " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -182,7 +182,7 @@ Command* InteractiveShell::readCommand() { free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - if(d_options.verbosity >= 0) { + if(d_options[options::verbosity] >= 0) { d_out << "CVC4> " << flush; } @@ -239,7 +239,7 @@ Command* InteractiveShell::readCommand() { input[n] = '\n'; if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : ""); + lineBuf = ::readline(d_options[options::verbosity] >= 0 ? "... > " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -247,7 +247,7 @@ Command* InteractiveShell::readCommand() { free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - if(d_options.verbosity >= 0) { + if(d_options[options::verbosity] >= 0) { d_out << "... > " << flush; } @@ -262,7 +262,7 @@ Command* InteractiveShell::readCommand() { } } - d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME)); + d_parser->setInput(Input::newStringInput(d_options[options::inputLanguage], input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 7f17b88d7..214ae0d02 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -21,6 +21,7 @@ #include <string> #include "util/language.h" +#include "options/options.h" namespace CVC4 { diff --git a/src/main/main.cpp b/src/main/main.cpp index b90ab433a..70f2783a5 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -34,7 +34,8 @@ #include "expr/command.h" #include "util/Assert.h" #include "util/configuration.h" -#include "util/options.h" +#include "main/options.h" +#include "theory/uf/options.h" #include "util/output.h" #include "util/result.h" #include "util/stats.h" @@ -51,22 +52,22 @@ using namespace CVC4::main; * Put everything in runCvc4(). */ int main(int argc, char* argv[]) { - Options options; + Options opts; try { - return runCvc4(argc, argv, options); + return runCvc4(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE - *options.out << "unknown" << endl; + *opts[options::out] << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl; - printUsage(options); + printUsage(opts); } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - *options.out << "unknown" << endl; + *opts[options::out] << "unknown" << endl; #endif - *options.err << "CVC4 Error:" << endl << e << endl; - if(options.statistics && pStatistics != NULL) { - pStatistics->flushInformation(*options.err); + *opts[options::err] << "CVC4 Error:" << endl << e << endl; + if(opts[options::statistics] && pStatistics != NULL) { + pStatistics->flushInformation(*opts[options::err]); } } exit(1); diff --git a/src/main/main.h b/src/main/main.h index 4df5ccc49..09ba60c94 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -19,7 +19,7 @@ #include <exception> #include <string> -#include "util/options.h" +#include "options/options.h" #include "util/exception.h" #include "util/stats.h" #include "util/tls.h" diff --git a/src/main/options b/src/main/options new file mode 100644 index 000000000..6defc8642 --- /dev/null +++ b/src/main/options @@ -0,0 +1,38 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DRIVER "main/options.h" Driver + +common-option version -V --version/ bool + identify this CVC4 binary + +common-option help -h --help/ bool + full command line reference + +common-option - --show-config void :handler CVC4::main::showConfiguration :handler-include "main/options_handlers.h" + show CVC4 static configuration + +option - --show-debug-tags void :handler CVC4::main::showDebugTags :handler-include "main/options_handlers.h" + show all available tags for debugging +option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-include "main/options_handlers.h" + show all available tags for tracing + +# portfolio options +option printWinner bool + enable printing the winning thread (pcvc4 only) +option - --threadN=string void + configures thread N (0..#threads-1) +option threadArgv std::vector<std::string> +#:includes <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 +option separateOutput bool :default false + In multi-threaded setting print output of each thread at the + end of run, separated by a divider ("----"). +option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write + don't share lemmas strictly longer than N + +endmodule diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h new file mode 100644 index 000000000..e607e13ce --- /dev/null +++ b/src/main/options_handlers.h @@ -0,0 +1,101 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Custom handlers and predicates for main driver options + ** + ** Custom handlers and predicates for main driver options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H +#define __CVC4__MAIN__OPTIONS_HANDLERS_H + +namespace CVC4 { +namespace main { + +inline void showConfiguration(std::string option, SmtEngine* smt) { + fputs(Configuration::about().c_str(), stdout); + printf("\n"); + printf("version : %s\n", Configuration::getVersionString().c_str()); + if(Configuration::isSubversionBuild()) { + printf("subversion : yes [%s r%u%s]\n", + Configuration::getSubversionBranchName(), + Configuration::getSubversionRevision(), + Configuration::hasSubversionModifications() ? + " (with modifications)" : ""); + } else { + printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no"); + } + printf("\n"); + printf("library : %u.%u.%u\n", + Configuration::getVersionMajor(), + Configuration::getVersionMinor(), + Configuration::getVersionRelease()); + printf("\n"); + printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); + printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); + printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); + printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); + printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); + printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); + printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); + printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); + printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); + printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); + printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); + printf("\n"); + printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); + printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); + printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); + printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); + exit(0); +} + +inline void showDebugTags(std::string option, SmtEngine* smt) { + if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumDebugTags(); + char const* const* tags = Configuration::getDebugTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } else if(! Configuration::isDebugBuild()) { + throw OptionException("debug tags not available in non-debug builds"); + } else { + throw OptionException("debug tags not available in non-tracing builds"); + } + exit(0); +} + +inline void showTraceTags(std::string option, SmtEngine* smt) { + if(Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumTraceTags(); + char const* const* tags = Configuration::getTraceTags(); + for (unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } else { + throw OptionException("trace tags not available in non-tracing build"); + } + exit(0); +} + + +}/* CVC4::main namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */ diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index fc22374cf..10c387b14 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -25,7 +25,7 @@ #include "smt/smt_engine.h" #include "util/result.h" -#include "util/options.h" +#include "options/options.h" using namespace boost; diff --git a/src/main/portfolio.h b/src/main/portfolio.h index 9bc911be3..1a82d651b 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -25,7 +25,7 @@ #include "smt/smt_engine.h" #include "expr/command.h" -#include "util/options.h" +#include "options/options.h" namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index 5877704ae..756c7d7a9 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -27,7 +27,7 @@ #include "util/Assert.h" #include "util/exception.h" -#include "util/options.h" +#include "options/options.h" #include "util/stats.h" #include "cvc4autoconfig.h" @@ -52,7 +52,7 @@ bool segvNoSpin = false; /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } abort(); @@ -61,7 +61,7 @@ void timeout_handler(int sig, siginfo_t* info, void*) { /** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } abort(); @@ -86,7 +86,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) { if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } abort(); @@ -106,7 +106,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) { } else if(addr < 10*1024) { cerr << "Looks like a NULL pointer was dereferenced." << endl; } - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } abort(); @@ -119,7 +119,7 @@ void ill_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } abort(); @@ -132,7 +132,7 @@ void ill_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 executed an illegal instruction.\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } abort(); @@ -156,7 +156,7 @@ void cvc4unexpected() { } if(segvNoSpin) { fprintf(stderr, "No-spin requested.\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } set_terminate(default_terminator); @@ -169,7 +169,7 @@ void cvc4unexpected() { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } set_terminate(default_terminator); @@ -182,7 +182,7 @@ void cvc4terminate() { "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " "(Don't do that.)\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } default_terminator(); @@ -190,7 +190,7 @@ void cvc4terminate() { fprintf(stderr, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); - if(pOptions->statistics && pStatistics != NULL) { + if((*pOptions)[options::statistics] && pStatistics != NULL) { pStatistics->flushInformation(cerr); } default_terminator(); |