From eee91ecc512e94358a02d2aa155764e4cda2e5fa Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 1 Jun 2010 01:26:24 +0000 Subject: [PATCH] In order for splitting on demand to be able to retract clauses every translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion. --- src/prop/cnf_stream.cpp | 253 +++++++++++++++++++++++++----- src/prop/cnf_stream.h | 17 +- src/prop/prop_engine.cpp | 4 +- test/unit/prop/cnf_stream_black.h | 24 +-- 4 files changed, 237 insertions(+), 61 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 350b6f5cf..225f95d54 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -326,66 +326,233 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { } -SatLiteral TseitinCnfStream::toCNF(TNode node) { - Debug("cnf") << "toCNF(" << node << ")" << endl; +SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { + Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; - // If the node has already been translated, return the previous translation - if(isCached(node)) { - return lookupInCache(node); - } + SatLiteral nodeLit; + Node negatedNode = node.notNode(); - // Handle each Boolean operator case - switch(node.getKind()) { - case NOT: - return handleNot(node); - case XOR: - return handleXor(node); - case ITE: - return handleIte(node); - case IFF: - return handleIff(node); - case IMPLIES: - return handleImplies(node); - case OR: - return handleOr(node); - case AND: - return handleAnd(node); - default: - { - //TODO make sure this does not contain any boolean substructure - return handleAtom(node); - //Unreachable(); - //Node atomic = handleNonAtomicNode(node); - //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic); + // If the non-negated node has already been translated, get the translation + if(isCached(node)) { + nodeLit = lookupInCache(node); + } else { + // Handle each Boolean operator case + switch(node.getKind()) { + case NOT: + nodeLit = handleNot(node); + break; + case XOR: + nodeLit = handleXor(node); + break; + case ITE: + nodeLit = handleIte(node); + break; + case IFF: + nodeLit = handleIff(node); + break; + case IMPLIES: + nodeLit = handleImplies(node); + break; + case OR: + nodeLit = handleOr(node); + break; + case AND: + nodeLit = handleAnd(node); + break; + default: + { + //TODO make sure this does not contain any boolean substructure + nodeLit = handleAtom(node); + //Unreachable(); + //Node atomic = handleNonAtomicNode(node); + //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic); + } } } + + // Return the appropriate (negated) literal + if (!negated) return nodeLit; + else return ~nodeLit; } -void TseitinCnfStream::convertAndAssert(TNode node, bool lemma) { - Debug("cnf") << "convertAndAssert(" << node << ")" << endl; - d_assertingLemma = lemma; - if(node.getKind() == AND) { +void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) { + Assert(node.getKind() == AND); + if (!negated) { // If the node is a conjunction, we handle each conjunct separately - for( TNode::const_iterator conjunct = node.begin(), - node_end = node.end(); - conjunct != node_end; - ++conjunct ) { - convertAndAssert(*conjunct, lemma); + for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); + conjunct != node_end; ++conjunct ) { + convertAndAssert(*conjunct, lemma, false); + } + } else { + // If the node is a disjunction, we construct a clause and assert it + int nChildren = node.getNumChildren(); + SatClause clause(nChildren); + TNode::const_iterator disjunct = node.begin(); + for(int i = 0; i < nChildren; ++ disjunct, ++ i) { + Assert( disjunct != node.end() ); + clause[i] = toCNF(*disjunct, true); } - } else if(node.getKind() == OR) { + Assert(disjunct == node.end()); + assertClause(node, clause); + } +} + +void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) { + Assert(node.getKind() == OR); + if (!negated) { // If the node is a disjunction, we construct a clause and assert it int nChildren = node.getNumChildren(); SatClause clause(nChildren); TNode::const_iterator disjunct = node.begin(); for(int i = 0; i < nChildren; ++ disjunct, ++ i) { Assert( disjunct != node.end() ); - clause[i] = toCNF(*disjunct); + clause[i] = toCNF(*disjunct, false); } - Assert( disjunct == node.end() ); + Assert(disjunct == node.end()); assertClause(node, clause); } else { - // Otherwise, we just convert using the definitional transformation - assertClause(node, toCNF(node)); + // If the node is a conjunction, we handle each conjunct separately + for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); + conjunct != node_end; ++conjunct ) { + convertAndAssert(*conjunct, lemma, true); + } + } +} + +void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) { + if (!negated) { + // p XOR q + SatLiteral p = toCNF(node[0], false); + SatLiteral q = toCNF(node[1], false); + // Construct the clauses (p => !q) and (!q => p) + SatClause clause1(2); + clause1[0] = ~p; + clause1[1] = ~q; + assertClause(node, clause1); + SatClause clause2(2); + clause2[0] = p; + clause2[1] = q; + assertClause(node, clause2); + } else { + // !(p XOR q) is the same as p <=> q + SatLiteral p = toCNF(node[0], false); + SatLiteral q = toCNF(node[1], false); + // Construct the clauses (p => q) and (q => p) + SatClause clause1(2); + clause1[0] = ~p; + clause1[1] = q; + assertClause(node, clause1); + SatClause clause2(2); + clause2[0] = p; + clause2[1] = ~q; + assertClause(node, clause2); + } +} + +void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) { + if (!negated) { + // p <=> q + SatLiteral p = toCNF(node[0], false); + SatLiteral q = toCNF(node[1], false); + // Construct the clauses (p => q) and (q => p) + SatClause clause1(2); + clause1[0] = ~p; + clause1[1] = q; + assertClause(node, clause1); + SatClause clause2(2); + clause2[0] = p; + clause2[1] = ~q; + assertClause(node, clause2); + } else { + // !(p <=> q) is the same as p XOR q + SatLiteral p = toCNF(node[0], false); + SatLiteral q = toCNF(node[1], false); + // Construct the clauses (p => !q) and (!q => p) + SatClause clause1(2); + clause1[0] = ~p; + clause1[1] = ~q; + assertClause(node, clause1); + SatClause clause2(2); + clause2[0] = p; + clause2[1] = q; + assertClause(node, clause2); + } +} + +void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) { + if (!negated) { + // p => q + SatLiteral p = toCNF(node[0], false); + SatLiteral q = toCNF(node[1], false); + // Construct the clause ~p || q + SatClause clause(2); + clause[0] = ~p; + clause[1] = q; + assertClause(node, clause); + } else {// Construct the + // !(p => q) is the same as (p && ~q) + convertAndAssert(node[0], lemma, false); + convertAndAssert(node[1], lemma, true); + } +} + +void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) { + // ITE(p, q, r) + SatLiteral p = toCNF(node[0], false); + SatLiteral q = toCNF(node[1], negated); + SatLiteral r = toCNF(node[2], negated); + // Construct the clauses: + // (p => q) and (!p => r) and (!q => !p) and (!r => p) + SatClause clause1(2); + clause1[0] = ~p; + clause1[1] = q; + assertClause(node, clause1); + SatClause clause2(2); + clause2[0] = p; + clause2[1] = r; + assertClause(node, clause2); + SatClause clause3(2); + clause3[0] = q; + clause3[1] = ~p; + assertClause(node, clause3); + SatClause clause4(2); + clause4[0] = r; + clause4[1] = p; + assertClause(node, clause4); +} + +// At the top level we must ensure that all clauses that are asserted are +// not unit, except for the direct assertions. This allows us to remove the +// clauses later when they are not needed anymore (lemmas for example). +void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) { + Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; + d_assertingLemma = lemma; + switch(node.getKind()) { + case AND: + convertAndAssertAnd(node, lemma, negated); + break; + case OR: + convertAndAssertOr(node, lemma, negated); + break; + case IFF: + convertAndAssertIff(node, lemma, negated); + break; + case XOR: + convertAndAssertXor(node, lemma, negated); + break; + case IMPLIES: + convertAndAssertImplies(node, lemma, negated); + break; + case ITE: + convertAndAssertIte(node, lemma, negated); + break; + case NOT: + convertAndAssert(node[0], lemma, !negated); + break; + default: + // Atoms + assertClause(node, toCNF(node, negated)); + break; } } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a574adf23..ce6c7eb1e 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -144,9 +144,10 @@ public: /** * Converts and asserts a formula. * @param node node to convert and assert - * @param whether the sat solver can choose to remove this clause + * @param whether the sat solver can choose to remove the clauses + * @param negated wheather we are asserting the node negated */ - virtual void convertAndAssert(TNode node, bool lemma = false) = 0; + virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -185,8 +186,9 @@ public: * Convert a given formula to CNF and assert it to the SAT solver. * @param node the formula to assert * @param lemma is this a lemma that is erasable + * @param negated true if negated */ - void convertAndAssert(TNode node, bool lemma); + void convertAndAssert(TNode node, bool lemma, bool negated = false); /** * Constructs the stream to use the given sat solver. @@ -215,13 +217,20 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); + void convertAndAssertAnd(TNode node, bool lemma, bool negated); + void convertAndAssertOr(TNode node, bool lemma, bool negated); + void convertAndAssertXor(TNode node, bool lemma, bool negated); + void convertAndAssertIff(TNode node, bool lemma, bool negated); + void convertAndAssertImplies(TNode node, bool lemma, bool negated); + void convertAndAssertIte(TNode node, bool lemma, bool negated); /** * Transforms the node into CNF recursively. * @param node the formula to transform + * @param negated wheather the literal is negated * @return the literal representing the root of the formula */ - SatLiteral toCNF(TNode node); + SatLiteral toCNF(TNode node, bool negated = false); }; /* class TseitinCnfStream */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index b9fbd3ce6..16881f9e4 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -77,14 +77,14 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node); + d_cnfStream->convertAndAssert(node, false, false); } void PropEngine::assertLemma(TNode node) { Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as removable - d_cnfStream->convertAndAssert(node); + d_cnfStream->convertAndAssert(node, false, false); } diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 9c8560783..bbae46df7 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -104,7 +104,7 @@ void testAnd() { 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) ); + d_nodeManager->mkNode(kind::AND, a, b, c), false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -125,13 +125,13 @@ void testComplexExpr() { d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode( kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))) ); + d_nodeManager->mkNode(kind::XOR, e, f)))), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false) ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -140,7 +140,7 @@ void testIff() { 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) ); + d_nodeManager->mkNode(kind::IFF, a, b), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -149,7 +149,7 @@ void testImplies() { 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) ); + d_nodeManager->mkNode(kind::IMPLIES, a, b), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -165,7 +165,7 @@ void testIte() { d_nodeManager->mkVar(d_nodeManager->integerType()) ), d_nodeManager->mkVar(d_nodeManager->integerType()) - )); + ), false); } @@ -173,7 +173,7 @@ void testNot() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a) ); + d_nodeManager->mkNode(kind::NOT, a), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -183,13 +183,13 @@ void testOr() { 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) ); + d_nodeManager->mkNode(kind::OR, a, b, c), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -197,10 +197,10 @@ void testVar() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a); + d_cnfStream->convertAndAssert(a, false); TS_ASSERT( d_satSolver->addClauseCalled() ); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b); + d_cnfStream->convertAndAssert(b, false); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -209,7 +209,7 @@ void testXor() { 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) ); + d_nodeManager->mkNode(kind::XOR, a, b), false ); TS_ASSERT( d_satSolver->addClauseCalled() ); } }; -- 2.30.2