diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-09 04:24:15 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-09 04:24:15 +0000 |
commit | 97668b64994c5749a5a75822136de49841d2c15d (patch) | |
tree | 23dd1852741a847f6228cc063b0a5ad7ec3c2af3 /src/theory/booleans/theory_bool.cpp | |
parent | e63abd23b45a078a42cafb277a4817abb4d044a1 (diff) |
Model generation for arith, boolean, and uf theories via
(get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work). Closes bug #213.
Diffstat (limited to 'src/theory/booleans/theory_bool.cpp')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 66 |
1 files changed, 65 insertions, 1 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index a7e343fdc..b1ff472ac 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,12 +18,12 @@ #include "theory/theory.h" #include "theory/booleans/theory_bool.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace theory { namespace booleans { - RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) { if(n.getKind() == kind::IFF) { NodeManager* nodeManager = NodeManager::currentNM(); @@ -140,6 +140,70 @@ RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) { return RewriteComplete(n); } +Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + 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 + return nodeManager->mkConst(! engine->getValue(n[0]).getConst<bool>()); + + case kind::AND: { // 2+ args + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(! engine->getValue(*i).getConst<bool>()) { + return nodeManager->mkConst(false); + } + } + return nodeManager->mkConst(true); + } + + case kind::IFF: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() == + engine->getValue(n[1]).getConst<bool>() ); + + case kind::IMPLIES: // 2 args + return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) || + engine->getValue(n[1]).getConst<bool>() ); + + case kind::OR: { // 2+ args + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(engine->getValue(*i).getConst<bool>()) { + return nodeManager->mkConst(true); + } + } + return nodeManager->mkConst(false); + } + + case kind::XOR: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() != + engine->getValue(n[1]).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() ); + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ? + engine->getValue(n[1]).getConst<bool>() : + engine->getValue(n[2]).getConst<bool>() ); + + default: + Unhandled(n.getKind()); + } +} }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ |