Some reversions of recent commits re: portfolio failure.

* Partial reversion of b8e28a7, do it a different way.

* Revert "Test portfolio with --no-wait-to-join."
  This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c.

diff --git a/.travis.yml b/.travis.yml
index 082a746c57bede5c33436839a95edfc44cc7995d..18204d3c6923eca209d24eeef863b7ab464c1be8 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -43,7 +43,7 @@ script:
      make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
    }
    makeCheckPortfolio() {
-     make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-wait-to-join --no-early-exit' RUN_REGRESSION_ARGS= ||
+     make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= ||
        error "PORTFOLIO TEST FAILED";
    }
    makeExamples() {

diff --git a/Makefile b/Makefile
index 50d85d37ab114a9e6d194efeb519e5d2d376f9b0..f0541bfae2b06d6a6d6d4e678c5289552a9fb20d 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -161,7 +161,7 @@ submission-parallel:
          ../../configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl; \
          $(MAKE) V=1; \
          strip src/main/pcvc4; \
-         $(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-wait-to-join' || true )
+         $(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS=--fallback-sequential || true )
        # package the parallel track zipfile
        mkdir -p cvc4-smtcomp-parallel-$(YEAR)/bin
        cp -p builds-smtcomp/parallel/src/main/pcvc4 cvc4-smtcomp-parallel-$(YEAR)/bin/pcvc4

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index d28f711af258dc167d633fb50e014ca4447954da..e6e3d3411786d42bbfb59d96d76c9ccd86c1b69c 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -52,17 +52,6 @@ public:
    */
   bool doCommand(CVC4::Command* cmd);
 
-  /**
-   * Allow one to set an option on the underlying SmtEngine.
-   * This could be done with a Command object, but then it's
-   * interpreted as a user command (and might result in "success"
-   * or "error" output, for example.  This function can throw
-   * exceptions.
-   */
-  void setOption(const std::string& key, const CVC4::SExpr& value) {
-    d_smtEngine->setOption(key, value);
-  }
-
   Result getResult() const { return d_result; }
   void reset();
 

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 54f6383ac71fe4e5f5845129ab3576a317d3e9cd..0cec616fdcfdc83d47b1f33ee8ad202b00ae4b02 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -272,11 +272,17 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           throw OptionException("--tear-down-incremental incompatible with --incremental");
         }
 
-        pExecutor->setOption("incremental", false);
+        cmd = new SetOptionCommand("incremental", false);
+        cmd->setMuted(true);
+        pExecutor->doCommand(cmd);
+        delete cmd;
       }
 #ifndef PORTFOLIO_BUILD
       if(!opts.wasSetByUser(options::incrementalSolving)) {
-        pExecutor->setOption("incremental", true);
+        cmd = new SetOptionCommand("incremental", true);
+        cmd->setMuted(true);
+        pExecutor->doCommand(cmd);
+        delete cmd;
       }
 #endif /* PORTFOLIO_BUILD */
       InteractiveShell shell(*exprMgr, opts);
@@ -307,7 +313,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           throw OptionException("--tear-down-incremental incompatible with --incremental");
         }
 
-        pExecutor->setOption("incremental", false);
+        cmd = new SetOptionCommand("incremental", false);
+        cmd->setMuted(true);
+        pExecutor->doCommand(cmd);
+        delete cmd;
       }
 
       ParserBuilder parserBuilder(exprMgr, filename, opts);
@@ -386,7 +395,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       delete parser;
     } else {
       if(!opts.wasSetByUser(options::incrementalSolving)) {
-        pExecutor->setOption("incremental", false);
+        cmd = new SetOptionCommand("incremental", false);
+        cmd->setMuted(true);
+        pExecutor->doCommand(cmd);
+        delete cmd;
       }
 
       ParserBuilder parserBuilder(exprMgr, filename, opts);