diff options
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 |