diff options
| -rwxr-xr-x | contrib/run-script-smtcomp2014-application | 2 | ||||
| -rw-r--r-- | src/main/command_executor.h | 11 | ||||
| -rw-r--r-- | src/main/driver_unified.cpp | 39 |
3 files changed, 29 insertions, 23 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index b04b33775..2decdb98a 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -9,7 +9,7 @@ function runcvc4 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" + cat "$bench" | $cvc4 -L smt2 --print-success --no-checking --no-interactive --no-incremental --tear-down-incremental "$@" } case "$logic" in diff --git a/src/main/command_executor.h b/src/main/command_executor.h index e6e3d3411..d28f711af 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -52,6 +52,17 @@ 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 9215c6073..c39627550 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -269,18 +269,14 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(opts[options::interactive] && inputFromStdin) { if(opts[options::tearDownIncremental] && opts[options::incrementalSolving]) { if(opts.wasSetByUser(options::incrementalSolving)) { - throw OptionException("--tear-down-incremental incompatible with --interactive"); + throw OptionException("--tear-down-incremental incompatible with --incremental"); } - cmd = new SetOptionCommand("incremental", false); - pExecutor->doCommand(cmd); - delete cmd; + pExecutor->setOption("incremental", false); } #ifndef PORTFOLIO_BUILD if(!opts.wasSetByUser(options::incrementalSolving)) { - cmd = new SetOptionCommand("incremental", true); - pExecutor->doCommand(cmd); - delete cmd; + pExecutor->setOption("incremental", true); } #endif /* PORTFOLIO_BUILD */ InteractiveShell shell(*exprMgr, opts); @@ -308,12 +304,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if(opts[options::tearDownIncremental]) { if(opts[options::incrementalSolving]) { if(opts.wasSetByUser(options::incrementalSolving)) { - throw OptionException("--tear-down-incremental incompatible with --interactive"); + throw OptionException("--tear-down-incremental incompatible with --incremental"); } - cmd = new SetOptionCommand("incremental", false); - pExecutor->doCommand(cmd); - delete cmd; + pExecutor->setOption("incremental", false); } ParserBuilder parserBuilder(exprMgr, filename, opts); @@ -338,7 +332,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); - bool succ = opts[options::printSuccess]; + bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]); + Command::printsuccess::setPrintSuccess(*opts[options::out], false); opts.set(options::printSuccess, false); for(size_t i = 0; i < allCommands.size(); ++i) { for(size_t j = 0; j < allCommands[i].size(); ++j) { @@ -347,15 +342,16 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } } - opts.set(options::printSuccess, succ); + Command::printsuccess::setPrintSuccess(*opts[options::out], succ); needReset = false; } + *opts[options::out] << CommandSuccess(); allCommands.push_back(vector<Command*>()); } else if(dynamic_cast<PopCommand*>(cmd) != NULL) { allCommands.pop_back(); // fixme leaks cmds here pExecutor->reset(); - bool succ = opts[options::printSuccess]; - opts.set(options::printSuccess, false); + bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]); + Command::printsuccess::setPrintSuccess(*opts[options::out], false); for(size_t i = 0; i < allCommands.size(); ++i) { for(size_t j = 0; j < allCommands[i].size(); ++j) { Command* cmd = allCommands[i][j]->clone(); @@ -363,13 +359,14 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } } - opts.set(options::printSuccess, succ); + Command::printsuccess::setPrintSuccess(*opts[options::out], succ); + *opts[options::out] << CommandSuccess(); } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || dynamic_cast<QueryCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); - bool succ = opts[options::printSuccess]; - opts.set(options::printSuccess, false); + bool succ = Command::printsuccess::getPrintSuccess(*opts[options::out]); + Command::printsuccess::setPrintSuccess(*opts[options::out], false); for(size_t i = 0; i < allCommands.size(); ++i) { for(size_t j = 0; j < allCommands[i].size(); ++j) { Command* cmd = allCommands[i][j]->clone(); @@ -377,7 +374,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } } - opts.set(options::printSuccess, succ); + Command::printsuccess::setPrintSuccess(*opts[options::out], succ); } status = pExecutor->doCommand(cmd); needReset = true; @@ -395,9 +392,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete parser; } else { if(!opts.wasSetByUser(options::incrementalSolving)) { - cmd = new SetOptionCommand("incremental", false); - pExecutor->doCommand(cmd); - delete cmd; + pExecutor->setOption("incremental", false); } ParserBuilder parserBuilder(exprMgr, filename, opts); |