Initialize cegis unif strategy (#1861)

7 files changed, 407 insertions, 154 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index ee8fb6f12..cc477fa62 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/quantifiers/sygus/cegis_unif.h"
 
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -55,6 +57,12 @@ bool CegisUnif::initialize(Node n,
       unif_candidates.push_back(c);
     }
   }
+  for (const Node& e : d_cond_enums)
+  {
+    Node g = d_tds->getActiveGuardForEnumerator(e);
+    Assert(!g.isNull());
+    d_enum_to_active_guard[e] = g;
+  }
   // initialize the enumeration manager
   d_u_enum_manager.initialize(unif_candidates);
   return true;
@@ -73,6 +81,8 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
     Valuation& valuation = d_qe->getValuation();
     for (const Node& e : d_cond_enums)
     {
+      Trace("cegis-unif-debug")
+          << "Check conditional enumerator : " << e << std::endl;
       Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
       Node g = d_enum_to_active_guard[e];
       /* Get whether the active guard for this enumerator is set. If so, then
@@ -109,8 +119,14 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     {
       continue;
     }
-    Trace("cegis-unif-enum") << "  " << enums[i] << " -> " << enum_values[i]
-                             << std::endl;
+    if (Trace.isOn("cegis-unif-enum"))
+    {
+      Trace("cegis-unif-enum") << "  " << enums[i] << " -> ";
+      std::stringstream ss;
+      Printer::getPrinter(options::outputLanguage())
+          ->toStreamSygus(ss, enum_values[i]);
+      Trace("cegis-unif-enum") << ss.str() << std::endl;
+    }
     unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
     if (i == 0 || sz < min_term_size)
     {
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index dc927388e..23b04aa4d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -41,7 +41,7 @@ void SygusUnif::initialize(QuantifiersEngine* qe,
   {
     d_candidates.push_back(f);
     // initialize the strategy
-    d_strategy[f].initialize(qe, f, enums, lemmas);
+    d_strategy[f].initialize(qe, f, enums);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index eb607d2c3..8f2038d31 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -477,6 +477,8 @@ void SygusUnifIo::initialize(QuantifiersEngine* qe,
   d_ecache.clear();
   d_candidate = funs[0];
   SygusUnif::initialize(qe, funs, enums, lemmas);
+  // learn redundant operators based on the strategy
+  d_strategy[d_candidate].staticLearnRedundantOps(lemmas);
 }
 
 void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 3b7cef4b9..2cf751927 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -31,11 +31,17 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
                              std::vector<Node>& lemmas)
 {
   d_ecache.clear();
-  d_cand_to_cond_enum.clear();
   d_cand_to_pt_enum.clear();
-  /* TODO populate d_unif_candidates and remove lemmas cleaning */
-  SygusUnif::initialize(qe, funs, enums, lemmas);
-  lemmas.clear();
+  // initialize
+  std::vector<Node> all_enums;
+  SygusUnif::initialize(qe, funs, all_enums, 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);
+  }
+  enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
   /* Copy candidates and check whether CegisUnif for any of them */
   for (const Node& c : d_unif_candidates)
   {
@@ -73,23 +79,28 @@ Node SygusUnifRl::purifyLemma(Node n,
   /* Recurse */
   unsigned size = n.getNumChildren();
   Kind k = n.getKind();
-  /* Whether application of a function-to-synthesize */
-  bool fapp = k == APPLY_UF && size > 0;
-  Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
-         == d_candidates.end());
-  /* Whether application of a (non-)unification function-to-synthesize */
-  bool u_fapp = fapp && usingUnif(n[0]);
-  bool nu_fapp = fapp && !usingUnif(n[0]);
   /* We retrive model value now because purified node may not have a value */
   Node nv = n;
-  /* get model value of non-top level applications of functions-to-synthesize
-     occurring under a unification function-to-synthesize */
-  if (ensureConst && fapp)
+  /* Whether application of a function-to-synthesize */
+  bool fapp = k == APPLY_UF && size > 0;
+  bool u_fapp = false;
+  bool nu_fapp = false;
+  if (fapp)
   {
-    nv = d_parent->getModelValue(n);
-    Assert(n != nv);
-    Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
-                                  << " is " << nv << "\n";
+    Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
+           != d_candidates.end());
+    /* Whether application of a (non-)unification function-to-synthesize */
+    u_fapp = usingUnif(n[0]);
+    nu_fapp = !usingUnif(n[0]);
+    /* get model value of non-top level applications of functions-to-synthesize
+      occurring under a unification function-to-synthesize */
+    if (ensureConst)
+    {
+      nv = d_parent->getModelValue(n);
+      Assert(n != nv);
+      Trace("sygus-unif-rl-purify")
+          << "PurifyLemma : model value for " << n << " is " << nv << "\n";
+    }
   }
   /* Travese to purify */
   bool childChanged = false;
@@ -210,6 +221,7 @@ void SygusUnifRl::initializeConstructSol() {}
 void SygusUnifRl::initializeConstructSolFor(Node f) {}
 bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
 {
+  initializeConstructSol();
   for (const Node& c : d_candidates)
   {
     if (!usingUnif(c))
@@ -221,7 +233,16 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
     }
     else
     {
-      return false;
+      initializeConstructSolFor(c);
+      Node v =
+          constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0);
+      if (v.isNull())
+      {
+        return false;
+      }
+      Trace("sygus-unif-rl-sol")
+          << "Adding solution " << v << " to unif candidate " << c << "\n";
+      sols.push_back(v);
     }
   }
   return true;
@@ -229,6 +250,20 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
 
 Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
 {
+  indent("sygus-unif-sol", ind);
+  Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl;
+  // is there a decision tree strategy?
+  if (nrole == role_equal)
+  {
+    std::map<Node, DecisionTreeInfo>::iterator itd = d_enum_to_dt.find(e);
+    if (itd != d_enum_to_dt.end())
+    {
+      indent("sygus-unif-sol", ind);
+      Trace("sygus-unif-sol")
+          << "...it has a decision tree strategy." << std::endl;
+    }
+  }
+
   return Node::null();
 }
 
@@ -237,6 +272,83 @@ bool SygusUnifRl::usingUnif(Node f)
   return d_unif_candidates.find(f) != d_unif_candidates.end();
 }
 
+void SygusUnifRl::registerStrategy(Node f)
+{
+  if (Trace.isOn("sygus-unif-rl-strat"))
+  {
+    Trace("sygus-unif-rl-strat")
+        << "Strategy for " << f << " is : " << std::endl;
+    d_strategy[f].debugPrint("sygus-unif-rl-strat");
+  }
+  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);
+}
+
+void SygusUnifRl::registerStrategyNode(
+    Node f,
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited)
+{
+  Trace("sygus-unif-rl-strat") << "  register node " << e << std::endl;
+  if (visited[e].find(nrole) != visited[e].end())
+  {
+    return;
+  }
+  visited[e][nrole] = true;
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+  {
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    StrategyType strat = etis->d_this;
+    // is this a simple recursive ITE strategy?
+    if (strat == strat_ITE && nrole == role_equal)
+    {
+      bool success = true;
+      for (unsigned c = 1; c <= 2; c++)
+      {
+        std::pair<Node, NodeRole> child = etis->d_cenum[c];
+        if (child.first != e || child.second != nrole)
+        {
+          success = false;
+          break;
+        }
+      }
+      if (success)
+      {
+        Node cond = etis->d_cenum[0].first;
+        Assert(etis->d_cenum[0].second == role_ite_condition);
+        Trace("sygus-unif-rl-strat")
+            << "  ...detected recursive ITE strategy, condition enumerator : "
+            << cond << std::endl;
+        // indicate that we will be enumerating values for cond
+        registerConditionalEnumerator(f, e, cond);
+      }
+    }
+    // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
+  }
+}
+
+void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond)
+{
+  // we will do unification for this candidate
+  d_unif_candidates.insert(f);
+  // add to the list of all conditional enumerators
+  if (std::find(d_cond_enums.begin(), d_cond_enums.end(), cond)
+      == d_cond_enums.end())
+  {
+    d_cond_enums.push_back(cond);
+    // register the conditional enumerator
+    d_tds->registerEnumerator(cond, f, d_parent, true);
+  }
+  // register that this enumerator has a decision tree construction
+  d_enum_to_dt[e].d_cond_enum = cond;
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index dc1b14641..b8ead4986 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -73,8 +73,6 @@ class SygusUnifRl : public SygusUnif
   CegConjecture* d_parent;
   /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
   std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
-  /* Maps unif candidates to their conditonal enumerators */
-  std::map<Node, Node> d_cand_to_cond_enum;
   /**
    * This class stores information regarding an enumerator, including: a
    * database
@@ -151,6 +149,50 @@ class SygusUnifRl : public SygusUnif
                    bool ensureConst,
                    std::vector<Node>& model_guards,
                    BoolNodePairMap& cache);
+  /*
+    --------------------------------------------------------------
+        Strategy information
+    --------------------------------------------------------------
+  */
+  /**
+   * This class stores the necessary information for building a decision tree
+   * for a particular node in the strategy tree of a candidate variable f.
+   */
+  class DecisionTreeInfo
+  {
+   public:
+    /**
+     * The enumerator in the strategy tree that stores conditions of the
+     * decision tree.
+     */
+    Node d_cond_enum;
+  };
+  /** map from enumerators in the strategy trees to the above data */
+  std::map<Node, DecisionTreeInfo> d_enum_to_dt;
+  /** all conditional enumerators */
+  std::vector<Node> d_cond_enums;
+  /** register strategy
+   *
+   * Initialize the above data for the relevant enumerators in the strategy tree
+   * of candidate variable f.
+   */
+  void registerStrategy(Node f);
+  /** 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.
+   */
+  void registerStrategyNode(Node f,
+                            Node e,
+                            NodeRole nrole,
+                            std::map<Node, std::map<NodeRole, bool>>& visited);
+  /** 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.
+   */
+  void registerConditionalEnumerator(Node f, Node e, Node cond);
 };
 
 } /* 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 86efffd1f..d3a5d6c23 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -80,8 +80,7 @@ std::ostream& operator<<(std::ostream& os, StrategyType st)
 
 void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
                                    Node f,
-                                   std::vector<Node>& enums,
-                                   std::vector<Node>& lemmas)
+                                   std::vector<Node>& enums)
 {
   Assert(d_candidate.isNull());
   d_candidate = f;
@@ -92,8 +91,10 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
   collectEnumeratorTypes(d_root, role_equal);
   // add the enumerators
   enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end());
-  // learn redundant ops
-  staticLearnRedundantOps(lemmas);
+  // finish the initialization of the strategy
+  // this computes if each node is conditional
+  std::map<Node, std::map<NodeRole, bool> > visited;
+  finishInit(getRootEnumerator(), role_equal, visited, false);
 }
 
 void SygusUnifStrategy::initializeType(TypeNode tn)
@@ -101,10 +102,13 @@ void SygusUnifStrategy::initializeType(TypeNode tn)
   d_tinfo[tn].d_this_type = tn;
 }
 
-Node SygusUnifStrategy::getRootEnumerator()
+Node SygusUnifStrategy::getRootEnumerator() const
 {
-  std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
-  Assert(it != d_tinfo[d_root].d_enum.end());
+  std::map<TypeNode, EnumTypeInfo>::const_iterator itt = d_tinfo.find(d_root);
+  Assert(itt != d_tinfo.end());
+  std::map<EnumRole, Node>::const_iterator it =
+      itt->second.d_enum.find(enum_io);
+  Assert(it != itt->second.d_enum.end());
   return it->second;
 }
 
@@ -702,10 +706,10 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
   Trace("sygus-unif") << std::endl;
   Trace("sygus-unif") << "Strategy for candidate " << d_candidate
                       << " is : " << std::endl;
+  debugPrint("sygus-unif");
   std::map<Node, std::map<NodeRole, bool> > visited;
   std::map<Node, std::map<unsigned, bool> > needs_cons;
-  staticLearnRedundantOps(
-      getRootEnumerator(), role_equal, visited, needs_cons, 0, false);
+  staticLearnRedundantOps(getRootEnumerator(), role_equal, visited, needs_cons);
   // now, check the needs_cons map
   for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
   {
@@ -730,124 +734,181 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
   }
 }
 
+void SygusUnifStrategy::debugPrint(const char* c)
+{
+  if (Trace.isOn(c))
+  {
+    std::map<Node, std::map<NodeRole, bool> > visited;
+    debugPrint(c, getRootEnumerator(), role_equal, visited, 0);
+  }
+}
+
 void SygusUnifStrategy::staticLearnRedundantOps(
     Node e,
     NodeRole nrole,
     std::map<Node, std::map<NodeRole, bool> >& visited,
-    std::map<Node, std::map<unsigned, bool> >& needs_cons,
-    int ind,
-    bool isCond)
+    std::map<Node, std::map<unsigned, bool> >& needs_cons)
 {
-  std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
-  Assert(itn != d_einfo.end());
-
-  if (visited[e].find(nrole) == visited[e].end()
-      || (isCond && !itn->second.isConditional()))
+  if (visited[e].find(nrole) != visited[e].end())
+  {
+    return;
+  }
+  visited[e][nrole] = true;
+  EnumInfo& ei = getEnumInfo(e);
+  if (ei.isTemplated())
   {
-    visited[e][nrole] = true;
-    // if conditional
-    if (isCond)
+    return;
+  }
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  if (snode.d_strats.empty())
+  {
+    return;
+  }
+  std::map<unsigned, bool> needs_cons_curr;
+  // various strategies
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+  {
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    int cindex = Datatype::indexOf(etis->d_cons.toExpr());
+    Assert(cindex != -1);
+    needs_cons_curr[static_cast<unsigned>(cindex)] = false;
+    for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
     {
-      itn->second.setConditional();
+      staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons);
     }
-    indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole;
-    Trace("sygus-unif")
-        << ", type : "
-        << ((DatatypeType)e.getType().toType()).getDatatype().getName();
-    if (isCond)
+  }
+  // get the master enumerator for the type of this enumerator
+  std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn);
+  if (itse == d_master_enum.end())
+  {
+    return;
+  }
+  Node em = itse->second;
+  Assert(!em.isNull());
+  // get the current datatype
+  const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype();
+  // all constructors that are not a part of a strategy are needed
+  for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
+  {
+    if (needs_cons_curr.find(j) == needs_cons_curr.end())
     {
-      Trace("sygus-unif") << ", conditional";
+      needs_cons_curr[j] = true;
     }
-    Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
-
-    if (itn->second.isTemplated())
+  }
+  // update the constructors that the master enumerator needs
+  if (needs_cons.find(em) == needs_cons.end())
+  {
+    needs_cons[em] = needs_cons_curr;
+  }
+  else
+  {
+    for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
     {
-      Trace("sygus-unif") << ", templated : (lambda "
-                          << itn->second.d_template_arg << " "
-                          << itn->second.d_template << ")" << std::endl;
+      needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
     }
-    else
+  }
+}
+
+void SygusUnifStrategy::finishInit(
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited,
+    bool isCond)
+{
+  EnumInfo& ei = getEnumInfo(e);
+  if (visited[e].find(nrole) != visited[e].end()
+      && (!isCond || ei.isConditional()))
+  {
+    return;
+  }
+  visited[e][nrole] = true;
+  // set conditional
+  if (isCond)
+  {
+    ei.setConditional();
+  }
+  if (ei.isTemplated())
+  {
+    return;
+  }
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+  {
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    StrategyType strat = etis->d_this;
+    bool newIsCond = isCond || strat == strat_ITE;
+    for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
     {
-      Trace("sygus-unif") << std::endl;
-      TypeNode etn = e.getType();
+      finishInit(cec.first, cec.second, visited, newIsCond);
+    }
+  }
+}
 
-      // enumerator type info
-      std::map<TypeNode, EnumTypeInfo>::iterator itt = d_tinfo.find(etn);
-      Assert(itt != d_tinfo.end());
-      EnumTypeInfo& tinfo = itt->second;
+void SygusUnifStrategy::debugPrint(
+    const char* c,
+    Node e,
+    NodeRole nrole,
+    std::map<Node, std::map<NodeRole, bool> >& visited,
+    int ind)
+{
+  if (visited[e].find(nrole) != visited[e].end())
+  {
+    indent(c, ind);
+    Trace(c) << e << " :: node role : " << nrole << std::endl;
+    return;
+  }
+  visited[e][nrole] = true;
+  EnumInfo& ei = getEnumInfo(e);
 
-      // strategy info
-      std::map<NodeRole, StrategyNode>::iterator itsn =
-          tinfo.d_snodes.find(nrole);
-      Assert(itsn != tinfo.d_snodes.end());
-      StrategyNode& snode = itsn->second;
+  TypeNode etn = e.getType();
 
-      if (snode.d_strats.empty())
-      {
-        return;
-      }
-      std::map<unsigned, bool> needs_cons_curr;
-      // various strategies
-      for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
-      {
-        EnumTypeInfoStrat* etis = snode.d_strats[j];
-        StrategyType strat = etis->d_this;
-        bool newIsCond = isCond || strat == strat_ITE;
-        indent("sygus-unif", ind + 1);
-        Trace("sygus-unif") << "Strategy : " << strat
-                            << ", from cons : " << etis->d_cons << std::endl;
-        int cindex = Datatype::indexOf(etis->d_cons.toExpr());
-        Assert(cindex != -1);
-        needs_cons_curr[static_cast<unsigned>(cindex)] = false;
-        for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
-        {
-          // recurse
-          staticLearnRedundantOps(
-              cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond);
-        }
-      }
-      // get the master enumerator for the type of this enumerator
-      std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn);
-      if (itse == d_master_enum.end())
-      {
-        return;
-      }
-      Node em = itse->second;
-      Assert(!em.isNull());
-      // get the current datatype
-      const Datatype& dt =
-          static_cast<DatatypeType>(etn.toType()).getDatatype();
-      // all constructors that are not a part of a strategy are needed
-      for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
-      {
-        if (needs_cons_curr.find(j) == needs_cons_curr.end())
-        {
-          needs_cons_curr[j] = true;
-        }
-      }
-      // update the constructors that the master enumerator needs
-      if (needs_cons.find(em) == needs_cons.end())
-      {
-        needs_cons[em] = needs_cons_curr;
-      }
-      else
-      {
-        for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
-        {
-          needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
-        }
-      }
-    }
+  indent(c, ind);
+  Trace(c) << e << " :: node role : " << nrole;
+  Trace(c) << ", type : "
+           << static_cast<DatatypeType>(etn.toType()).getDatatype().getName();
+  if (ei.isConditional())
+  {
+    Trace(c) << ", conditional";
   }
-  else
+  Trace(c) << ", enum role : " << ei.getRole();
+
+  if (ei.isTemplated())
+  {
+    Trace(c) << ", templated : (lambda " << ei.d_template_arg << " "
+             << ei.d_template << ")";
+  }
+  Trace(c) << std::endl;
+
+  EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
   {
-    indent("sygus-unif", ind);
-    Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
+    EnumTypeInfoStrat* etis = snode.d_strats[j];
+    StrategyType strat = etis->d_this;
+    indent(c, ind + 1);
+    Trace(c) << "Strategy : " << strat << ", from cons : " << etis->d_cons
+             << std::endl;
+    for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
+    {
+      // recurse
+      debugPrint(c, cec.first, cec.second, visited, ind + 2);
+    }
   }
 }
 
 void EnumInfo::initialize(EnumRole role) { d_role = role; }
+
+StrategyNode& EnumTypeInfo::getStrategyNode(NodeRole nrole)
+{
+  std::map<NodeRole, StrategyNode>::iterator it = d_snodes.find(nrole);
+  Assert(it != d_snodes.end());
+  return it->second;
+}
+
 bool EnumTypeInfoStrat::isValid(UnifContext& x)
 {
   if ((x.getCurrentRole() == role_string_prefix
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 0ab7ea1d6..8f9adefb9 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -198,6 +198,8 @@ class EnumTypeInfo
   std::map<EnumRole, Node> d_enum;
   /** map from node roles to strategy nodes */
   std::map<NodeRole, StrategyNode> d_snodes;
+  /** get strategy node for node role */
+  StrategyNode& getStrategyNode(NodeRole nrole);
 };
 
 /** represents a strategy for a SyGuS datatype type
@@ -253,18 +255,10 @@ class SygusUnifStrategy
    *
    * This call constructs a set of enumerators for the relevant subfields of
    * the grammar of f and adds them to enums.
-   *
-   * This also may result in lemmas being added to 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).
    */
-  void initialize(QuantifiersEngine* qe,
-                  Node f,
-                  std::vector<Node>& enums,
-                  std::vector<Node>& lemmas);
+  void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums);
   /** Get the root enumerator for this class */
-  Node getRootEnumerator();
+  Node getRootEnumerator() const;
   /**
    * Get the enumerator info for enumerator e, where e must be an enumerator
    * initialized by this class (in enums after a call to initialize).
@@ -276,6 +270,20 @@ class SygusUnifStrategy
    */
   EnumTypeInfo& getEnumTypeInfo(TypeNode tn);
 
+  /** static learn redundant operators
+   *
+   * 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.
+   *
+   * 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);
+  /** debug print this strategy on Trace c */
+  void debugPrint(const char* c);
+
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
@@ -332,13 +340,6 @@ class SygusUnifStrategy
                      Node n,
                      std::map<Node, unsigned>& templ_var_index,
                      std::map<unsigned, unsigned>& templ_injection);
-  /** static learn redundant operators
-   *
-   * 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.
-   */
-  void staticLearnRedundantOps(std::vector<Node>& lemmas);
   /** helper for static learn redundant operators
    *
    * (e, nrole) specify the strategy node in the graph we are currently
@@ -346,19 +347,38 @@ class SygusUnifStrategy
    *
    * This method builds the mapping needs_cons, which maps (master) enumerators
    * to a map from the constructors that it needs.
-   *
-   * ind is the depth in the strategy graph we are at (for debugging).
-   *
-   * isCond is whether the current enumerator is conditional (beneath a
-   * conditional of an strat_ITE strategy).
    */
   void staticLearnRedundantOps(
       Node e,
       NodeRole nrole,
       std::map<Node, std::map<NodeRole, bool> >& visited,
-      std::map<Node, std::map<unsigned, bool> >& needs_cons,
-      int ind,
-      bool isCond);
+      std::map<Node, std::map<unsigned, bool> >& needs_cons);
+  /** finish initialization of the strategy tree
+   *
+   * (e, nrole) specify the strategy node in the graph we are currently
+   * analyzing, visited stores the nodes we have already visited.
+   *
+   * isCond is whether the current enumerator is conditional (beneath a
+   * conditional of an strat_ITE strategy).
+   */
+  void finishInit(Node e,
+                  NodeRole nrole,
+                  std::map<Node, std::map<NodeRole, bool> >& visited,
+                  bool isCond);
+  /** helper for debug print
+   *
+   * Prints the node e with role nrole on Trace(c).
+   *
+   * (e, nrole) specify the strategy node in the graph we are currently
+   * analyzing, visited stores the nodes we have already visited.
+   *
+   * ind is the current level of indentation (for debugging)
+   */
+  void debugPrint(const char* c,
+                  Node e,
+                  NodeRole nrole,
+                  std::map<Node, std::map<NodeRole, bool> >& visited,
+                  int ind);
   //------------------------------ end strategy registration
 };