diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-28 22:46:09 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-28 22:46:09 +0000 |
commit | 589bf879f00d2d8df4ccdaf3db28674ce3639512 (patch) | |
tree | 467b33e449ff47556388707000ab6b1edfb70411 /src/main | |
parent | 730ea7d49ae56f8674e63ac9085adf06b6adf6f5 (diff) |
Some fixes to portfolio
* respect output lang
* fix export variable for BOUND_VARIABLE
* support export of SUBRANGE_TYPE
* statistic for lastWinner, other minor stat changes
* fix running of multiple threads on checsat/query
* changes of Assert -> assert which became private
* fix some destruction time order issues
* fix Pickler with AssertionException going private
Fixed by not fixing:
* portfolio+datatypes does not work
- added ExportUnsupportedException to more places, switches
to sequential
(still TODO / decide : not switch silently, but print error)
> note: this exception now needs to be (and is) defined in expr.h
Known issues:
* problems in portfolio+quantifiers
- at least some problems appear to be because of static variables
(will be later "fixed" like the datatypes)
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.h | 6 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 69 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.h | 3 | ||||
-rw-r--r-- | src/main/portfolio_util.cpp | 3 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 4 |
5 files changed, 46 insertions, 39 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 435299ce3..a5bd78abe 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -38,14 +38,8 @@ protected: StatisticsRegistry d_stats; public: - // Note: though the options are not cached (instead a reference is - // used), the portfolio command executer currently parses them - // during initalization, creating thread-specific options and - // storing them CommandExecutor(ExprManager &exprMgr, Options &options); - ~CommandExecutor() {} - /** * Executes a command. Recursively handles if cmd is a command * sequence. Eventually uses doCommandSingleton (which can be diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 32a507d78..b9bf39002 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -48,9 +48,13 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_lastWinner(0), d_channelsOut(), d_channelsIn(), - d_ostringstreams() + d_ostringstreams(), + d_statLastWinner("portfolio::lastWinner") { - Assert(d_threadOptions.size() == d_numThreads); + assert(d_threadOptions.size() == d_numThreads); + + d_statLastWinner.setData(d_lastWinner); + d_stats.registerStat_(&d_statLastWinner); /* Duplication, Individualisation */ d_exprMgrs.push_back(&d_exprMgr); @@ -64,7 +68,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_smts.push_back(new SmtEngine(d_exprMgrs[i])); } - Assert(d_vmaps.size() == 0); + assert(d_vmaps.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { d_vmaps.push_back(new ExprManagerMapCollection()); } @@ -72,15 +76,15 @@ CommandExecutorPortfolio::CommandExecutorPortfolio CommandExecutorPortfolio::~CommandExecutorPortfolio() { - Assert(d_seq != NULL); + assert(d_seq != NULL); delete d_seq; - Assert(d_smts.size() == d_numThreads); + assert(d_smts.size() == d_numThreads); for(unsigned i = 1; i < d_numThreads; ++i) { // the 0-th one is responsibility of parent class - delete d_exprMgrs[i]; delete d_smts[i]; + delete d_exprMgrs[i]; } d_exprMgrs.clear(); d_smts.clear(); @@ -89,8 +93,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio() void CommandExecutorPortfolio::lemmaSharingInit() { /* Sharing channels */ - Assert(d_channelsIn.size() == 0); - Assert(d_channelsOut.size() == 0); + assert(d_channelsIn.size() == 0); + assert(d_channelsOut.size() == 0); if(d_numThreads == 1) { // Disable sharing @@ -130,10 +134,14 @@ void CommandExecutorPortfolio::lemmaSharingInit() /* Output to string stream */ if(d_options[options::verbosity] == 0 || d_options[options::separateOutput]) { - Assert(d_ostringstreams.size() == 0); + 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]); + + // important even for muzzled builds (to get result output right) + *d_threadOptions[i][options::out] + << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]); } } } @@ -141,11 +149,11 @@ void CommandExecutorPortfolio::lemmaSharingInit() void CommandExecutorPortfolio::lemmaSharingCleanup() { - Assert(d_numThreads == d_options[options::threads]); + assert(d_numThreads == d_options[options::threads]); // Channel cleanup - Assert(d_channelsIn.size() == d_numThreads); - Assert(d_channelsOut.size() == d_numThreads); + assert(d_channelsIn.size() == d_numThreads); + assert(d_channelsOut.size() == d_numThreads); for(unsigned i = 0; i < d_numThreads; ++i) { delete d_channelsIn[i]; delete d_channelsOut[i]; @@ -157,7 +165,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() // sstreams cleanup (if used) if(d_ostringstreams.size() != 0) { - Assert(d_ostringstreams.size() == d_numThreads); + assert(d_ostringstreams.size() == d_numThreads); for(unsigned i = 0; i < d_numThreads; ++i) { d_threadOptions[i].set(options::out, d_options[options::out]); delete d_ostringstreams[i]; @@ -180,12 +188,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // mode = 1 : run a porfolio // mode = 2 : run the last winner - // if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || - // dynamic_cast<QueryCommand*>(cmd) != NULL) { - // mode = 1; - // } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) { - // mode = 2; - // } + if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || + dynamic_cast<QueryCommand*>(cmd) != NULL) { + mode = 1; + } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) { + mode = 2; + } if(mode == 0) { d_seq->addCommand(cmd->clone()); @@ -213,7 +221,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) */ try { seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); - }catch(ExportToUnsupportedException& e){ + }catch(ExportUnsupportedException& e){ return CommandExecutor::doCommandSingleton(cmd); } } @@ -244,9 +252,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) ); } - Assert(d_channelsIn.size() == d_numThreads); - Assert(d_channelsOut.size() == d_numThreads); - Assert(d_smts.size() == d_numThreads); + assert(d_channelsIn.size() == d_numThreads); + assert(d_channelsOut.size() == d_numThreads); + assert(d_smts.size() == d_numThreads); boost::function<void()> smFn = boost::bind(sharingManager<ChannelFormat>, d_numThreads, @@ -269,9 +277,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // << std::endl; if(d_ostringstreams.size() != 0) { - Assert(d_numThreads == d_options[options::threads]); - Assert(portfolioReturn.first >= 0); - Assert(unsigned(portfolioReturn.first) < d_numThreads); + assert(d_numThreads == d_options[options::threads]); + assert(portfolioReturn.first >= 0); + assert(unsigned(portfolioReturn.first) < d_numThreads); *d_options[options::out] << d_ostringstreams[portfolioReturn.first]->str(); @@ -286,7 +294,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) cmd, d_threadOptions[d_lastWinner][options::out]); } else { - Unreachable(); + // Unreachable(); + assert(false); } }/* CommandExecutorPortfolio::doCommandSingleton() */ @@ -297,15 +306,15 @@ std::string CommandExecutorPortfolio::getSmtEngineStatus() } 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 = "ExprManager thread #" + string emTag = "thread#" + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); Statistics stats = d_exprMgrs[i]->getStatistics(); stats.setPrefix(emTag); stats.flushInformation(out); - string smtTag = "SmtEngine thread #" + string smtTag = "thread#" + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); stats = d_smts[i]->getStatistics(); stats.setPrefix(smtTag); diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index 72a677789..867b62d31 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -52,6 +52,9 @@ class CommandExecutorPortfolio : public CommandExecutor { std::vector< SharedChannel<ChannelFormat>* > d_channelsIn; std::vector<std::ostringstream*> d_ostringstreams; + // Stats + ReferenceStat<int> d_statLastWinner; + public: CommandExecutorPortfolio(ExprManager &exprMgr, Options &options, diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index b208b2479..b16ac2d34 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -14,6 +14,7 @@ ** \brief Code relevant only for portfolio builds **/ +#include <cassert> #include <vector> #include <unistd.h> #include "options/options.h" @@ -97,7 +98,7 @@ vector<Options> parseThreadSpecificOptions(Options opts) } } - Assert(numThreads >= 1); //do we need this? + assert(numThreads >= 1); //do we need this? return threadOptions; } diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 1955a29a7..416b9f44a 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -155,7 +155,7 @@ void sharingManager(unsigned numThreads, /* Alert if channel full, so that we increase sharingChannelSize or decrease sharingBroadcastInterval */ - Assert(not channelsOut[t]->full()); + assert(not channelsOut[t]->full()); T data = channelsOut[t]->pop(); @@ -177,7 +177,7 @@ void sharingManager(unsigned numThreads, for(unsigned t = 0; t < numThreads; ++t){ /* Alert if channel full, so that we increase sharingChannelSize or decrease sharingBroadcastInterval */ - Assert(not channelsIn[t]->full()); + assert(not channelsIn[t]->full()); while(!queues[t].empty() && !channelsIn[t]->full()){ Trace("sharing") << "sharing: pushing on channel " << t << std::endl; |