Static learn redundant operators in CegisUnif (#1899)

12 files changed, 205 insertions, 82 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index a5ab27bf3..2456839e7 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -40,7 +40,8 @@ bool CegisUnif::initialize(Node n,
 {
   Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
   // Init UNIF util
-  d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
+  std::map<Node, std::vector<Node>> strategy_lemmas;
+  d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas);
   Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
   std::vector<Node> unif_candidates;
   // Initialize enumerators for non-unif functions-to-synhesize
@@ -64,7 +65,7 @@ bool CegisUnif::initialize(Node n,
     d_enum_to_active_guard[e] = g;
   }
   // initialize the enumeration manager
-  d_u_enum_manager.initialize(unif_candidates);
+  d_u_enum_manager.initialize(unif_candidates, strategy_lemmas);
   return true;
 }
 
@@ -175,13 +176,14 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
                                         std::vector<Node>& lems)
 {
   // Notify lemma to unification utility and get its purified form
-  std::map<Node, std::vector<Node> > eval_pts;
+  std::map<Node, std::vector<Node>> eval_pts;
   Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
   d_refinement_lemmas.push_back(plem);
   Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n";
   // Notify the enumeration manager if there are new evaluation points
-  for (const std::pair<const Node, std::vector<Node> >& ep : eval_pts)
+  for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
   {
+    Trace("cegis-unif") << "** Registering new point:\n" << plem << "\n";
     d_u_enum_manager.registerEvalPts(ep.second, ep.first);
   }
   // Make the refinement lemma and add it to lems. This lemma is guarded by the
@@ -208,7 +210,9 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
   d_tds = d_qe->getTermDatabaseSygus();
 }
 
-void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
+void CegisUnifEnumManager::initialize(
+    const std::vector<Node>& cs,
+    const std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   Assert(!d_initialized);
   d_initialized = true;
@@ -216,12 +220,51 @@ void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
   {
     return;
   }
+  // process strategy lemmas
+  std::map<TypeNode, std::pair<Node, std::vector<Node>>> tn_strategy_lemmas;
+  for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
+  {
+    if (Trace.isOn("cegis-unif-enum-debug"))
+    {
+      Trace("cegis-unif-enum-debug") << "...lemmas of strategy pt " << p.first
+                                     << ":\n";
+      for (const Node& lem : p.second)
+      {
+        Trace("cegis-unif-enum-debug") << "\t" << lem << "\n";
+      }
+    }
+    TypeNode tn = p.first.getType();
+    Assert(tn_strategy_lemmas.find(tn) == tn_strategy_lemmas.end());
+    tn_strategy_lemmas[tn].first = p.first;
+    tn_strategy_lemmas[tn].second = p.second;
+  }
+  // initialize type information for candidates
+  NodeManager* nm = NodeManager::currentNM();
   for (const Node& c : cs)
   {
+    Trace("cegis-unif-enum-debug") << "...adding candidate " << c << "\n";
     // currently, we allocate the same enumerators for candidates of the same
     // type
     TypeNode tn = c.getType();
     d_ce_info[tn].d_candidates.push_back(c);
+    // retrieve symmetry breaking lemma template for type if not already init
+    if (!d_ce_info[tn].d_sbt_lemma.isNull())
+    {
+      continue;
+    }
+    std::map<const TypeNode, std::pair<Node, std::vector<Node>>>::iterator it =
+        tn_strategy_lemmas.find(tn);
+    if (it == tn_strategy_lemmas.end())
+    {
+      continue;
+    }
+    // collect lemmas for removing redundant ops for this candidate's type
+    d_ce_info[tn].d_sbt_lemma = nm->mkNode(AND, it->second.second);
+    Trace("cegis-unif-enum-debug")
+        << "...adding lemma template to remove redundant operators for " << c
+        << " and its type " << tn << " --> " << d_ce_info[tn].d_sbt_lemma
+        << "\n";
+    d_ce_info[tn].d_sbt_arg = it->second.first;
   }
   // initialize the current literal
   incrementNumEnumerators();
@@ -299,6 +342,17 @@ void CegisUnifEnumManager::incrementNumEnumerators()
     {
       TypeNode ct = ci.first;
       Node eu = nm->mkSkolem("eu", ct);
+      // instantiate template for removing redundant operators
+      if (!ci.second.d_sbt_lemma.isNull())
+      {
+        Node templ = ci.second.d_sbt_lemma;
+        TNode templ_var = ci.second.d_sbt_arg;
+        Node sym_break_red_ops = templ.substitute(templ_var, eu);
+        Trace("cegis-unif-enum-lemma")
+            << "CegisUnifEnum::lemma, remove redundant ops of " << eu << " : "
+            << sym_break_red_ops << "\n";
+        d_qe->getOutputChannel().lemma(sym_break_red_ops);
+      }
       if (!ci.second.d_enums.empty())
       {
         Node eu_prev = ci.second.d_enums.back();
@@ -368,8 +422,8 @@ void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct,
     disj.push_back(ei.eqNode(itc->second.d_enums[i]));
   }
   Node lem = NodeManager::currentNM()->mkNode(OR, disj);
-  Trace("cegis-unif-enum-lemma")
-      << "CegisUnifEnum::lemma, domain:" << lem << "\n";
+  Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem
+                                 << "\n";
   d_qe->getOutputChannel().lemma(lem);
 }
 
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;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index cae2a432d..7faeb0252 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -113,30 +113,38 @@ bool CegConjecturePbe::initialize(Node n,
                                   std::vector<Node>& lemmas)
 {
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
-  
-  for( unsigned i=0; i<candidates.size(); i++ ){
+
+  for (unsigned i = 0; i < candidates.size(); i++)
+  {
     Node v = candidates[i];
     d_examples[v].clear();
     d_examples_out[v].clear();
     d_examples_term[v].clear();
   }
-  
-  std::map< Node, bool > visited;
-  collectExamples( n, visited, true, true );
-  
-  for( unsigned i=0; i<candidates.size(); i++ ){
+
+  std::map<Node, bool> visited;
+  collectExamples(n, visited, true, true);
+
+  for (unsigned i = 0; i < candidates.size(); i++)
+  {
     Node v = candidates[i];
     Trace("sygus-pbe") << "  examples for " << v << " : ";
-    if( d_examples_invalid.find( v )!=d_examples_invalid.end() ){
+    if (d_examples_invalid.find(v) != d_examples_invalid.end())
+    {
       Trace("sygus-pbe") << "INVALID" << std::endl;
-    }else{
+    }
+    else
+    {
       Trace("sygus-pbe") << std::endl;
-      for( unsigned j=0; j<d_examples[v].size(); j++ ){
+      for (unsigned j = 0; j < d_examples[v].size(); j++)
+      {
         Trace("sygus-pbe") << "    ";
-        for( unsigned k=0; k<d_examples[v][j].size(); k++ ){
+        for (unsigned k = 0; k < d_examples[v][j].size(); k++)
+        {
           Trace("sygus-pbe") << d_examples[v][j][k] << " ";
         }
-        if( !d_examples_out[v][j].isNull() ){
+        if (!d_examples_out[v][j].isNull())
+        {
           Trace("sygus-pbe") << " -> " << d_examples_out[v][j];
         }
         Trace("sygus-pbe") << std::endl;
@@ -168,8 +176,14 @@ bool CegConjecturePbe::initialize(Node n,
                        << std::endl;
     std::vector<Node> singleton_c;
     singleton_c.push_back(c);
+    std::map<Node, std::vector<Node>> strategy_lemmas;
     d_sygus_unif[c].initialize(
-        d_qe, singleton_c, d_candidate_to_enum[c], lemmas);
+        d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas);
+    // collect lemmas from all strategies
+    for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
+    {
+      lemmas.insert(lemmas.end(), p.second.begin(), p.second.end());
+    }
     Assert(!d_candidate_to_enum[c].empty());
     Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
                        << " enumerators for " << c << "..." << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 235fbe3dd..fbf89fee9 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -189,7 +189,7 @@ class CegConjecturePbe : public SygusModule
 
  private:
   /** sygus term database of d_qe */
-  quantifiers::TermDbSygus * d_tds;
+  quantifiers::TermDbSygus* d_tds;
   /** true and false nodes */
   Node d_true;
   Node d_false;
@@ -200,7 +200,7 @@ class CegConjecturePbe : public SygusModule
   * In other words, all occurrences of f are guarded by equalities that
   * constraint its arguments to constants.
   */
-  std::map< Node, bool > d_examples_invalid;
+  std::map<Node, bool> d_examples_invalid;
   /** for each candidate variable (function-to-synthesize), whether the
   * conjecture is purely PBE for that variable.
   * An example of a conjecture for which d_examples_invalid is false but
@@ -213,7 +213,7 @@ class CegConjecturePbe : public SygusModule
   * However, the domain of f in both cases is finite, which can be used for
   * search space pruning.
   */
-  std::map< Node, bool > d_examples_out_invalid;
+  std::map<Node, bool> d_examples_out_invalid;
   /**
    * Map from candidates to sygus unif utility. This class implements
    * the core algorithm (e.g. decision tree learning) that this module relies
@@ -231,19 +231,22 @@ class CegConjecturePbe : public SygusModule
   std::map<Node, Node> d_enum_to_active_guard;
   /** for each candidate variable (function-to-synthesize), input of I/O
    * examples */
-  std::map< Node, std::vector< std::vector< Node > > > d_examples;
+  std::map<Node, std::vector<std::vector<Node> > > d_examples;
   /** for each candidate variable (function-to-synthesize), output of I/O
    * examples */
-  std::map< Node, std::vector< Node > > d_examples_out;
+  std::map<Node, std::vector<Node> > d_examples_out;
   /** the list of example terms
    * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
    */
-  std::map< Node, std::vector< Node > > d_examples_term;
+  std::map<Node, std::vector<Node> > d_examples_term;
   /** collect the PBE examples in n
   * This is called on the input conjecture, and will populate the above vectors.
   *   hasPol/pol denote the polarity of n in the conjecture.
   */
-  void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
+  void collectExamples(Node n,
+                       std::map<Node, bool>& visited,
+                       bool hasPol,
+                       bool pol);
 
   //--------------------------------- PBE search values
   /**
@@ -254,7 +257,8 @@ class CegConjecturePbe : public SygusModule
    *   term x+y is indexed by 1,4
    *   term 0 is indexed by 0,0.
    */
-  class PbeTrie {
+  class PbeTrie
+  {
    public:
     PbeTrie() {}
     ~PbeTrie() {}
@@ -271,13 +275,21 @@ class CegConjecturePbe : public SygusModule
      * index : the index of the example we are processing,
      * ntotal : the total of the examples for enumerator e.
      */
-    Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
-                       unsigned index, unsigned ntotal);
+    Node addPbeExample(TypeNode etn,
+                       Node e,
+                       Node b,
+                       CegConjecturePbe* cpbe,
+                       unsigned index,
+                       unsigned ntotal);
 
    private:
     /** Helper function for above, called when we get the current example ex. */
-    Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
-                           CegConjecturePbe* cpbe, unsigned index,
+    Node addPbeExampleEval(TypeNode etn,
+                           Node e,
+                           Node b,
+                           std::vector<Node>& ex,
+                           CegConjecturePbe* cpbe,
+                           unsigned index,
                            unsigned ntotal);
   };
   /** trie of candidate solutions tried
@@ -288,11 +300,10 @@ class CegConjecturePbe : public SygusModule
   */
   std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
   //--------------------------------- end PBE search values
-
 };
 
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
 
 #endif
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 23b04aa4d..5cf96e513 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -27,12 +27,11 @@ namespace theory {
 namespace quantifiers {
 
 SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
-
 SygusUnif::~SygusUnif() {}
 void SygusUnif::initialize(QuantifiersEngine* qe,
                            const std::vector<Node>& funs,
                            std::vector<Node>& enums,
-                           std::vector<Node>& lemmas)
+                           std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   Assert(d_candidates.empty());
   d_qe = qe;
@@ -98,7 +97,7 @@ Node SygusUnif::constructBestConditional(const std::vector<Node>& conds)
 Node SygusUnif::constructBestStringToConcat(
     const std::vector<Node>& strs,
     const std::map<Node, unsigned>& total_inc,
-    const std::map<Node, std::vector<unsigned> >& incr)
+    const std::map<Node, std::vector<unsigned>>& incr)
 {
   Assert(!strs.empty());
   std::vector<Node> strs_tmp = strs;
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
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 8f2038d31..60a3d70d8 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -469,16 +469,16 @@ SygusUnifIo::~SygusUnifIo() {}
 void SygusUnifIo::initialize(QuantifiersEngine* qe,
                              const std::vector<Node>& funs,
                              std::vector<Node>& enums,
-                             std::vector<Node>& lemmas)
+                             std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   Assert(funs.size() == 1);
   d_examples.clear();
   d_examples_out.clear();
   d_ecache.clear();
   d_candidate = funs[0];
-  SygusUnif::initialize(qe, funs, enums, lemmas);
+  SygusUnif::initialize(qe, funs, enums, strategy_lemmas);
   // learn redundant operators based on the strategy
-  d_strategy[d_candidate].staticLearnRedundantOps(lemmas);
+  d_strategy[d_candidate].staticLearnRedundantOps(strategy_lemmas);
 }
 
 void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index b0d6ce3ce..359aa4443 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -37,7 +37,7 @@ class UnifContextIo : public UnifContext
  public:
   UnifContextIo();
   /** get current role */
-  virtual NodeRole getCurrentRole() override;
+  NodeRole getCurrentRole() override;
 
   /**
    * This intiializes this context based on information in sui regarding the
@@ -122,7 +122,7 @@ class UnifContextIo : public UnifContext
   * This is the current set of enumerator/node role pairs we are currently
   * visiting. This set is cleared when the context is updated.
   */
-  std::map<Node, std::map<NodeRole, bool> > d_visit_role;
+  std::map<Node, std::map<NodeRole, bool>> d_visit_role;
 
   /** unif context enumerator information */
   class UEnumInfo
@@ -142,7 +142,7 @@ class UnifContextIo : public UnifContext
     * resulting in 2 and 4, are equal to the output value for the respective
     * pairs.
     */
-    std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+    std::map<Node, std::map<unsigned, Node>> d_look_ahead_sols;
   };
   /** map from enumerators to the above info class */
   std::map<Node, UEnumInfo> d_uinfo;
@@ -214,7 +214,7 @@ class SubsumeTrie
   */
   void getLeaves(const std::vector<Node>& vals,
                  bool pol,
-                 std::map<int, std::vector<Node> >& v);
+                 std::map<int, std::vector<Node>>& v);
   /** is this trie empty? */
   bool isEmpty() { return d_term.isNull() && d_children.empty(); }
   /** clear this trie */
@@ -242,7 +242,7 @@ class SubsumeTrie
   /** helper function for above functions */
   void getLeavesInternal(const std::vector<Node>& vals,
                          bool pol,
-                         std::map<int, std::vector<Node> >& v,
+                         std::map<int, std::vector<Node>>& v,
                          unsigned index,
                          int status);
 };
@@ -276,17 +276,15 @@ class SygusUnifIo : public SygusUnif
    * The vector funs should be of length one, since I/O specifications across
    * multiple functions can be separated.
    */
-  virtual void initialize(QuantifiersEngine* qe,
-                          const std::vector<Node>& funs,
-                          std::vector<Node>& enums,
-                          std::vector<Node>& lemmas) override;
+  void initialize(QuantifiersEngine* qe,
+                  const std::vector<Node>& funs,
+                  std::vector<Node>& enums,
+                  std::map<Node, std::vector<Node>>& strategy_lemmas) override;
   /** Notify enumeration */
-  virtual void notifyEnumeration(Node e,
-                                 Node v,
-                                 std::vector<Node>& lemmas) override;
+  void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
 
   /** Construct solution */
-  virtual bool constructSolution(std::vector<Node>& sols) override;
+  bool constructSolution(std::vector<Node>& sols) override;
 
   /** add example
    *
@@ -314,7 +312,7 @@ class SygusUnifIo : public SygusUnif
   Node d_true;
   Node d_false;
   /** input of I/O examples */
-  std::vector<std::vector<Node> > d_examples;
+  std::vector<std::vector<Node>> d_examples;
   /** output of I/O examples */
   std::vector<Node> d_examples_out;
 
@@ -347,7 +345,7 @@ class SygusUnifIo : public SygusUnif
       * This either stores the values of f( I ) for inputs
       * or the value of f( I ) = O if d_role==enum_io
       */
-    std::vector<std::vector<Node> > d_enum_vals_res;
+    std::vector<std::vector<Node>> d_enum_vals_res;
     /**
     * The set of values in d_enum_vals that have been "subsumed" by others
     * (see SubsumeTrie for explanation of subsumed).
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index a2299f834..427d413c8 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -28,16 +28,17 @@ SygusUnifRl::~SygusUnifRl() {}
 void SygusUnifRl::initialize(QuantifiersEngine* qe,
                              const std::vector<Node>& funs,
                              std::vector<Node>& enums,
-                             std::vector<Node>& lemmas)
+                             std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   // initialize
   std::vector<Node> all_enums;
-  SygusUnif::initialize(qe, funs, all_enums, lemmas);
+  SygusUnif::initialize(qe, funs, all_enums, strategy_lemmas);
   // based on the strategy inferred for each function, determine if we are
   // using a unification strategy that is compatible our approach.
   for (const Node& f : funs)
   {
-    registerStrategy(f);
+    d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
+    registerStrategy(f, strategy_lemmas);
   }
   enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
   // Copy candidates and check whether CegisUnif for any of them
@@ -363,7 +364,8 @@ std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
   return it->second;
 }
 
-void SygusUnifRl::registerStrategy(Node f)
+void SygusUnifRl::registerStrategy(
+    Node f, std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   if (Trace.isOn("sygus-unif-rl-strat"))
   {
@@ -374,14 +376,15 @@ void SygusUnifRl::registerStrategy(Node f)
   Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
   Node e = d_strategy[f].getRootEnumerator();
   std::map<Node, std::map<NodeRole, bool>> visited;
-  registerStrategyNode(f, e, role_equal, visited);
+  registerStrategyNode(f, e, role_equal, visited, strategy_lemmas);
 }
 
 void SygusUnifRl::registerStrategyNode(
     Node f,
     Node e,
     NodeRole nrole,
-    std::map<Node, std::map<NodeRole, bool>>& visited)
+    std::map<Node, std::map<NodeRole, bool>>& visited,
+    std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   Trace("sygus-unif-rl-strat") << "  register node " << e << std::endl;
   if (visited[e].find(nrole) != visited[e].end())
@@ -417,17 +420,19 @@ void SygusUnifRl::registerStrategyNode(
             << "  ...detected recursive ITE strategy, condition enumerator : "
             << cond << std::endl;
         // indicate that we will be enumerating values for cond
-        registerConditionalEnumerator(f, e, cond, j);
+        registerConditionalEnumerator(f, e, cond, j, strategy_lemmas);
       }
     }
     // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
   }
 }
 
-void SygusUnifRl::registerConditionalEnumerator(Node f,
-                                                Node e,
-                                                Node cond,
-                                                unsigned strategy_index)
+void SygusUnifRl::registerConditionalEnumerator(
+    Node f,
+    Node e,
+    Node cond,
+    unsigned strategy_index,
+    std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   // we will do unification for this candidate
   d_unif_candidates.insert(f);
@@ -440,6 +445,20 @@ void SygusUnifRl::registerConditionalEnumerator(Node f,
     // register the conditional enumerator
     d_tds->registerEnumerator(cond, f, d_parent, true);
     d_cenum_to_stratpt[cond].clear();
+    // register lemmas to remove redundant operators from condition enumeration
+    std::map<const Node, std::vector<Node>>::iterator it =
+        strategy_lemmas.find(cond);
+    if (it != strategy_lemmas.end())
+    {
+      for (const Node& lemma : it->second)
+      {
+        Trace("cegis-unif-enum-debug")
+            << "* Registering lemma to remove redundand operators for " << cond
+            << " --> " << lemma << "\n";
+        d_qe->getOutputChannel().lemma(lemma);
+      }
+      strategy_lemmas.erase(cond);
+    }
   }
   // register that this strategy node has a decision tree construction
   d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 58cf9011e..941bb5763 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -53,7 +53,7 @@ class SygusUnifRl : public SygusUnif
   void initialize(QuantifiersEngine* qe,
                   const std::vector<Node>& funs,
                   std::vector<Node>& enums,
-                  std::vector<Node>& lemmas) override;
+                  std::map<Node, std::vector<Node>>& strategy_lemmas) override;
   /** Notify enumeration */
   void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
   /** Construct solution */
@@ -261,27 +261,40 @@ class SygusUnifRl : public SygusUnif
    *
    * Initialize the above data for the relevant enumerators in the strategy tree
    * of candidate variable f.
+   *
+   * Lemmas to remove redundant operators from enumerators of specific strategy
+   * points, if any, are retrived from strategy_lemmas.
    */
-  void registerStrategy(Node f);
+  void registerStrategy(Node f,
+                        std::map<Node, std::vector<Node>>& strategy_lemmas);
   /** register strategy node
    *
    * Called while traversing the strategy tree of f. The arguments e and nrole
    * indicate the current node in the tree we are traversing, and visited
    * indicates the nodes we have already visited.
+   *
+   * Lemmas to remove redundant operators from enumerators of specific strategy
+   * points, if any, are retrived from strategy_lemmas.
    */
   void registerStrategyNode(Node f,
                             Node e,
                             NodeRole nrole,
-                            std::map<Node, std::map<NodeRole, bool>>& visited);
+                            std::map<Node, std::map<NodeRole, bool>>& visited,
+                            std::map<Node, std::vector<Node>>& strategy_lemmas);
   /** register conditional enumerator
    *
    * Registers that cond is a conditional enumerator for building a (recursive)
    * decision tree at strategy node e within the strategy tree of f.
+   *
+   * Lemmas to remove redundant operators from enumerators of specific strategy
+   * points, if any, are retrived from strategy_lemmas.
    */
-  void registerConditionalEnumerator(Node f,
-                                     Node e,
-                                     Node cond,
-                                     unsigned strategy_index);
+  void registerConditionalEnumerator(
+      Node f,
+      Node e,
+      Node cond,
+      unsigned strategy_index,
+      std::map<Node, std::vector<Node>>& strategy_lemmas);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index d3a5d6c23..a3158fbe8 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -680,7 +680,8 @@ bool SygusUnifStrategy::inferTemplate(
   return true;
 }
 
-void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
+void SygusUnifStrategy::staticLearnRedundantOps(
+    std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
   for (unsigned i = 0; i < d_esym_list.size(); i++)
   {
@@ -716,6 +717,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
     Node em = nce.first;
     const Datatype& dt =
         static_cast<DatatypeType>(em.getType().toType()).getDatatype();
+    std::vector<Node> lemmas;
     for (std::pair<const unsigned, bool>& nc : nce.second)
     {
       Assert(nc.first < dt.getNumConstructors());
@@ -723,6 +725,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
       {
         Node tst =
             datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
+
         if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
         {
           Trace("sygus-unif") << "...can exclude based on  : " << tst
@@ -731,6 +734,10 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
         }
       }
     }
+    if (!lemmas.empty())
+    {
+      strategy_lemmas[em] = lemmas;
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 8f9adefb9..a24e323e8 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -274,13 +274,15 @@ class SygusUnifStrategy
    *
    * This learns static lemmas for pruning enumerative space based on the
    * strategy for the function-to-synthesize of this class, and stores these
-   * into lemmas.
+   * into strategy_lemmas.
    *
    * These may 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).
    */
-  void staticLearnRedundantOps(std::vector<Node>& lemmas);
+  void staticLearnRedundantOps(
+      std::map<Node, std::vector<Node>>& strategy_lemmas);
+
   /** debug print this strategy on Trace c */
   void debugPrint(const char* c);