summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r--src/prop/cnf_stream.cpp489
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback