From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 15 Jan 2016 22:57:56 +0000 (+0100)
Subject: Type enumerators take optional argument indicating fixed cardinalities of uninterpret... 
X-Git-Tag: cvc5-1.0.0~6109
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d677333439c15677b6891ee8f6bd368a5df9f0a;p=cvc5.git

Type enumerators take optional argument indicating fixed cardinalities of uninterpreted sorts. Modify TheoryModelBuilder.  Fix bug in fmf-empty-sorts.
---

diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index c4501fc43..dc2b6f115 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -34,7 +34,7 @@ class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
 
 public:
 
-  RationalEnumerator(TypeNode type) throw(AssertionException) :
+  RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<RationalEnumerator>(type),
     d_rat(0) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
@@ -81,7 +81,7 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
 
 public:
 
-  IntegerEnumerator(TypeNode type) throw(AssertionException) :
+  IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<IntegerEnumerator>(type),
     d_int(0) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
@@ -115,7 +115,7 @@ class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
 
 public:
 
-  SubrangeEnumerator(TypeNode type) throw(AssertionException) :
+  SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<SubrangeEnumerator>(type),
     d_int(0),
     d_bounds(type.getConst<SubrangeBounds>()),
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 2c6fc56ab..ace23eb82 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -29,6 +29,8 @@ namespace theory {
 namespace arrays {
 
 class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
+  /** type properties */
+  TypeEnumeratorProperties * d_tep;
   TypeEnumerator d_index;
   TypeNode d_constituentType;
   NodeManager* d_nm;
@@ -39,9 +41,10 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
 
 public:
 
-  ArrayEnumerator(TypeNode type) throw(AssertionException) :
+  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<ArrayEnumerator>(type),
-    d_index(type.getArrayIndexType()),
+    d_tep(tep),
+    d_index(type.getArrayIndexType(), tep),
     d_constituentType(type.getArrayConstituentType()),
     d_nm(NodeManager::currentNM()),
     d_indexVec(),
@@ -50,8 +53,9 @@ public:
     d_arrayConst()
   {
     d_indexVec.push_back(*d_index);
-    d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
     d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
+    Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
   }
 
   // An array enumerator could be large, and generally you don't want to
@@ -59,6 +63,7 @@ public:
   // by the TypeEnumerator framework.
   ArrayEnumerator(const ArrayEnumerator& ae) throw() :
     TypeEnumeratorBase<ArrayEnumerator>(ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
+    d_tep(ae.d_tep),
     d_index(ae.d_index),
     d_constituentType(ae.d_constituentType),
     d_nm(ae.d_nm),
@@ -122,7 +127,7 @@ public:
         return *this;
       }
       d_indexVec.push_back(*d_index);
-      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
       ++(*d_constituentVec.back());
       if (d_constituentVec.back()->isFinished()) {
         Trace("array-type-enum") << "operator++ finished!" << std::endl;
@@ -132,7 +137,7 @@ public:
     }
 
     while (d_constituentVec.size() < d_indexVec.size()) {
-      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
     }
 
     Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl;
diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index 34b1401e8..3849f8435 100644
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -32,7 +32,7 @@ class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
 
 public:
 
-  BooleanEnumerator(TypeNode type) :
+  BooleanEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
     TypeEnumeratorBase<BooleanEnumerator>(type),
     d_value(FALSE) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 635cf7dc7..5ef0e4ab8 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -31,16 +31,32 @@ namespace builtin {
 
 class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortEnumerator> {
   Integer d_count;
-
+  bool d_has_fixed_bound;
+  Integer d_fixed_bound;
 public:
 
-  UninterpretedSortEnumerator(TypeNode type) throw(AssertionException) :
+  UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<UninterpretedSortEnumerator>(type),
     d_count(0) {
     Assert(type.getKind() == kind::SORT_TYPE);
+    d_has_fixed_bound = false;
+    Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl;
+    if( tep && tep->d_fixed_usort_card ){
+      d_has_fixed_bound = true;
+      std::map< TypeNode, Integer >::iterator it = tep->d_fixed_card.find( type );
+      if( it!=tep->d_fixed_card.end() ){
+        d_fixed_bound = it->second;
+      }else{
+        d_fixed_bound = Integer(1);
+      }
+      Trace("uf-type-enum") << "...fixed bound : " << d_fixed_bound << std::endl;
+    }
   }
 
-  Node operator*() throw() {
+  Node operator*() throw(NoMoreValuesException) {
+    if(isFinished()) {
+      throw NoMoreValuesException(getType());
+    }
     return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count));
   }
 
@@ -50,7 +66,11 @@ public:
   }
 
   bool isFinished() throw() {
-    return false;
+    if( d_has_fixed_bound ){
+      return d_count>=d_fixed_bound;
+    }else{
+      return false;
+    }
   }
 
 };/* class UninterpretedSortEnumerator */
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index db98ef66b..da06b1152 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -35,7 +35,7 @@ class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> {
 
 public:
 
-  BitVectorEnumerator(TypeNode type) throw(AssertionException) :
+  BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<BitVectorEnumerator>(type),
     d_size(type.getBitVectorSize()),
     d_bits(0) {
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 26689c81a..57d16d31c 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -35,10 +35,10 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
        d_te_index[tn] = tei;
        if( tn.isDatatype() && d_has_debruijn ){
          //must indicate that this is a child enumerator (do not normalize constants for it)
-         DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true );
+         DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
          d_children.push_back( TypeEnumerator( dte ) );
        }else{
-         d_children.push_back( TypeEnumerator( tn ) );
+         d_children.push_back( TypeEnumerator( tn, d_tep ) );
        }
        d_terms[tn].push_back( *d_children[tei] );
      }else{
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 0e5aad640..67dabafe4 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -30,6 +30,8 @@ namespace datatypes {
 
 
 class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
+  /** type properties */
+  TypeEnumeratorProperties * d_tep;
   /** The datatype we're enumerating */
   const Datatype& d_datatype;
   /** extra cons */
@@ -78,15 +80,17 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   void init();
 public:
 
-  DatatypesEnumerator(TypeNode type) throw() :
+  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
     TypeEnumeratorBase<DatatypesEnumerator>(type),
+    d_tep(tep),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
     d_type(type) {
     d_child_enum = false;
     init();
   }
-  DatatypesEnumerator(TypeNode type, bool childEnum) throw() :
+  DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) throw() :
     TypeEnumeratorBase<DatatypesEnumerator>(type),
+    d_tep(tep),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
     d_type(type) {
     d_child_enum = childEnum;
@@ -94,6 +98,7 @@ public:
   }
   DatatypesEnumerator(const DatatypesEnumerator& de) throw() :
     TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
+    d_tep(de.d_tep),
     d_datatype(de.d_datatype),
     d_type(de.d_type),
     d_ctor(de.d_ctor),
@@ -172,13 +177,14 @@ public:
 };/* DatatypesEnumerator */
 
 class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
+  TypeEnumeratorProperties * d_tep;
   TypeEnumerator** d_enumerators;
 
   /** Allocate and initialize the delegate enumerators */
   void newEnumerators() {
     d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
     for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-      d_enumerators[i] = new TypeEnumerator(getType()[i]);
+      d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep);
     }
   }
 
@@ -194,14 +200,15 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
 
 public:
 
-  TupleEnumerator(TypeNode type) throw() :
-    TypeEnumeratorBase<TupleEnumerator>(type) {
+  TupleEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+    TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) {
     Assert(type.isTuple());
     newEnumerators();
   }
 
   TupleEnumerator(const TupleEnumerator& te) throw() :
     TypeEnumeratorBase<TupleEnumerator>(te.getType()),
+    d_tep(te.d_tep),
     d_enumerators(NULL) {
 
     if(te.d_enumerators != NULL) {
@@ -236,7 +243,7 @@ public:
     size_t i;
     for(i = 0; i < getType().getNumChildren(); ++i) {
       if(d_enumerators[i]->isFinished()) {
-        *d_enumerators[i] = TypeEnumerator(getType()[i]);
+        *d_enumerators[i] = TypeEnumerator(getType()[i], d_tep);
       } else {
         ++*d_enumerators[i];
         return *this;
@@ -255,6 +262,7 @@ public:
 };/* TupleEnumerator */
 
 class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
+  TypeEnumeratorProperties * d_tep;
   TypeEnumerator** d_enumerators;
 
   /** Allocate and initialize the delegate enumerators */
@@ -279,14 +287,15 @@ class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
 
 public:
 
-  RecordEnumerator(TypeNode type) throw() :
-    TypeEnumeratorBase<RecordEnumerator>(type) {
+  RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+    TypeEnumeratorBase<RecordEnumerator>(type), d_tep(tep) {
     Assert(type.isRecord());
     newEnumerators();
   }
 
   RecordEnumerator(const RecordEnumerator& re) throw() :
     TypeEnumeratorBase<RecordEnumerator>(re.getType()),
+    d_tep(re.d_tep),
     d_enumerators(NULL) {
 
     if(re.d_enumerators != NULL) {
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index d6725997d..b6162ec38 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -234,14 +234,14 @@ function enumerator {
 #line $lineno \"$kf\"
     case $1:
 #line $lineno \"$kf\"
-      return new $2(type);
+      return new $2(type, tep);
 "
   elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then
     mk_type_enumerator_cases="${mk_type_enumerator_cases}
 #line $lineno \"$kf\"
   case kind::$1:
 #line $lineno \"$kf\"
-    return new $2(type);
+    return new $2(type, tep);
 "
   else
     echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index eb827edc3..4b173c833 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -232,7 +232,7 @@ bool ModelEngine::considerQuantifiedFormula( Node q ) {
       for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
         TypeNode tn = q[0][i].getType();
         //we are allowed to assume the type is empty
-        if( d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
+        if( tn.isSort() && d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
           Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
           return false;
         }
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index fa8f108c3..bb0e1794c 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Kshitij Bansal
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -32,6 +32,8 @@ namespace theory {
 namespace sets {
 
 class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
+  /** type properties */
+  TypeEnumeratorProperties * d_tep;
   unsigned d_index;
   TypeNode d_constituentType;
   NodeManager* d_nm;
@@ -42,8 +44,9 @@ class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
 
 public:
 
-  SetEnumerator(TypeNode type) throw(AssertionException) :
+  SetEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<SetEnumerator>(type),
+    d_tep(tep),
     d_index(0),
     d_constituentType(type.getSetElementType()),
     d_nm(NodeManager::currentNM()),
@@ -62,6 +65,7 @@ public:
   // by the TypeEnumerator framework.
   SetEnumerator(const SetEnumerator& ae) throw() :
     TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+    d_tep(ae.d_tep),
     d_index(ae.d_index),
     d_constituentType(ae.d_constituentType),
     d_nm(ae.d_nm),
@@ -145,7 +149,7 @@ public:
 
     if (d_constituentVec.empty()) {
       ++d_index;
-      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
     }
 
     while (d_constituentVec.size() < d_index) {
diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index cfc3fe02b..bdaa683c1 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tianyi Liang
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -40,7 +40,7 @@ class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> {
   }
 public:
 
-  StringEnumerator(TypeNode type) throw(AssertionException) :
+  StringEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
     TypeEnumeratorBase<StringEnumerator>(type) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == STRING_TYPE);
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c6837ddf4..5ddb1c31a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -587,6 +587,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   // Process all terms in the equality engine, store representatives for each EC
   std::map< Node, Node > assertedReps, constantReps;
   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+  TypeEnumeratorProperties tep;
+  if( options::finiteModelFind() ){
+    tep.d_fixed_usort_card = true;
+    for( std::map< TypeNode, unsigned >::iterator it = eqc_usort_count.begin(); it != eqc_usort_count.end(); ++it ){
+      tep.d_fixed_card[it->first] = Integer(it->second);
+    }
+    typeConstSet.setTypeEnumeratorProperties( &tep );
+  }
   std::set< TypeNode > allTypes;
   eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
   for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
@@ -810,14 +818,20 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             do{
               n = typeConstSet.nextTypeEnum(t, true);
               //--- AJR: this code checks whether n is a legal value
+              Assert( !n.isNull() );
               success = true;
+              Trace("exc-value-debug") << "Check if excluded : " << n << std::endl;
               if( isUSortFiniteRestricted ){
+#ifdef CVC4_ASSERTIONS
                 //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
+                //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint.
                 std::map< Node, bool > visited;
                 success = !isExcludedUSortValue( eqc_usort_count, n, visited );
                 if( !success ){
                   Trace("exc-value") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
                 }
+                Assert( success );
+#endif
               }
               if( success && isCorecursive ){
                 if (repSet != NULL && !repSet->empty()) {
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 8ee4e843d..e609bf703 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -130,8 +130,10 @@ public:
 private:
   TypeSetMap d_typeSet;
   TypeToTypeEnumMap d_teMap;
+  TypeEnumeratorProperties * d_tep;
 
   public:
+  TypeSet() : d_tep(NULL) {}
   ~TypeSet() {
     iterator it;
     for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
@@ -146,7 +148,7 @@ private:
       }
     }
   }
-
+  void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; }
   void add(TypeNode t, TNode n)
   {
     iterator it = d_typeSet.find(t);
@@ -175,7 +177,7 @@ private:
     TypeEnumerator* te;
     TypeToTypeEnumMap::iterator it = d_teMap.find(t);
     if (it == d_teMap.end()) {
-      te = new TypeEnumerator(t);
+      te = new TypeEnumerator(t, d_tep);
       d_teMap[t] = te;
     }
     else {
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 015cbb288..951967f50 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -62,6 +62,18 @@ public:
 
 };/* class TypeEnumeratorInterface */
 
+// AJR: This class stores particular information that is relevant to type enumeration.
+//      For finite model finding, we set d_fixed_usort=true,
+//      and store the finite cardinality bounds for each uninterpreted sort encountered in the model.
+class TypeEnumeratorProperties
+{
+public:
+  TypeEnumeratorProperties() : d_fixed_usort_card(false){}
+  Integer getFixedCardinality( TypeNode tn ) { return d_fixed_card[tn]; }
+  bool d_fixed_usort_card;
+  std::map< TypeNode, Integer > d_fixed_card;
+};
+
 template <class T>
 class TypeEnumeratorBase : public TypeEnumeratorInterface {
 public:
@@ -77,13 +89,13 @@ public:
 class TypeEnumerator {
   TypeEnumeratorInterface* d_te;
 
-  static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type)
+  static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep)
     throw(AssertionException);
 
 public:
 
-  TypeEnumerator(TypeNode type) throw() :
-    d_te(mkTypeEnumerator(type)) {
+  TypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+    d_te(mkTypeEnumerator(type, tep)) {
   }
 
   TypeEnumerator(const TypeEnumerator& te) :
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index f0eafed18..6f9b565bf 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -29,7 +29,7 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
-TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type) throw(AssertionException) {
+TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep) throw(AssertionException) {
   switch(type.getKind()) {
   case kind::TYPE_CONSTANT:
     switch(type.getConst<TypeConstant>()) {