Make conjecture generator's uf term enumeration safer (#2172)

This ensures that the function getEnumerateUfTerm does not have out of bounds accesses. This is an alternative fix to the one brought up in #2158.

1 files changed, 29 insertions, 2 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index ad278f8c5..8c6b5afbc 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1066,6 +1066,8 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
 void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
   if( n.getNumChildren()>0 ){
     TermEnumeration* te = d_quantEngine->getTermEnumeration();
+    // below, we do a fair enumeration of vectors vec of indices whose sum is
+    // 1,2,3, ...
     std::vector< int > vec;
     std::vector< TypeNode > types;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
@@ -1078,6 +1080,10 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
         return;
       }
     }
+    // the index of the last child is determined by the limit of the sum
+    // of indices of children (size_limit) and the sum of the indices of the
+    // other children (vec_sum). Hence, we pop here and add this value at each
+    // iteration of the loop.
     vec.pop_back();
     int size_limit = 0;
     int vec_sum = -1;
@@ -1087,25 +1093,44 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
       bool success = true;
       if( vec_sum==-1 ){
         vec_sum = 0;
+        // we will construct a new child below
+        // since sum is 0, the index of last child is limit
         vec.push_back( size_limit );
-      }else{
+      }
+      else if (index < vec.size())
+      {
+        Assert(index < types.size());
         //see if we can iterate current
         if (vec_sum < size_limit
             && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull())
         {
           vec[index]++;
           vec_sum++;
+          // we will construct a new child below
+          // add the index of the last child, its index is (limit-sum)
           vec.push_back( size_limit - vec_sum );
         }else{
+          // reset the index
           vec_sum -= vec[index];
           vec[index] = 0;
           index++;
-          if( index==n.getNumChildren() ){
+          if (index == vec.size())
+          {
+            // no more indices to iterate, we increment limit and reset below
             success = false;
           }
         }
       }
+      else
+      {
+        // This should never happen due to invariants of this loop.
+        // However, if it does, we simply abort while not fully enumerating the
+        // full set of terms.
+        Assert(false);
+        return;
+      }
       if( success ){
+        // if we are ready to construct the term
         if( vec.size()==n.getNumChildren() ){
           Node lc =
               te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]);
@@ -1131,6 +1156,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
             Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl;
             terms.push_back( n );
           }
+          // pop the index for the last child
           vec.pop_back();
           index = 0;
         }
@@ -1143,6 +1169,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
           }
           vec_sum = -1;
         }else{
+          // we've saturated, no more terms can be enumerated
           return;
         }
       }