Static learn redundant operators in CegisUnif (#1899)

1 files changed, 4 insertions, 3 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index e55f7e6ff..fe80a3d44 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -55,15 +55,16 @@ class SygusUnif
    * the grammar of f and adds them to enums. These enumerators are those that
    * should be later given to calls to notifyEnumeration below.
    *
-   * This also may result in lemmas being added to lemmas,
+   * This also may result in lemmas being added to strategy_lemmas,
    * which correspond to static symmetry breaking predicates (for example,
    * those that exclude ITE from enumerators whose role is enum_io when the
-   * strategy is ITE_strat).
+   * strategy is ITE_strat). The lemmas are associated with a strategy point of
+   * the respective function-to-synthesize.
    */
   virtual void initialize(QuantifiersEngine* qe,
                           const std::vector<Node>& funs,
                           std::vector<Node>& enums,
-                          std::vector<Node>& lemmas);
+                          std::map<Node, std::vector<Node>>& strategy_lemmas);
 
   /**
    * Notify that the value v has been enumerated for enumerator e. This call