diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 16:51:26 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 16:51:26 -0500 |
commit | 86e687cb9566e8623d2e842e383e3a09db609739 (patch) | |
tree | bcce845fd55989703456d25c4f32fc7590a42fa3 /src/smt | |
parent | 4ad0191e20e4d812d9a5dc3a733153cb10f6d728 (diff) | |
parent | 6a6630bf6fa4b68c6a483b767be4c696da8fd0bd (diff) |
Merge branch '1.4.x'
Conflicts:
src/smt/model_postprocessor.cpp
Diffstat (limited to 'src/smt')
-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 |