diff options
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index be1b06cb8..242e018f6 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -39,6 +39,7 @@ namespace CVC4 { const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); +const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); std::ostream& operator<<(std::ostream& out, const Command& c) throw() { c.toStream(out, @@ -97,6 +98,10 @@ bool Command::fail() const throw() { return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL; } +bool Command::interrupted() const throw() { + return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL; +} + void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { invoke(smtEngine); if(!(isMuted() && ok())) { @@ -201,6 +206,8 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->assertFormula(d_expr, d_inUnsatCore); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -224,6 +231,8 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->push(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -247,6 +256,8 @@ void PopCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->pop(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -840,6 +851,8 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->simplify(d_term); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -953,6 +966,8 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { } d_result = em->mkExpr(kind::SEXPR, result); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -1000,6 +1015,8 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getAssignment(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -1043,6 +1060,8 @@ void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { d_result = smtEngine->getModel(); d_smtEngine = smtEngine; d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -1089,6 +1108,8 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getProof(); d_commandStatus = CommandSuccess::instance(); + } catch(UnsafeInterruptException& e) { + d_commandStatus = new CommandInterrupted(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } |