From c96ca24439e02a1413188b728e5b5c415d398c39 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Jun 2014 16:00:50 -0400 Subject: [PATCH] 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. --- .travis.yml | 2 +- Makefile | 2 +- src/main/command_executor.h | 11 ----------- src/main/driver_unified.cpp | 20 ++++++++++++++++---- 4 files changed, 18 insertions(+), 17 deletions(-) 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); -- 2.30.2