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 | |
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')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 23 | ||||
-rw-r--r-- | src/main/options | 4 |
2 files changed, 20 insertions, 7 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); diff --git a/src/main/options b/src/main/options index 9fdef3865..53c04a2c4 100644 --- a/src/main/options +++ b/src/main/options @@ -23,8 +23,6 @@ expert-option earlyExit --early-exit bool :default true do not run destructors at exit; default on except in debug builds # portfolio options -option printWinner bool - enable printing the winning thread (pcvc4 only) option threads --threads=N unsigned :default 2 :predicate greater(0) Total number of threads for portfolio option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h" @@ -37,6 +35,8 @@ option separateOutput bool :default false In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----"). option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write don't share (among portfolio threads) lemmas strictly longer than N +option fallbackSequential --fallback-sequential bool :default false + Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode expert-option waitToJoin --wait-to-join bool :default true wait for other threads to join before quitting |