diff options
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index 98046c242..123fe0182 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -37,6 +37,7 @@ #include "util/sexpr.h" #include "util/datatype.h" #include "util/proof.h" +#include "util/model.h" namespace CVC4 { @@ -316,9 +317,10 @@ public: class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: + Expr d_func; Type d_type; public: - DeclareFunctionCommand(const std::string& id, Type type) throw(); + DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); ~DeclareFunctionCommand() throw() {} Type getType() const throw(); void invoke(SmtEngine* smtEngine) throw(); @@ -462,6 +464,20 @@ public: Command* clone() const; };/* class GetAssignmentCommand */ +class CVC4_PUBLIC GetModelCommand : public Command { +protected: + Model* d_result; + SmtEngine* d_smtEngine; +public: + GetModelCommand() throw(); + ~GetModelCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Model* getResult() const throw(); + void printResult(std::ostream& out) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; +};/* class GetModelCommand */ + class CVC4_PUBLIC GetProofCommand : public Command { protected: Proof* d_result; |