added getCardinality to model

2 files changed, 18 insertions, 3 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index dc0ae7877..ed2d69308 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -59,6 +59,21 @@ Expr TheoryModel::getValue( const Expr& expr ){
   return ret.toExpr();
 }
 
+/** get cardinality for sort */
+Cardinality TheoryModel::getCardinality( const Type& t ){
+  TypeNode tn = TypeNode::fromType( t );
+  //for now, we only handle cardinalities for uninterpreted sorts
+  if( tn.isSort() ){
+    if( d_rep_set.hasType( tn ) ){
+      return Cardinality( d_rep_set.d_type_reps[tn].size() );
+    }else{
+      return Cardinality( CardinalityUnknown() );
+    }
+  }else{
+    return Cardinality( CardinalityUnknown() );
+  }
+}
+
 void TheoryModel::toStream( std::ostream& out ){
   /*//for debugging
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -76,7 +91,7 @@ void TheoryModel::toStream( std::ostream& out ){
     ++eqcs_i;
   }
   */
-  //need this function?
+  out << this;
 }
 
 Node TheoryModel::getModelValue( TNode n ){
diff --git a/src/theory/model.h b/src/theory/model.h
index ea1fa0fed..2f4ebfdbf 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -116,8 +116,8 @@ public:
 public:
   /** get value function for Exprs. */
   Expr getValue( const Expr& expr );
-
-
+  /** get cardinality for sort */
+  Cardinality getCardinality( const Type& t );
   /** to stream function */
   void toStream( std::ostream& out );
 public: