diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 13:02:02 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 13:02:02 -0600 |
commit | 62b673a6b8444c14c169a984dd6e3fc8f685851e (patch) | |
tree | f0703edec34e3512dac340ce0059cba6368d7dd8 /src/expr/node_manager.cpp | |
parent | 7acc2844df65ab6fdbf8166653c71eaa26d4d151 (diff) |
Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 123 |
1 files changed, 55 insertions, 68 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e52776fce..e6e44928d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -461,79 +461,66 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) return TypeNode(mkTypeConst(bounds)); } -TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { - Assert(t.isTuple() || t.isRecord()); - - //AJR: not sure why .getBaseType() was used in two cases below, - // disabling this, which is necessary to fix bug 605/667, - // which involves records of INT which were mapped to records of REAL below. - TypeNode tOrig = t; - if(t.isTuple()) { - vector<TypeNode> v; - bool changed = false; - for(size_t i = 0; i < t.getNumChildren(); ++i) { - TypeNode tn = t[i]; - TypeNode base; - if(tn.isTuple() || tn.isRecord()) { - base = getDatatypeForTupleRecord(tn); - } else { - base = tn;//.getBaseType(); - } - changed = changed || (tn != base); - v.push_back(base); - } - if(changed) { - t = mkTupleType(v); - } - } else { - const Record& r = t.getRecord(); - std::vector< std::pair<std::string, Type> > v; - bool changed = false; - const Record::FieldVector& fields = r.getFields(); - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - Type tn = (*i).second; - Type base; - if(tn.isTuple() || tn.isRecord()) { - base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType(); - } else { - base = tn;//.getBaseType(); - } - changed = changed || (tn != base); - v.push_back(std::make_pair((*i).first, base)); - } - if(changed) { - t = mkRecordType(Record(v)); +TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { + std::vector< TypeNode > ts; + Debug("tuprec-debug") << "Make tuple type : "; + for (unsigned i = 0; i < types.size(); ++ i) { + CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples"); + ts.push_back( types[i] ); + Debug("tuprec-debug") << types[i] << " "; + } + Debug("tuprec-debug") << std::endl; + //index based on function type + TypeNode tindex; + if( types.empty() ){ + //do nothing (will index on null type) + }else if( types.size()==1 ){ + tindex = types[0]; + }else{ + TypeNode tt = ts.back(); + ts.pop_back(); + tindex = mkFunctionType( ts, tt ); + ts.push_back( tt ); + } + TypeNode& dtt = d_tupleAndRecordTypes[tindex]; + if(dtt.isNull()) { + Datatype dt("__cvc4_tuple"); + dt.setTuple(); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for (unsigned i = 0; i < ts.size(); ++ i) { + std::stringstream ss; + ss << "__cvc4_tuple_stor_" << i; + c.addArg(ss.str().c_str(), ts[i].toType()); } + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + dtt.setAttribute(DatatypeTupleAttr(), tindex); + Debug("tuprec-debug") << "Return type : " << dtt << std::endl; + }else{ + Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; } + Assert(!dtt.isNull()); + return dtt; +} - // if the type doesn't have an associated datatype, then make one for it - TypeNode& dtt = d_tupleAndRecordTypes[t]; +TypeNode NodeManager::mkRecordType(const Record& rec) { + //index based on type constant + TypeNode tindex = mkTypeConst(rec); + TypeNode& dtt = d_tupleAndRecordTypes[tindex]; if(dtt.isNull()) { - if(t.isTuple()) { - Datatype dt("__cvc4_tuple"); - DatatypeConstructor c("__cvc4_tuple_ctor"); - for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) { - c.addArg("__cvc4_tuple_stor", (*i).toType()); - } - dt.addConstructor(c); - dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); - Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; - dtt.setAttribute(DatatypeTupleAttr(), tOrig); - } else { - const Record& rec = t.getRecord(); - const Record::FieldVector& fields = rec.getFields(); - Datatype dt("__cvc4_record"); - DatatypeConstructor c("__cvc4_record_ctor"); - for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { - c.addArg((*i).first, (*i).second); - } - dt.addConstructor(c); - dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); - Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; - dtt.setAttribute(DatatypeRecordAttr(), tOrig); + const Record::FieldVector& fields = rec.getFields(); + Datatype dt("__cvc4_record"); + dt.setRecord(); + DatatypeConstructor c("__cvc4_record_ctor"); + for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) { + c.addArg((*i).first, (*i).second); } - } else { - Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl; + dt.addConstructor(c); + dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); + dtt.setAttribute(DatatypeRecordAttr(), tindex); + Debug("tuprec-debug") << "Return type : " << dtt << std::endl; + }else{ + Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl; } Assert(!dtt.isNull()); return dtt; |