diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-01 22:11:26 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-01 22:11:26 +0000 |
commit | 35ac65b0034eacf2766d9e94be1c7fe9c116bb75 (patch) | |
tree | de4a0848b08485fa2d9fa60738e0a47b5c876dc5 /src/main/command_executor_portfolio.cpp | |
parent | 2ee52cf8ccaa2e4514cd0e2023ee71a2b8b8d467 (diff) |
"Fix" (disable) portfolio when using quantifiers
Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index b9bf39002..4867082e6 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -104,13 +104,6 @@ void CommandExecutorPortfolio::lemmaSharingInit() const unsigned int sharingChannelSize = 1000000; for(unsigned i = 0; i < d_numThreads; ++i){ - if(Debug.isOn("channel-empty")) { - d_channelsOut.push_back - (new EmptySharedChannel<ChannelFormat>(sharingChannelSize)); - d_channelsIn.push_back - (new EmptySharedChannel<ChannelFormat>(sharingChannelSize)); - continue; - } d_channelsOut.push_back (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); d_channelsIn.push_back @@ -199,6 +192,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_seq->addCommand(cmd->clone()); return CommandExecutor::doCommandSingleton(cmd); } else if(mode == 1) { // portfolio + + // If quantified, stay sequential + if(d_smts[0]->getLogicInfo().isQuantified()) { + return CommandExecutor::doCommandSingleton(cmd); + } + d_seq->addCommand(cmd->clone()); // We currently don't support changing number of threads for each @@ -271,11 +270,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_lastWinner = portfolioReturn.first; - // *d_options[options::out] - // << "Winner = " - // << portfolioReturn.first - // << std::endl; - if(d_ostringstreams.size() != 0) { assert(d_numThreads == d_options[options::threads]); assert(portfolioReturn.first >= 0); |