From 3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Nov 2014 10:15:41 -0500 Subject: [PATCH] Revert "Fix missing case in model postprocessor (resolves bug #595)." This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am --- src/smt/model_postprocessor.cpp | 39 +++----------------------------- src/smt/smt_engine.cpp | 1 - test/regress/regress0/bug595.cvc | 7 ------ 3 files changed, 3 insertions(+), 44 deletions(-) delete mode 100644 test/regress/regress0/bug595.cvc 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 921d75315..577fa7413 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3568,7 +3568,6 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { ModelPostprocessor mpost; NodeVisitor 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); diff --git a/test/regress/regress0/bug595.cvc b/test/regress/regress0/bug595.cvc deleted file mode 100644 index c11cfb6e4..000000000 --- a/test/regress/regress0/bug595.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% EXPECT: sat - -f : INT -> [# i:INT, b:INT #]; -a : INT; -ASSERT f(a) /= (# i := 0, b := 0 #); - -CHECKSAT; -- 2.30.2