From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 11 Sep 2012 23:44:49 +0000 (+0000)
Subject: added getCardinality to model
X-Git-Tag: cvc5-1.0.0~7816
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78482ce84a4652c69baa8a07d5d714408ab6cf03;p=cvc5.git

added getCardinality to model
---

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:
diff --git a/src/util/model.h b/src/util/model.h
index ca7565aaa..9b7db536f 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "util/cardinality.h"
 
 namespace CVC4 {
 
@@ -54,8 +55,10 @@ public:
   /** get type of command */
   int getCommandType( int i ) { return d_command_types[i]; }
 public:
-  /** get value */
+  /** get value for expression */
   virtual Expr getValue( const Expr& expr ) = 0;
+  /** get cardinality for sort */
+  virtual Cardinality getCardinality( const Type& t ) = 0;
   /** to stream function */
   virtual void toStream(std::ostream& out) = 0;
 };/* class Model */