diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/util/unsafe_interrupt_exception.h | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/util/unsafe_interrupt_exception.h')
-rw-r--r-- | src/util/unsafe_interrupt_exception.h | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h new file mode 100644 index 000000000..e19fc37ce --- /dev/null +++ b/src/util/unsafe_interrupt_exception.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file modal_exception.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An exception that is thrown when the solver is out of time/resources + ** and is interrupted in an unsafe state + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H +#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC UnsafeInterruptException : public CVC4::Exception { +public: + UnsafeInterruptException() : + Exception("Interrupted in unsafe state due to " + "time/resource limit.") { + } + + UnsafeInterruptException(const std::string& msg) : + Exception(msg) { + } + + UnsafeInterruptException(const char* msg) : + Exception(msg) { + } +};/* class UnsafeInterruptException */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */ |