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.

2 files changed, 64 insertions, 4 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() {
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;