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.

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index ad278f8c5720de4d93f70ebf3aa4d2f7bc82285f..8c6b5afbc63bfc3f6e252366efa0f390d83bc651 100644 (file)
--- 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;
         }
       }

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index b0363c59be947fa6abc550c635359656e7c94e5d..6d626038db789e0da10b69fc27a51f5808aea5b7 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -378,7 +378,23 @@ private:
   std::map< TypeNode, Node > d_typ_pred;
   //get predicate for type
   Node getPredicateForType( TypeNode tn );
-  //
+  /** get enumerate uf term
+   *
+   * This function adds up to #num f-applications to terms, where f is
+   * n.getOperator(). These applications are enumerated in a fair manner based
+   * on an iterative deepening of the sum of indices of the arguments. For
+   * example, if f : U x U -> U, an the term enumerator for U gives t1, t2, t3
+   * ..., then we add f-applications to terms in this order:
+   *   f( t1, t1 )
+   *   f( t2, t1 )
+   *   f( t1, t2 )
+   *   f( t1, t3 )
+   *   f( t2, t2 )
+   *   f( t3, t1 )
+   *   ...
+   * This function may add fewer than #num terms to terms if the enumeration is
+   * exhausted, or if an internal error occurs.
+   */
   void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );
   //
   void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );