diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-15 22:41:03 +0000 |
commit | c00efa92e9d61d808a8346e1d8bb3523e24d8ee2 (patch) | |
tree | 85ecfd0e8770ef539f36ec04afd34a583e75cf38 /src/expr/command.h | |
parent | c09fae89b38b525c6e2ab1691be4363d0cb1157b (diff) |
minor interface improvements, compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index 70e71a111..5786f4e71 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -475,6 +475,21 @@ public: Command* clone() const; };/* class SimplifyCommand */ +class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { +protected: + Expr d_term; + Expr d_result; +public: + ExpandDefinitionsCommand(Expr term) throw(); + ~ExpandDefinitionsCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class ExpandDefinitionsCommand */ + class CVC4_PUBLIC GetValueCommand : public Command { protected: std::vector<Expr> d_terms; @@ -531,6 +546,18 @@ public: Command* clone() const; };/* class GetProofCommand */ +class CVC4_PUBLIC GetUnsatCoreCommand : public Command { +protected: + //UnsatCore* d_result; +public: + GetUnsatCoreCommand() throw(); + ~GetUnsatCoreCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class GetUnsatCoreCommand */ + class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; |