diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-27 20:34:18 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-27 20:34:18 +0000 |
commit | d1acfe81a013d1f8960bd0267dcd685185ffc785 (patch) | |
tree | 70870c5ccbea9fff7edf5ba26c5f8e68fe16c20e /src/prop | |
parent | e5c77b0674a9cb698e6012ccc1950fef9bee4f8d (diff) |
Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 51ae695cf..a245eb469 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -359,6 +359,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) { } if(somethingChanged) { + rewrite = nodeManager->mkNode(node.getKind(), newChildren); nodeManager->setAttribute(node, IteRewriteAttr(), rewrite); return rewrite; @@ -399,7 +400,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { case AND: return handleAnd(node); default: - return handleAtom(handleNonAtomicNode(node)); + { + Node atomic = handleNonAtomicNode(node); + AlwaysAssert(isCached(atomic) || atomic.isAtomic()); + return toCNF(atomic); + } } } |