diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-05 23:51:57 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-05 23:51:57 +0000 |
commit | a8d7333d8fb03c95ef3d1d7d9501076b97add756 (patch) | |
tree | 9f217a8cdb8905dea26529684584b401c4a47323 /src/theory | |
parent | 9bdf1355af20c4dd2b97ea9bc5f34cc20fbdde0f (diff) |
ensureLiteral() in CNF stream to support Andy's quantifiers work; an update to model gen on booleans; and a little cleanup
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 75 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/valuation.cpp | 11 | ||||
-rw-r--r-- | src/theory/valuation.h | 11 |
4 files changed, 79 insertions, 19 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 2be1dac55..229a40532 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -45,52 +45,89 @@ Node TheoryBool::getValue(TNode n) { // should be handled by IFF Unreachable(); - case kind::NOT: // 1 arg - return nodeManager->mkConst(! d_valuation.getValue(n[0]).getConst<bool>()); + 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) { - if(! d_valuation.getValue(*i).getConst<bool>()) { + Node v = d_valuation.getValue(*i); + if(v.isNull()) { + foundNull = true; + } else if(! v.getConst<bool>()) { return nodeManager->mkConst(false); } } - return nodeManager->mkConst(true); + return foundNull ? Node::null() : nodeManager->mkConst(true); } - case kind::IFF: // 2 args - return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() == - d_valuation.getValue(n[1]).getConst<bool>() ); + 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 - return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst<bool>()) || - d_valuation.getValue(n[1]).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) { - if(d_valuation.getValue(*i).getConst<bool>()) { + Node v = d_valuation.getValue(*i); + if(v.isNull()) { + foundNull = true; + } else if(v.getConst<bool>()) { return nodeManager->mkConst(true); } } - return nodeManager->mkConst(false); + return foundNull ? Node::null() : nodeManager->mkConst(false); } - case kind::XOR: // 2 args - return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() != - d_valuation.getValue(n[1]).getConst<bool>() ); + 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 + 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( d_valuation.getValue(n[0]).getConst<bool>() ? - d_valuation.getValue(n[1]).getConst<bool>() : - d_valuation.getValue(n[2]).getConst<bool>() ); + 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()); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a3b91c132..2d4672776 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -298,6 +298,7 @@ Node TheoryEngine::getValue(TNode node) { // otherwise ask the theory-in-charge return theoryOf(node)->getValue(node); + }/* TheoryEngine::getValue(TNode node) */ bool TheoryEngine::presolve() { diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 9375998f9..148b95632 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -19,6 +19,7 @@ #include "expr/node.h" #include "theory/valuation.h" #include "theory/theory_engine.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { @@ -49,5 +50,15 @@ bool Valuation::hasSatValue(TNode n, bool& value) const { return d_engine->getPropEngine()->hasValue(n, value); } +Node Valuation::ensureLiteral(TNode n) { + Debug("ensureLiteral") << "rewriting: " << n << std::endl; + Node rewritten = Rewriter::rewrite(n); + Debug("ensureLiteral") << " got: " << rewritten << std::endl; + Node preprocessed = d_engine->preprocess(rewritten); + Debug("ensureLiteral") << "preproced: " << preprocessed << std::endl; + d_engine->getPropEngine()->ensureLiteral(preprocessed); + return preprocessed; +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index f819eff9d..71b194905 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -69,6 +69,17 @@ public: */ bool hasSatValue(TNode n, bool& value) const; + /** + * Ensure that the given node will have a designated SAT literal + * that is definitionally equal to it. The result of this function + * is a Node that can be queried via getSatValue(). + * + * @return the actual node that's been "literalized," which may + * differ from the input due to theory-rewriting and preprocessing, + * as well as CNF conversion + */ + Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT; + };/* class Valuation */ }/* CVC4::theory namespace */ |