diff options
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 489 |
1 files changed, 211 insertions, 278 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index b4a0a297e..011d8ba5a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -27,36 +27,36 @@ using namespace std; namespace CVC4 { namespace prop { -CnfStream::CnfStream(PropEngine *pe) : - d_propEngine(pe) { +CnfStream::CnfStream(SatSolver *satSolver) : + d_satSolver(satSolver) { } -TseitinCnfStream::TseitinCnfStream(PropEngine *pe) : - CnfStream(pe) { +TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver) : + CnfStream(satSolver) { } -void CnfStream::insertClauseIntoStream(SatClause& c) { +void CnfStream::assertClause(SatClause& c) { Debug("cnf") << "Inserting into stream " << c << endl; - d_propEngine->assertClause(c); + d_satSolver->addClause(c); } -void CnfStream::insertClauseIntoStream(SatLiteral a) { +void CnfStream::assertClause(SatLiteral a) { SatClause clause(1); clause[0] = a; - insertClauseIntoStream(clause); + assertClause(clause); } -void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b) { +void CnfStream::assertClause(SatLiteral a, SatLiteral b) { SatClause clause(2); clause[0] = a; clause[1] = b; - insertClauseIntoStream(clause); + assertClause(clause); } -void CnfStream::insertClauseIntoStream(SatLiteral a, SatLiteral b, SatLiteral c) { +void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) { SatClause clause(3); clause[0] = a; clause[1] = b; clause[2] = c; - insertClauseIntoStream(clause); + assertClause(clause); } bool CnfStream::isCached(const Node& n) const { @@ -64,328 +64,261 @@ bool CnfStream::isCached(const Node& n) const { } SatLiteral CnfStream::lookupInCache(const Node& n) const { - Assert(isCached(n), - "Node is not in cnf translation cache"); + Assert(isCached(n), "Node is not in CNF translation cache"); return d_translationCache.find(n)->second; } -void CnfStream::flushCache() { - Debug("cnf") << "flushing the translation cache" << endl; - d_translationCache.clear(); -} - void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) { Debug("cnf") << "caching translation " << node << " to " << lit << endl; d_translationCache.insert(make_pair(node, lit)); } -SatLiteral CnfStream::aquireAndRegister(const Node& node, bool atom) { - SatVariable var = atom ? d_propEngine->registerAtom(node) - : d_propEngine->requestFreshVar(); - SatLiteral lit(var); +SatLiteral CnfStream::newLiteral(const Node& node) { + SatLiteral lit = SatLiteral(d_satSolver->newVar()); cacheTranslation(node, lit); return lit; } -bool CnfStream::isAtomMapped(const Node& n) const { - return d_propEngine->isAtomMapped(n); -} - -SatVariable CnfStream::lookupAtom(const Node& n) const { - return d_propEngine->lookupAtom(n); -} - -/***********************************************/ -/***********************************************/ -/************ End of CnfStream *****************/ -/***********************************************/ -/***********************************************/ +SatLiteral TseitinCnfStream::handleAtom(const Node& node) { + Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); + Assert(!isCached(node), "atom already mapped!"); -SatLiteral TseitinCnfStream::handleAtom(const Node& n) { - Assert(n.isAtomic(), "handleAtom(n) expects n to be an atom"); + Debug("cnf") << "handleAtom(" << node << ")" << endl; - Debug("cnf") << "handling atom" << endl; + SatLiteral lit = newLiteral(node); - SatLiteral l = aquireAndRegister(n, true); - switch(n.getKind()) { /* TRUE and FALSE are handled specially. */ + switch(node.getKind()) { case TRUE: - insertClauseIntoStream(l); + assertClause(lit); break; case FALSE: - insertClauseIntoStream(~l); + assertClause(~lit); break; - default: //Does nothing else + default: break; } - return l; + + return lit; } -SatLiteral TseitinCnfStream::handleXor(const Node& n) { - // n: a XOR b +SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) { + Assert(!isCached(xorNode), "Atom already mapped!"); + Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!"); + Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!"); - SatLiteral a = recTransform(n[0]); - SatLiteral b = recTransform(n[1]); + SatLiteral a = toCNF(xorNode[0]); + SatLiteral b = toCNF(xorNode[1]); - SatLiteral l = aquireAndRegister(n); + SatLiteral xorLit = newLiteral(xorNode); - insertClauseIntoStream(a, b, ~l); - insertClauseIntoStream(a, ~b, l); - insertClauseIntoStream(~a, b, l); - insertClauseIntoStream(~a, ~b, ~l); + assertClause(a, b, ~xorLit); + assertClause(~a, ~b, ~xorLit); + assertClause(a, ~b, xorLit); + assertClause(~a, b, xorLit); - return l; + return xorLit; } -/* For a small efficiency boost target needs to already be allocated to have - size of the number of children of n. - */ -void TseitinCnfStream::mapRecTransformOverChildren(const Node& n, - SatClause& target) { - Assert((unsigned)target.size() == n.getNumChildren(), - "Size of the children must be the same the constructed clause"); - - int i = 0; - Node::iterator subExprIter = n.begin(); - - while(subExprIter != n.end()) { - SatLiteral equivalentLit = recTransform(*subExprIter); - target[i] = equivalentLit; - ++subExprIter; - ++i; +SatLiteral TseitinCnfStream::handleOr(const Node& orNode) { + Assert(!isCached(orNode), "Atom already mapped!"); + Assert(orNode.getKind() == OR, "Expecting an OR expression!"); + Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!"); + + // Number of children + unsigned n_children = orNode.getNumChildren(); + + // Transform all the children first + Node::iterator node_it = orNode.begin(); + Node::iterator node_it_end = orNode.end(); + SatClause clause(n_children + 1); + for(int i = 0; node_it != node_it_end; ++node_it, ++i) { + clause[i] = toCNF(*node_it); } -} -SatLiteral TseitinCnfStream::handleOr(const Node& n) { - //child_literals - SatClause lits(n.getNumChildren()); - mapRecTransformOverChildren(n, lits); - - SatLiteral e = aquireAndRegister(n); - - /* e <-> (a1 | a2 | a3 | ...) - *: e -> (a1 | a2 | a3 | ...) - * : ~e | ( - * : ~e | a1 | a2 | a3 | ... - * e <- (a1 | a2 | a3 | ...) - * : e <- (a1 | a2 | a3 |...) - * : e | ~(a1 | a2 | a3 |...) - * : - * : (e | ~a1) & (e |~a2) & (e & ~a3) & ... - */ - - SatClause c(1 + lits.size()); - - for(int index = 0; index < lits.size(); ++index) { - SatLiteral a = lits[index]; - c[index] = a; - insertClauseIntoStream(e, ~a); + // Get the literal for this node + SatLiteral orLit = newLiteral(orNode); + + // lit <- (a_1 | a_2 | a_3 | ... | a_n) + // lit | ~(a_1 | a_2 | a_3 | ... | a_n) + // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) + for(unsigned i = 0; i < n_children; ++i) { + assertClause(orLit, ~clause[i]); } - c[lits.size()] = ~e; - insertClauseIntoStream(c); - return e; -} + // lit -> (a_1 | a_2 | a_3 | ... | a_n) + // ~lit | a_1 | a_2 | a_3 | ... | a_n + clause[n_children] = ~orLit; + // This needs to go last, as the clause might get modified by the SAT solver + assertClause(clause); -/* TODO: this only supports 2-ary <=> nodes atm. - * Should this be changed? - */ -SatLiteral TseitinCnfStream::handleIff(const Node& n) { - Assert(n.getKind() == IFF); - Assert(n.getNumChildren() == 2); - // n: a <=> b; - - SatLiteral a = recTransform(n[0]); - SatLiteral b = recTransform(n[1]); - - SatLiteral l = aquireAndRegister(n); - - /* l <-> (a<->b) - * : l -> ((a-> b) & (b->a)) - * : ~l | ((~a | b) & (~b |a)) - * : (~a | b | ~l ) & (~b | a | ~l) - * - * : (a<->b) -> l - * : ~((a & b) | (~a & ~b)) | l - * : (~(a & b)) & (~(~a & ~b)) | l - * : ((~a | ~b) & (a | b)) | l - * : (~a | ~b | l) & (a | b | l) - */ - - insertClauseIntoStream(~a, b, ~l); - insertClauseIntoStream(a, ~b, ~l); - insertClauseIntoStream(~a, ~b, l); - insertClauseIntoStream(a, b, l); - - return l; + // Return the literal + return orLit; } -SatLiteral TseitinCnfStream::handleAnd(const Node& n) { - Assert(n.getKind() == AND); - Assert(n.getNumChildren() >= 1); - - //TODO: we know the exact size of the this. - //Dynamically allocated array would have less overhead no? - SatClause lits(n.getNumChildren()); - mapRecTransformOverChildren(n, lits); - - SatLiteral e = aquireAndRegister(n); - - /* e <-> (a1 & a2 & a3 & ...) - * : e -> (a1 & a2 & a3 & ...) - * : ~e | (a1 & a2 & a3 & ...) - * : (~e | a1) & (~e | a2) & ... - * e <- (a1 & a2 & a3 & ...) - * : e <- (a1 & a2 & a3 & ...) - * : e | ~(a1 & a2 & a3 & ...) - * : e | (~a1 | ~a2 | ~a3 | ...) - * : e | ~a1 | ~a2 | ~a3 | ... - */ - - SatClause c(lits.size() + 1); - for(int index = 0; index < lits.size(); ++index) { - SatLiteral a = lits[index]; - c[index] = (~a); - insertClauseIntoStream(~e, a); +SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) { + Assert(!isCached(andNode), "Atom already mapped!"); + Assert(andNode.getKind() == AND, "Expecting an AND expression!"); + Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!"); + + // Number of children + unsigned n_children = andNode.getNumChildren(); + + // Transform all the children first (remembering the negation) + Node::iterator node_it = andNode.begin(); + Node::iterator node_it_end = andNode.end(); + SatClause clause(n_children + 1); + for(int i = 0; node_it != node_it_end; ++node_it, ++i) { + clause[i] = ~toCNF(*node_it); } - c[lits.size()] = e; - insertClauseIntoStream(c); + // Get the literal for this node + SatLiteral andLit = newLiteral(andNode); + + // lit -> (a_1 & a_2 & a_3 & ... & a_n) + // ~lit | (a_1 & a_2 & a_3 & ... & a_n) + // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) + for(unsigned i = 0; i < n_children; ++i) { + assertClause(~andLit, ~clause[i]); + } + + // lit <- (a_1 & a_2 & a_3 & ... a_n) + // lit | ~(a_1 & a_2 & a_3 & ... & a_n) + // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n + clause[n_children] = andLit; + // This needs to go last, as the clause might get modified by the SAT solver + assertClause(clause); + return andLit; +} + +SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) { + Assert(!isCached(impliesNode), "Atom already mapped!"); + Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!"); + Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!"); + + // Convert the children to cnf + SatLiteral a = toCNF(impliesNode[0]); + SatLiteral b = toCNF(impliesNode[1]); + + SatLiteral impliesLit = newLiteral(impliesNode); + + // lit -> (a->b) + // ~lit | ~ a | b + assertClause(~impliesLit, ~a, b); + + // (a->b) -> lit + // ~(~a | b) | lit + // (a | l) & (~b | l) + assertClause(a, impliesLit); + assertClause(~b, impliesLit); - return e; + return impliesLit; } -SatLiteral TseitinCnfStream::handleImplies(const Node& n) { - Assert(n.getKind() == IMPLIES); - Assert(n.getNumChildren() == 2); - // n: a => b; - - SatLiteral a = recTransform(n[0]); - SatLiteral b = recTransform(n[1]); - - SatLiteral l = aquireAndRegister(n); - - /* l <-> (a->b) - * (l -> (a->b)) & (l <- (a->b)) - * : l -> (a -> b) - * : ~l | (~ a | b) - * : (~l | ~a | b) - * (~l | ~a | b) & (l<- (a->b)) - * : (a->b) -> l - * : ~(~a | b) | l - * : (a & ~b) | l - * : (a | l) & (~b | l) - * (~l | ~a | b) & (a | l) & (~b | l) - */ - - insertClauseIntoStream(a, l); - insertClauseIntoStream(~b, l); - insertClauseIntoStream(~l, ~a, b); - - return l; + +SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) { + Assert(!isCached(iffNode), "Atom already mapped!"); + Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); + Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); + + // Convert the children to CNF + SatLiteral a = toCNF(iffNode[0]); + SatLiteral b = toCNF(iffNode[1]); + + // Get the now literal + SatLiteral iffLit = newLiteral(iffNode); + + // lit -> ((a-> b) & (b->a)) + // ~lit | ((~a | b) & (~b | a)) + // (~a | b | ~lit) & (~b | a | ~lit) + assertClause(~a, b, ~iffLit); + assertClause(a, ~b, ~iffLit); + + // (a<->b) -> lit + // ~((a & b) | (~a & ~b)) | lit + // (~(a & b)) & (~(~a & ~b)) | lit + // ((~a | ~b) & (a | b)) | lit + // (~a | ~b | lit) & (a | b | lit) + assertClause(~a, ~b, iffLit); + assertClause(a, b, iffLit); + + return iffLit; } -SatLiteral TseitinCnfStream::handleNot(const Node& n) { - Assert(n.getKind() == NOT); - Assert(n.getNumChildren() == 1); - // n : NOT m - Node m = n[0]; - SatLiteral equivM = recTransform(m); +SatLiteral TseitinCnfStream::handleNot(const Node& notNode) { + Assert(!isCached(notNode), "Atom already mapped!"); + Assert(notNode.getKind() == NOT, "Expecting a NOT expression!"); + Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!"); - SatLiteral equivN = ~equivM; + SatLiteral notLit = ~toCNF(notNode[0]); - cacheTranslation(n, equivN); + // Since we don't introduce new variables, we need to cache the translation + cacheTranslation(notNode, notLit); - return equivN; + return notLit; } -SatLiteral TseitinCnfStream::handleIte(const Node& n) { - Assert(n.getKind() == ITE); - Assert(n.getNumChildren() == 3); - - // n : IF c THEN t ELSE f ENDIF; - SatLiteral c = recTransform(n[0]); - SatLiteral t = recTransform(n[1]); - SatLiteral f = recTransform(n[2]); - - // d <-> IF c THEN tB ELSE fb - // : d -> (c & tB) | (~c & fB) - // : ~d | ( (c & tB) | (~c & fB) ) - // : x | (y & z) = (x | y) & (x | z) - // : ~d | ( ((c & t) | ~c ) & ((c & t) | f ) ) - // : ~d | ( (((c | ~c) & (~c | t))) & ((c | f) & (f | t)) ) - // : ~d | ( (~c | t) & (c | f) & (f | t) ) - // : (~d | ~c | t) & (~d | c | f) & (~d | f | t) - - // : ~d | (c & t & f) - // : (~d | c) & (~d | t) & (~d | f) - // ( IF c THEN tB ELSE fb) -> d - // :~((c & tB) | (~c & fB)) | d - // : ((~c | ~t)& ( c |~fb)) | d - // : (~c | ~ t | d) & (c | ~f | d) - - SatLiteral d = aquireAndRegister(n); - - insertClauseIntoStream(~d, ~c, t); - insertClauseIntoStream(~d, c, f); - insertClauseIntoStream(~d, f, t); - insertClauseIntoStream(~c, ~t, d); - insertClauseIntoStream(c, ~f, d); - - return d; +SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) { + Assert(iteNode.getKind() == ITE); + Assert(iteNode.getNumChildren() == 3); + + SatLiteral condLit = toCNF(iteNode[0]); + SatLiteral thenLit = toCNF(iteNode[1]); + SatLiteral elseLit = toCNF(iteNode[2]); + + SatLiteral iteLit = newLiteral(iteNode); + + // If ITE is true then one of the branches is true and the condition + // implies which one + assertClause(~iteLit, ~condLit, thenLit); + assertClause(~iteLit, condLit, elseLit); + assertClause(~iteLit, elseLit, thenLit); + + // If ITE is false then one of the branches is false and the condition + // implies which one + assertClause(iteLit, ~condLit, ~thenLit); + assertClause(iteLit, condLit, ~elseLit); + assertClause(iteLit, ~thenLit, ~elseLit); + + return iteLit; } -//TODO: The following code assumes everything is either -// an atom or is a logical connective. This ignores quantifiers and lambdas. -SatLiteral TseitinCnfStream::recTransform(const Node& n) { - if(isCached(n)) { - return lookupInCache(n); +SatLiteral TseitinCnfStream::toCNF(const Node& node) { + + // If the node has already been translated, return the previous translation + if(isCached(node)) { + return lookupInCache(node); + } + + // Atomic nodes are treated specially + if(node.isAtomic()) { + return handleAtom(node); } - if(n.isAtomic()) { - - /* Unfortunately we need to potentially allow - * for n to be to the Atom <-> Var map but not the - * translation cache. - * This is because the translation cache can be flushed. - * It is really not clear where this check should go, but - * it needs to be done. - */ - if(isAtomMapped(n)) { - /* Puts the atom in the translation cache after looking it up. - * Avoids doing 2 map lookups for this atom in the future. - */ - SatLiteral l(lookupAtom(n)); - cacheTranslation(n, l); - return l; - } - return handleAtom(n); - } else { - //Assume n is a logical connective - switch(n.getKind()) { - case NOT: - return handleNot(n); - case XOR: - return handleXor(n); - case ITE: - return handleIte(n); - case IFF: - return handleIff(n); - case IMPLIES: - return handleImplies(n); - case OR: - return handleOr(n); - case AND: - return handleAnd(n); - default: - Unreachable(); - } + // 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: + Unreachable(); } } -void TseitinCnfStream::convertAndAssert(const Node& n) { - SatLiteral e = recTransform(n); - insertClauseIntoStream(e); +void TseitinCnfStream::convertAndAssert(const Node& node) { + Debug("cnf") << "convertAndAssert(" << node << ")" << endl; + assertClause(toCNF(node)); } }/* CVC4::prop namespace */ |