Robust check to avoid store all instantiations. Fix prior commit for sort inference.

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 70b7d31f4c6d612b0064a5d3651a48f0211fda3f..454fe8971263de58aeb185b0a22c46ebce62b33c 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -47,14 +47,34 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{
   }
 }
 
+bool containsStoreAll( Node n, std::vector< Node >& cache ){
+  if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
+    cache.push_back( n );
+    if( n.getKind()==STORE_ALL ){
+      return true;
+    }else{
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( containsStoreAll( n[i], cache ) ){
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
 void RepSet::add( TypeNode tn, Node n ){
   //for now, do not add array constants FIXME
-  if( !tn.isArray() || !n.isConst() ){
-    Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
-    Assert( n.getType().isSubtypeOf( tn ) );
-    d_tmap[ n ] = (int)d_type_reps[tn].size();
-    d_type_reps[tn].push_back( n );
+  if( tn.isArray() ){
+    std::vector< Node > cache;
+    if( containsStoreAll( n, cache ) ){
+      return;
+    }
   }
+  Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
+  Assert( n.getType().isSubtypeOf( tn ) );
+  d_tmap[ n ] = (int)d_type_reps[tn].size();
+  d_type_reps[tn].push_back( n );
 }
 
 int RepSet::getIndexFor( Node n ) const {

diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 76e39c2b35f08ee0e37db3f5a7128240a0e85e19..9aef059bdeec348b938c6ab643f3e38096cc04c9 100644 (file)
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -290,7 +290,6 @@ void SortInference::setEqual( int t1, int t2 ){
         rt1 = rt2;
         rt2 = swap;
       }
-      d_type_union_find.d_eqc[rt1] = rt2;
       std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
       if( it1!=d_type_types.end() ){
         if( d_type_types.find( rt2 )==d_type_types.end() ){
@@ -298,8 +297,10 @@ void SortInference::setEqual( int t1, int t2 ){
           d_type_types.erase( rt1 );
         }else{
           //may happen for mixed int/real
+          return;
         }
       }
+      d_type_union_find.d_eqc[rt1] = rt2;
     }
   }
 }