diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
commit | 80daa7fd5917526513a510261fd3901f03949dfa (patch) | |
tree | 7fa74722e30c6e5cc59d96b045273c2bdaf27701 /src/expr | |
parent | f31163c1f6bb1816365e9f22505d9558a7bc1802 (diff) |
More simplification to internal implementation of tuples and records.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 18 | ||||
-rw-r--r-- | src/expr/datatype.h | 17 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 98 | ||||
-rw-r--r-- | src/expr/node_manager.h | 15 | ||||
-rw-r--r-- | src/expr/node_manager_attributes.h | 6 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 157 |
7 files changed, 140 insertions, 173 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 32c0bb6dd..99698df99 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -51,6 +51,10 @@ typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFin typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr; typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr; +Datatype::~Datatype(){ + delete d_record; +} + const Datatype& Datatype::datatypeOf(Expr item) { ExprManagerScope ems(item); TypeNode t = Node::fromExpr(item).getType(); @@ -133,6 +137,14 @@ void Datatype::resolve(ExprManager* em, d_involvesUt = true; } } + + if( d_isRecord ){ + std::vector< std::pair<std::string, Type> > fields; + for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){ + fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) ); + } + d_record = new Record(fields); + } } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -152,10 +164,12 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ } void Datatype::setTuple() { + PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype"); d_isTuple = true; } void Datatype::setRecord() { + PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype"); d_isRecord = true; } @@ -974,6 +988,10 @@ SelectorType DatatypeConstructorArg::getType() const { return getSelector().getType(); } +Type DatatypeConstructorArg::getRangeType() const { + return getType().getRangeType(); +} + bool DatatypeConstructorArg::isUnresolvedSelf() const throw() { return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 625fbb5d4..c64b71f5a 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -155,6 +155,11 @@ public: SelectorType getType() const; /** + * Get the range type of this argument. + */ + Type getRangeType() const; + + /** * Get the name of the type of this constructor argument * (Datatype field). Can be used for not-yet-resolved Datatypes * (in which case the name of the unresolved type, or "[self]" @@ -474,6 +479,7 @@ private: bool d_isCo; bool d_isTuple; bool d_isRecord; + Record * d_record; std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; @@ -553,6 +559,8 @@ public: */ inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false); + ~Datatype(); + /** * Add a constructor to this Datatype. Constructor names need not * be unique; they are for convenience and pretty-printing only. @@ -602,6 +610,9 @@ public: /** is this a record datatype? */ inline bool isRecord() const; + /** get the record representation for this datatype */ + inline Record * getRecord() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -772,6 +783,7 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_isCo(isCo), d_isTuple(false), d_isRecord(false), + d_record(NULL), d_constructors(), d_resolved(false), d_self(), @@ -788,6 +800,7 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo d_isCo(isCo), d_isTuple(false), d_isRecord(false), + d_record(NULL), d_constructors(), d_resolved(false), d_self(), @@ -844,6 +857,10 @@ inline bool Datatype::isRecord() const { return d_isRecord; } +inline Record * Datatype::getRecord() const { + return d_record; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index ce7a92b48..39a2a268c 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -791,7 +791,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { j != j_end; ++j) { const DatatypeConstructorArg& a = *j; - Type selectorType = a.getSelector().getType(); + Type selectorType = a.getType(); Assert(a.isResolved() && selectorType.isSelector() && SelectorType(selectorType).getDomain() == dtt, diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e6e44928d..db4269ca6 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -170,7 +170,9 @@ NodeManager::~NodeManager() { d_operators[i] = Node::null(); } - d_tupleAndRecordTypes.clear(); + //d_tupleAndRecordTypes.clear(); + d_tt_cache.d_children.clear(); + d_rt_cache.d_children.clear(); Assert(!d_attrManager->inGarbageCollection() ); while(!d_zombies.empty()) { @@ -461,6 +463,47 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) return TypeNode(mkTypeConst(bounds)); } +TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { + if( index==types.size() ){ + if( d_data.isNull() ){ + Datatype dt("__cvc4_tuple"); + dt.setTuple(); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for (unsigned i = 0; i < types.size(); ++ i) { + std::stringstream ss; + ss << "__cvc4_tuple_stor_" << i; + c.addArg(ss.str().c_str(), types[i].toType()); + } + dt.addConstructor(c); + d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); + Debug("tuprec-debug") << "Return type : " << d_data << std::endl; + } + return d_data; + }else{ + return d_children[types[index]].getTupleType( nm, types, index+1 ); + } +} + +TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) { + if( index==rec.getNumFields() ){ + if( d_data.isNull() ){ + 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); + } + dt.addConstructor(c); + d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt)); + Debug("tuprec-debug") << "Return type : " << d_data << std::endl; + } + return d_data; + }else{ + return d_children[TypeNode::fromType( rec[index].second )][rec[index].first].getRecordType( nm, rec, index+1 ); + } +} + TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { std::vector< TypeNode > ts; Debug("tuprec-debug") << "Make tuple type : "; @@ -470,60 +513,11 @@ TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { 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; + return d_tt_cache.getTupleType( this, ts ); } TypeNode NodeManager::mkRecordType(const Record& rec) { - //index based on type constant - TypeNode tindex = mkTypeConst(rec); - TypeNode& dtt = d_tupleAndRecordTypes[tindex]; - if(dtt.isNull()) { - 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); - } - 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; + return d_rt_cache.getRecordType( this, rec ); } void NodeManager::reclaimAllZombies(){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 45c9afbde..974a1ed94 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -166,7 +166,20 @@ class NodeManager { /** * A map of tuple and record types to their corresponding datatype. */ - std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes; + class TupleTypeCache { + public: + std::map< TypeNode, TupleTypeCache > d_children; + TypeNode d_data; + TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 ); + }; + class RecTypeCache { + public: + std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children; + TypeNode d_data; + TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 ); + }; + TupleTypeCache d_tt_cache; + RecTypeCache d_rt_cache; /** * Keep a count of all abstract values produced by this NodeManager. diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index 41086ac21..1f67a09a5 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -28,8 +28,6 @@ namespace attr { struct VarNameTag { }; struct GlobalVarTag { }; struct SortArityTag { }; - struct DatatypeTupleTag { }; - struct DatatypeRecordTag { }; struct TypeTag { }; struct TypeCheckedTag { }; }/* CVC4::expr::attr namespace */ @@ -37,10 +35,6 @@ namespace attr { typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr; typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; -/** Attribute true for datatype types that are replacements for tuple types */ -typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr; -/** Attribute true for datatype types that are replacements for record types */ -typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr; typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr; typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 755b16e46..eecb2c206 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -93,37 +93,21 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { t.getConst<TypeConstant>() == REAL_TYPE ); } } - if(isTuple() || isRecord()) { - if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { + if(isTuple() && t.isTuple()) { + const Datatype& dt1 = getDatatype(); + const Datatype& dt2 = t.getDatatype(); + if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){ return false; } - if(isTuple()) { - if(getNumChildren() != t.getNumChildren()) { + // r1's fields must be subtypes of r2's, in order + for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){ + if( !dt1[0][i].getRangeType().isSubtypeOf( dt2[0][i].getRangeType() ) ){ return false; } - // children must be subtypes of t's, in order - for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { - if(!(*i).isSubtypeOf(*j)) { - return false; - } - } - } else { - const Record& r1 = getRecord(); - const Record& r2 = t.getRecord(); - if(r1.getNumFields() != r2.getNumFields()) { - return false; - } - const Record::FieldVector& fields1 = r1.getFields(); - const Record::FieldVector& fields2 = r2.getFields(); - // r1's fields must be subtypes of r2's, in order - // names must match also - for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) { - if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) { - return false; - } - } } return true; + }else if( t.isRecord() && t.isRecord() ){ + //TBD } if(isFunction()) { // A function is a subtype of another if the args are the same type, and @@ -163,39 +147,21 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isSubtypeOf(NodeManager::currentNM()->realType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } - if(isTuple() || isRecord()) { - if(t.isTuple() || t.isRecord()) { - if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) { + if(isTuple() && t.isTuple()) { + const Datatype& dt1 = getDatatype(); + const Datatype& dt2 = t.getDatatype(); + if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){ + return false; + } + // r1's fields must be subtypes of r2's, in order + for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){ + if( !dt1[0][i].getRangeType().isComparableTo( dt2[0][i].getRangeType() ) ){ return false; } - if(isTuple()) { - if(getNumChildren() != t.getNumChildren()) { - return false; - } - // children must be comparable to t's, in order - for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) { - if(!(*i).isComparableTo(*j)) { - return false; - } - } - } else { - const Record& r1 = getRecord(); - const Record& r2 = t.getRecord(); - if(r1.getNumFields() != r2.getNumFields()) { - return false; - } - // r1's fields must be comparable to r2's, in order - // names must match also - const Record::FieldVector& fields1 = r1.getFields(); - const Record::FieldVector& fields2 = r2.getFields(); - for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) { - if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) { - return false; - } - } - } - return true; } + return true; + }else if( isRecord() && t.isRecord() ){ + //TBD } else if(isParametricDatatype() && t.isParametricDatatype()) { Assert(getKind() == kind::PARAMETRIC_DATATYPE); Assert(t.getKind() == kind::PARAMETRIC_DATATYPE); @@ -271,13 +237,13 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { /** Is this a tuple type? */ bool TypeNode::isTuple() const { - return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) || + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) || ( isPredicateSubtype() && getSubtypeParentType().isTuple() ); } /** Is this a record type? */ bool TypeNode::isRecord() const { - return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) ) || + return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) || ( isPredicateSubtype() && getSubtypeParentType().isRecord() ); } @@ -294,14 +260,16 @@ vector<TypeNode> TypeNode::getTupleTypes() const { Assert(dt.getNumConstructors()==1); vector<TypeNode> types; for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { - types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType())); + types.push_back(TypeNode::fromType(dt[0][i].getRangeType())); } return types; } const Record& TypeNode::getRecord() const { Assert(isRecord()); - return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); + const Datatype & dt = getDatatype(); + return *(dt.getRecord()); + //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); } vector<TypeNode> TypeNode::getSExprTypes() const { @@ -449,61 +417,24 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ Assert(t1.isInteger()); return TypeNode(); } -/* - case kind::TUPLE_TYPE: { - // if the other == this one, we returned already, above - if(t0.getBaseType() == t1) { - return t1; - } - if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector<TypeNode> types; - // construct childwise leastCommonType, if one exists - for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) { - TypeNode kid = leastCommonTypeNode(*i, *j); - if(kid.isNull()) { - // no common supertype: types t0, t1 not compatible - return TypeNode(); - } - types.push_back(kid); - } - // if we make it here, we constructed the least common type - return NodeManager::currentNM()->mkTupleType(types); - } - case kind::RECORD_TYPE: { - // if the other == this one, we returned already, above - if(t0.getBaseType() == t1) { - return t1; - } - const Record& r0 = t0.getConst<Record>(); - if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector< std::pair<std::string, Type> > fields; - const Record& r1 = t1.getConst<Record>(); - const Record::FieldVector& fields0 = r0.getFields(); - const Record::FieldVector& fields1 = r1.getFields(); - // construct childwise leastCommonType, if one exists - for(Record::FieldVector::const_iterator i = fields0.begin(), j = fields1.begin(); i != fields0.end(); ++i, ++j) { - TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second)); - if((*i).first != (*j).first || kid.isNull()) { - // if field names differ, or no common supertype, then - // types t0, t1 not compatible - return TypeNode(); - } - fields.push_back(std::make_pair((*i).first, kid.toType())); - } - // if we make it here, we constructed the least common type - return NodeManager::currentNM()->mkRecordType(Record(fields)); - } -*/ case kind::DATATYPE_TYPE: - // t1 might be a subtype tuple or record - if(t1.getBaseType() == t0) { - return t0; + if( t0.isTuple() && t1.isTuple() ){ + const Datatype& dt1 = t0.getDatatype(); + const Datatype& dt2 = t1.getDatatype(); + if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ + std::vector< TypeNode > lc_types; + for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){ + TypeNode tc = leastCommonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ) ); + if( tc.isNull() ){ + return tc; + }else{ + lc_types.push_back( tc ); + } + } + return NodeManager::currentNM()->mkTupleType( lc_types ); + } + }else if( t0.isRecord() && t1.isRecord() ){ + //TBD } // otherwise no common ancestor return TypeNode(); |