diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-19 00:56:11 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-19 00:56:11 +0000 |
commit | 28af31bf1efff6fc143da3a9db9996162c2befab (patch) | |
tree | 0d2648eaf6b4793c7faf39a99a9b308910d2c046 /src/main/command_executor_portfolio.cpp | |
parent | 7f10c78f572debd0ddf717bfb9f9453a42c015cb (diff) |
--fallback-sequential / --no-fallback-sequential option
closes bug 419, fix typo, fix warning
(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 | 23 |
1 files changed, 18 insertions, 5 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 9f9c270a8..883989fb0 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -195,7 +195,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) LogicInfo logicInfo = d_smts[0]->getLogicInfo(); logicInfo.lock(); if(logicInfo.isQuantified()) { - return CommandExecutor::doCommandSingleton(cmd); + if(d_options[options::fallbackSequential]) + return CommandExecutor::doCommandSingleton(cmd); + else + throw Exception("Quantified formulas are (currenltly) unsupported in portfolio mode.\n" + "Please see option --fallback-sequential to make this a soft error."); } d_seq->addCommand(cmd->clone()); @@ -221,7 +225,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) try { seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); }catch(ExportUnsupportedException& e){ - return CommandExecutor::doCommandSingleton(cmd); + if(d_options[options::fallbackSequential]) + 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."); } } @@ -285,9 +293,14 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) return portfolioReturn.second; } else if(mode == 2) { - return smtEngineInvoke(d_smts[d_lastWinner], - cmd, - d_threadOptions[d_lastWinner][options::out]); + Command* cmdExported = + d_lastWinner == 0 ? + cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); + int ret = smtEngineInvoke(d_smts[d_lastWinner], + cmdExported, + d_threadOptions[d_lastWinner][options::out]); + if(d_lastWinner != 0) delete cmdExported; + return ret; } else { // Unreachable(); assert(false); |