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.h11
1 files changed, 10 insertions, 1 deletions
diff --git a/src/expr/command.h b/src/expr/command.h
index 0f517e7f2..3c919c374 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -50,6 +50,14 @@ std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
+class ExportToUnsupportedException : public Exception {
+public:
+ ExportToUnsupportedException() throw() :
+ Exception("exportTo unsupported for command") {
+ }
+};/* class NoMoreValuesException */
+
+
/** The status an SMT benchmark can have */
enum BenchmarkStatus {
/** Benchmark is satisfiable */
@@ -233,7 +241,8 @@ public:
* variableMap for the translation and extending it with any new
* mappings.
*/
- virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0;
+ virtual Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) = 0;
/**
* Clone this Command (make a shallow copy).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback