diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
commit | cfa9e2cbbdf77a325791b5548b41093a0781311c (patch) | |
tree | e843d38afe4b197a2dd81316998477cedac26c52 /src/expr/command.h | |
parent | 6935324f45bd7f2c735ca4120a9e800ef8903442 (diff) |
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 11 |
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). |