diff options
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 96c7cfadf..4255e3454 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -132,6 +132,19 @@ public: friend class ExprManager; };/* class TypeCheckingException */ +/** + * Exception thrown in case of failure to export + */ +class CVC4_PUBLIC ExportUnsupportedException : public Exception { +public: + ExportUnsupportedException() throw(): + Exception("export unsupported") { + } + ExportUnsupportedException(const char* msg) throw(): + Exception(msg) { + } +};/* class DatatypeExportUnsupportedException */ + std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) CVC4_PUBLIC; |