--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.)

4 files changed, 22 insertions, 9 deletions

diff --git a/INSTALL b/INSTALL
index f914f4fe9..a9986a073 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,4 +1,4 @@
- is CVC4 release version 1.0.
+CVC4 release version 1.0.
 
 *** Quick-start instructions
 
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
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index e0ab047ab..4c30f6841 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -763,7 +763,7 @@ void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp
     int counter = 0;
     for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
       Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i );
-      if( counter<f[0].getNumChildren() ){
+      if( (int)counter< (int)f[0].getNumChildren() ){
         if( fp[0][i]==f[0][counter] ){
           Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter );
           Node n = m.getValue( ic );