From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 17 Jun 2014 20:00:50 +0000 (-0400)
Subject: Some reversions of recent commits re: portfolio failure.
X-Git-Tag: cvc5-1.0.0~6700^2~13
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c96ca24439e02a1413188b728e5b5c415d398c39;p=cvc5.git

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 082a746c5..18204d3c6 100644
--- 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 50d85d37a..f0541bfae 100644
--- 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 d28f711af..e6e3d3411 100644
--- 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 54f6383ac..0cec616fd 100644
--- 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);