diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/main/driver_unified.cpp | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 251 |
1 files changed, 100 insertions, 151 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 71f47906d..83b85c170 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -25,6 +25,7 @@ // This must come before PORTFOLIO_BUILD. #include "cvc4autoconfig.h" +#include "base/configuration.h" #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" @@ -36,18 +37,12 @@ #include "main/interactive_shell.h" #include "main/main.h" -#include "options/base_options.h" -#include "options/main_options.h" #include "options/options.h" -#include "options/quantifiers_options.h" #include "options/set_language.h" -#include "options/smt_options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" -#include "smt/smt_options_handler.h" #include "smt_util/command.h" -#include "util/configuration.h" #include "util/result.h" #include "util/statistics_registry.h" @@ -79,47 +74,18 @@ namespace CVC4 { void printUsage(Options& opts, bool full) { stringstream ss; - 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; + ss << "usage: " << opts.getBinaryName() << " [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(), *opts[options::out] ); + Options::printUsage( ss.str(), *(opts.getOut()) ); } else { - Options::printShortUsage( ss.str(), *opts[options::out] ); + Options::printShortUsage( ss.str(), *(opts.getOut()) ); } } -void printStatsFilterZeros(std::ostream& out, const std::string& statsString) { - // read each line, if a number, check zero and skip if so - // Stat are assumed to one-per line: "<statName>, <statValue>" - - std::istringstream iss(statsString); - std::string statName, statValue; - - std::getline(iss, statName, ','); - - while( !iss.eof() ) { - - std::getline(iss, statValue, '\n'); - - double curFloat; - bool isFloat = (std::istringstream(statValue) >> curFloat); - - if( (isFloat && curFloat == 0) || - statValue == " \"0\"" || - statValue == " \"[]\"") { - // skip - } else { - out << statName << "," << statValue << std::endl; - } - - std::getline(iss, statName, ','); - } - -} - int runCvc4(int argc, char* argv[], Options& opts) { // Timer statistic @@ -134,38 +100,35 @@ int runCvc4(int argc, char* argv[], Options& opts) { progPath = argv[0]; -#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." - smt::SmtOptionsHandler optionsHandler(NULL); - // Parse the options - vector<string> filenames = opts.parseOptions(argc, argv, &optionsHandler); + vector<string> filenames = opts.parseOptions(argc, argv); # ifndef PORTFOLIO_BUILD - if( opts.wasSetByUser(options::threads) || - opts.wasSetByUser(options::threadStackSize) || - ! opts[options::threadArgv].empty() ) { + if( opts.wasSetByUserThreads() || + opts.wasSetByUserThreadStackSize() || + (! opts.getThreadArgv().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(); + progName = opts.getBinaryName().c_str(); - if( opts[options::help] ) { + if( opts.getHelp() ) { printUsage(opts, true); exit(1); - } else if( opts[options::languageHelp] ) { - Options::printLanguageHelp(*opts[options::out]); + } else if( opts.getLanguageHelp() ) { + Options::printLanguageHelp(*(opts.getOut())); exit(1); - } else if( opts[options::version] ) { - *opts[options::out] << Configuration::about().c_str() << flush; + } else if( opts.getVersion() ) { + *(opts.getOut()) << Configuration::about().c_str() << flush; exit(0); } - segvSpin = opts[options::segvSpin]; + segvSpin = opts.getSegvSpin(); // If in competition mode, set output stream option to flush immediately #ifdef CVC4_COMPETITION_MODE - *opts[options::out] << unitbuf; + *(opts.getOut()) << unitbuf; #endif /* CVC4_COMPETITION_MODE */ // We only accept one input file @@ -177,66 +140,66 @@ int runCvc4(int argc, char* argv[], Options& opts) { 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)) { - opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin))); + if(!opts.wasSetByUserInteractive()) { + opts.setInteractive(inputFromStdin && isatty(fileno(stdin))); } // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str(); - if(opts[options::inputLanguage] == language::input::LANG_AUTO) { + if(opts.getInputLanguage() == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - opts.set(options::inputLanguage, language::input::LANG_CVC4); + opts.setInputLanguage(language::input::LANG_CVC4); } else { unsigned len = strlen(filename); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_0); + opts.setInputLanguage(language::input::LANG_SMTLIB_V2_0); } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); + opts.setInputLanguage(language::input::LANG_SMTLIB_V1); } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); + opts.setInputLanguage(language::input::LANG_SMTLIB_V1); } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - opts.set(options::inputLanguage, language::input::LANG_TPTP); + opts.setInputLanguage(language::input::LANG_TPTP); } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - opts.set(options::inputLanguage, language::input::LANG_CVC4); + opts.setInputLanguage(language::input::LANG_CVC4); } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { - opts.set(options::inputLanguage, language::input::LANG_SYGUS); + opts.setInputLanguage(language::input::LANG_SYGUS); //since there is no sygus output language, set this to SMT lib 2 - //opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0); + //opts.setOutputLanguage(language::output::LANG_SMTLIB_V2_0); } } } - if(opts[options::outputLanguage] == language::output::LANG_AUTO) { - opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage])); + if(opts.getOutputLanguage() == language::output::LANG_AUTO) { + opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage())); } // if doing sygus, turn on CEGQI by default - if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){ - if( !opts.wasSetByUser(options::ceGuidedInst)) { - opts.set(options::ceGuidedInst, true); + if(opts.getInputLanguage() == language::input::LANG_SYGUS ){ + if( !opts.wasSetByUserCeGuidedInst()) { + opts.setCeGuidedInst(true); } - if( !opts.wasSetByUser(options::dumpSynth)) { - opts.set(options::dumpSynth, true); + if( !opts.wasSetByUserDumpSynth()) { + opts.setDumpSynth(true); } } // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { - DebugChannel.setStream(CVC4::null_os); - TraceChannel.setStream(CVC4::null_os); - NoticeChannel.setStream(CVC4::null_os); - ChatChannel.setStream(CVC4::null_os); - MessageChannel.setStream(CVC4::null_os); - WarningChannel.setStream(CVC4::null_os); + DebugChannel.setStream(&CVC4::null_os); + TraceChannel.setStream(&CVC4::null_os); + NoticeChannel.setStream(&CVC4::null_os); + ChatChannel.setStream(&CVC4::null_os); + MessageChannel.setStream(&CVC4::null_os); + WarningChannel.setStream(&CVC4::null_os); } // important even for muzzled builds (to get result output right) - *opts[options::out] << language::SetLanguage(opts[options::outputLanguage]); + (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage()); // Create the expression manager using appropriate options ExprManager* exprMgr; @@ -244,20 +207,24 @@ int runCvc4(int argc, char* argv[], Options& opts) { exprMgr = new ExprManager(opts); pExecutor = new CommandExecutor(*exprMgr, opts); # else - vector<Options> threadOpts = parseThreadSpecificOptions(opts); + OptionsList threadOpts; + parseThreadSpecificOptions(threadOpts, opts); + bool useParallelExecutor = true; // incremental? - if(opts.wasSetByUser(options::incrementalSolving) && - opts[options::incrementalSolving] && - !opts[options::incrementalParallel]) { - Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n" + if(opts.wasSetByUserIncrementalSolving() && + opts.getIncrementalSolving() && + (! opts.getIncrementalParallel()) ) { + Notice() << "Notice: In --incremental mode, using the sequential solver" + << " unless forced by...\n" << "Notice: ...the experimental --incremental-parallel option.\n"; useParallelExecutor = false; } // proofs? - if(opts[options::checkProofs]) { - if(opts[options::fallbackSequential]) { - Warning() << "Warning: Falling back to sequential mode, as cannot run portfolio in check-proofs mode.\n"; + if(opts.getCheckProofs()) { + if(opts.getFallbackSequential()) { + Warning() << "Warning: Falling back to sequential mode, as cannot run" + << " portfolio in check-proofs mode.\n"; useParallelExecutor = false; } else { @@ -275,41 +242,41 @@ int runCvc4(int argc, char* argv[], Options& opts) { # endif Parser* replayParser = NULL; - if( opts[options::replayFilename] != "" ) { - ParserBuilder replayParserBuilder(exprMgr, opts[options::replayFilename], opts); + if( opts.getReplayInputFilename() != "" ) { + std::string replayFilename = opts.getReplayInputFilename(); + ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts); - if( opts[options::replayFilename] == "-") { + if( replayFilename == "-") { if( inputFromStdin ) { throw OptionException("Replay file and input file can't both be stdin."); } replayParserBuilder.withStreamInput(cin); } replayParser = replayParserBuilder.build(); - pExecutor->globals()->setReplayStream(new Parser::ExprStream(replayParser)); - } - if( pExecutor->globals()->getReplayLog() != NULL ) { - *(pExecutor->globals()->getReplayLog()) << - language::SetLanguage(opts[options::outputLanguage]) << expr::ExprSetDepth(-1); + pExecutor->setReplayStream(new Parser::ExprStream(replayParser)); } int returnValue = 0; { // Timer statistic - RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), pTotalTime); + RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), + pTotalTime); // Filename statistics ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename); + RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), + &s_statFilename); // Parse and execute commands until we are done Command* cmd; bool status = true; - if(opts[options::interactive] && inputFromStdin) { - if(opts[options::tearDownIncremental] > 0) { - throw OptionException("--tear-down-incremental doesn't work in interactive mode"); + if(opts.getInteractive() && inputFromStdin) { + if(opts.getTearDownIncremental() > 0) { + throw OptionException( + "--tear-down-incremental doesn't work in interactive mode"); } #ifndef PORTFOLIO_BUILD - if(!opts.wasSetByUser(options::incrementalSolving)) { + if(!opts.wasSetByUserIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); @@ -317,7 +284,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #endif /* PORTFOLIO_BUILD */ InteractiveShell shell(*exprMgr, opts); - if(opts[options::interactivePrompt]) { + if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); if(Configuration::isGitBuild()) { @@ -339,7 +306,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { try { cmd = shell.readCommand(); } catch(UnsafeInterruptException& e) { - *opts[options::out] << CommandInterrupted(); + (*opts.getOut()) << CommandInterrupted(); break; } if (cmd == NULL) @@ -351,14 +318,15 @@ int runCvc4(int argc, char* argv[], Options& opts) { } delete cmd; } - } else if(opts[options::tearDownIncremental] > 0) { - if(!opts[options::incrementalSolving]) { + } else if( opts.getTearDownIncremental() > 0) { + if(!opts.getIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; - // if(opts.wasSetByUser(options::incrementalSolving)) { - // throw OptionException("--tear-down-incremental incompatible with --incremental"); + // if(opts.wasSetByUserIncrementalSolving()) { + // throw OptionException( + // "--tear-down-incremental incompatible with --incremental"); // } // cmd = new SetOptionCommand("incremental", SExpr(false)); @@ -387,9 +355,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { int needReset = 0; // true if one of the commands was interrupted bool interrupted = false; - while (status || opts[options::continuedExecution]) { + while (status || opts.getContinuedExecution()) { if (interrupted) { - *opts[options::out] << CommandInterrupted(); + (*opts.getOut()) << CommandInterrupted(); break; } @@ -402,11 +370,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { } if(dynamic_cast<PushCommand*>(cmd) != NULL) { - if(needReset >= opts[options::tearDownIncremental]) { + if(needReset >= opts.getTearDownIncremental()) { pExecutor->reset(); for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { if (interrupted) break; - for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) + { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); @@ -428,10 +397,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } else if(dynamic_cast<PopCommand*>(cmd) != NULL) { allCommands.pop_back(); // fixme leaks cmds here - if (needReset >= opts[options::tearDownIncremental]) { + if (needReset >= opts.getTearDownIncremental()) { pExecutor->reset(); for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { - for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) + { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); @@ -442,7 +412,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } if (interrupted) continue; - *opts[options::out] << CommandSuccess(); + (*opts.getOut()) << CommandSuccess(); needReset = 0; } else { status = pExecutor->doCommand(cmd); @@ -453,10 +423,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || dynamic_cast<QueryCommand*>(cmd) != NULL) { - if(needReset >= opts[options::tearDownIncremental]) { + if(needReset >= opts.getTearDownIncremental()) { pExecutor->reset(); for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { - for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) + { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); @@ -516,7 +487,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Remove the parser delete parser; } else { - if(!opts.wasSetByUser(options::incrementalSolving)) { + if(!opts.wasSetByUserIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(false)); cmd->setMuted(true); pExecutor->doCommand(cmd); @@ -539,9 +510,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool interrupted = false; - while(status || opts[options::continuedExecution]) { + while(status || opts.getContinuedExecution()) { if (interrupted) { - *opts[options::out] << CommandInterrupted(); + (*opts.getOut()) << CommandInterrupted(); pExecutor->reset(); break; } @@ -569,13 +540,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete parser; } - if( pExecutor->globals()->getReplayStream() != NULL ) { - ExprStream* replayStream = pExecutor->globals()->getReplayStream(); - pExecutor->globals()->setReplayStream(NULL); - // this deletes the expression parser too - delete replayStream; - } - Result result; if(status) { result = pExecutor->getResult(); @@ -586,7 +550,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #ifdef CVC4_COMPETITION_MODE - *opts[options::out] << flush; + opts.flushOut(); // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors // or other on_exit/atexit stuff. @@ -594,37 +558,22 @@ int runCvc4(int argc, char* argv[], Options& opts) { #endif /* CVC4_COMPETITION_MODE */ ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult); + RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), + &s_statSatResult); pTotalTime->stop(); + // Tim: I think that following comment is out of date? // Set the global executor pointer to NULL first. If we get a // signal while dumping statistics, we don't want to try again. - if(opts[options::statistics]) { - if(opts[options::statsHideZeros] == false) { - pExecutor->flushStatistics(*opts[options::err]); - } else { - std::ostringstream ossStats; - pExecutor->flushStatistics(ossStats); - printStatsFilterZeros(*opts[options::err], ossStats.str()); - } - } - - // make sure to flush replay output log before early-exit - if( pExecutor->globals()->getReplayLog() != NULL ) { - *(pExecutor->globals()->getReplayLog()) << flush; - } - - // make sure out and err streams are flushed too - *opts[options::out] << flush; - *opts[options::err] << flush; + pExecutor->flushOutputStreams(); #ifdef CVC4_DEBUG - if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) { + if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) { _exit(returnValue); } #else /* CVC4_DEBUG */ - if(opts[options::earlyExit]) { + if(opts.getEarlyExit()) { _exit(returnValue); } #endif /* CVC4_DEBUG */ |