From a8d7333d8fb03c95ef3d1d7d9501076b97add756 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 5 Oct 2011 23:51:57 +0000 Subject: [PATCH] ensureLiteral() in CNF stream to support Andy's quantifiers work; an update to model gen on booleans; and a little cleanup --- src/prop/cnf_stream.cpp | 58 +++++++++++++++++++--- src/prop/cnf_stream.h | 33 +++++++------ src/prop/prop_engine.cpp | 5 +- src/prop/prop_engine.h | 7 +++ src/theory/booleans/theory_bool.cpp | 75 +++++++++++++++++++++-------- src/theory/theory_engine.cpp | 1 + src/theory/valuation.cpp | 11 +++++ src/theory/valuation.h | 11 +++++ test/unit/prop/cnf_stream_black.h | 44 +++++++++-------- 9 files changed, 181 insertions(+), 64 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c211a9c71..6810d3a94 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -22,6 +22,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "theory/theory_engine.h" +#include "theory/theory.h" #include "expr/node.h" #include "util/Assert.h" #include "util/output.h" @@ -100,17 +101,59 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral bool CnfStream::isTranslated(TNode n) const { TranslationCache::const_iterator find = d_translationCache.find(n); - return find != d_translationCache.end() && find->second.level >= 0; + return find != d_translationCache.end() && (*find).second.level >= 0; } -bool CnfStream::hasEverHadLiteral(TNode n) const { +bool CnfStream::hasLiteral(TNode n) const { TranslationCache::const_iterator find = d_translationCache.find(n); return find != d_translationCache.end(); } -bool CnfStream::currentlyHasLiteral(TNode n) const { - TranslationCache::const_iterator find = d_translationCache.find(n); - return find != d_translationCache.end() && (*find).second.level != -1; +void TseitinCnfStream::ensureLiteral(TNode n) { + if(hasLiteral(n)) { + // Already a literal! + SatLiteral lit = getLiteral(n); + NodeCache::iterator i = d_nodeCache.find(lit); + if(i == d_nodeCache.end()) { + // Store backward-mappings + d_nodeCache[lit] = n; + d_nodeCache[~lit] = n.notNode(); + } + return; + } + + CheckArgument(n.getType().isBoolean(), n, + "CnfStream::ensureLiteral() requires a node of Boolean type.\n" + "got node: %s\n" + "its type: %s\n", + n.toString().c_str(), + n.getType().toString().c_str()); + + bool negated = false; + SatLiteral lit; + + if(n.getKind() == kind::NOT) { + negated = true; + n = n[0]; + } + + if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL && + n.getMetaKind() != kind::metakind::VARIABLE ) { + // If we were called with something other than a theory atom (or + // Boolean variable), we get a SatLiteral that is definitionally + // equal to it. + lit = toCNF(n, false); + + // Store backward-mappings + d_nodeCache[lit] = n; + d_nodeCache[~lit] = n.notNode(); + } else { + // We have a theory atom or variable. + lit = convertAtom(n); + } + + Assert(hasLiteral(n) && getNode(lit) == n); + Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl; } SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { @@ -118,7 +161,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // Get the literal for this node SatLiteral lit; - if (!hasEverHadLiteral(node)) { + if (!hasLiteral(node)) { // If no literal, well make one lit = variableToLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; @@ -605,7 +648,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; /* - if(currentlyHasLiteral(node)) { + if(isTranslated(node)) { Debug("cnf") << "==> fortunate literal detected!" << endl; ++d_fortunateLiterals; SatLiteral lit = getLiteral(node); @@ -739,7 +782,6 @@ void CnfStream::moveToBaseLevel(TNode node) { moveToBaseLevel(*child); ++ child; } - } }/* CVC4::prop namespace */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 3ef636811..5eaeeef94 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -61,7 +61,7 @@ public: /** Cache of what literals have been registered to a node. */ typedef __gnu_cxx::hash_map TranslationCache; -private: +protected: /** The SAT solver we will be using */ SatInputInterface *d_satSolver; @@ -69,8 +69,6 @@ private: TranslationCache d_translationCache; NodeCache d_nodeCache; -protected: - /** The "registrar" for pre-registration of terms */ theory::Registrar d_registrar; @@ -154,13 +152,6 @@ protected: */ void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); - /** - * Returns true if the node has been cached in the translation cache. - * @param node the node - * @return true if the node has been cached - */ - bool isTranslated(TNode node) const; - /** * Acquires a new variable from the SAT solver to represent the node * and inserts the necessary data it into the mapping tables. @@ -203,7 +194,7 @@ public: * Converts and asserts a formula. * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses - * @param negated wheather we are asserting the node negated + * @param negated whether we are asserting the node negated */ virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0; @@ -215,16 +206,26 @@ public: TNode getNode(const SatLiteral& literal); /** - * Returns true iff the node has an assigned literal (it might not be translated). + * Returns true if the node has been cached in the translation cache. * @param node the node + * @return true if the node has been cached */ - bool hasEverHadLiteral(TNode node) const; + bool isTranslated(TNode node) const; /** - * Returns true iff the node has an assigned literal and it's translated. + * Returns true iff the node has an assigned literal (it might not be translated). * @param node the node */ - bool currentlyHasLiteral(TNode node) const; + bool hasLiteral(TNode node) const; + + /** + * Ensure that the given node will have a designated SAT literal + * that is definitionally equal to it. The result of this function + * is that the Node can be queried via getSatValue(). Essentially, + * this is like a "convert-but-don't-assert" version of + * convertAndAssert(). + */ + virtual void ensureLiteral(TNode n) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -319,6 +320,8 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); + void ensureLiteral(TNode n); + };/* class TseitinCnfStream */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7b4155bde..e123db0ed 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -167,7 +167,7 @@ Node PropEngine::getValue(TNode node) { } bool PropEngine::isSatLiteral(TNode node) { - return d_cnfStream->hasEverHadLiteral(node); + return d_cnfStream->hasLiteral(node); } bool PropEngine::hasValue(TNode node, bool& value) { @@ -187,6 +187,9 @@ bool PropEngine::hasValue(TNode node, bool& value) { } } +void PropEngine::ensureLiteral(TNode n) { + d_cnfStream->ensureLiteral(n); +} void PropEngine::push() { Assert(!d_inCheckSat, "Sat solver in solve()!"); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index bb8ed86e1..16cb34e04 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -126,6 +126,13 @@ public: */ bool hasValue(TNode node, bool& value); + /** + * Ensure that the given node will have a designated SAT literal + * that is definitionally equal to it. The result of this function + * is that the Node can be queried via getSatValue(). + */ + void ensureLiteral(TNode n); + /** * Push the context level. */ 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()); + case kind::NOT: { // 1 arg + Node v = d_valuation.getValue(n[0]); + return v.isNull() ? Node::null() : nodeManager->mkConst(! v.getConst()); + } 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()) { + Node v = d_valuation.getValue(*i); + if(v.isNull()) { + foundNull = true; + } else if(! v.getConst()) { 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() == - d_valuation.getValue(n[1]).getConst() ); + 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() == v1.getConst() ); + } - case kind::IMPLIES: // 2 args - return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst()) || - d_valuation.getValue(n[1]).getConst() ); + 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()); + } + if(! v1.isNull()) { + value = value || v1.getConst(); + } + 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()) { + Node v = d_valuation.getValue(*i); + if(v.isNull()) { + foundNull = true; + } else if(v.getConst()) { 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() != - d_valuation.getValue(n[1]).getConst() ); + 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() != v1.getConst() ); + } - 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() ? - d_valuation.getValue(n[1]).getConst() : - d_valuation.getValue(n[2]).getConst() ); + 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() ? v1.getConst() : v2.getConst() ); + } 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 */ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 62117d4c1..26b490d2d 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -144,8 +144,7 @@ public: Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::AND, a, b, c), false, false); + d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -157,22 +156,18 @@ public: Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode( - kind::IMPLIES, + d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b), - d_nodeManager->mkNode( - kind::IFF, + d_nodeManager->mkNode(kind::IFF, d_nodeManager->mkNode(kind::OR, c, d), - d_nodeManager->mkNode( - kind::NOT, + d_nodeManager->mkNode(kind::NOT, d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -180,8 +175,7 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IFF, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -189,8 +183,7 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -214,8 +207,7 @@ public: void testNot() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -224,14 +216,13 @@ public: Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -250,8 +241,19 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::XOR, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } + + void testEnsureLiteral() { + NodeManagerScope nms(d_nodeManager); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b); + d_cnfStream->ensureLiteral(a_and_b); + // Clauses are necessary to "literal-ize" a_and_b; this perhaps + // doesn't belong in a black-box test though... + TS_ASSERT( d_satSolver->addClauseCalled() ); + TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) ); + } }; -- 2.30.2