From 0a983828b92c573269b50cd95e23b9f311337073 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 16 Oct 2015 14:27:15 +0200 Subject: [PATCH] Throw error for recursively defined types involving Boolean. --- src/smt/boolean_terms.cpp | 237 ++++++++++++++++++++------------------ src/smt/boolean_terms.h | 2 +- 2 files changed, 127 insertions(+), 112 deletions(-) diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 54a6b5416..69dc06e47 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -121,7 +121,8 @@ static inline bool isBoolean(TNode top, unsigned i) { // Note this isn't the case any longer, and parts of what's below have // been repurposed for *forward* conversion, meaning this works in either // direction. -Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { +Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw() { + Debug("boolean-terms2") << "Rewrite as " << in << " " << as << std::endl; if(in.getType() == as) { return in; } @@ -132,128 +133,140 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) { return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in); } - if(in.getType().isRecord()) { - Assert(as.isRecord()); - const Record& inRec = in.getType().getConst(); - const Record& asRec = as.getConst(); - Assert(inRec.getNumFields() == asRec.getNumFields()); - NodeBuilder<> nb(kind::RECORD); - nb << NodeManager::currentNM()->mkConst(asRec); - for(size_t i = 0; i < asRec.getNumFields(); ++i) { - Assert(inRec[i].first == asRec[i].first); - Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in); - if(inRec[i].second != asRec[i].second) { - arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second)); + TypeNode in_t = in.getType(); + if( processing.find( in_t )==processing.end() ){ + processing[in_t] = true; + if(in.getType().isRecord()) { + Assert(as.isRecord()); + const Record& inRec = in.getType().getConst(); + const Record& asRec = as.getConst(); + Assert(inRec.getNumFields() == asRec.getNumFields()); + NodeBuilder<> nb(kind::RECORD); + nb << NodeManager::currentNM()->mkConst(asRec); + for(size_t i = 0; i < asRec.getNumFields(); ++i) { + Assert(inRec[i].first == asRec[i].first); + Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in); + if(inRec[i].second != asRec[i].second) { + arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing); + } + nb << arg; } - nb << arg; + Node out = nb; + processing.erase( in_t ); + return out; } - Node out = nb; - return out; - } - if(in.getType().isTuple()) { - Assert(as.isTuple()); - Assert(in.getType().getNumChildren() == as.getNumChildren()); - NodeBuilder<> nb(kind::TUPLE); - for(size_t i = 0; i < as.getNumChildren(); ++i) { - Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in); - if(in.getType()[i] != as[i]) { - arg = rewriteAs(arg, as[i]); + if(in.getType().isTuple()) { + Assert(as.isTuple()); + Assert(in.getType().getNumChildren() == as.getNumChildren()); + NodeBuilder<> nb(kind::TUPLE); + for(size_t i = 0; i < as.getNumChildren(); ++i) { + Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in); + if(in.getType()[i] != as[i]) { + arg = rewriteAs(arg, as[i], processing); + } + nb << arg; } - nb << arg; - } - Node out = nb; - return out; - } - if(in.getType().isDatatype()) { - if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); + Node out = nb; + processing.erase( in_t ); + return out; } - Assert(as.isDatatype()); - const Datatype* dt2 = &as.getDatatype(); - const Datatype* dt1; - if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { - dt1 = d_datatypeCache[dt2]; - } else { - dt1 = d_datatypeReverseCache[dt2]; - } - Assert(dt1 != NULL, "expected datatype in cache"); - 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) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + if(in.getType().isDatatype()) { + if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { + processing.erase( in_t ); + return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); } - Node appctor = appctorb; - if(i == 0) { - out = appctor; + Assert(as.isDatatype()); + const Datatype* dt2 = &as.getDatatype(); + const Datatype* dt1; + if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { + dt1 = d_datatypeCache[dt2]; } else { - Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); - out = newOut; + dt1 = d_datatypeReverseCache[dt2]; } + Assert(dt1 != NULL, "expected datatype in cache"); + 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) { + 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) { + out = appctor; + } else { + Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); + out = newOut; + } + } + processing.erase( in_t ); + return out; } - 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()); - Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime); - Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam); - Assert(out.getType() == as); - 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 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; - if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { - dt1 = d_datatypeCache[dt2]; - } else { - dt1 = d_datatypeReverseCache[dt2]; + 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; } - 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_TOTAL, ctor[j].getSelector(), in), asType); + 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 fromParams, toParams; + for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { + fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); + toParams.push_back(as[i + 1]); } - Node appctor = appctorb; - if(i == 0) { - out = appctor; + const Datatype* dt1; + if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { + dt1 = d_datatypeCache[dt2]; } else { - Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); - out = newOut; + dt1 = d_datatypeReverseCache[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_TOTAL, ctor[j].getSelector(), in), asType, processing); + } + Node appctor = appctorb; + if(i == 0) { + out = appctor; + } else { + Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); + out = newOut; + } + } + processing.erase( in_t ); + return out; } - return out; + Unhandled(in); + }else{ + Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl; + exit( 0 ); } - - Unhandled(in); } const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() { @@ -573,7 +586,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa Node var = nm->mkBoundVar(t[j]); boundVarsBuilder << var; if(t[j] != argTypes[j]) { - bodyBuilder << rewriteAs(var, argTypes[j]); + std::map< TypeNode, bool > processing; + bodyBuilder << rewriteAs(var, argTypes[j], processing); } else { bodyBuilder << var; } @@ -581,7 +595,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa Node boundVars = boundVarsBuilder; Node body = bodyBuilder; if(t.getRangeType() != rangeType) { - Node convbody = rewriteAs(body, t.getRangeType()); + std::map< TypeNode, bool > processing; + Node convbody = rewriteAs(body, t.getRangeType(), processing); body = convbody; } Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index ed676c667..e1865f29f 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -72,7 +72,7 @@ class BooleanTermConverter { /** A (reverse) cache for Boolean term datatype conversion */ BooleanTermDatatypeCache d_datatypeReverseCache; - Node rewriteAs(TNode in, TypeNode as) throw(); + Node rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw(); /** * Scan a datatype for and convert as necessary. -- 2.30.2