diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
commit | c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 (patch) | |
tree | f4a8372d8cd693df5f33e8d49cea53dbb418349e /src/expr | |
parent | 623e701247ed08e3f59d57b18ebe42f4d4db221e (diff) |
Bug fixes and refactoring of parametric datatypes, add some regressions.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 129 | ||||
-rw-r--r-- | src/expr/datatype.h | 30 | ||||
-rw-r--r-- | src/expr/type.cpp | 10 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 5 | ||||
-rw-r--r-- | src/expr/type_node.h | 12 |
5 files changed, 106 insertions, 80 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 537fc2b1a..bc39ced13 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -173,14 +173,14 @@ void Datatype::setRecord() { d_isRecord = true; } -Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { +Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); std::vector< Type > processing; - computeCardinality( processing ); + computeCardinality( t, processing ); return d_card; } -Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ +Cardinality Datatype::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ d_card = Cardinality::INTEGERS; @@ -188,7 +188,7 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons processing.push_back( d_self ); Cardinality c = 0; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - c += (*i).computeCardinality( processing ); + c += (*i).computeCardinality( t, processing ); } d_card = c; processing.pop_back(); @@ -196,64 +196,64 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons return d_card; } -bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) { +bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - if( d_card_rec_singleton==0 ){ + if( d_card_rec_singleton[t]==0 ){ if( isCodatatype() ){ - Assert( d_card_u_assume.empty() ); + Assert( d_card_u_assume[t].empty() ); std::vector< Type > processing; - if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){ - d_card_rec_singleton = 1; + if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){ + d_card_rec_singleton[t] = 1; }else{ - d_card_rec_singleton = -1; + d_card_rec_singleton[t] = -1; } - if( d_card_rec_singleton==1 ){ - Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl; - for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ - Trace("dt-card") << " " << d_card_u_assume [i] << std::endl; + if( d_card_rec_singleton[t]==1 ){ + Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume[t].size() << " uninterpreted sorts: " << std::endl; + for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){ + Trace("dt-card") << " " << d_card_u_assume[t][i] << std::endl; } Trace("dt-card") << std::endl; } }else{ - d_card_rec_singleton = -1; + d_card_rec_singleton[t] = -1; } } - return d_card_rec_singleton==1; + return d_card_rec_singleton[t]==1; } -unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) { - return d_card_u_assume.size(); +unsigned Datatype::getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException) { + return d_card_u_assume[t].size(); } -Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) { - return d_card_u_assume[i]; +Type Datatype::getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException) { + return d_card_u_assume[t][i]; } -bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){ +bool Datatype::computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){ if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ return true; }else{ - if( d_card_rec_singleton==0 ){ + if( d_card_rec_singleton[t]==0 ){ //if not yet computed if( d_constructors.size()==1 ){ bool success = false; processing.push_back( d_self ); for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) { - Type t = ((SelectorType)d_constructors[0][i].getType()).getRangeType(); + Type tc = ((SelectorType)d_constructors[0][i].getType()).getRangeType(); //if it is an uninterpreted sort, then we depend on it having cardinality one - if( t.isSort() ){ - if( std::find( u_assume.begin(), u_assume.end(), t )==u_assume.end() ){ - u_assume.push_back( t ); + if( tc.isSort() ){ + if( std::find( u_assume.begin(), u_assume.end(), tc )==u_assume.end() ){ + u_assume.push_back( tc ); } //if it is a datatype, recurse - }else if( t.isDatatype() ){ - const Datatype & dt = ((DatatypeType)t).getDatatype(); - if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){ + }else if( tc.isDatatype() ){ + const Datatype & dt = ((DatatypeType)tc).getDatatype(); + if( !dt.computeCardinalityRecSingleton( t, processing, u_assume ) ){ return false; }else{ success = true; } //if it is a builtin type, it must have cardinality one - }else if( !t.getCardinality().isOne() ){ + }else if( !tc.getCardinality().isOne() ){ return false; } } @@ -262,12 +262,12 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, }else{ return false; } - }else if( d_card_rec_singleton==-1 ){ + }else if( d_card_rec_singleton[t]==-1 ){ return false; }else{ - for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ - if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[i] )==u_assume.end() ){ - u_assume.push_back( d_card_u_assume[i] ); + for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){ + if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[t][i] )==u_assume.end() ){ + u_assume.push_back( d_card_u_assume[t][i] ); } } return true; @@ -275,7 +275,7 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, } } -bool Datatype::isFinite() const throw(IllegalArgumentException) { +bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -286,7 +286,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { return self.getAttribute(DatatypeFiniteAttr()); } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! (*i).isFinite()) { + if(! (*i).isFinite( t )) { self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), false); return false; @@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { return true; } -bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) { +bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); @@ -310,7 +310,7 @@ bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! (*i).isInterpretedFinite()) { + if(! (*i).isInterpretedFinite( t )) { return false; } } @@ -787,7 +787,7 @@ bool DatatypeConstructor::isSygusIdFunc() const { return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; } -Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { +Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); Cardinality c = 1; @@ -800,15 +800,24 @@ Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentExc } /** compute the cardinality of this datatype */ -Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ +Cardinality DatatypeConstructor::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){ Cardinality c = 1; + std::vector< Type > instTypes; + std::vector< Type > paramTypes; + if( DatatypeType(t).isParametric() ){ + paramTypes = DatatypeType(t).getDatatype().getParameters(); + instTypes = DatatypeType(t).getParamTypes(); + } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - Type t = SelectorType((*i).getSelector().getType()).getRangeType(); - if( t.isDatatype() ){ - const Datatype& dt = ((DatatypeType)t).getDatatype(); - c *= dt.computeCardinality( processing ); + Type tc = SelectorType((*i).getSelector().getType()).getRangeType(); + if( DatatypeType(t).isParametric() ){ + tc = tc.substitute( paramTypes, instTypes ); + } + if( tc.isDatatype() ){ + const Datatype& dt = ((DatatypeType)tc).getDatatype(); + c *= dt.computeCardinality( t, processing ); }else{ - c *= t.getCardinality(); + c *= tc.getCardinality(); } } return c; @@ -828,7 +837,7 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) } -bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { +bool DatatypeConstructor::isFinite( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context @@ -838,8 +847,18 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeFiniteComputedAttr())) { return self.getAttribute(DatatypeFiniteAttr()); } + std::vector< Type > instTypes; + std::vector< Type > paramTypes; + if( DatatypeType(t).isParametric() ){ + paramTypes = DatatypeType(t).getDatatype().getParameters(); + instTypes = DatatypeType(t).getParamTypes(); + } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! (*i).getRangeType().getCardinality().isFinite()) { + Type tc = (*i).getRangeType(); + if( DatatypeType(t).isParametric() ){ + tc = tc.substitute( paramTypes, instTypes ); + } + if(! tc.getCardinality().isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), false); return false; @@ -850,7 +869,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return true; } -bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) { +bool DatatypeConstructor::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -859,9 +878,19 @@ bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentExcep if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } + std::vector< Type > instTypes; + std::vector< Type > paramTypes; + if( DatatypeType(t).isParametric() ){ + paramTypes = DatatypeType(t).getDatatype().getParameters(); + instTypes = DatatypeType(t).getParamTypes(); + } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - TypeNode t = TypeNode::fromType( (*i).getRangeType() ); - if(!t.isInterpretedFinite()) { + Type tc = (*i).getRangeType(); + if( DatatypeType(t).isParametric() ){ + tc = tc.substitute( paramTypes, instTypes ); + } + TypeNode tcn = TypeNode::fromType( tc ); + if(!tcn.isInterpretedFinite()) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); return false; diff --git a/src/expr/datatype.h b/src/expr/datatype.h index f81d2358d..49189959b 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -221,7 +221,7 @@ private: const std::vector< DatatypeType >& paramReplacements); /** compute the cardinality of this datatype */ - Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); + Cardinality computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute whether this datatype is well-founded */ bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute ground term */ @@ -329,21 +329,21 @@ public: * Return the cardinality of this constructor (the product of the * cardinalities of its arguments). */ - Cardinality getCardinality() const throw(IllegalArgumentException); + Cardinality getCardinality( Type t ) const throw(IllegalArgumentException); /** * Return true iff this constructor is finite (it is nullary or * each of its argument types are finite). This function can * only be called for resolved constructors. */ - bool isFinite() const throw(IllegalArgumentException); + bool isFinite( Type t ) const throw(IllegalArgumentException); /** * Return true iff this constructor is finite (it is nullary or * each of its argument types are finite) under assumption * uninterpreted sorts are finite. This function can * only be called for resolved constructors. */ - bool isInterpretedFinite() const throw(IllegalArgumentException); + bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -497,10 +497,10 @@ private: mutable Cardinality d_card; // is this type a recursive singleton type - mutable int d_card_rec_singleton; + mutable std::map< Type, int > d_card_rec_singleton; // if d_card_rec_singleton is true, // infinite cardinality depends on at least one of the following uninterpreted sorts having cardinality > 1 - mutable std::vector< Type > d_card_u_assume; + mutable std::map< Type, std::vector< Type > > d_card_u_assume; // is this well-founded mutable int d_well_founded; // ground term for this datatype @@ -542,9 +542,9 @@ private: friend class ExprManager;// for access to resolve() /** compute the cardinality of this datatype */ - Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); + Cardinality computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute whether this datatype is a recursive singleton */ - bool computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException); + bool computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException); /** compute whether this datatype is well-founded */ bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute ground term */ @@ -619,7 +619,7 @@ public: * cardinalities of its constructors). The Datatype must be * resolved. */ - Cardinality getCardinality() const throw(IllegalArgumentException); + Cardinality getCardinality( Type t ) const throw(IllegalArgumentException); /** * Return true iff this Datatype is finite (all constructors are @@ -627,7 +627,7 @@ public: * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. */ - bool isFinite() const throw(IllegalArgumentException); + bool isFinite( Type t ) const throw(IllegalArgumentException); /** * Return true iff this Datatype is finite (all constructors are * finite, i.e., there are finitely many ground terms) under the @@ -635,7 +635,7 @@ public: * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. */ - bool isInterpretedFinite() const throw(IllegalArgumentException); + bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground @@ -646,12 +646,12 @@ public: /** * Return true iff this datatype is a recursive singleton */ - bool isRecursiveSingleton() const throw(IllegalArgumentException); + bool isRecursiveSingleton( Type t ) const throw(IllegalArgumentException); /** get number of recursive singleton argument types */ - unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException); - Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException); + unsigned getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException); + Type getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException); /** * Construct and return a ground term of this Datatype. The @@ -836,7 +836,6 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_involvesExt(false), d_involvesUt(false), d_card(CardinalityUnknown()), - d_card_rec_singleton(0), d_well_founded(0) { } @@ -853,7 +852,6 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo d_involvesExt(false), d_involvesUt(false), d_card(CardinalityUnknown()), - d_card_rec_singleton(0), d_well_founded(0) { } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 11a45db79..5f62317ee 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -250,7 +250,7 @@ bool Type::isFloatingPoint() const { /** Is this a datatype type? */ bool Type::isDatatype() const { NodeManagerScope nms(d_nodeManager); - return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype(); + return d_typeNode->isDatatype(); } /** Is this the Constructor type? */ @@ -564,13 +564,7 @@ std::vector<Type> ConstructorType::getArgTypes() const { const Datatype& DatatypeType::getDatatype() const { NodeManagerScope nms(d_nodeManager); - if( d_typeNode->isParametricDatatype() ) { - PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this); - const Datatype& dt = (*d_typeNode)[0].getDatatype(); - return dt; - } else { - return d_typeNode->getDatatype(); - } + return d_typeNode->getDatatype(); } bool DatatypeType::isParametric() const { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ede710dad..f11aa019e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -72,9 +72,10 @@ bool TypeNode::isInterpretedFinite() const { if( options::finiteModelFind() ){ if( isSort() ){ return true; - }else if( isDatatype() || isParametricDatatype() ){ + }else if( isDatatype() ){ + TypeNode tn = *this; const Datatype& dt = getDatatype(); - return dt.isInterpretedFinite(); + return dt.isInterpretedFinite( tn.toType() ); }else if( isArray() ){ return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite(); }else if( isSet() ) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9fffbdeb2..0abbc9a1b 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -969,7 +969,7 @@ inline bool TypeNode::isBitVector() const { /** Is this a datatype type */ inline bool TypeNode::isDatatype() const { - return getKind() == kind::DATATYPE_TYPE || + return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE || ( isPredicateSubtype() && getSubtypeParentType().isDatatype() ); } @@ -1023,9 +1023,13 @@ inline bool TypeNode::isBitVector(unsigned size) const { /** Get the datatype specification from a datatype type */ inline const Datatype& TypeNode::getDatatype() const { Assert(isDatatype()); - //return getConst<Datatype>(); - DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); - return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() ); + if( getKind() == kind::DATATYPE_TYPE ){ + DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); + return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() ); + }else{ + Assert( getKind() == kind::PARAMETRIC_DATATYPE ); + return (*this)[0].getDatatype(); + } } /** Get the exponent size of this floating-point type */ |