added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts

1 files changed, 3 insertions, 10 deletions

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 4ae7f2d0c..2df0c3f61 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;