From 0a9a1f848cd5dcf0386ace435f068286dbe2c6fd Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 26 Feb 2013 16:41:56 -0500 Subject: [PATCH] Bug fix for rep-set. (Cherry-picked from commit c71ec27 in master.) --- src/theory/rep_set.cpp | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) 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; -- 2.30.2