diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-16 19:59:24 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 09:06:31 -0400 |
commit | e5b7840fbcd43c29e709dc3b9ddfb8d60b444ce4 (patch) | |
tree | aeb4d6341237e65d8f10f02cbb611fd013214458 /src/main | |
parent | a86a9bc9198cc5c1bfd538c4e8728f091d114335 (diff) |
Some fixes for tear-down-incremental and "success" output.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.h | 11 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 39 |
2 files changed, 28 insertions, 22 deletions
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); |