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;