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, 1 insertions, 99 deletions

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 520adc228..f096987db 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -32,106 +32,8 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-Node TheoryBool::getValue(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
+void TheoryBool::collectModelInfo( TheoryModel* m ){
 
-  switch(n.getKind()) {
-  case kind::VARIABLE:
-    // case for Boolean vars is implemented in TheoryEngine (since it
-    // appeals to the PropEngine to get the value)
-    Unreachable();
-
-  case kind::EQUAL: // 2 args
-    // should be handled by IFF
-    Unreachable();
-
-  case kind::NOT: { // 1 arg
-    Node v = d_valuation.getValue(n[0]);
-    return v.isNull() ? Node::null() : nodeManager->mkConst(! v.getConst<bool>());
-  }
-
-  case kind::AND: { // 2+ args
-    bool foundNull = false;
-    for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
-      Node v = d_valuation.getValue(*i);
-      if(v.isNull()) {
-        foundNull = true;
-      } else if(! v.getConst<bool>()) {
-        return nodeManager->mkConst(false);
-      }
-    }
-    return foundNull ? Node::null() : nodeManager->mkConst(true);
-  }
-
-  case kind::IFF: { // 2 args
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    if(v0.isNull() || v1.isNull()) {
-      return Node::null();
-    }
-    return nodeManager->mkConst( v0.getConst<bool>() == v1.getConst<bool>() );
-  }
-
-  case kind::IMPLIES: { // 2 args
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    if(v0.isNull() && v1.isNull()) {
-      return Node::null();
-    }
-    bool value = false;
-    if(! v0.isNull()) {
-      value = value || (! v0.getConst<bool>());
-    }
-    if(! v1.isNull()) {
-      value = value || v1.getConst<bool>();
-    }
-    return nodeManager->mkConst(value);
-  }
-
-  case kind::OR: { // 2+ args
-    bool foundNull = false;
-    for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
-      Node v = d_valuation.getValue(*i);
-      if(v.isNull()) {
-        foundNull = true;
-      } else if(v.getConst<bool>()) {
-        return nodeManager->mkConst(true);
-      }
-    }
-    return foundNull ? Node::null() : nodeManager->mkConst(false);
-  }
-
-  case kind::XOR: { // 2 args
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    if(v0.isNull() || v1.isNull()) {
-      return Node::null();
-    }
-    return nodeManager->mkConst( v0.getConst<bool>() != v1.getConst<bool>() );
-  }
-
-  case kind::ITE: { // 3 args
-    // all ITEs should be gone except (bool,bool,bool) ones
-    Assert( n[1].getType() == nodeManager->booleanType() &&
-            n[2].getType() == nodeManager->booleanType() );
-    Node v0 = d_valuation.getValue(n[0]);
-    Node v1 = d_valuation.getValue(n[1]);
-    Node v2 = d_valuation.getValue(n[2]);
-    if(v0.isNull()) {
-      return v1 == v2 ? v1 : Node::null();
-    }
-    return nodeManager->mkConst( v0.getConst<bool>() ? v1.getConst<bool>() : v2.getConst<bool>() );
-  }
-
-  default:
-    Unhandled(n.getKind());
-  }
 }
 
 Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {