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 | |
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')
-rw-r--r-- | src/main/command_executor.cpp | 116 | ||||
-rw-r--r-- | src/main/command_executor.h | 12 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 158 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.h | 4 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 251 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 44 | ||||
-rw-r--r-- | src/main/main.cpp | 21 | ||||
-rw-r--r-- | src/main/portfolio_util.cpp | 81 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 22 | ||||
-rw-r--r-- | src/main/util.cpp | 26 |
10 files changed, 399 insertions, 336 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index aa43cff0f..b2dbaf39b 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -22,10 +22,6 @@ #include <string> #include "main/main.h" -#include "options/base_options.h" -#include "options/main_options.h" -#include "options/printer_options.h" -#include "options/smt_options.h" #include "smt_util/command.h" @@ -55,12 +51,19 @@ CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) : d_smtEngine(new SmtEngine(&exprMgr)), d_options(options), d_stats("driver"), - d_result() { + d_result(), + d_replayStream(NULL) +{} + +void CommandExecutor::setReplayStream(ExprStream* replayStream) { + assert(d_replayStream == NULL); + d_replayStream = replayStream; + d_smtEngine->setReplayStream(d_replayStream); } bool CommandExecutor::doCommand(Command* cmd) { - if( d_options[options::parseOnly] ) { + if( d_options.getParseOnly() ) { return true; } @@ -70,15 +73,15 @@ bool CommandExecutor::doCommand(Command* cmd) bool status = true; for(CommandSequence::iterator subcmd = seq->begin(); - (status || d_options[options::continuedExecution]) && subcmd != seq->end(); + (status || d_options.getContinuedExecution()) && subcmd != seq->end(); ++subcmd) { status = doCommand(*subcmd); } return status; } else { - if(d_options[options::verbosity] > 2) { - *d_options[options::out] << "Invoking: " << *cmd << std::endl; + if(d_options.getVerbosity() > 2) { + *d_options.getOut() << "Invoking: " << *cmd << std::endl; } return doCommandSingleton(cmd); @@ -87,8 +90,8 @@ bool CommandExecutor::doCommand(Command* cmd) void CommandExecutor::reset() { - if(d_options[options::statistics]) { - flushStatistics(*d_options[options::err]); + if(d_options.getStatistics()) { + flushStatistics(*d_options.getErr()); } delete d_smtEngine; d_smtEngine = new SmtEngine(&d_exprMgr); @@ -97,8 +100,8 @@ void CommandExecutor::reset() bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; - if(d_options[options::verbosity] >= -1) { - status = smtEngineInvoke(d_smtEngine, cmd, d_options[options::out]); + if(d_options.getVerbosity() >= -1) { + status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut()); } else { status = smtEngineInvoke(d_smtEngine, cmd, NULL); } @@ -113,42 +116,53 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) d_result = res = q->getResult(); } - if((cs != NULL || q != NULL) && d_options[options::statsEveryQuery]) { + if((cs != NULL || q != NULL) && d_options.getStatsEveryQuery()) { std::ostringstream ossCurStats; flushStatistics(ossCurStats); - printStatsIncremental(*d_options[options::err], d_lastStatistics, ossCurStats.str()); + std::ostream& err = *d_options.getErr(); + printStatsIncremental(err, d_lastStatistics, ossCurStats.str()); d_lastStatistics = ossCurStats.str(); } // dump the model/proof/unsat core if option is set if(status) { Command* g = NULL; - if( d_options[options::produceModels] && - d_options[options::dumpModels] && + if( d_options.getProduceModels() && + d_options.getDumpModels() && ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) { g = new GetModelCommand(); } - if( d_options[options::proof] && - d_options[options::dumpProofs] && + if( d_options.getProof() && + d_options.getDumpProofs() && res.asSatisfiabilityResult() == Result::UNSAT ) { g = new GetProofCommand(); } - if( d_options[options::dumpInstantiations] && - ( ( d_options[options::instFormatMode] != INST_FORMAT_MODE_SZS && - ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || - res.asSatisfiabilityResult() == Result::UNSAT ) ) { + + if( d_options.getDumpInstantiations() && + ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && + ( res.asSatisfiabilityResult() == Result::SAT || + (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) || + res.asSatisfiabilityResult() == Result::UNSAT ) ) + { g = new GetInstantiationsCommand(); } - if( d_options[options::dumpSynth] && res.asSatisfiabilityResult() == Result::UNSAT ){ + + if( d_options.getDumpSynth() && + res.asSatisfiabilityResult() == Result::UNSAT ) + { g = new GetSynthSolutionCommand(); } - if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) { + + if( d_options.getDumpUnsatCores() && + res.asSatisfiabilityResult() == Result::UNSAT ) + { g = new GetUnsatCoreCommand(); } + if(g != NULL) { // set no time limit during dumping if applicable - if( d_options[options::forceNoLimitCpuWhileDump] ){ + if( d_options.getForceNoLimitCpuWhileDump() ){ setNoLimitCPU(); } status = doCommandSingleton(g); @@ -165,7 +179,9 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) cmd->invoke(smt, *out); } // ignore the error if the command-verbosity is 0 for this command - if(smt->getOption(std::string("command-verbosity:") + cmd->getCommandName()).getIntegerValue() == 0) { + std::string commandName = + std::string("command-verbosity:") + cmd->getCommandName(); + if(smt->getOption(commandName).getIntegerValue() == 0) { return true; } return !cmd->fail(); @@ -223,5 +239,51 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString } } +void CommandExecutor::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, ','); + } + +} + +void CommandExecutor::flushOutputStreams() { + if(d_options.getStatistics()) { + if(d_options.getStatsHideZeros() == false) { + flushStatistics(*(d_options.getErr())); + } else { + std::ostringstream ossStats; + flushStatistics(ossStats); + printStatsFilterZeros(*(d_options.getErr()), ossStats.str()); + } + } + + // make sure out and err streams are flushed too + d_options.flushOut(); + d_options.flushErr(); +} + }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 7b6c2fab5..03bbe661b 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -37,12 +37,16 @@ protected: Options& d_options; StatisticsRegistry d_stats; Result d_result; + ExprStream* d_replayStream; public: CommandExecutor(ExprManager &exprMgr, Options &options); virtual ~CommandExecutor() { delete d_smtEngine; + if(d_replayStream != NULL){ + delete d_replayStream; + } } /** @@ -65,7 +69,13 @@ public: d_stats.flushInformation(out); } - SmtGlobals* globals() { return d_smtEngine->globals(); } + static void printStatsFilterZeros(std::ostream& out, + const std::string& statsString); + + LemmaChannels* channels() { return d_smtEngine->channels(); } + void flushOutputStreams(); + + void setReplayStream(ExprStream* replayStream); protected: /** Executes treating cmd as a singleton */ diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 9d0042694..bf1143647 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -31,12 +31,8 @@ #include "expr/pickler.h" #include "main/main.h" #include "main/portfolio.h" -#include "options/base_options.h" -#include "options/main_options.h" #include "options/options.h" -#include "options/printer_options.h" #include "options/set_language.h" -#include "options/smt_options.h" #include "smt_util/command.h" @@ -45,25 +41,26 @@ using namespace std; namespace CVC4 { namespace main { -CommandExecutorPortfolio::CommandExecutorPortfolio -(ExprManager &exprMgr, Options &options, vector<Options>& tOpts): - CommandExecutor(exprMgr, options), - d_numThreads(options[options::threads]), - d_smts(), - d_seq(new CommandSequence()), - d_threadOptions(tOpts), - d_vmaps(), - d_lastWinner(0), - d_channelsOut(), - d_channelsIn(), - d_ostringstreams(), - d_statLastWinner("portfolio::lastWinner"), - d_statWaitTime("portfolio::waitTime") +CommandExecutorPortfolio::CommandExecutorPortfolio( + ExprManager &exprMgr, Options &options, OptionsList& tOpts) + : CommandExecutor(exprMgr, options), + d_numThreads(options.getThreads()), + d_smts(), + d_seq(new CommandSequence()), + d_threadOptions(tOpts), + d_vmaps(), + d_lastWinner(0), + d_channelsOut(), + d_channelsIn(), + d_ostringstreams(), + d_statLastWinner("portfolio::lastWinner"), + d_statWaitTime("portfolio::waitTime") { assert(d_threadOptions.size() == d_numThreads); d_statLastWinner.setData(d_lastWinner); d_stats.registerStat(&d_statLastWinner); + d_stats.registerStat(&d_statWaitTime); /* Duplication, individualization */ @@ -111,7 +108,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() if(d_numThreads == 1) { // Disable sharing - d_threadOptions[0].set(options::sharingFilterByLength, 0); + d_threadOptions[0].setSharingFilterByLength(0); } else { // Setup sharing channels const unsigned int sharingChannelSize = 1000000; @@ -125,34 +122,34 @@ void CommandExecutorPortfolio::lemmaSharingInit() /* Lemma I/O channels */ for(unsigned i = 0; i < d_numThreads; ++i) { - string tag = "thread #" + - boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); + int thread_id = d_threadOptions[i].getThreadId(); + string tag = "thread #" + boost::lexical_cast<string>(thread_id); LemmaOutputChannel* outputChannel = new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], d_vmaps[i]->d_from, d_vmaps[i]->d_to); LemmaInputChannel* inputChannel = new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], d_vmaps[i]->d_from, d_vmaps[i]->d_to); - d_smts[i]->globals()->setLemmaInputChannel(inputChannel); - d_smts[i]->globals()->setLemmaOutputChannel(outputChannel); + d_smts[i]->channels()->setLemmaInputChannel(inputChannel); + d_smts[i]->channels()->setLemmaOutputChannel(outputChannel); } /* Output to string stream */ assert(d_ostringstreams.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { d_ostringstreams.push_back(new ostringstream); - d_threadOptions[i].set(options::out, d_ostringstreams[i]); + d_threadOptions[i].setOut(d_ostringstreams[i]); + OutputLanguage outputLanguage = d_threadOptions[i].getOutputLanguage(); // important even for muzzled builds (to get result output right) - *d_threadOptions[i][options::out] - << language::SetLanguage(d_threadOptions[i][options::outputLanguage]); + *(d_threadOptions[i].getOut()) << language::SetLanguage(outputLanguage); } } }/* CommandExecutorPortfolio::lemmaSharingInit() */ void CommandExecutorPortfolio::lemmaSharingCleanup() { - assert(d_numThreads == d_options[options::threads]); + assert(d_numThreads == d_options.getThreads()); if(d_numThreads == 1) return; @@ -163,10 +160,10 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() for(unsigned i = 0; i < d_numThreads; ++i) { delete d_channelsIn[i]; delete d_channelsOut[i]; - delete d_smts[i]->globals()->getLemmaInputChannel(); - d_smts[i]->globals()->setLemmaInputChannel(NULL); - delete d_smts[i]->globals()->getLemmaOutputChannel(); - d_smts[i]->globals()->setLemmaOutputChannel(NULL); + delete d_smts[i]->channels()->getLemmaInputChannel(); + d_smts[i]->channels()->setLemmaInputChannel(NULL); + delete d_smts[i]->channels()->getLemmaOutputChannel(); + d_smts[i]->channels()->setLemmaOutputChannel(NULL); } d_channelsIn.clear(); d_channelsOut.clear(); @@ -175,7 +172,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() if(d_ostringstreams.size() != 0) { assert(d_ostringstreams.size() == d_numThreads); for(unsigned i = 0; i < d_numThreads; ++i) { - d_threadOptions[i].set(options::out, d_options[options::out]); + d_threadOptions[i].setOut(d_options.getOut()); delete d_ostringstreams[i]; } d_ostringstreams.clear(); @@ -225,9 +222,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Command* cmdExported = d_lastWinner == 0 ? cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); - bool ret = smtEngineInvoke(d_smts[d_lastWinner], - cmdExported, - d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL); + std::ostream* winnersOut = d_options.getVerbosity() >= -1 ? + (d_threadOptions[d_lastWinner]).getOut() : NULL; + bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, winnersOut); if(d_lastWinner != 0) delete cmdExported; return ret; } else if(mode == 1) { // portfolio @@ -260,13 +257,15 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) : d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); } catch(ExportUnsupportedException& e) { - if(d_options[options::fallbackSequential]) { - Notice() << "Unsupported theory encountered, switching to sequential mode."; + if(d_options.getFallbackSequential()) { + Notice() << "Unsupported theory encountered." + << "Switching to sequential mode."; return CommandExecutor::doCommandSingleton(cmd); } else - throw Exception("Certain theories (e.g., datatypes) are (currently) unsupported in portfolio\n" - "mode. Please see option --fallback-sequential to make this a soft error."); + throw Exception("Certain theories (e.g., datatypes) are (currently)" + " unsupported in portfolio\n mode. Please see option" + " --fallback-sequential to make this a soft error."); } } @@ -289,11 +288,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) /* Portfolio */ boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads]; for(unsigned i = 0; i < d_numThreads; ++i) { - fns[i] = boost::bind(smtEngineInvoke, - d_smts[i], - seqs[i], - d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL - ); + std::ostream* current_out_or_null = d_options.getVerbosity() >= -1 ? + d_threadOptions[i].getOut() : NULL; + + fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i], + current_out_or_null); } assert(d_channelsIn.size() == d_numThreads @@ -311,12 +310,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) &d_channelsIn[0], &d_smts[0]); - size_t threadStackSize = d_options[options::threadStackSize]; + size_t threadStackSize = d_options.getThreadStackSize(); threadStackSize *= 1024 * 1024; pair<int, bool> portfolioReturn = runPortfolio(d_numThreads, smFn, fns, threadStackSize, - d_options[options::waitToJoin], d_statWaitTime); + d_options.getWaitToJoin(), d_statWaitTime); #ifdef CVC4_STATISTICS_ON assert( d_statWaitTime.running() ); @@ -327,25 +326,24 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_result = d_smts[d_lastWinner]->getStatusOfLastCommand(); if(d_ostringstreams.size() != 0) { - assert(d_numThreads == d_options[options::threads]); + assert(d_numThreads == d_options.getThreads()); assert(portfolioReturn.first >= 0); assert(unsigned(portfolioReturn.first) < d_numThreads); + std::ostream& out = *d_options.getOut(); if(Debug.isOn("treat-unknown-error")) { if(d_ostringstreams[portfolioReturn.first]->str() == "unknown\n") { - *d_options[options::out] - << "portfolioReturn = (" << portfolioReturn.first << ", " << portfolioReturn.second - << ")\n"; + out << "portfolioReturn = (" << portfolioReturn.first << ", " + << portfolioReturn.second << ")\n"; for(unsigned i = 0; i < d_numThreads; ++i) - *d_options[options::out] - << "thread " << i << ": " << d_ostringstreams[i]->str() << std::endl; + out << "thread " << i << ": " << d_ostringstreams[i]->str() + << std::endl; throw Exception("unknown encountered"); } } - *d_options[options::out] - << d_ostringstreams[portfolioReturn.first]->str() - << std::flush; + out << d_ostringstreams[portfolioReturn.first]->str() + << std::flush; #ifdef CVC4_COMPETITION_MODE // We use CVC4 in competition with --no-wait-to-join. If @@ -366,27 +364,32 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // dump the model/proof/unsat core if option is set if(status) { - if( d_options[options::produceModels] && - d_options[options::dumpModels] && + if( d_options.getProduceModels() && + d_options.getDumpModels() && ( d_result.asSatisfiabilityResult() == Result::SAT || - (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) { + (d_result.isUnknown() && + d_result.whyUnknown() == Result::INCOMPLETE) ) ) + { Command* gm = new GetModelCommand(); status = doCommandSingleton(gm); - } else if( d_options[options::proof] && - d_options[options::dumpProofs] && + } else if( d_options.getProof() && + d_options.getDumpProofs() && d_result.asSatisfiabilityResult() == Result::UNSAT ) { Command* gp = new GetProofCommand(); status = doCommandSingleton(gp); - } else if( d_options[options::dumpInstantiations] && - ( ( d_options[options::instFormatMode]!=INST_FORMAT_MODE_SZS && - ( d_result.asSatisfiabilityResult() == Result::SAT || (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) || - d_result.asSatisfiabilityResult() == Result::UNSAT ) ) { + } else if( d_options.getDumpInstantiations() && + ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && + ( d_result.asSatisfiabilityResult() == Result::SAT || + (d_result.isUnknown() && + d_result.whyUnknown() == Result::INCOMPLETE) ) ) || + d_result.asSatisfiabilityResult() == Result::UNSAT ) ) { Command* gi = new GetInstantiationsCommand(); status = doCommandSingleton(gi); - } else if( d_options[options::dumpSynth] && d_result.asSatisfiabilityResult() == Result::UNSAT ){ + } else if( d_options.getDumpSynth() && + d_result.asSatisfiabilityResult() == Result::UNSAT ){ Command* gi = new GetSynthSolutionCommand(); status = doCommandSingleton(gi); - } else if( d_options[options::dumpUnsatCores] && + } else if( d_options.getDumpUnsatCores() && d_result.asSatisfiabilityResult() == Result::UNSAT ) { Command* guc = new GetUnsatCoreCommand(); status = doCommandSingleton(guc); @@ -395,13 +398,15 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) return status; } else if(mode == 2) { - Command* cmdExported = - d_lastWinner == 0 ? - cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); - bool ret = smtEngineInvoke(d_smts[d_lastWinner], - cmdExported, - d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL); - if(d_lastWinner != 0) delete cmdExported; + Command* cmdExported = d_lastWinner == 0 ? + cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner])); + std::ostream* winner_out_if_verbose = d_options.getVerbosity() >= -1 ? + d_threadOptions[d_lastWinner].getOut() : NULL; + bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, + winner_out_if_verbose); + if(d_lastWinner != 0){ + delete cmdExported; + } return ret; } else { // Unreachable(); @@ -412,16 +417,17 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) }/* CommandExecutorPortfolio::doCommandSingleton() */ void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const { - assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size()); + assert(d_numThreads == d_exprMgrs.size() && + d_exprMgrs.size() == d_smts.size()); for(size_t i = 0; i < d_numThreads; ++i) { string emTag = "thread#" - + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); + + boost::lexical_cast<string>(d_threadOptions[i].getThreadId()); Statistics stats = d_exprMgrs[i]->getStatistics(); stats.setPrefix(emTag); stats.flushInformation(out); string smtTag = "thread#" - + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); + + boost::lexical_cast<string>(d_threadOptions[i].getThreadId()); stats = d_smts[i]->getStatistics(); stats.setPrefix(smtTag); stats.flushInformation(out); diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index ee2b270fb..ce9a80a4e 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -40,7 +40,7 @@ class CommandExecutorPortfolio : public CommandExecutor { // not too hard to support this changing std::vector<SmtEngine*> d_smts; CommandSequence* d_seq; - std::vector<Options>& d_threadOptions; + OptionsList& d_threadOptions; std::vector<ExprManagerMapCollection*> d_vmaps; int d_lastWinner; @@ -57,7 +57,7 @@ class CommandExecutorPortfolio : public CommandExecutor { public: CommandExecutorPortfolio(ExprManager &exprMgr, Options &options, - std::vector<Options>& tOpts); + OptionsList& tOpts); ~CommandExecutorPortfolio(); 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 */ diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 6888d3af5..19e4859b0 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -40,10 +40,7 @@ #include "base/output.h" #include "options/language.h" -#include "options/base_options.h" -#include "options/main_options.h" #include "options/options.h" -#include "options/smt_options.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -92,16 +89,18 @@ static set<string> s_declarations; #endif /* HAVE_LIBREADLINE */ InteractiveShell::InteractiveShell(ExprManager& exprManager, - const Options& options) : - d_in(*options[options::in]), - d_out(*options[options::out]), - d_options(options), - d_quit(false) { + const Options& options) + : d_in(*options.getIn()), + d_out(*options.getOutConst()), + d_options(options), + d_quit(false) +{ ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); - if(d_options.wasSetByUser(options::forceLogic)) { - d_parser->forceLogic(d_options[options::forceLogic]->getLogicString()); + if(d_options.wasSetByUserForceLogicString()) { + LogicInfo tmp(d_options.getForceLogicString()); + d_parser->forceLogic(tmp.getLogicString()); } #if HAVE_LIBREADLINE @@ -114,7 +113,8 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, #endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */ ::using_history(); - switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) { + OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage()); + switch(lang) { case output::LANG_CVC4: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; commandsBegin = cvc_commands; @@ -195,7 +195,8 @@ restart: /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options[options::interactivePrompt] ? (line == "" ? "CVC4> " : "... > ") : ""); + lineBuf = ::readline(d_options.getInteractivePrompt() + ? (line == "" ? "CVC4> " : "... > ") : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -203,7 +204,7 @@ restart: free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - if(d_options[options::interactivePrompt]) { + if(d_options.getInteractivePrompt()) { if(line == "") { d_out << "CVC4> " << flush; } else { @@ -219,7 +220,8 @@ restart: string input = ""; while(true) { - Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; + Debug("interactive") << "Input now '" << input << line << "'" << endl + << flush; assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); @@ -260,7 +262,8 @@ restart: /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); assert(c == '\n'); - Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; + Debug("interactive") << "Next char is '" << (char)c << "'" << endl + << flush; } input += line; @@ -271,7 +274,7 @@ restart: input[n] = '\n'; if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline(d_options[options::interactivePrompt] ? "... > " : ""); + lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -279,7 +282,7 @@ restart: free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - if(d_options[options::interactivePrompt]) { + if(d_options.getInteractivePrompt()) { d_out << "... > " << flush; } @@ -295,7 +298,8 @@ restart: } } - d_parser->setInput(Input::newStringInput(d_options[options::inputLanguage], input, INPUT_FILENAME)); + d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(), + input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ @@ -326,8 +330,8 @@ restart: line += "\n"; goto restart; } catch(ParserException& pe) { - if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_0 || - d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_5) { + if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 || + d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5) { d_out << "(error \"" << pe << "\")" << endl; } else { d_out << pe << endl; diff --git a/src/main/main.cpp b/src/main/main.cpp index 92902ac11..9151d8bf7 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,19 +22,18 @@ #include <stdio.h> #include <unistd.h> +#include "base/configuration.h" #include "base/output.h" #include "expr/expr_manager.h" #include "main/command_executor.h" #include "main/interactive_shell.h" -#include "options/base_options.h" #include "options/language.h" -#include "options/main_options.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" #include "smt/smt_engine.h" #include "smt_util/command.h" -#include "util/configuration.h" #include "util/result.h" #include "util/statistics.h" @@ -56,24 +55,24 @@ int main(int argc, char* argv[]) { return runCvc4(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC4_COMPETITION_MODE - *opts[options::out] << "unknown" << endl; + *opts.getOut() << "unknown" << endl; #endif cerr << "CVC4 Error:" << endl << e << endl << endl << "Please use --help to get help on command-line options." << endl; } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE - *opts[options::out] << "unknown" << endl; + *opts.getOut() << "unknown" << endl; #endif - if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2_0 || - opts[options::outputLanguage] == output::LANG_SMTLIB_V2_5) { - *opts[options::out] << "(error \"" << e << "\")" << endl; + if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 || + opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5) { + *opts.getOut() << "(error \"" << e << "\")" << endl; } else { - *opts[options::err] << "CVC4 Error:" << endl << e << endl; + *opts.getErr() << "CVC4 Error:" << endl << e << endl; } - if(opts[options::statistics] && pExecutor != NULL) { + if(opts.getStatistics() && pExecutor != NULL) { pTotalTime->stop(); - pExecutor->flushStatistics(*opts[options::err]); + pExecutor->flushStatistics(*opts.getErr()); } } exit(1); diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index 1ec0b961c..e42787fea 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -19,45 +19,68 @@ #include <cassert> #include <vector> -#include "options/base_options.h" -#include "options/main_options.h" #include "options/options.h" -#include "options/prop_options.h" -#include "options/smt_options.h" -#include "smt/smt_options_handler.h" using namespace std; namespace CVC4 { -vector<Options> parseThreadSpecificOptions(Options opts) -{ - vector<Options> threadOptions; +OptionsList::OptionsList() : d_options() {} + +OptionsList::~OptionsList(){ + for(std::vector<Options*>::iterator i = d_options.begin(), + iend = d_options.end(); i != iend; ++i) + { + Options* current = *i; + delete current; + } + d_options.clear(); +} + +void OptionsList::push_back_copy(const Options& opts) { + Options* copy = new Options; + copy->copyValues(opts); + d_options.push_back(copy); +} + +Options& OptionsList::operator[](size_t position){ + return *(d_options[position]); +} + +const Options& OptionsList::operator[](size_t position) const { + return *(d_options[position]); +} -#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." - smt::SmtOptionsHandler optionsHandler(NULL); +Options& OptionsList::back() { + return *(d_options.back()); +} - unsigned numThreads = opts[options::threads]; +size_t OptionsList::size() const { + return d_options.size(); +} + +void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts) +{ + + unsigned numThreads = opts.getThreads(); for(unsigned i = 0; i < numThreads; ++i) { - threadOptions.push_back(opts); + threadOptions.push_back_copy(opts); Options& tOpts = threadOptions.back(); // Set thread identifier - tOpts.set(options::thread_id, i); - - if(i < opts[options::threadArgv].size() && - !opts[options::threadArgv][i].empty()) { - + tOpts.setThreadId(i); + const std::vector<std::string>& optThreadArgvs = opts.getThreadArgv(); + if(i < optThreadArgvs.size() && (! optThreadArgvs[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(opts[options::threadArgv][i].c_str()); + char* tbuf = strdup(optThreadArgvs[i].c_str()); char* p = tbuf; // string length is certainly an upper bound on size needed - char** targv = new char*[opts[options::threadArgv][i].size()]; + char** targv = new char*[optThreadArgvs[i].size()]; char** vp = targv; *vp++ = strdup(optid.c_str()); p = strtok(p, " "); @@ -69,7 +92,7 @@ vector<Options> parseThreadSpecificOptions(Options opts) *vp++ = NULL; if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " try { - tOpts.parseOptions(targc, targv, &optionsHandler); + tOpts.parseOptions(targc, targv); } catch(OptionException& e) { stringstream ss; ss << optid << ": " << e.getMessage(); @@ -81,8 +104,8 @@ vector<Options> parseThreadSpecificOptions(Options opts) << "' in thread configuration " << optid << " !"; throw OptionException(ss.str()); } - if(tOpts[options::threads] != numThreads - || tOpts[options::threadArgv] != opts[options::threadArgv]) { + if(tOpts.getThreads() != numThreads || + tOpts.getThreadArgv() != opts.getThreadArgv()) { stringstream ss; ss << "not allowed to set thread options in " << optid << " !"; throw OptionException(ss.str()); @@ -95,12 +118,10 @@ vector<Options> parseThreadSpecificOptions(Options opts) } assert(numThreads >= 1); //do we need this? - - return threadOptions; } void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { - if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { + if(int(lemma.getNumChildren()) > Options::currentGetSharingFilterByLength()) { return; } ++cnt; @@ -109,9 +130,9 @@ void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { try { d_pickler.toPickle(lemma, pkl); d_sharedChannel->push(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: notifyNewLemma: " << lemma - << std::endl; + if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) { + (*(Options::currentGetOut())) + << "thread #0: notifyNewLemma: " << lemma << std::endl; } } catch(expr::pickle::PicklingException& p){ Trace("sharing::blocked") << lemma << std::endl; @@ -137,8 +158,8 @@ Expr PortfolioLemmaInputChannel::getNewLemma() { expr::pickle::Pickle pkl = d_sharedChannel->pop(); Expr e = d_pickler.fromPickle(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: getNewLemma: " << e << std::endl; + if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) { + (*Options::currentGetOut()) << "thread #0: getNewLemma: " << e << std::endl; } return e; } diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 2b1e22754..50cf0060a 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -19,7 +19,6 @@ #include "base/output.h" #include "expr/pickler.h" -#include "options/main_options.h" #include "smt/smt_engine.h" #include "smt_util/lemma_input_channel.h" #include "smt_util/lemma_output_channel.h" @@ -73,7 +72,26 @@ public: };/* class PortfolioLemmaInputChannel */ -std::vector<Options> parseThreadSpecificOptions(Options opts); +class OptionsList { + public: + OptionsList(); + ~OptionsList(); + + void push_back_copy(const Options& options); + + Options& operator[](size_t position); + const Options& operator[](size_t position) const; + + Options& back(); + + size_t size() const; + private: + OptionsList(const OptionsList&) CVC4_UNDEFINED; + OptionsList& operator=(const OptionsList&) CVC4_UNDEFINED; + std::vector<Options*> d_options; +}; + +void parseThreadSpecificOptions(OptionsList& list, const Options& opts); template<typename T> void sharingManager(unsigned numThreads, diff --git a/src/main/util.cpp b/src/main/util.cpp index abcdcc7c5..71b46e67a 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -33,7 +33,6 @@ #include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/main.h" -#include "options/base_options.h" #include "options/options.h" #include "smt/smt_engine.h" #include "util/statistics.h" @@ -42,11 +41,6 @@ using CVC4::Exception; using namespace std; namespace CVC4 { - -#ifdef CVC4_DEBUG -//extern CVC4_THREADLOCAL(const char*) s_debugLastException; -#endif /* CVC4_DEBUG */ - namespace main { /** @@ -64,7 +58,7 @@ void* cvc4StackBase; /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -74,7 +68,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)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -99,7 +93,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) { } if(!segvSpin) { - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -121,7 +115,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)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -134,7 +128,7 @@ void ill_handler(int sig, siginfo_t* info, void*) { #ifdef CVC4_DEBUG fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if(!segvSpin) { - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -149,7 +143,7 @@ void ill_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 executed an illegal instruction.\n"); - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -177,7 +171,7 @@ void cvc4unexpected() { fprintf(stderr, "The exception is:\n%s\n\n", lastContents); } if(!segvSpin) { - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -192,7 +186,7 @@ void cvc4unexpected() { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -211,7 +205,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)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } @@ -220,7 +214,7 @@ void cvc4terminate() { fprintf(stderr, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); - if((*pOptions)[options::statistics] && pExecutor != NULL) { + if(pOptions->getStatistics() && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(cerr); } |