diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/boolean_terms.cpp | 4 | ||||
-rw-r--r-- | src/smt/model_postprocessor.cpp | 37 |
2 files changed, 40 insertions, 1 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 6ce8efef9..29caa92b3 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..db0ce3487 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -235,6 +235,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 |