diff options
Diffstat (limited to 'src/theory/booleans/theory_bool.cpp')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 100 |
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) { |