diff options
Diffstat (limited to 'src/util/ite_removal.cpp')
-rw-r--r-- | src/util/ite_removal.cpp | 39 |
1 files changed, 23 insertions, 16 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 9d2524170..9a4fc8dc2 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -79,23 +79,30 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } // If not an ITE, go deep - vector<Node> newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Remove the ITEs from the children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } + if( node.getKind() != kind::FORALL && + node.getKind() != kind::EXISTS && + node.getKind() != kind::REWRITE_RULE ) { + vector<Node> newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output, iteSkolemMap); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } - // If changes, we rewrite - if(somethingChanged) { - cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); - nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite); - return cachedRewrite; + // If changes, we rewrite + if(somethingChanged) { + cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); + nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite); + return cachedRewrite; + } else { + nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); + return node; + } } else { nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); return node; |