diff options
| -rw-r--r-- | src/smt/boolean_terms.cpp | 4 | ||||
| -rw-r--r-- | src/smt/model_postprocessor.cpp | 46 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bug595.cvc | 7 |
5 files changed, 59 insertions, 2 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 89f35bf05..7744f64ca 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -282,11 +282,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( const Datatype& newD = newDtt.getDatatype(); for(c = dt.begin(); c != dt.end(); ++c) { Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl; - Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr? + const DatatypeConstructor *newC; + Node::fromExpr((*(newC = &newD[(*c).getName() + "'"])).getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr? Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl; d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { + Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr? d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); } } diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index dd9d0a78c..7c2742ce4 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -27,6 +27,15 @@ 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; @@ -235,6 +244,43 @@ void ModelPostprocessor::visit(TNode current, TNode parent) { Debug("boolean-terms") << "model-post: " << current << endl << "- returning " << n << endl; d_nodes[current] = n; + } else if(current.getKind() == kind::LAMBDA) { + // 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()); + if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { + TNode op = current.getOperator(); + Node realOp; + if(op.getAttribute(BooleanTermAttr(), realOp)) { + nb << realOp; + } else { + nb << op; + } + } + 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; + } } else { Debug("tuprec") << "returning self for kind " << current.getKind() << endl; // rewrite to self diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dcfc526ec..ea52f43a7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3417,6 +3417,7 @@ 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); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index c0ee0f2bb..15888fbce 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -166,7 +166,8 @@ BUG_TESTS = \ bug576a.smt2 \ bug578.smt2 \ bug585.cvc \ - bug586.cvc + bug586.cvc \ + bug595.cvc TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug595.cvc b/test/regress/regress0/bug595.cvc new file mode 100644 index 000000000..c11cfb6e4 --- /dev/null +++ b/test/regress/regress0/bug595.cvc @@ -0,0 +1,7 @@ +% EXPECT: sat + +f : INT -> [# i:INT, b:INT #]; +a : INT; +ASSERT f(a) /= (# i := 0, b := 0 #); + +CHECKSAT; |