Fix unit test for datatypes, add interface functions to datatypes.

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