diff options
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 89 |
1 files changed, 80 insertions, 9 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index df71f13c9..9035ed8b8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -298,8 +298,21 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the declarations input interactively replayParser->useDeclarationsFrom(shell.getParser()); } - while((cmd = shell.readCommand())) { + + while(true) { + try { + cmd = shell.readCommand(); + } catch(UnsafeInterruptException& e) { + *opts[options::out] << CommandInterrupted(); + break; + } + if (cmd == NULL) + break; status = pExecutor->doCommand(cmd) && status; + if (cmd->interrupted()) { + delete cmd; + break; + } delete cmd; } } else if(opts[options::tearDownIncremental]) { @@ -332,15 +345,34 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(parser); } bool needReset = false; - while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { + // true if one of the commands was interrupted + bool interrupted = false; + while (status || opts[options::continuedExecution]) { + if (interrupted) { + *opts[options::out] << CommandInterrupted(); + break; + } + + try { + cmd = parser->nextCommand(); + if (cmd == NULL) break; + } catch (UnsafeInterruptException& e) { + interrupted = true; + continue; + } + if(dynamic_cast<PushCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + if (interrupted) break; + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } @@ -351,29 +383,44 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if(dynamic_cast<PopCommand*>(cmd) != NULL) { allCommands.pop_back(); // fixme leaks cmds here pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } + if (interrupted) continue; *opts[options::out] << CommandSuccess(); } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || dynamic_cast<QueryCommand*>(cmd) != NULL) { if(needReset) { pExecutor->reset(); - for(size_t i = 0; i < allCommands.size(); ++i) { - for(size_t j = 0; j < allCommands[i].size(); ++j) { + for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { + for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { Command* cmd = allCommands[i][j]->clone(); cmd->setMuted(true); pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + } delete cmd; } } } + if (interrupted) { + continue; + } + status = pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + continue; + } needReset = true; } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) { pExecutor->doCommand(cmd); @@ -396,6 +443,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { allCommands.back().push_back(copy); } status = pExecutor->doCommand(cmd); + if(cmd->interrupted()) { + interrupted = true; + continue; + } + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; break; @@ -428,8 +480,27 @@ int runCvc4(int argc, char* argv[], Options& opts) { // have the replay parser use the file's declarations replayParser->useDeclarationsFrom(parser); } - while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) { + bool interrupted = false; + while(status || opts[options::continuedExecution]) { + if (interrupted) { + *opts[options::out] << CommandInterrupted(); + pExecutor->reset(); + break; + } + try { + cmd = parser->nextCommand(); + if (cmd == NULL) break; + } catch (UnsafeInterruptException& e) { + interrupted = true; + continue; + } + status = pExecutor->doCommand(cmd); + if (cmd->interrupted() && status == 0) { + interrupted = true; + break; + } + if(dynamic_cast<QuitCommand*>(cmd) != NULL) { delete cmd; break; |