diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/boolean_terms.cpp | 80 |
1 files changed, 40 insertions, 40 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 51ae0fd11..ba7902d32 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -137,13 +137,17 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, TypeNode in_t = in.getType(); if( processing.find( in_t )==processing.end() ){ processing[in_t] = true; - if(in.getType().isDatatype()) { - if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { - processing.erase( in_t ); - return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); + 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]); } - Assert(as.isDatatype()); - const Datatype* dt2 = &as.getDatatype(); const Datatype* dt1; if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { dt1 = d_datatypeCache[dt2]; @@ -151,14 +155,16 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, dt1 = d_datatypeReverseCache[dt2]; } Assert(dt1 != NULL, "expected datatype in cache"); - Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes"); + 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) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing); + 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_TOTAL, ctor[j].getSelector(), in), asType, processing); } Node appctor = appctorb; if(i == 0) { @@ -171,35 +177,13 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, processing.erase( in_t ); return out; } - if(in.getType().isArray()) { - // convert in to in' - // e.g. in : (Array Int Bool) - // for in' : (Array Int (_ BitVec 1)) - // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x] - Assert(as.isArray()); - Assert(as.getArrayIndexType() == in.getType().getArrayIndexType()); - Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType()); - Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType()); - Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x); - Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x); - Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing); - Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime); - Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam); - Assert(out.getType() == as); - processing.erase( in_t ); - 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]); + if(in.getType().isDatatype()) { + if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { + processing.erase( in_t ); + return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); } + Assert(as.isDatatype()); + const Datatype* dt2 = &as.getDatatype(); const Datatype* dt1; if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { dt1 = d_datatypeCache[dt2]; @@ -207,16 +191,14 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, dt1 = d_datatypeReverseCache[dt2]; } Assert(dt1 != NULL, "expected datatype in cache"); - Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes"); + Assert(*dt1 == in.getType().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_TOTAL, ctor[j].getSelector(), in), asType, processing); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing); } Node appctor = appctorb; if(i == 0) { @@ -229,6 +211,24 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, processing.erase( in_t ); return out; } + if(in.getType().isArray()) { + // convert in to in' + // e.g. in : (Array Int Bool) + // for in' : (Array Int (_ BitVec 1)) + // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x] + Assert(as.isArray()); + Assert(as.getArrayIndexType() == in.getType().getArrayIndexType()); + Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType()); + Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType()); + Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x); + Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x); + Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing); + Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime); + Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam); + Assert(out.getType() == as); + processing.erase( in_t ); + return out; + } Unhandled(in); }else{ Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl; |