From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 13 Jun 2015 21:45:11 +0000 (+0200)
Subject: Robust check to avoid store all instantiations. Fix prior commit for sort inference.
X-Git-Tag: cvc5-1.0.0~6277
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16955c76a25a8030dc24840e74d0ab24d54f0a35;p=cvc5.git

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 70b7d31f4..454fe8971 100644
--- 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 76e39c2b3..9aef059bd 100644
--- 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;
     }
   }
 }