diff options
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 18 |
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 ); |