From 44c278ce99b7d84b070d260196c44569209f1528 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 3 Dec 2016 13:54:55 -0600 Subject: [PATCH] Fix unit test for datatypes, add interface functions to datatypes. --- src/expr/datatype.cpp | 39 ++++++++++++++++++++++++++++++++++++++- src/expr/datatype.h | 17 ++++++++++++++++- 2 files changed, 54 insertions(+), 2 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index bc39ced13..02edab533 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -175,11 +175,17 @@ void Datatype::setRecord() { Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); std::vector< Type > processing; computeCardinality( t, processing ); return d_card; } +Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { + PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric"); + return getCardinality( d_self ); +} + 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() ){ @@ -198,7 +204,8 @@ Cardinality Datatype::computeCardinality( Type t, std::vector< Type >& processin bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - if( d_card_rec_singleton[t]==0 ){ + Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); + if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){ if( isCodatatype() ){ Assert( d_card_u_assume[t].empty() ); std::vector< Type > processing; @@ -221,13 +228,33 @@ bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentExcepti return d_card_rec_singleton[t]==1; } +bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) { + PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric"); + return isRecursiveSingleton( d_self ); +} + unsigned Datatype::getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException) { + Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() ); + Assert( isRecursiveSingleton( t ) ); return d_card_u_assume[t].size(); } + +unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) { + PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric"); + return getNumRecursiveSingletonArgTypes( d_self ); +} + Type Datatype::getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException) { + Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() ); + Assert( isRecursiveSingleton( t ) ); return d_card_u_assume[t][i]; } +Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) { + PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric"); + return getRecursiveSingletonArgType( d_self, i ); +} + 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; @@ -277,6 +304,7 @@ bool Datatype::computeCardinalityRecSingleton( Type t, std::vector< Type >& proc bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); @@ -296,9 +324,14 @@ bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) { self.setAttribute(DatatypeFiniteAttr(), true); return true; } +bool Datatype::isFinite() const throw(IllegalArgumentException) { + PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric"); + return isFinite( d_self ); +} bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); TypeNode self = TypeNode::fromType(d_self); @@ -318,6 +351,10 @@ bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentExceptio self.setAttribute(DatatypeUFiniteAttr(), true); return true; } +bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) { + PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric"); + return isInterpretedFinite( d_self ); +} bool Datatype::isWellFounded() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 49189959b..5a09730d0 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -618,24 +618,31 @@ public: * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be * resolved. + * Version taking Type t is required for parametric datatypes. */ Cardinality getCardinality( Type t ) const throw(IllegalArgumentException); + Cardinality getCardinality() const throw(IllegalArgumentException); /** * Return true iff this Datatype is finite (all constructors are * finite, i.e., there are finitely many ground terms). If the * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. + * Version taking Type t is required for parametric. */ bool isFinite( Type t ) const throw(IllegalArgumentException); + bool isFinite() const throw(IllegalArgumentException); + /** * Return true iff this Datatype is finite (all constructors are * finite, i.e., there are finitely many ground terms) under the * assumption unintepreted sorts are finite. If the * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. + * Version taking Type t is required for parametric datatypes. */ bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException); + bool isInterpretedFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground @@ -645,13 +652,21 @@ public: /** * Return true iff this datatype is a recursive singleton + * Version taking Type t is required for parametric datatypes. */ bool isRecursiveSingleton( Type t ) const throw(IllegalArgumentException); + bool isRecursiveSingleton() const throw(IllegalArgumentException); - /** get number of recursive singleton argument types */ + /** + * Get recursive singleton argument types (uninterpreted sorts that the singleton cardinality + * of this datatype is dependent upon). + * Versions taking Type t are required for parametric datatypes. + */ unsigned getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException); Type getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException); + unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException); + Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException); /** * Construct and return a ground term of this Datatype. The -- 2.30.2