diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 10:16:00 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 10:16:00 -0500 |
commit | 1993e1c4d13b7d0c85f3e77bf29686c856d4aba7 (patch) | |
tree | 321d84fbb8d1d0d65bbf9948e708addb09dd79dd /src | |
parent | 61042cf551b19d06673be2b069bacc7cb1cd775a (diff) |
Revert "Fix missing case in model postprocessor (resolves bug #595)."
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/model_postprocessor.cpp | 39 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 1 |
2 files changed, 3 insertions, 37 deletions
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index c0c865b98..dd9d0a78c 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -27,15 +27,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { // good to go, we have the right type return n; } - if(n.getKind() == kind::LAMBDA) { - Assert(asType.isFunction()); - Node rhs = rewriteAs(n[1], asType[1]); - Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs); - Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl; - Debug("boolean-terms") << "need type " << asType << endl; - Assert(out.getType() == asType); - return out; - } if(!n.isConst()) { // we don't handle non-const right now return n; @@ -245,32 +236,8 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { << "- returning " << n << endl; d_nodes[current] = n; } else { - // rewrite based on children - bool self = true; - for(size_t i = 0; i < current.getNumChildren(); ++i) { - Assert(d_nodes.find(current[i]) != d_nodes.end()); - if(!d_nodes[current[i]].isNull()) { - self = false; - break; - } - } - if(self) { - Debug("tuprec") << "returning self for kind " << current.getKind() << endl; - // rewrite to self - d_nodes[current] = Node::null(); - } else { - // rewrite based on children - NodeBuilder<> nb(current.getKind()); - for(size_t i = 0; i < current.getNumChildren(); ++i) { - Assert(d_nodes.find(current[i]) != d_nodes.end()); - TNode rw = d_nodes[current[i]]; - if(rw.isNull()) { - rw = current[i]; - } - nb << rw; - } - d_nodes[current] = nb; - Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << endl; - } + Debug("tuprec") << "returning self for kind " << current.getKind() << endl; + // rewrite to self + d_nodes[current] = Node::null(); } }/* ModelPostprocessor::visit() */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ea52f43a7..dcfc526ec 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3417,7 +3417,6 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { ModelPostprocessor mpost; NodeVisitor<ModelPostprocessor> visitor; - Debug("boolean-terms") << "postproc: visit " << node << endl; Node value = visitor.run(mpost, node); Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl; Node realValue = mpost.rewriteAs(value, expectedType); |