Static learn redundant operators in CegisUnif (#1899)

1 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ed38c9268..dd98b20ba 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -54,7 +54,8 @@ class CegisUnifEnumManager
    * Each candidate c in cs should be such that we are using a
    * synthesis-by-unification approach for c.
    */
-  void initialize(const std::vector<Node>& cs);
+  void initialize(const std::vector<Node>& cs,
+                  const std::map<Node, std::vector<Node>>& strategy_lemmas);
   /** register evaluation point for candidate
    *
    * This notifies this class that eis is a set of heads of evaluation points
@@ -100,6 +101,10 @@ class CegisUnifEnumManager
     std::vector<Node> d_enums;
     /** the set of evaluation points of this type */
     std::vector<Node> d_eval_points;
+    /** symmetry breaking lemma template for this type */
+    Node d_sbt_lemma;
+    /** argument (to be instantiated) of symmetry breaking lemma template */
+    Node d_sbt_arg;
   };
   /** map types to the above info */
   std::map<TypeNode, TypeInfo> d_ce_info;