diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-05 14:07:47 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-05 15:41:21 -0500 |
commit | 7eb063762c8b1d9366cf2b4d4687019f7733411b (patch) | |
tree | c89c4e018610c56e18b35d2835f3b200208dc27e /src/smt | |
parent | c0b0632a83ca1e997b9002bf9e67b0dbbbd154b1 (diff) |
Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/boolean_terms.cpp | 34 | ||||
-rw-r--r-- | src/smt/model_postprocessor.cpp | 25 |
2 files changed, 59 insertions, 0 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 108c88829..30aa79aca 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -152,6 +152,40 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { } return out; } + if(in.getType().isParametricDatatype() && + in.getType().isInstantiatedDatatype()) { + // We have something here like (Pair Bool Bool)---need to dig inside + // and make it (Pair BV1 BV1) + Assert(as.isParametricDatatype() && as.isInstantiatedDatatype()); + const Datatype* dt2 = &as[0].getDatatype(); + std::vector<TypeNode> fromParams, toParams; + for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { + fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); + toParams.push_back(as[i + 1]); + } + const Datatype* dt1 = d_datatypeCache[dt2]; + Assert(dt1 != NULL, "expected datatype in cache"); + Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes"); + Node out; + for(size_t i = 0; i < dt1->getNumConstructors(); ++i) { + DatatypeConstructor ctor = (*dt1)[i]; + NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); + appctorb << (*dt2)[i].getConstructor(); + for(size_t j = 0; j < ctor.getNumArgs(); ++j) { + TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); + asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType); + } + Node appctor = appctorb; + if(i == 0) { + out = appctor; + } else { + Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); + out = newOut; + } + } + return out; + } Unhandled(in); } diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 686ecbbe6..a66e02778 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -88,6 +88,31 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { Node val = rewriteAs(asa.getExpr(), asType[1]); return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr())); } + if(n.getType().isParametricDatatype() && + n.getType().isInstantiatedDatatype() && + asType.isParametricDatatype() && + asType.isInstantiatedDatatype() && + n.getType()[0] == asType[0]) { + // Here, we're doing something like rewriting a (Pair BV1 BV1) as a + // (Pair Bool Bool). + const Datatype* dt2 = &asType[0].getDatatype(); + std::vector<TypeNode> fromParams, toParams; + for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { + fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); + toParams.push_back(asType[i + 1]); + } + Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr())); + size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr()); + NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); + appctorb << (*dt2)[ctor_ix].getConstructor(); + for(size_t j = 0; j < n.getNumChildren(); ++j) { + TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType()); + asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); + appctorb << rewriteAs(n[j], asType); + } + Node out = appctorb; + return out; + } if(asType.getNumChildren() != n.getNumChildren() || n.getMetaKind() == kind::metakind::CONSTANT) { return n; |