From 65798541fa437278cde0c759ab70fd9fa4fe9638 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Jul 2012 18:30:15 +0000
Subject: merged fmf-devel branch, includes support for SMT2 command get-value
 and (extended) SMT command get-model.  added collectModelInfo and removed
 getValue from theory interface.  merge also includes major updates to finite
 model finding module (from CASC), added fmf options, some updates to strong
 solver and quantifiers engine interface.  The test recursion_breaker_black
 currently fails for me on production builds, Morgan is planning to look into
 this.

---
 src/expr/command.cpp | 50 +++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 47 insertions(+), 3 deletions(-)

(limited to 'src/expr/command.cpp')

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() {
-- 
cgit v1.2.3