Infrastructure to mark unused sygus strategies (#1950)

4 files changed, 56 insertions, 17 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index be8d6c5ca..a96505ce4 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -44,8 +44,9 @@ void SygusUnifRl::initializeCandidate(
   {
     restrictions.d_iteReturnBoolConst = true;
   }
+  // register the strategy
+  registerStrategy(f, enums, restrictions.d_unused_strategies);
   d_strategy[f].staticLearnRedundantOps(strategy_lemmas, restrictions);
-  registerStrategy(f, enums);
   // Copy candidates and check whether CegisUnif for any of them
   if (d_unif_candidates.find(f) != d_unif_candidates.end())
   {
@@ -386,7 +387,10 @@ std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
   return it->second;
 }
 
-void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums)
+void SygusUnifRl::registerStrategy(
+    Node f,
+    std::vector<Node>& enums,
+    std::map<Node, std::unordered_set<unsigned>>& unused_strats)
 {
   if (Trace.isOn("sygus-unif-rl-strat"))
   {
@@ -397,7 +401,7 @@ void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums)
   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, enums);
+  registerStrategyNode(f, e, role_equal, visited, enums, unused_strats);
 }
 
 void SygusUnifRl::registerStrategyNode(
@@ -405,7 +409,8 @@ void SygusUnifRl::registerStrategyNode(
     Node e,
     NodeRole nrole,
     std::map<Node, std::map<NodeRole, bool>>& visited,
-    std::vector<Node>& enums)
+    std::vector<Node>& enums,
+    std::map<Node, std::unordered_set<unsigned>>& unused_strats)
 {
   Trace("sygus-unif-rl-strat") << "  register node " << e << std::endl;
   if (visited[e].find(nrole) != visited[e].end())
@@ -421,9 +426,10 @@ void SygusUnifRl::registerStrategyNode(
     EnumTypeInfoStrat* etis = snode.d_strats[j];
     StrategyType strat = etis->d_this;
     // is this a simple recursive ITE strategy?
+    bool success = false;
     if (strat == strat_ITE && nrole == role_equal)
     {
-      bool success = true;
+      success = true;
       for (unsigned c = 1; c <= 2; c++)
       {
         std::pair<Node, NodeRole> child = etis->d_cenum[c];
@@ -446,6 +452,10 @@ void SygusUnifRl::registerStrategyNode(
         enums.push_back(e);
       }
     }
+    if (!success)
+    {
+      unused_strats[e].insert(j);
+    }
     // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
   }
 }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 8a5230d15..072766b21 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -297,21 +297,29 @@ class SygusUnifRl : public SygusUnif
    *
    * Initialize the above data for the relevant enumerators in the strategy tree
    * of candidate variable f. For each strategy point e which there is a
-   * decision tree strategy, we add e to enums.
+   * decision tree strategy, we add e to enums. For each strategy with index
+   * i in an strategy point e, if we are not using the strategy, we add i to
+   * unused_strats[e]. This map is later passed to
+   * SygusUnifStrategy::staticLearnRedundantOps.
    */
-  void registerStrategy(Node f, std::vector<Node>& enums);
+  void registerStrategy(
+      Node f,
+      std::vector<Node>& enums,
+      std::map<Node, std::unordered_set<unsigned>>& unused_strats);
   /** 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. If e has a decision tree
-   * strategy, it is added to enums.
+   * indicates the nodes we have already visited. The arguments enums and
+   * unused_strats are modified as described above.
    */
-  void registerStrategyNode(Node f,
-                            Node e,
-                            NodeRole nrole,
-                            std::map<Node, std::map<NodeRole, bool>>& visited,
-                            std::vector<Node>& enums);
+  void registerStrategyNode(
+      Node f,
+      Node e,
+      NodeRole nrole,
+      std::map<Node, std::map<NodeRole, bool>>& visited,
+      std::vector<Node>& enums,
+      std::map<Node, std::unordered_set<unsigned>>& unused_strats);
   /** register conditional enumerator
    *
    * Registers that cond is a conditional enumerator for building a (recursive)
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 2f3d5b874..e236613c0 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -785,15 +785,29 @@ void SygusUnifStrategy::staticLearnRedundantOps(
   TypeNode etn = e.getType();
   EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
   StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  // the constructors of the current strategy point we need
   std::map<unsigned, bool> needs_cons_curr;
-  // constructors that correspond to strategies are not needed
-  // the intuition is that the strategy itself is responsible for constructing
-  // all terms that use the given constructor
+  // get the unused strategies
+  std::map<Node, std::unordered_set<unsigned>>::iterator itus =
+      restrictions.d_unused_strategies.find(e);
+  std::unordered_set<unsigned> unused_strats;
+  if (itus != restrictions.d_unused_strategies.end())
+  {
+    unused_strats.insert(itus->second.begin(), itus->second.end());
+  }
   for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
   {
+    // if we are not using this strategy, there is nothing to do
+    if (unused_strats.find(j) != unused_strats.end())
+    {
+      continue;
+    }
     EnumTypeInfoStrat* etis = snode.d_strats[j];
     unsigned cindex =
         static_cast<unsigned>(Datatype::indexOf(etis->d_cons.toExpr()));
+    // constructors that correspond to strategies are not needed
+    // the intuition is that the strategy itself is responsible for constructing
+    // all terms that use the given constructor
     Trace("sygus-strat-slearn") << "...by strategy, can exclude operator "
                                 << etis->d_cons << std::endl;
     needs_cons_curr[cindex] = false;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 0c7f207be..cbce5e70c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -256,6 +256,13 @@ struct StrategyRestrictions
    * the condition values of ITEs to be restricted to atoms
    */
   bool d_iteCondOnlyAtoms;
+  /**
+   * A list of unused strategies. This maps strategy points to the indices
+   * in StrategyNode::d_strats that are not used by the caller of
+   * staticLearnRedundantOps, and hence should not be taken into account
+   * when doing redundant operator learning.
+   */
+  std::map<Node, std::unordered_set<unsigned>> d_unused_strategies;
 };
 
 /**