summaryrefslogtreecommitdiff
path: root/src/expr/command.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/command.h')
-rw-r--r--src/expr/command.h12
1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/command.h b/src/expr/command.h
index c4f2fc1bc..cfa00bff4 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -168,6 +168,13 @@ public:
CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
};/* class CommandSuccess */
+class CVC4_PUBLIC CommandInterrupted : public CommandStatus {
+ static const CommandInterrupted* s_instance;
+public:
+ static const CommandInterrupted* instance() throw() { return s_instance; }
+ CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); }
+};/* class CommandInterrupted */
+
class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
public:
CommandStatus& clone() const { return *new CommandUnsupported(*this); }
@@ -240,6 +247,11 @@ public:
*/
bool fail() const throw();
+ /**
+ * The command was ran but was interrupted due to resource limiting.
+ */
+ bool interrupted() const throw();
+
/** Get the command status (it's NULL if we haven't run yet). */
const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback