diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-14 22:50:17 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-14 22:50:17 +0000 |
commit | 07e1a1668a27e90563f23bcf5abb5cb7fe30da86 (patch) | |
tree | 6af918e2d1c753b1254fbfb20677618a489ecd01 /src/prop/cnf_stream.cpp | |
parent | 06b5f38e17a1275e966e50c2d74274ef4d4d4697 (diff) |
Adding debugging code in PropEngine/CnfStream
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 27 |
1 files changed, 25 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 233032706..eb77b0d54 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -47,12 +47,14 @@ void CnfStream::assertClause(SatLiteral a) { clause[0] = a; assertClause(clause); } + void CnfStream::assertClause(SatLiteral a, SatLiteral b) { SatClause clause(2); clause[0] = a; clause[1] = b; assertClause(clause); } + void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) { SatClause clause(3); clause[0] = a; @@ -104,6 +106,14 @@ SatLiteral CnfStream::getLiteral(TNode node) { return literal; } +const CnfStream::NodeCache& CnfStream::getNodeCache() const { + return d_nodeCache; +} + +const CnfStream::TranslationCache& CnfStream::getTranslationCache() const { + return d_translationCache; +} + SatLiteral TseitinCnfStream::handleAtom(TNode node) { Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom"); Assert(!isCached(node), "atom already mapped!"); @@ -285,6 +295,8 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { Assert(iteNode.getKind() == ITE); Assert(iteNode.getNumChildren() == 3); + Debug("cnf") << "handlIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl; + SatLiteral condLit = toCNF(iteNode[0]); SatLiteral thenLit = toCNF(iteNode[1]); SatLiteral elseLit = toCNF(iteNode[2]); @@ -293,20 +305,30 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // If ITE is true then one of the branches is true and the condition // implies which one + // lit -> (ite b t e) + // lit -> (t | e) & (b -> t) & (!b -> e) + // lit -> (t | e) & (!b | t) & (b | e) + // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) + assertClause(~iteLit, thenLit, elseLit); 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 + // !lit -> !(ite b t e) + // !lit -> (!t | !e) & (b -> !t) & (!b -> !e) + // !lit -> (!t | !e) & (!b | !t) & (b | !e) + // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) + assertClause(iteLit, ~thenLit, ~elseLit); assertClause(iteLit, ~condLit, ~thenLit); assertClause(iteLit, condLit, ~elseLit); - assertClause(iteLit, ~thenLit, ~elseLit); return iteLit; } Node TseitinCnfStream::handleNonAtomicNode(TNode node) { + Debug("cnf") << "handleNonAtomicNode(" << node << ")" << endl; + /* Our main goal here is to tease out any ITE's sitting under a theory operator. */ Node rewrite; NodeManager *nodeManager = NodeManager::currentNM(); @@ -347,6 +369,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) { } SatLiteral TseitinCnfStream::toCNF(TNode node) { + Debug("cnf") << "toCNF(" << node << ")" << endl; // If the node has already been translated, return the previous translation if(isCached(node)) { |