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, 2 insertions, 31 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index e955539d5..fa176243c 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -19,6 +19,7 @@
 #include "theory/builtin/theory_builtin.h"
 #include "theory/valuation.h"
 #include "expr/kind.h"
+#include "theory/model.h"
 
 using namespace std;
 
@@ -26,38 +27,8 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-Node TheoryBuiltin::getValue(TNode n) {
-  switch(n.getKind()) {
+void TheoryBuiltin::collectModelInfo( TheoryModel* m ){
 
-  case kind::VARIABLE:
-    // no variables that the builtin theory is responsible for
-    Unreachable();
-
-  case kind::EQUAL: { // 2 args
-    // has to be an EQUAL over tuples, since all others should be
-    // handled elsewhere
-    Assert(n[0].getKind() == kind::TUPLE &&
-           n[1].getKind() == kind::TUPLE);
-    return NodeManager::currentNM()->
-      mkConst( getValue(n[0]) == getValue(n[1]) );
-  }
-
-  case kind::TUPLE: { // 2+ args
-    NodeBuilder<> nb(kind::TUPLE);
-    for(TNode::iterator i = n.begin(),
-          iend = n.end();
-        i != iend;
-        ++i) {
-      nb << d_valuation.getValue(*i);
-    }
-    return Node(nb);
-  }
-
-  default:
-    // all other "builtins" should have been rewritten away or handled
-    // by the valuation, or handled elsewhere.
-    Unhandled(n.getKind());
-  }
 }
 
 }/* CVC4::theory::builtin namespace */