1 files changed, 47 insertions, 3 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8b7f1bfa4..5b889712d 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -456,8 +456,9 @@ std::string DeclarationDefinitionCommand::getSymbol() const throw() {
 
 /* class DeclareFunctionCommand */
 
-DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) throw() :
+DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() :
   DeclarationDefinitionCommand(id),
+  d_func(func),
   d_type(t) {
 }
 
@@ -467,17 +468,18 @@ Type DeclareFunctionCommand::getType() const throw() {
 
 void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this;
+  smtEngine->addToModelFunction( d_func );
   d_commandStatus = CommandSuccess::instance();
 }
 
 Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
                                           ExprManagerMapCollection& variableMap) {
-  return new DeclareFunctionCommand(d_symbol,
+  return new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap),
                                     d_type.exportTo(exprManager, variableMap));
 }
 
 Command* DeclareFunctionCommand::clone() const {
-  return new DeclareFunctionCommand(d_symbol, d_type);
+  return new DeclareFunctionCommand(d_symbol, d_func, d_type);
 }
 
 /* class DeclareTypeCommand */
@@ -498,6 +500,7 @@ Type DeclareTypeCommand::getType() const throw() {
 
 void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this;
+  smtEngine->addToModelType( d_type );
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -762,6 +765,47 @@ Command* GetAssignmentCommand::clone() const {
   return c;
 }
 
+/* class GetModelCommand */
+
+GetModelCommand::GetModelCommand() throw() {
+}
+
+void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->getModel();
+    d_smtEngine = smtEngine;
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Model* GetModelCommand::getResult() const throw() {
+  return d_result;
+}
+
+void GetModelCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    d_smtEngine->printModel( out, d_result );
+  }
+}
+
+Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetModelCommand* c = new GetModelCommand();
+  c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
+Command* GetModelCommand::clone() const {
+  GetModelCommand* c = new GetModelCommand();
+  c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
+  return c;
+}
+
 /* class GetProofCommand */
 
 GetProofCommand::GetProofCommand() throw() {