From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 26 Feb 2013 21:41:56 +0000 (-0500)
Subject: Bug fix for rep-set.
X-Git-Tag: cvc5-1.0.0~7391^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a9a1f848cd5dcf0386ace435f068286dbe2c6fd;p=cvc5.git

Bug fix for rep-set.

(Cherry-picked from commit c71ec27 in master.)
---

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 3b5ba0cef..3057e4a93 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -135,16 +135,9 @@ bool RepSetIterator::initialize(){
     }else if( tn.isInteger() || tn.isReal() ){
       Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
       d_incomplete = true;
-    }else if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      //if finite, then complete all values of the domain
-      if( dt.isFinite() ){
-        d_rep_set->complete( tn );
-        //d_incomplete = true;
-      }else{
-        Trace("fmf-incomplete") << "Incomplete because of infinite datatype " << tn << std::endl;
-        d_incomplete = true;
-      }
+    //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
+    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
+      d_rep_set->complete( tn );
     }else{
       Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
       d_incomplete = true;