From 80daa7fd5917526513a510261fd3901f03949dfa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 15 Feb 2016 18:10:42 -0600 Subject: [PATCH] More simplification to internal implementation of tuples and records. --- src/compat/cvc3_compat.cpp | 3 +- src/expr/datatype.cpp | 18 ++ src/expr/datatype.h | 17 ++ src/expr/expr_manager_template.cpp | 2 +- src/expr/node_manager.cpp | 98 +++++------ src/expr/node_manager.h | 15 +- src/expr/node_manager_attributes.h | 6 - src/expr/type_node.cpp | 157 +++++------------- src/smt/boolean_terms.cpp | 20 --- src/theory/datatypes/kinds | 22 --- src/theory/datatypes/theory_datatypes.cpp | 14 -- .../datatypes/theory_datatypes_type_rules.h | 61 ------- src/theory/datatypes/type_enumerator.h | 86 ---------- .../quantifiers/quantifiers_rewriter.cpp | 3 +- src/theory/quantifiers/term_database.cpp | 4 +- 15 files changed, 144 insertions(+), 382 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 52174dce0..a9982e336 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1818,8 +1818,7 @@ Expr ValidityChecker::recordExpr(const std::vector& fields, Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) { Type t = record.getType(); const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); - const CVC4::Record& rec = ((CVC4::DatatypeType)t).getRecord(); - unsigned index = rec.getIndex(field); + unsigned index = CVC4::Datatype::indexOf( dt[0].getSelector(field) ); return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record); } 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 DatatypeFin typedef expr::Attribute DatatypeUFiniteAttr; typedef expr::Attribute 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 > fields; + for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){ + fields.push_back( std::pair( (*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 @@ -154,6 +154,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 @@ -474,6 +479,7 @@ private: bool d_isCo; bool d_isTuple; bool d_isRecord; + Record * d_record; std::vector d_constructors; bool d_resolved; Type d_self; @@ -553,6 +559,8 @@ public: */ inline Datatype(std::string name, const std::vector& 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& 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& types) { std::vector< TypeNode > ts; Debug("tuprec-debug") << "Make tuple type : "; @@ -470,60 +513,11 @@ TypeNode NodeManager::mkTupleType(const std::vector& 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 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 VarNameAttr; typedef Attribute GlobalVarAttr; typedef Attribute SortArityAttr; -/** Attribute true for datatype types that are replacements for tuple types */ -typedef expr::Attribute DatatypeTupleAttr; -/** Attribute true for datatype types that are replacements for record types */ -typedef expr::Attribute DatatypeRecordAttr; typedef expr::Attribute TypeAttr; typedef expr::Attribute 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() == 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; irealType())) { 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 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::getTupleTypes() const { Assert(dt.getNumConstructors()==1); vector 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(); + const Datatype & dt = getDatatype(); + return *(dt.getRecord()); + //return getAttribute(expr::DatatypeRecordAttr()).getConst(); } vector 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 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(); - if(!t1.isRecord() || r0.getNumFields() != t1.getConst().getNumFields()) { - // no compatibility between t0, t1 - return TypeNode(); - } - std::vector< std::pair > fields; - const Record& r1 = t1.getConst(); - 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; imkTupleType( lc_types ); + } + }else if( t0.isRecord() && t1.isRecord() ){ + //TBD } // otherwise no common ancestor return TypeNode(); diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 07d78a6fd..1adc71d70 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -137,26 +137,6 @@ 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().isRecord()) { - Assert(as.isRecord()); - const Record& inRec = in.getType().getRecord(); - const Record& asRec = as.getRecord(); - Assert(inRec.getNumFields() == asRec.getNumFields()); - const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype(); - NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR); - 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(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in); - if(inRec[i].second != asRec[i].second) { - arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing); - } - nb << arg; - } - Node out = nb; - processing.erase( in_t ); - return out; - } if(in.getType().isDatatype()) { if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { processing.erase( in_t ); diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index c31a462bd..d035f0fa7 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -85,12 +85,6 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType # constructor applications are constant if they are applied only to constants construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule -## for co-datatypes -operator MU 2 "a mu operator, first argument is a bound variable, second argument is body" -typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule -# mu applications are constant expressions -construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule - constant TUPLE_UPDATE_OP \ ::CVC4::TupleUpdate \ ::CVC4::TupleUpdateHashFunction \ @@ -99,22 +93,6 @@ constant TUPLE_UPDATE_OP \ parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index" typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule -constant RECORD_TYPE \ - ::CVC4::Record \ - ::CVC4::RecordHashFunction \ - "expr/record.h" \ - "record type" -cardinality RECORD_TYPE \ - "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \ - "theory/datatypes/theory_datatypes_type_rules.h" -well-founded RECORD_TYPE \ - "::CVC4::theory::datatypes::RecordProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \ - "theory/datatypes/theory_datatypes_type_rules.h" -enumerator RECORD_TYPE \ - "::CVC4::theory::datatypes::RecordEnumerator" \ - "theory/datatypes/type_enumerator.h" - constant RECORD_UPDATE_OP \ ::CVC4::RecordUpdate \ ::CVC4::RecordUpdateHashFunction \ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index ad2b1a297..51300bfba 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -582,20 +582,6 @@ Node TheoryDatatypes::ppRewrite(TNode in) { return n; } - if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { - Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; - Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl; - if(t.isTuple()) { - Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl; - Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl; - t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr())); - } else { - Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl; - Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl; - t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr())); - } - } - if( in.getKind()==EQUAL ){ Node nn; std::vector< Node > rew; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 477ce6ba5..e50d714e7 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -210,49 +210,6 @@ struct DatatypeAscriptionTypeRule { } };/* struct DatatypeAscriptionTypeRule */ -/* For co-datatypes */ -class DatatypeMuTypeRule { -private: - //a Mu-expression is constant iff its body is composed of constructors applied to constant expr and bound variables only - inline static bool computeIsConstNode(TNode n, std::vector< TNode >& fv ){ - if( n.getKind()==kind::MU ){ - fv.push_back( n[0] ); - bool ret = computeIsConstNode( n[1], fv ); - fv.pop_back(); - return ret; - }else if( n.isConst() || std::find( fv.begin(), fv.end(), n )!=fv.end() ){ - return true; - }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){ - for( unsigned i=0; i fv; - return computeIsConstNode( n, fv ); - } -}; - - struct ConstructorProperties { inline static Cardinality computeCardinality(TypeNode type) { // Constructors aren't exactly functions, they're like @@ -276,7 +233,6 @@ struct TupleUpdateTypeRule { if(check) { if(!tupleType.isTuple()) { throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple"); - tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr()); } if(tu.getIndex() >= tupleType.getTupleLength()) { std::stringstream ss; @@ -313,23 +269,6 @@ struct RecordUpdateTypeRule { } };/* struct RecordUpdateTypeRule */ -struct RecordProperties { - inline static Node mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::RECORD_TYPE); - return Node::null(); - } - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - return true; - } - inline static Cardinality computeCardinality(TypeNode type) { - Cardinality card(1); - return card; - } - inline static bool isWellFounded(TypeNode type) { - return true; - } -};/* struct RecordProperties */ - class DtSizeTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 1f30498d6..2cf72e8e9 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -177,92 +177,6 @@ public: };/* DatatypesEnumerator */ - -class RecordEnumerator : public TypeEnumeratorBase { - TypeEnumeratorProperties * d_tep; - TypeEnumerator** d_enumerators; - - /** Allocate and initialize the delegate enumerators */ - void newEnumerators() { - const Record& rec = getType().getConst(); - d_enumerators = new TypeEnumerator*[rec.getNumFields()]; - for(size_t i = 0; i < rec.getNumFields(); ++i) { - d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second)); - } - } - - void deleteEnumerators() throw() { - if(d_enumerators != NULL) { - const Record& rec = getType().getConst(); - for(size_t i = 0; i < rec.getNumFields(); ++i) { - delete d_enumerators[i]; - } - delete [] d_enumerators; - d_enumerators = NULL; - } - } - -public: - - RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() : - TypeEnumeratorBase(type), d_tep(tep) { - Assert(type.isRecord()); - newEnumerators(); - } - - RecordEnumerator(const RecordEnumerator& re) throw() : - TypeEnumeratorBase(re.getType()), - d_tep(re.d_tep), - d_enumerators(NULL) { - - if(re.d_enumerators != NULL) { - newEnumerators(); - for(size_t i = 0; i < getType().getNumChildren(); ++i) { - *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]); - } - } - } - - virtual ~RecordEnumerator() throw() { - deleteEnumerators(); - } - - Node operator*() throw(NoMoreValuesException) { - if(isFinished()) { - throw NoMoreValuesException(getType()); - } - - - return Node::null(); - } - - RecordEnumerator& operator++() throw() { - if(isFinished()) { - return *this; - } - - size_t i; - const Record& rec = getType().getConst(); - for(i = 0; i < rec.getNumFields(); ++i) { - if(d_enumerators[i]->isFinished()) { - *d_enumerators[i] = TypeEnumerator(TypeNode::fromType(rec[i].second)); - } else { - ++*d_enumerators[i]; - return *this; - } - } - - deleteEnumerators(); - - return *this; - } - - bool isFinished() throw() { - return d_enumerators == NULL; - } - -};/* RecordEnumerator */ - }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index afe8cd598..881210d78 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -932,8 +932,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto newChildren.push_back( Node::fromExpr( c.getConstructor() ) ); std::vector< Node > newVars; for( unsigned j=0; jmkBoundVar( tn ); newChildren.push_back( v ); newVars.push_back( v ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 560f68810..a679ccfa8 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -855,7 +855,7 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ for( unsigned j=0; j ssc; if( tn==ntn ){ ssc.push_back( n ); @@ -1050,7 +1050,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) { const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); for( unsigned i=0; i