Piecing solutions together in CegisUnif (#1894)

6 files changed, 277 insertions, 85 deletions

diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp
index 9e910b43a..21a87c792 100644
--- a/src/theory/quantifiers/lazy_trie.cpp
+++ b/src/theory/quantifiers/lazy_trie.cpp
@@ -59,8 +59,6 @@ Node LazyTrie::add(Node n,
   return Node::null();
 }
 
-using IndTriePair = std::pair<unsigned, LazyTrie*>;
-
 void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal)
 {
   Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
index 2da76d6ef..935b9bec1 100644
--- a/src/theory/quantifiers/lazy_trie.h
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -94,6 +94,8 @@ class LazyTrie
            bool forceKeep);
 };
 
+using IndTriePair = std::pair<unsigned, LazyTrie*>;
+
 /** Lazy trie with multiple elements per leaf
  *
  * As the above trie, but allows multiple elements per leaf. This is done by
@@ -157,7 +159,6 @@ class LazyTrieMulti
    * containing only itself.
    */
   Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
- private:
   /** A regular lazy trie */
   LazyTrie d_trie;
 };
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 06b552276..a99e726b6 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -73,25 +73,32 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
 {
   for (const Node& c : candidates)
   {
+    // Non-unif candidate are themselves the enumerators
     if (!d_sygus_unif.usingUnif(c))
     {
       enums.push_back(c);
       continue;
     }
-    Valuation& valuation = d_qe->getValuation();
-    for (const Node& e : d_cond_enums)
+    // Collect heads of candidate
+    for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
     {
-      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.
-      Node gstatus = valuation.getSatValue(g);
-      if (!gstatus.isNull() && gstatus.getConst<bool>())
-      {
-        enums.push_back(e);
-      }
+      Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd "
+                                     << hd << "\n";
+      enums.push_back(hd);
+    }
+  }
+  // Collect condition enumerators
+  Valuation& valuation = d_qe->getValuation();
+  for (const Node& e : d_cond_enums)
+  {
+    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.
+    Node gstatus = valuation.getSatValue(g);
+    if (!gstatus.isNull() && gstatus.getConst<bool>())
+    {
+      enums.push_back(e);
     }
   }
 }
@@ -102,21 +109,15 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
                                     std::vector<Node>& candidate_values,
                                     std::vector<Node>& lems)
 {
-  if (addEvalLemmas(enums, enum_values))
-  {
-    Trace("cegis-unif-lemma") << "Added eval lemmas\n";
-    return false;
-  }
-  unsigned min_term_size = 0;
-  std::vector<unsigned> enum_consider;
   NodeManager* nm = NodeManager::currentNM();
   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
-    if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i])
-        == d_cond_enums.end())
+    // Non-unif enums (which are the very candidates) should not be notified
+    if (enums[i] == candidates[i] && !d_sygus_unif.usingUnif(enums[i]))
     {
+      Trace("cegis-unif-enum") << "  Ignoring non-unif candidate " << enums[i]
+                               << std::endl;
       continue;
     }
     if (Trace.isOn("cegis-unif-enum"))
@@ -127,41 +128,43 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
           ->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)
-    {
-      enum_consider.clear();
-      min_term_size = sz;
-      enum_consider.push_back(i);
-    }
-    else if (sz == min_term_size)
-    {
-      enum_consider.push_back(i);
-    }
-  }
-  // 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)
-  {
-    unsigned j = enum_consider[i];
-    Node e = enums[j], v = enum_values[j];
+    Node e = enums[i], v = enum_values[i];
     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
-    Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
-    Node g = d_enum_to_active_guard[e];
+    // introduce lemmas to exclude this value of a condition enumerator from
+    // future consideration
+    std::map<Node, Node>::iterator it = d_enum_to_active_guard.find(e);
+    if (it == d_enum_to_active_guard.end())
+    {
+      continue;
+    }
     for (unsigned j = 0, size = enum_lems.size(); j < size; ++j)
     {
-      enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
+      enum_lems[j] = nm->mkNode(OR, it->second.negate(), enum_lems[j]);
     }
     lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
   }
-  // divide-and-conquer solution bulding for candidates using unif util
+  // evaluate on refinement lemmas
+  if (addEvalLemmas(enums, enum_values))
+  {
+    Trace("cegis-unif-lemma") << "Added eval lemmas\n";
+    return false;
+  }
+  // build solutions (for unif candidates a divide-and-conquer approach is used)
   std::vector<Node> sols;
   if (d_sygus_unif.constructSolution(sols))
   {
     candidate_values.insert(candidate_values.end(), sols.begin(), sols.end());
+    if (Trace.isOn("cegis-unif"))
+    {
+      Trace("cegis-unif") << "* Candidate solutions are:\n";
+      for (const Node& sol : sols)
+      {
+        Trace("cegis-unif")
+            << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n";
+      }
+      Trace("cegis-unif") << "---CegisUnif Engine---\n";
+    }
     return true;
   }
   return false;
@@ -175,6 +178,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
   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)
   {
@@ -200,11 +204,14 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
       d_ret_dec(qe->getSatContext(), false),
       d_curr_guq_val(qe->getSatContext(), 0)
 {
+  d_initialized = false;
   d_tds = d_qe->getTermDatabaseSygus();
 }
 
 void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
 {
+  Assert(!d_initialized);
+  d_initialized = true;
   if (cs.empty())
   {
     return;
@@ -234,6 +241,8 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c)
     for (const Node& ei : eis)
     {
       Assert(ei.getType() == ct);
+      Trace("cegis-unif-enum") << "...for cand " << c << " adding hd " << ei
+                               << " at size " << p.first << "\n";
       registerEvalPtAtSize(ct, ei, p.second, p.first);
     }
   }
@@ -241,12 +250,12 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c)
 
 Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
 {
-  // have we returned our decision in the current SAT context?
-  if (d_ret_dec.get())
+  // are we not initialized or have we returned our decision in the current SAT
+  // context?
+  if (!d_initialized || d_ret_dec.get())
   {
     return Node::null();
   }
-  // only call this after initialization
   if (d_ce_info.empty())
   {
     // if no enumerators, the decision is null
@@ -257,7 +266,6 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
   bool value;
   if (!d_qe->getValuation().hasSatValue(lit, value))
   {
-    d_ret_dec = true;
     priority = 0;
     return lit;
   }
@@ -267,6 +275,7 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
     incrementNumEnumerators();
     return getNextDecisionRequest(priority);
   }
+  d_ret_dec = true;
   return Node::null();
 }
 
@@ -308,6 +317,8 @@ void CegisUnifEnumManager::incrementNumEnumerators()
       TypeNode ct = ci.first;
       for (const Node& ei : ci.second.d_eval_points)
       {
+        Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
+                                 << " to new size " << new_size << "\n";
         registerEvalPtAtSize(ct, ei, new_lit, new_size);
       }
     }
@@ -342,6 +353,7 @@ 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") << "Adding lemma " << 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 4ea6a887a..ed38c9268 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -85,6 +85,8 @@ class CegisUnifEnumManager
   TermDbSygus* d_tds;
   /** reference to the parent conjecture */
   CegConjecture* d_parent;
+  /** whether this module has been initialized */
+  bool d_initialized;
   /** null node */
   Node d_null;
   /** information per initialized type */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 1260c62af..a2299f834 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -174,7 +174,10 @@ Node SygusUnifRl::purifyLemma(Node n,
       // Build purified head with fresh skolem and recreate node
       std::stringstream ss;
       ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
-      Node new_f = nm->mkSkolem(ss.str(), nb[0].getType());
+      Node new_f = nm->mkSkolem(ss.str(),
+                                nb[0].getType(),
+                                "head of unif evaluation point",
+                                NodeManager::SKOLEM_EXACT_NAME);
       // Adds new enumerator to map from candidate
       Trace("sygus-unif-rl-purify") << "...new enum " << new_f
                                     << " for candidate " << nb[0] << "\n";
@@ -317,25 +320,32 @@ 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;
+  // retrieve strategy information
+  TypeNode etn = e.getType();
+  EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+  StrategyNode& snode = tinfo.getStrategyNode(nrole);
+  if (nrole != role_equal)
+  {
+    return Node::null();
+  }
   // is there a decision tree strategy?
-  if (nrole == role_equal)
+  std::map<Node, DecisionTreeInfo>::iterator itd = d_stratpt_to_dt.find(e);
+  // for now only considering simple case of sole "ITE(cond, e, e)" strategy
+  if (itd == d_stratpt_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.\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);
-      }
-    }
+    return Node::null();
   }
-
-  return Node::null();
+  indent("sygus-unif-sol", ind);
+  Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n";
+  // whether empty set of points
+  if (d_cand_to_eval_hds[f].empty())
+  {
+    Trace("sygus-unif-sol") << "...... no points, return root enum value "
+                            << d_parent->getModelValue(e) << "\n";
+    return d_parent->getModelValue(e);
+  }
+  EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
+  return itd->second.buildSol(etis->d_cons);
 }
 
 bool SygusUnifRl::usingUnif(Node f)
@@ -343,6 +353,16 @@ bool SygusUnifRl::usingUnif(Node f)
   return d_unif_candidates.find(f) != d_unif_candidates.end();
 }
 
+std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
+{
+  std::map<Node, std::vector<Node>>::iterator it = d_cand_to_eval_hds.find(c);
+  if (it == d_cand_to_eval_hds.end())
+  {
+    return std::vector<Node>();
+  }
+  return it->second;
+}
+
 void SygusUnifRl::registerStrategy(Node f)
 {
   if (Trace.isOn("sygus-unif-rl-strat"))
@@ -397,14 +417,17 @@ 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);
+        registerConditionalEnumerator(f, e, cond, j);
       }
     }
     // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
   }
 }
 
-void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond)
+void SygusUnifRl::registerConditionalEnumerator(Node f,
+                                                Node e,
+                                                Node cond,
+                                                unsigned strategy_index)
 {
   // we will do unification for this candidate
   d_unif_candidates.insert(f);
@@ -419,18 +442,20 @@ void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond)
     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]);
+  d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
   // 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)
+                                               SygusUnifStrategy* strategy,
+                                               unsigned strategy_index)
 {
   d_cond_enum = cond_enum;
   d_unif = unif;
   d_strategy = strategy;
+  d_strategy_index = strategy_index;
   // Retrieve template
   EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum);
   d_template = NodePair(eiv.d_template, eiv.d_template_arg);
@@ -449,30 +474,154 @@ void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv)
   d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1);
 }
 
+unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const
+{
+  return d_strategy_index;
+}
+
+using UNodePair = std::pair<unsigned, Node>;
+
+Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons)
+{
+  if (!d_template.first.isNull())
+  {
+    Trace("sygus-unif-sol") << "...templated conditions unsupported\n";
+    return Node::null();
+  }
+  if (!isSeparated())
+  {
+    Trace("sygus-unif-sol") << "...separation check failed\n";
+    return Node::null();
+  }
+  Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+  // Traverse trie and build ITE with cons
+  NodeManager* nm = NodeManager::currentNM();
+  std::map<IndTriePair, Node> cache;
+  std::map<IndTriePair, Node>::iterator it;
+  std::vector<IndTriePair> visit;
+  unsigned index = 0;
+  LazyTrie* trie;
+  IndTriePair root = IndTriePair(0, &d_pt_sep.d_trie.d_trie);
+  visit.push_back(root);
+  while (!visit.empty())
+  {
+    index = visit.back().first;
+    trie = visit.back().second;
+    visit.pop_back();
+    IndTriePair cur = IndTriePair(index, trie);
+    it = cache.find(cur);
+    // traverse children so results are saved to build node for parent
+    if (it == cache.end())
+    {
+      // leaf
+      if (trie->d_children.empty())
+      {
+        Assert(d_hd_values.find(trie->d_lazy_child) != d_hd_values.end());
+        cache[cur] = d_hd_values[trie->d_lazy_child];
+        Trace("sygus-unif-sol-debug")
+            << "......leaf, build "
+            << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+            << "\n";
+        continue;
+      }
+      cache[cur] = Node::null();
+      visit.push_back(cur);
+      for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
+      {
+        visit.push_back(IndTriePair(index + 1, &p_nt.second));
+      }
+      continue;
+    }
+    // retrieve terms of children and build result
+    Assert(it->second.isNull());
+    Assert(trie->d_children.size() == 1 || trie->d_children.size() == 2);
+    std::vector<Node> children(4);
+    children[0] = cons;
+    children[1] = d_conds[index];
+    unsigned i = 0;
+    for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
+    {
+      i = p_nt.first.getConst<bool>() ? 2 : 3;
+      Assert(cache.find(IndTriePair(index + 1, &p_nt.second)) != cache.end());
+      children[i] = cache[IndTriePair(index + 1, &p_nt.second)];
+      Assert(!children[i].isNull());
+    }
+    // condition is useless or result children are equal, no no need for ITE
+    if (trie->d_children.size() == 1 || children[2] == children[3])
+    {
+      cache[cur] = children[i];
+      Trace("sygus-unif-sol-debug")
+          << "......no cond, build "
+          << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+          << "\n";
+      continue;
+    }
+    Assert(trie->d_children.size() == 2);
+    cache[cur] = nm->mkNode(APPLY_CONSTRUCTOR, children);
+    Trace("sygus-unif-sol-debug")
+        << "......build node "
+        << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+        << "\n";
+  }
+  Assert(cache.find(root) != cache.end());
+  Assert(!cache.find(root)->second.isNull());
+  Trace("sygus-unif-sol") << "...solution is "
+                          << d_unif->d_tds->sygusToBuiltin(
+                                 cache[root], cache[root].getType())
+                          << "\n";
+  return cache[root];
+}
+
 bool SygusUnifRl::DecisionTreeInfo::isSeparated()
 {
+  d_hd_values.clear();
   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];
+    Node v = d_unif->d_parent->getModelValue(rep_to_class.second[0]);
+    if (Trace.isOn("sygus-unif-rl-dt-debug"))
+    {
+      Trace("sygus-unif-rl-dt-debug") << "...class of ("
+                                      << rep_to_class.second[0];
+      Assert(d_unif->d_hd_to_pt.find(rep_to_class.second[0])
+             != d_unif->d_hd_to_pt.end());
+      for (const Node& pti : d_unif->d_hd_to_pt[rep_to_class.second[0]])
+      {
+        Trace("sygus-unif-rl-dt-debug") << " " << pti << " ";
+      }
+      Trace("sygus-unif-rl-dt-debug") << ") "
+                                      << " with hd value " << v << "\n";
+    }
+    d_hd_values[rep_to_class.second[0]] = v;
     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]);
+      Assert(d_hd_values.find(rep_to_class.second[i]) == d_hd_values.end());
+      d_hd_values[rep_to_class.second[i]] = vi;
+      if (Trace.isOn("sygus-unif-rl-dt-debug"))
+      {
+        Trace("sygus-unif-rl-dt-debug") << "...class of ("
+                                        << rep_to_class.second[i];
+        Assert(d_unif->d_hd_to_pt.find(rep_to_class.second[i])
+               != d_unif->d_hd_to_pt.end());
+        for (const Node& pti : d_unif->d_hd_to_pt[rep_to_class.second[i]])
+        {
+          Trace("sygus-unif-rl-dt-debug") << " " << pti << " ";
+        }
+        Trace("sygus-unif-rl-dt-debug") << ") "
+                                        << " with hd value " << vi << "\n";
+      }
+      // Heads with different model values
       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;
+        return false;
       }
     }
-    // Heads with different model values
-    if (i != size)
-    {
-      return false;
-    }
   }
   return true;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index d618876da..58cf9011e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -32,6 +32,7 @@ using BoolNodePairHashFunction =
     PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
 using BoolNodePairMap =
     std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
+using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>;
 using NodePair = std::pair<Node, Node>;
 
 class CegConjecture;
@@ -79,6 +80,9 @@ class SygusUnifRl : public SygusUnif
     */
   bool usingUnif(Node f);
 
+  /** retrieve the head of evaluation points for candidate c, if any */
+  std::vector<Node> getEvalPointHeads(Node c);
+
  protected:
   /** reference to the parent conjecture */
   CegConjecture* d_parent;
@@ -168,11 +172,25 @@ class SygusUnifRl : public SygusUnif
     /** initializes this class */
     void initialize(Node cond_enum,
                     SygusUnifRl* unif,
-                    SygusUnifStrategy* strategy);
+                    SygusUnifStrategy* strategy,
+                    unsigned strategy_index);
     /** 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);
+    /** returns index of strategy information of strategy node for this DT */
+    unsigned getStrategyIndex() const;
+    /** builds solution stored in DT, if any, using the given constructor
+     *
+     * The DT contains a solution when no class contains two heads of evaluation
+     * points with different model values, i.e. when all points that must be
+     * separated indeed are separated.
+     *
+     * This function tests separation of the points in the above sense and may
+     * create separation lemmas to enforce guide the synthesis of conditons that
+     * will separate points not currently separated.
+     */
+    Node buildSol(Node cons);
     /** whether all points that must be separated are separated **/
     bool isSeparated();
     /** reference to parent unif util */
@@ -184,15 +202,24 @@ class SygusUnifRl : public SygusUnif
 
    private:
     /**
-     * reference to infered strategy for the function-to-synthesize this DT is
+     * reference to inferred strategy for the function-to-synthesize this DT is
      * associated with
      */
     SygusUnifStrategy* d_strategy;
+    /** index of strategy information of strategy node this DT is based on
+     *
+     * this is the index of the strategy (d_strats[index]) in the strategy node
+     * to which this decision tree corresponds, which can be accessed through
+     * the above strategy reference
+     */
+    unsigned d_strategy_index;
     /**
      * The enumerator in the strategy tree that stores conditions of the
      * decision tree.
      */
     Node d_cond_enum;
+    /** chache of model values of heads of evaluation points */
+    NodePairMap d_hd_values;
     /** Classifies evaluation points according to enumerated condition values
      *
      * Maintains the invariant that points evaluated in the same way in the
@@ -251,7 +278,10 @@ class SygusUnifRl : public SygusUnif
    * 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);
+  void registerConditionalEnumerator(Node f,
+                                     Node e,
+                                     Node cond,
+                                     unsigned strategy_index);
 };
 
 } /* CVC4::theory::quantifiers namespace */