Support UF in default sygus grammars (#3319)

1 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index b4fb220db..8939cf6da 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -123,7 +123,13 @@ class TransitionInference
    * The node n should be the inner body of the negated synthesis conjecture,
    * prior to generating the deep embedding. That is, given:
    *   forall f. ~forall x. P( f, x ),
-   * this method expects n to be P( f, x ).
+   * this method expects n to be P( f, x ), and the argument f to be the
+   * function f above.
+   */
+  void process(Node n, Node f);
+  /**
+   * Same as above, without specifying f. This will try to infer a function f
+   * based on the body of n.
    */
   void process(Node n);
   /**