diff options
| -rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index e60d51063..4b00a9451 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -93,20 +93,6 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); } } - if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) { - // resolve away the lambda - context::Context fakeContext; - theory::SubstitutionMap substitutions(&fakeContext); - TNode lambda = node.getOperator(); - for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) { - // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc. - Assert(formal != node.end()); - // This rewrite step is important: see note in postRewrite(). - Node n = Rewriter::rewrite(*arg); - substitutions.addSubstitution(*formal, n); - } - return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); - } return RewriteResponse(REWRITE_DONE, node); } |