diff options
Diffstat (limited to 'src/expr/datatype.h')
| -rw-r--r-- | src/expr/datatype.h | 30 |
1 files changed, 14 insertions, 16 deletions
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) { } |