Classifying data in SygusUnifRL (#1886)

4 files changed, 290 insertions, 94 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 8fa4af99c..06b552276 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -2,7 +2,7 @@
 /*! \file cegis_unif.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -39,11 +39,11 @@ bool CegisUnif::initialize(Node n,
                            std::vector<Node>& lemmas)
 {
   Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
-  /* Init UNIF util */
+  // Init UNIF util
   d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
   Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
   std::vector<Node> unif_candidates;
-  /* Initialize enumerators for non-unif functions-to-synhesize */
+  // Initialize enumerators for non-unif functions-to-synhesize
   for (const Node& c : candidates)
   {
     if (!d_sygus_unif.usingUnif(c))
@@ -81,12 +81,12 @@ 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;
+      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
-         there may exist more values for it, and hence we add it to enums. */
+      // Get whether the active guard for this enumerator is set. If so, then
+      // there may exist more values for it, and hence we add it to enums.
       Node gstatus = valuation.getSatValue(g);
       if (!gstatus.isNull() && gstatus.getConst<bool>())
       {
@@ -113,7 +113,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
   Trace("cegis-unif-enum") << "Register new enumerated values :\n";
   for (unsigned i = 0, size = enums.size(); i < size; ++i)
   {
-    /* Only conditional enumerators will be notified to unif utility */
+    // Only conditional enumerators will be notified to unif utility
     if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i])
         == d_cond_enums.end())
     {
@@ -139,7 +139,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
       enum_consider.push_back(i);
     }
   }
-  /* only consider the enumerators that are at minimum size (for fairness) */
+  // only consider the enumerators that are at minimum size (for fairness)
   Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / "
                            << enums.size() << std::endl;
   for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i)
@@ -148,7 +148,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     Node e = enums[j], v = enum_values[j];
     std::vector<Node> enum_lems;
     d_sygus_unif.notifyEnumeration(e, v, enum_lems);
-    /* the lemmas must be guarded by the active guard of the enumerator */
+    // the lemmas must be guarded by the active guard of the enumerator
     Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
     Node g = d_enum_to_active_guard[e];
     for (unsigned j = 0, size = enum_lems.size(); j < size; ++j)
@@ -157,7 +157,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     }
     lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
   }
-  /* divide-and-conquer solution bulding for candidates using unif util */
+  // divide-and-conquer solution bulding for candidates using unif util
   std::vector<Node> sols;
   if (d_sygus_unif.constructSolution(sols))
   {
@@ -180,10 +180,10 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
   {
     d_u_enum_manager.registerEvalPts(ep.second, ep.first);
   }
-  /* Make the refinement lemma and add it to lems. This lemma is guarded by the
-     parent's guard, which has the semantics "this conjecture has a solution",
-     hence this lemma states: if the parent conjecture has a solution, it
-     satisfies the specification for the given concrete point. */
+  // Make the refinement lemma and add it to lems. This lemma is guarded by the
+  // parent's guard, which has the semantics "this conjecture has a solution",
+  // hence this lemma states: if the parent conjecture has a solution, it
+  // satisfies the specification for the given concrete point.
   lems.push_back(NodeManager::currentNM()->mkNode(
       OR, d_parent->getGuard().negate(), plem));
 }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 93ab69668..4ea6a887a 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -2,7 +2,7 @@
 /*! \file cegis_unif.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 2f0460c64..1260c62af 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus_unif_rl.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -30,8 +30,6 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
                              std::vector<Node>& enums,
                              std::vector<Node>& lemmas)
 {
-  d_ecache.clear();
-  d_cand_to_eval_hds.clear();
   // initialize
   std::vector<Node> all_enums;
   SygusUnif::initialize(qe, funs, all_enums, lemmas);
@@ -42,12 +40,12 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe,
     registerStrategy(f);
   }
   enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
-  /* Copy candidates and check whether CegisUnif for any of them */
+  // Copy candidates and check whether CegisUnif for any of them
   for (const Node& c : d_unif_candidates)
   {
-    d_app_to_pt[c].clear();
+    d_hd_to_pt[c].clear();
     d_cand_to_eval_hds[c].clear();
-    d_purified_count[c] = 0;
+    d_cand_to_hd_count[c] = 0;
   }
 }
 
@@ -55,13 +53,29 @@ void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
 {
   Trace("sygus-unif-rl-notify") << "SyGuSUnifRl: Adding to enum " << e
                                 << " value " << v << "\n";
-  d_ecache[e].d_enum_vals.push_back(v);
-  /* Exclude v from next enumerations for e */
+  // Exclude v from next enumerations for e
   Node exc_lemma =
       d_tds->getExplain()->getExplanationForEquality(e, v).negate();
-  Trace("sygus-unif-rl-notify")
+  Trace("sygus-unif-rl-notify-debug")
       << "SygusUnifRl : enumeration exclude lemma : " << exc_lemma << std::endl;
   lemmas.push_back(exc_lemma);
+  // Update all desicion trees in which this enumerator is a conditional
+  // enumerator, if any
+  std::map<Node, std::vector<Node>>::iterator it = d_cenum_to_stratpt.find(e);
+  if (it == d_cenum_to_stratpt.end())
+  {
+    return;
+  }
+  for (const Node& stratpt : it->second)
+  {
+    Trace("sygus-unif-rl-dt")
+        << "...adding value " << v
+        << " to decision tree of strategy point  : " << stratpt << std::endl;
+    Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end());
+    // Register new condition value
+    d_stratpt_to_dt[stratpt].addCondValue(v);
+    Trace("sygus-unif-rl-dt") << "...added\n";
+  }
 }
 
 Node SygusUnifRl::purifyLemma(Node n,
@@ -76,12 +90,12 @@ Node SygusUnifRl::purifyLemma(Node n,
     Trace("sygus-unif-rl-purify-debug") << "... already visited " << n << "\n";
     return it->second;
   }
-  /* Recurse */
+  // Recurse
   unsigned size = n.getNumChildren();
   Kind k = n.getKind();
-  /* We retrive model value now because purified node may not have a value */
+  // We retrive model value now because purified node may not have a value
   Node nv = n;
-  /* Whether application of a function-to-synthesize */
+  // Whether application of a function-to-synthesize
   bool fapp = k == APPLY_UF && size > 0;
   bool u_fapp = false;
   bool nu_fapp = false;
@@ -89,20 +103,20 @@ Node SygusUnifRl::purifyLemma(Node n,
   {
     Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
            != d_candidates.end());
-    /* Whether application of a (non-)unification function-to-synthesize */
+    // 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 */
+    // 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";
+      Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
+                                    << " is " << nv << "\n";
     }
   }
-  /* Travese to purify */
+  // Travese to purify
   bool childChanged = false;
   std::vector<Node> children;
   NodeManager* nm = NodeManager::currentNM();
@@ -113,7 +127,7 @@ Node SygusUnifRl::purifyLemma(Node n,
       children.push_back(n[i]);
       continue;
     }
-    /* Arguments of non-unif functions do not need to be constant */
+    // Arguments of non-unif functions do not need to be constant
     Node child = purifyLemma(
         n[i], !nu_fapp && (ensureConst || u_fapp), model_guards, cache);
     children.push_back(child);
@@ -122,10 +136,21 @@ Node SygusUnifRl::purifyLemma(Node n,
   Node nb;
   if (childChanged)
   {
-    if (n.hasOperator())
+    if (fapp && n.hasOperator())
     {
+      Trace("sygus-unif-rl-purify-debug") << "Node " << n
+                                          << " has operator and fapp is true\n";
       children.insert(children.begin(), n.getOperator());
     }
+    if (Trace.isOn("sygus-unif-rl-purify-debug"))
+    {
+      Trace("sygus-unif-rl-purify-debug")
+          << "...rebuilding " << n << " with kind " << k << " and children:\n";
+      for (const Node& child : children)
+      {
+        Trace("sygus-unif-rl-purify-debug") << "...... " << child << "\n";
+      }
+    }
     nb = NodeManager::currentNM()->mkNode(k, children);
     Trace("sygus-unif-rl-purify") << "PurifyLemma : transformed " << n
                                   << " into " << nb << "\n";
@@ -134,7 +159,7 @@ Node SygusUnifRl::purifyLemma(Node n,
   {
     nb = n;
   }
-  /* Map to point enumerator every unification function-to-synthesize  */
+  // Map to point enumerator every unification function-to-synthesize
   if (u_fapp)
   {
     Node np;
@@ -146,28 +171,29 @@ Node SygusUnifRl::purifyLemma(Node n,
         Assert(nb.hasOperator());
         children.insert(children.begin(), n.getOperator());
       }
-      /* Build purified head with fresh skolem and recreate node */
+      // Build purified head with fresh skolem and recreate node
       std::stringstream ss;
-      ss << nb[0] << "_" << d_purified_count[nb[0]]++;
+      ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
       Node new_f = nm->mkSkolem(ss.str(), nb[0].getType());
-      /* Adds new enumerator to map from candidate */
+      // Adds new enumerator to map from candidate
       Trace("sygus-unif-rl-purify") << "...new enum " << new_f
-                                        << " for candidate " << nb[0] << "\n";
+                                    << " for candidate " << nb[0] << "\n";
       d_cand_to_eval_hds[nb[0]].push_back(new_f);
-      /* Maps new enumerator to its respective tuple of arguments */
-      d_app_to_pt[new_f] =
+      // Maps new enumerator to its respective tuple of arguments
+      d_hd_to_pt[new_f] =
           std::vector<Node>(children.begin() + 2, children.end());
-      if (Trace.isOn("sygus-unif-rl-purify"))
+      if (Trace.isOn("sygus-unif-rl-purify-debug"))
       {
-        Trace("sygus-unif-rl-purify") << "...[" << new_f << "] --> (";
-        for (const Node& pt_i : d_app_to_pt[new_f])
+        Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> (";
+        for (const Node& pt_i : d_hd_to_pt[new_f])
         {
-          Trace("sygus-unif-rl-purify") << pt_i << " ";
+          Trace("sygus-unif-rl-purify-debug") << pt_i << " ";
         }
-        Trace("sygus-unif-rl-purify") << ")\n";
+        Trace("sygus-unif-rl-purify-debug") << ")\n";
       }
-      /* replace first child and rebulid node */
+      // replace first child and rebulid node
       children[1] = new_f;
+      Assert(children.size() > 1);
       np = NodeManager::currentNM()->mkNode(k, children);
       d_app_to_purified[nb] = np;
     }
@@ -180,7 +206,7 @@ Node SygusUnifRl::purifyLemma(Node n,
         << np << "\n";
     nb = np;
   }
-  /* Add equality between purified fapp and model value */
+  // Add equality between purified fapp and model value
   if (ensureConst && fapp)
   {
     model_guards.push_back(
@@ -190,8 +216,8 @@ Node SygusUnifRl::purifyLemma(Node n,
                                   << model_guards.back() << "\n";
   }
   nb = Rewriter::rewrite(nb);
-  /* every non-top level application of function-to-synthesize must be reduced
-     to a concrete constant */
+  // every non-top level application of function-to-synthesize must be reduced
+  // to a concrete constant
   Assert(!ensureConst || nb.isConst());
   Trace("sygus-unif-rl-purify-debug") << "... caching [" << n << "] = " << nb
                                       << "\n";
@@ -203,7 +229,7 @@ Node SygusUnifRl::addRefLemma(Node lemma,
                               std::map<Node, std::vector<Node>>& eval_hds)
 {
   Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma
-                               << "\n";
+                                << "\n";
   std::vector<Node> model_guards;
   BoolNodePairMap cache;
   // cache previous sizes
@@ -213,7 +239,7 @@ Node SygusUnifRl::addRefLemma(Node lemma,
     prev_n_eval_hds[cp.first] = cp.second.size();
   }
 
-  /* Make the purified lemma which will guide the unification utility. */
+  // Make the purified lemma which will guide the unification utility.
   Node plem = purifyLemma(lemma, false, model_guards, cache);
   if (!model_guards.empty())
   {
@@ -236,6 +262,20 @@ Node SygusUnifRl::addRefLemma(Node lemma,
     for (unsigned j = prevn, size = cp.second.size(); j < size; j++)
     {
       eval_hds[c].push_back(cp.second[j]);
+      // Add new point to respective decision trees
+      Assert(d_cand_cenums.find(c) != d_cand_cenums.end());
+      for (const Node& cenum : d_cand_cenums[c])
+      {
+        Assert(d_cenum_to_stratpt.find(cenum) != d_cenum_to_stratpt.end());
+        for (const Node& stratpt : d_cenum_to_stratpt[cenum])
+        {
+          Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end());
+          Trace("sygus-unif-rl-dt") << "Add point with head " << cp.second[j]
+                                    << " to strategy point " << stratpt << "\n";
+          // Register new point from new head
+          d_stratpt_to_dt[stratpt].addPoint(cp.second[j]);
+        }
+      }
     }
   }
 
@@ -265,8 +305,8 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
       {
         return false;
       }
-      Trace("sygus-unif-rl-sol")
-          << "Adding solution " << v << " to unif candidate " << c << "\n";
+      Trace("sygus-unif-rl-sol") << "Adding solution " << v
+                                 << " to unif candidate " << c << "\n";
       sols.push_back(v);
     }
   }
@@ -280,12 +320,18 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
   // 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())
+    std::map<Node, DecisionTreeInfo>::iterator itd = d_stratpt_to_dt.find(e);
+    if (itd != d_stratpt_to_dt.end())
     {
       indent("sygus-unif-sol", ind);
-      Trace("sygus-unif-sol")
-          << "...it has a decision tree strategy." << std::endl;
+      Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n";
+      if (itd->second.isSeparated())
+      {
+        Trace("sygus-unif-sol")
+            << "...... points are separated and I have for root enum the value "
+            << d_parent->getModelValue(e) << "\n";
+        return d_parent->getModelValue(e);
+      }
     }
   }
 
@@ -301,13 +347,13 @@ void SygusUnifRl::registerStrategy(Node f)
 {
   if (Trace.isOn("sygus-unif-rl-strat"))
   {
-    Trace("sygus-unif-rl-strat")
-        << "Strategy for " << f << " is : " << std::endl;
+    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;
+  std::map<Node, std::map<NodeRole, bool>> visited;
   registerStrategyNode(f, e, role_equal, visited);
 }
 
@@ -315,7 +361,7 @@ 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)
 {
   Trace("sygus-unif-rl-strat") << "  register node " << e << std::endl;
   if (visited[e].find(nrole) != visited[e].end())
@@ -367,11 +413,111 @@ void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond)
       == d_cond_enums.end())
   {
     d_cond_enums.push_back(cond);
+    d_cand_cenums[f].push_back(cond);
     // register the conditional enumerator
     d_tds->registerEnumerator(cond, f, d_parent, true);
+    d_cenum_to_stratpt[cond].clear();
+  }
+  // register that this strategy node has a decision tree construction
+  d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f]);
+  // associate conditional enumerator with strategy node
+  d_cenum_to_stratpt[cond].push_back(e);
+}
+
+void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum,
+                                               SygusUnifRl* unif,
+                                               SygusUnifStrategy* strategy)
+{
+  d_cond_enum = cond_enum;
+  d_unif = unif;
+  d_strategy = strategy;
+  // Retrieve template
+  EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum);
+  d_template = NodePair(eiv.d_template, eiv.d_template_arg);
+  // Initialize classifier
+  d_pt_sep.initialize(this);
+}
+
+void SygusUnifRl::DecisionTreeInfo::addPoint(Node f)
+{
+  d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
+}
+
+void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv)
+{
+  d_conds.push_back(condv);
+  d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1);
+}
+
+bool SygusUnifRl::DecisionTreeInfo::isSeparated()
+{
+  for (const std::pair<const Node, std::vector<Node>>& rep_to_class :
+       d_pt_sep.d_trie.d_rep_to_class)
+  {
+    Assert(!rep_to_class.second.empty());
+    Node v = rep_to_class.second[0];
+    unsigned i, size = rep_to_class.second.size();
+    for (i = 1; i < size; ++i)
+    {
+      Node vi = d_unif->d_parent->getModelValue(rep_to_class.second[i]);
+      if (v != vi)
+      {
+        Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: "
+                                  << rep_to_class.second[0] << " and "
+                                  << rep_to_class.second[i] << "\n";
+        break;
+      }
+    }
+    // Heads with different model values
+    if (i != size)
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize(
+    DecisionTreeInfo* dt)
+{
+  d_dt = dt;
+}
+
+Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n,
+                                                             unsigned index)
+{
+  Assert(index < d_dt->d_conds.size());
+  // Retrieve respective built_in condition
+  Node cond = d_dt->d_conds[index];
+  TypeNode tn = cond.getType();
+  Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn);
+  // Retrieve evaluation point
+  Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end());
+  std::vector<Node> pt = d_dt->d_unif->d_hd_to_pt[n];
+  // compute the result
+  Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
+  if (Trace.isOn("sygus-unif-rl-sep"))
+  {
+    Trace("sygus-unif-rl-sep") << "...got res = " << res << " from cond "
+                               << builtin_cond << " on pt " << n << " ( ";
+    for (const Node& pti : pt)
+    {
+      Trace("sygus-unif-rl-sep") << pti << " ";
+    }
+    Trace("sygus-unif-rl-sep") << ")\n";
+  }
+  // If condition is templated, recompute result accordingly
+  Node templ = d_dt->d_template.first;
+  TNode templ_var = d_dt->d_template.second;
+  if (!templ.isNull())
+  {
+    res = templ.substitute(templ_var, res);
+    res = Rewriter::rewrite(res);
+    Trace("sygus-unif-rl-sep") << "...after template res = " << res
+                               << std::endl;
   }
-  // register that this enumerator has a decision tree construction
-  d_enum_to_dt[e].d_cond_enum = cond;
+  Assert(res.isConst());
+  return res;
 }
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 29c67aa81..d618876da 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -2,7 +2,7 @@
 /*! \file sygus_unif_rl.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -20,6 +20,7 @@
 #include <map>
 #include "theory/quantifiers/sygus/sygus_unif.h"
 
+#include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -31,6 +32,7 @@ using BoolNodePairHashFunction =
     PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
 using BoolNodePairMap =
     std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
+using NodePair = std::pair<Node, Node>;
 
 class CegConjecture;
 
@@ -82,20 +84,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;
-  /**
-   * This class stores information regarding an enumerator, including: a
-   * database of values that have been enumerated for this enumerator.
-   */
-  class EnumCache
-  {
-   public:
-    EnumCache() {}
-    ~EnumCache() {}
-    /** Values that have been enumerated for this enumerator */
-    std::vector<Node> d_enum_vals;
-  };
-  /** maps enumerators to the information above */
-  std::map<Node, EnumCache> d_ecache;
   /** construct sol */
   Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
   /** collects data from refinement lemmas to drive solution construction
@@ -111,16 +99,20 @@ class SygusUnifRl : public SygusUnif
         Purification
     --------------------------------------------------------------
   */
-  /* Maps unif candidates to heads of their evaluation points */
+  /**
+   * maps heads of applications of a unif function-to-synthesize to their tuple
+   * of arguments (which constitute a "data point" aka an "evaluation point")
+   */
+  std::map<Node, std::vector<Node>> d_hd_to_pt;
+  /** maps unif candidates to heads of their evaluation points */
   std::map<Node, std::vector<Node>> d_cand_to_eval_hds;
   /**
-   * maps applications of the function-to-synthesize to their tuple of arguments
-   * (which constitute a "data point") */
-  std::map<Node, std::vector<Node>> d_app_to_pt;
-  /** Maps applications of unif functions-to-synthesize to purified symbols*/
+   * maps applications of unif functions-to-synthesize to the result of their
+   * purification */
   std::map<Node, Node> d_app_to_purified;
-  /** Maps unif functions-to-synthesize to counters of purified symbols */
-  std::map<Node, unsigned> d_purified_count;
+  /** maps unif functions-to-synthesize to counters of heads of evaluation
+   * points */
+  std::map<Node, unsigned> d_cand_to_hd_count;
   /**
    * This is called on the refinement lemma and will rewrite applications of
    * functions-to-synthesize to their respective purified form, i.e. such that
@@ -136,10 +128,10 @@ class SygusUnifRl : public SygusUnif
    *
    * When the traversal encounters an application of a unification
    * function-to-synthesize it will proceed to ensure that the arguments of that
-   * function application are constants (the ensureConst becomes "true"). If an
+   * function application are constants (ensureConst becomes "true"). If an
    * applicatin of a non-unif function-to-synthesize is reached, the requirement
-   * is lifted (the ensureConst becomes "false"). This avoides introducing
-   * spurious equalities in model_guards.
+   * is lifted (ensureConst becomes "false"). This avoides introducing spurious
+   * equalities in model_guards.
    *
    * For example if "f" is being synthesized with a unification strategy and "g"
    * is not then the application
@@ -152,7 +144,8 @@ class SygusUnifRl : public SygusUnif
    * would be purified into
    *   g(0) = c1 ^ f1(c1) = c2 => f2(+(0,c2))
    *
-   * This function also populates the maps for point enumerators
+   * This function also populates the maps between candidates, heads and
+   * evaluation points
    */
   Node purifyLemma(Node n,
                    bool ensureConst,
@@ -170,14 +163,71 @@ class SygusUnifRl : public SygusUnif
   class DecisionTreeInfo
   {
    public:
+    DecisionTreeInfo() {}
+    ~DecisionTreeInfo() {}
+    /** initializes this class */
+    void initialize(Node cond_enum,
+                    SygusUnifRl* unif,
+                    SygusUnifStrategy* strategy);
+    /** adds the respective evaluation point of the head f  */
+    void addPoint(Node f);
+    /** adds a condition value to the pool of condition values */
+    void addCondValue(Node condv);
+    /** whether all points that must be separated are separated **/
+    bool isSeparated();
+    /** reference to parent unif util */
+    SygusUnifRl* d_unif;
+    /** enumerator template (if no templates, nodes in pair are Node::null()) */
+    NodePair d_template;
+    /** enumerated condition values */
+    std::vector<Node> d_conds;
+
+   private:
+    /**
+     * reference to infered strategy for the function-to-synthesize this DT is
+     * associated with
+     */
+    SygusUnifStrategy* d_strategy;
     /**
      * The enumerator in the strategy tree that stores conditions of the
      * decision tree.
      */
     Node d_cond_enum;
+    /** Classifies evaluation points according to enumerated condition values
+     *
+     * Maintains the invariant that points evaluated in the same way in the
+     * current condition values are kept in the same "separation class."
+     */
+    class PointSeparator : public LazyTrieEvaluator
+    {
+     public:
+      /** initializes this class */
+      void initialize(DecisionTreeInfo* dt);
+      /**
+       * evaluates the respective evaluation point of the head n on the index-th
+       * condition
+       */
+      Node evaluate(Node n, unsigned index) override;
+
+      /** the lazy trie for building the separation classes */
+      LazyTrieMulti d_trie;
+
+     private:
+      /** reference to parent unif util */
+      DecisionTreeInfo* d_dt;
+    };
+    /**
+     * Utility for determining how evaluation points are separated by currently
+     * enumerated condiotion values
+     */
+    PointSeparator d_pt_sep;
   };
-  /** map from enumerators in the strategy trees to the above data */
-  std::map<Node, DecisionTreeInfo> d_enum_to_dt;
+  /** maps strategy points in the strategy tree to the above data */
+  std::map<Node, DecisionTreeInfo> d_stratpt_to_dt;
+  /** maps conditional enumerators to strategy points in which they occur */
+  std::map<Node, std::vector<Node>> d_cenum_to_stratpt;
+  /** maps unif candidates to their conditional enumerators */
+  std::map<Node, std::vector<Node>> d_cand_cenums;
   /** all conditional enumerators */
   std::vector<Node> d_cond_enums;
   /** register strategy