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.

1 files changed, 67 insertions, 14 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 08e335717..4cccb8d10 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -59,6 +59,7 @@
 #include "theory/theory_traits.h"
 #include "theory/logic_info.h"
 #include "util/ite_removal.h"
+#include "theory/model.h"
 
 using namespace std;
 using namespace CVC4;
@@ -743,7 +744,8 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
     } else if(key == ":produce-unsat-cores") {
       throw BadOptionException();
     } else if(key == ":produce-models") {
-      throw BadOptionException();
+      //throw BadOptionException();
+      const_cast<Options*>( Options::s_current )->produceModels = true;
     } else if(key == ":produce-assignments") {
       throw BadOptionException();
     } else {
@@ -935,7 +937,7 @@ void SmtEnginePrivate::removeITEs() {
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
     d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]);
   }
-  
+
 }
 
 void SmtEnginePrivate::staticLearning() {
@@ -1467,7 +1469,7 @@ void SmtEnginePrivate::processAssertions() {
         expandDefinitions(d_assertionsToPreprocess[i], cache);
     }
   }
-    
+
   // Apply the substitutions we already have, and normalize
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "applying substitutions" << endl;
@@ -1766,16 +1768,15 @@ Expr SmtEngine::getValue(const Expr& e)
     throw ModalException(msg);
   }
   if(d_status.isNull() ||
-     d_status.asSatisfiabilityResult() != Result::SAT ||
+     d_status.asSatisfiabilityResult() == Result::UNSAT ||
      d_problemExtended) {
     const char* msg =
-      "Cannot get value unless immediately preceded by SAT/INVALID response.";
+      "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
-  if(type.isFunction() || type.isPredicate() ||
-     type.isKind() || type.isSortConstructor()) {
+  if(type.isKind() || type.isSortConstructor()) {
     const char* msg =
-      "Cannot get value of a function, predicate, or sort.";
+      "Cannot get value of a sort.";
     throw ModalException(msg);
   }
 
@@ -1786,10 +1787,14 @@ Expr SmtEngine::getValue(const Expr& e)
   n = Rewriter::rewrite(n);
 
   Trace("smt") << "--- getting value of " << n << endl;
-  Node resultNode = d_theoryEngine->getValue(n);
-
+  theory::TheoryModel* m = d_theoryEngine->getModel();
+  Node resultNode;
+  if( m ){
+    resultNode = m->getValue( n );
+  }
+  Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
   // type-check the result we got
-  Assert(resultNode.isNull() || resultNode.getType() == n.getType());
+  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf( n.getType() ));
   return Expr(d_exprManager, new Node(resultNode));
 }
 
@@ -1835,11 +1840,11 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
     throw ModalException(msg);
   }
   if(d_status.isNull() ||
-     d_status.asSatisfiabilityResult() != Result::SAT ||
+     d_status.asSatisfiabilityResult() == Result::UNSAT  ||
      d_problemExtended) {
     const char* msg =
       "Cannot get the current assignment unless immediately "
-      "preceded by SAT/INVALID response.";
+      "preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
 
@@ -1859,7 +1864,11 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
     Node n = Rewriter::rewrite(*i);
 
     Trace("smt") << "--- getting value of " << n << endl;
-    Node resultNode = d_theoryEngine->getValue(n);
+    theory::TheoryModel* m = d_theoryEngine->getModel();
+    Node resultNode;
+    if( m ){
+      resultNode = m->getValue( n );
+    }
 
     // type-check the result we got
     Assert(resultNode.isNull() || resultNode.getType() == boolType);
@@ -1878,6 +1887,45 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   return SExpr(sexprs);
 }
 
+
+void SmtEngine::addToModelType( Type& t ){
+  Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
+  NodeManagerScope nms(d_nodeManager);
+  if( Options::current()->produceModels ) {
+    d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
+  }
+}
+
+void SmtEngine::addToModelFunction( Expr& e ){
+  Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
+  NodeManagerScope nms(d_nodeManager);
+  if( Options::current()->produceModels ) {
+    d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
+  }
+}
+
+
+Model* SmtEngine::getModel() throw(ModalException, AssertionException){
+  Trace("smt") << "SMT getModel()" << endl;
+  NodeManagerScope nms(d_nodeManager);
+
+  if(!Options::current()->produceModels) {
+    const char* msg =
+      "Cannot get value when produce-models options is off.";
+    throw ModalException(msg);
+  }
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() == Result::UNSAT  ||
+     d_problemExtended) {
+    const char* msg =
+      "Cannot get the current model unless immediately "
+      "preceded by SAT/INVALID or UNKNOWN response.";
+    throw ModalException(msg);
+  }
+
+  return d_theoryEngine->getModel();
+}
+
 Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getProof()" << endl;
   NodeManagerScope nms(d_nodeManager);
@@ -2063,4 +2111,9 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
   return d_exprManager->d_nodeManager->getStatisticsRegistry();
 }
 
+void SmtEngine::printModel( std::ostream& out, Model* m ){
+  NodeManagerScope nms(d_nodeManager);
+  m->toStream(out);
+}
+
 }/* CVC4 namespace */