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, 17 insertions, 1 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index b0363c59b..6d626038d 100644
--- 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 );