diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 16:00:50 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 20:32:36 -0400 |
commit | c96ca24439e02a1413188b728e5b5c415d398c39 (patch) | |
tree | fd9bf4735f996f411bc711a5b180e25a1bbbe3c0 /src/main | |
parent | 21178e5599464d9d0569ff7989fad9517dd92419 (diff) |
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.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.h | 11 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 20 |
2 files changed, 16 insertions, 15 deletions
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); |