diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-28 20:17:48 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-28 20:17:48 +0000 |
commit | 7d9d562bb560cb4b83ffaaf94918f834916dad2f (patch) | |
tree | 0ebef47f2ea702d36afe53fb9e82ac31304811be /src/prop | |
parent | 4806691be59909eeaecb0fa652d84e40c966fe2e (diff) |
Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 50 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 3 |
2 files changed, 5 insertions, 48 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 219c25399..350b6f5cf 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -325,49 +325,6 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { 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(); - if(nodeManager->getAttribute(node, IteRewriteAttr(), rewrite)) { - return rewrite.isNull() ? Node(node) : rewrite; - } - - if(node.getKind() == ITE) { - Assert( node.getNumChildren() == 3 ); - //TODO should this be a skolem? - Node skolem = nodeManager->mkVar(node.getType()); - Node newAssertion = - nodeManager->mkNode( - ITE, - node[0], - nodeManager->mkNode(EQUAL, skolem, node[1]), - nodeManager->mkNode(EQUAL, skolem, node[2])); - nodeManager->setAttribute(node, IteRewriteAttr(), skolem); - convertAndAssert(newAssertion, d_assertingLemma); - return skolem; - } else { - std::vector<Node> newChildren; - bool somethingChanged = false; - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = handleNonAtomicNode(*it); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - if(somethingChanged) { - - rewrite = nodeManager->mkNode(node.getKind(), newChildren); - nodeManager->setAttribute(node, IteRewriteAttr(), rewrite); - return rewrite; - } else { - nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); - return node; - } - } -} SatLiteral TseitinCnfStream::toCNF(TNode node) { Debug("cnf") << "toCNF(" << node << ")" << endl; @@ -395,8 +352,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { return handleAnd(node); default: { - Node atomic = handleNonAtomicNode(node); - return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic); + //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); } } } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 1ea600322..a574adf23 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -215,9 +215,6 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - struct IteRewriteTag {}; - typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr; - Node handleNonAtomicNode(TNode node); /** * Transforms the node into CNF recursively. |