Using a single condition enumerator in sygus-unif (#2440)

This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).

In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:

- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.

A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.

There is also small improvements for trace messages.

5 files changed, 247 insertions, 76 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 7319ba73e..204daa49a 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -166,7 +166,17 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     Trace("cegis") << "  Enumerators :\n";
     for (unsigned i = 0, size = enums.size(); i < size; ++i)
     {
-      Trace("cegis") << "    " << enums[i] << " -> ";
+      bool isUnit = false;
+      for (const Node& hd_unit : d_rl_eval_hds)
+      {
+        if (enums[i] == hd_unit[0])
+        {
+          isUnit = true;
+          break;
+        }
+      }
+      Trace("cegis") << "    " << enums[i]
+                     << (options::sygusUnif() && isUnit ? "*" : "") << " -> ";
       std::stringstream ss;
       Printer::getPrinter(options::outputLanguage())
           ->toStreamSygus(ss, enum_values[i]);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 89a11eb0c..1245cba1f 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -68,8 +68,8 @@ bool CegisUnif::processInitialize(Node n,
       {
         Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
         Assert(!cond.isNull());
-        Trace("cegis-unif") << "  " << e << " with condition : " << cond
-                            << std::endl;
+        Trace("cegis-unif")
+            << "  " << e << " with condition : " << cond << std::endl;
         pt_to_cond[e] = cond;
       }
     }
@@ -90,8 +90,8 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
     // Collect heads of candidates
     for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
     {
-      Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd "
-                                     << hd << "\n";
+      Trace("cegis-unif-enum-debug")
+          << "......cand " << c << " with enum hd " << hd << "\n";
       enums.push_back(hd);
     }
   }
@@ -112,12 +112,15 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   }
   if (!satisfiedRl)
   {
+    Trace("cegis-unif")
+        << "..added refinement lemmas\n---CegisUnif Engine---\n";
     // if we didn't satisfy the specification, there is no way to repair
     return false;
   }
   // the unification enumerators (return values, conditions) and their model
   // values
   NodeManager* nm = NodeManager::currentNM();
+  Valuation& valuation = d_qe->getValuation();
   bool addedUnifEnumSymBreakLemma = false;
   Node cost_lit = d_u_enum_manager.getCurrentLiteral();
   std::map<Node, std::vector<Node>> unif_enums[2];
@@ -135,6 +138,21 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
         // get the current unification enumerators
         d_u_enum_manager.getEnumeratorsForStrategyPt(
             e, unif_enums[index][e], index);
+        if (index == 1 && options::sygusUnifCondIndependent())
+        {
+          Assert(unif_enums[index][e].size() == 1);
+          Node eu = unif_enums[index][e][0];
+          Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
+          // If active guard for this enumerator is not true, there are no more
+          // values for it, and hence we ignore it
+          Node gstatus = valuation.getSatValue(g);
+          if (gstatus.isNull() || !gstatus.getConst<bool>())
+          {
+            Trace("cegis") << "    " << eu << " -> N/A\n";
+            unif_enums[index][e].clear();
+            continue;
+          }
+        }
         // get the model value of each enumerator
         for (const Node& eu : unif_enums[index][e])
         {
@@ -149,9 +167,9 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
           }
           unif_values[index][e].push_back(m_eu);
         }
+        // inter-enumerator symmetry breaking for return values
         if (index == 0)
         {
-          // inter-enumerator symmetry breaking
           // given a pool of unification enumerators eu_1, ..., eu_n,
           // CegisUnifEnumManager insists that size(eu_1) <= ... <= size(eu_n).
           // We additionally insist that M(eu_i) < M(eu_{i+1}) when
@@ -198,6 +216,8 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   }
   if (addedUnifEnumSymBreakLemma)
   {
+    Trace("cegis-unif") << "..added unif enum symmetry breaking "
+                           "lemma\n---CegisUnif Engine---\n";
     return false;
   }
   // set the conditions
@@ -207,6 +227,16 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
     {
       d_sygus_unif.setConditions(
           e, cost_lit, unif_enums[1][e], unif_values[1][e]);
+      // if condition enumerator had value, exclude this value
+      if (options::sygusUnifCondIndependent() && !unif_enums[1][e].empty())
+      {
+        Node eu = unif_enums[1][e][0];
+        Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
+        Node exp_exc = d_tds->getExplain()
+                           ->getExplanationForEquality(eu, unif_values[1][e][0])
+                           .negate();
+        lems.push_back(nm->mkNode(OR, g.negate(), exp_exc));
+      }
     }
   }
   // build solutions (for unif candidates a divide-and-conquer approach is used)
@@ -228,13 +258,15 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
     return true;
   }
 
-  Assert(!lemmas.empty());
+  // TODO tie this to the lemma for getting a new condition value
+  Assert(options::sygusUnifCondIndependent() || !lemmas.empty());
   for (const Node& lem : lemmas)
   {
-    Trace("cegis-unif") << "CegisUnif::lemma, separation lemma : " << lem
-                        << "\n";
+    Trace("cegis-unif-lemma")
+        << "CegisUnif::lemma, separation lemma : " << lem << "\n";
     d_qe->getOutputChannel().lemma(lem);
   }
+  Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
   return false;
 }
 
@@ -246,12 +278,13 @@ 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);
   addRefinementLemma(plem);
-  Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n";
+  Trace("cegis-unif-lemma")
+      << "CegisUnif::lemma, refinement lemma : " << plem << "\n";
   // Notify the enumeration manager if there are new evaluation points
   for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
   {
     Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end());
-    // Notify each startegy point of the respective candidate
+    // Notify each strategy point of the respective candidate
     for (const Node& n : d_cand_to_strat_pt[ep.first])
     {
       d_u_enum_manager.registerEvalPts(ep.second, n);
@@ -303,8 +336,8 @@ void CegisUnifEnumManager::initialize(
     std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e);
     Assert(itcc != e_to_cond.end());
     Node cond = itcc->second;
-    Trace("cegis-unif-enum-debug") << "...its condition strategy point is "
-                                   << cond << "\n";
+    Trace("cegis-unif-enum-debug")
+        << "...its condition strategy point is " << cond << "\n";
     d_ce_info[e].d_ce_type = cond.getType();
     // initialize the symmetry breaking lemma templates
     for (unsigned index = 0; index < 2; index++)
@@ -329,6 +362,17 @@ void CegisUnifEnumManager::initialize(
   }
   // initialize the current literal
   incrementNumEnumerators();
+  // create single condition enumerator for each decision tree strategy
+  if (options::sygusUnifCondIndependent())
+  {
+    // allocate a condition enumerator for each candidate
+    for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
+    {
+      Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+      setUpEnumerator(ceu, ci.second, 1);
+      d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu);
+    }
+  }
 }
 
 void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
@@ -340,8 +384,8 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
   Assert(num_enums > 0);
   if (index == 1)
   {
-    // we always use (cost-1) conditions
-    num_enums = num_enums - 1;
+    // we always use (cost-1) conditions, or 1 if in the indepedent case
+    num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1;
   }
   if (num_enums > 0)
   {
@@ -354,6 +398,46 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
   }
 }
 
+Node CegisUnifEnumManager::getActiveGuardForEnumerator(Node e)
+{
+  Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
+  return d_enum_to_active_guard[e];
+}
+
+void CegisUnifEnumManager::setUpEnumerator(Node e,
+                                           StrategyPtInfo& si,
+                                           unsigned index)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  // instantiate template for removing redundant operators
+  if (!si.d_sbt_lemma_tmpl[index].first.isNull())
+  {
+    Node templ = si.d_sbt_lemma_tmpl[index].first;
+    TNode templ_var = si.d_sbt_lemma_tmpl[index].second;
+    Node sym_break_red_ops = templ.substitute(templ_var, e);
+    Trace("cegis-unif-enum-lemma")
+        << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
+        << sym_break_red_ops << "\n";
+    d_qe->getOutputChannel().lemma(sym_break_red_ops);
+  }
+  // symmetry breaking between enumerators
+  if (!si.d_enums[index].empty() && index == 0)
+  {
+    Node e_prev = si.d_enums[index].back();
+    Node size_e = nm->mkNode(DT_SIZE, e);
+    Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
+    Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
+    Trace("cegis-unif-enum-lemma")
+        << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
+    d_qe->getOutputChannel().lemma(sym_break);
+  }
+  // register the enumerator
+  si.d_enums[index].push_back(e);
+  Trace("cegis-unif-enum") << "* Registering new enumerator " << e
+                           << " to strategy point " << si.d_pt << "\n";
+  d_tds->registerEnumerator(e, si.d_pt, d_parent);
+}
+
 void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
 {
   // candidates of the same type are managed
@@ -427,7 +511,7 @@ void CegisUnifEnumManager::incrementNumEnumerators()
       TypeNode ct = c.getType();
       Node eu = nm->mkSkolem("eu", ct);
       Node ceu;
-      if (!ci.second.d_enums[0].empty())
+      if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
       {
         // make a new conditional enumerator as well, starting the
         // second type around
@@ -441,38 +525,7 @@ void CegisUnifEnumManager::incrementNumEnumerators()
         {
           continue;
         }
-        // instantiate template for removing redundant operators
-        if (!ci.second.d_sbt_lemma_tmpl[index].first.isNull())
-        {
-          Node templ = ci.second.d_sbt_lemma_tmpl[index].first;
-          TNode templ_var = ci.second.d_sbt_lemma_tmpl[index].second;
-          Node sym_break_red_ops = templ.substitute(templ_var, e);
-          Trace("cegis-unif-enum-lemma")
-              << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
-              << sym_break_red_ops << "\n";
-          d_qe->getOutputChannel().lemma(sym_break_red_ops);
-        }
-        // symmetry breaking between enumerators
-        if (!ci.second.d_enums[index].empty() && index == 0)
-        {
-          Node e_prev = ci.second.d_enums[index].back();
-          Node size_e = nm->mkNode(DT_SIZE, e);
-          Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
-          Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
-          Trace("cegis-unif-enum-lemma")
-              << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
-          d_qe->getOutputChannel().lemma(sym_break);
-        }
-        // register the enumerator
-        ci.second.d_enums[index].push_back(e);
-        Trace("cegis-unif-enum") << "* Registering new enumerator " << e
-                                 << " to strategy point " << ci.second.d_pt
-                                 << "\n";
-        d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
-        // TODO symmetry breaking for making
-        //   e distinct from ei : (ci.second.d_enums[index] \ {e})
-        // if its respective type has had at least
-        // ci.second.d_enums[index].size() distinct values enumerated
+        setUpEnumerator(e, ci.second, index);
       }
     }
     // register the evaluation points at the new value
@@ -568,8 +621,8 @@ void CegisUnifEnumManager::registerEvalPtAtSize(Node e,
     disj.push_back(ei.eqNode(itc->second.d_enums[0][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 858a83bce..69d6ee25f 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -76,6 +76,8 @@ class CegisUnifEnumManager
    * registerEvalPtAtValue on the output channel of d_qe.
    */
   void registerEvalPts(const std::vector<Node>& eis, Node e);
+  /** Retrieves active guard for enumerator */
+  Node getActiveGuardForEnumerator(Node e);
   /** get next decision request
    *
    * This function has the same contract as Theory::getNextDecisionRequest.
@@ -105,6 +107,9 @@ class CegisUnifEnumManager
   bool d_initialized;
   /** null node */
   Node d_null;
+  /** map from condition enumerators to active guards (in case they are
+   * enumerated indepedently of the return values) */
+  std::map<Node, Node> d_enum_to_active_guard;
   /** information per initialized type */
   class StrategyPtInfo
   {
@@ -165,6 +170,15 @@ class CegisUnifEnumManager
    * current SAT context.
    */
   context::CDO<unsigned> d_curr_guq_val;
+  /** Registers an enumerator and adds symmetry breaking lemmas
+   *
+   * The symmetry breaking lemmas are generated according to the stored
+   * information from the enumerator's respective strategy point and whether it
+   * is a condition or return value enumerator. For the latter we add symmetry
+   * breaking lemmas that force enumerators to consider values in an increasing
+   * order of size.
+   */
+  void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index);
   /** increment the number of enumerators */
   void incrementNumEnumerators();
   /** get literal G_uq_n */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 183f40b66..51b14f3e1 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -345,10 +345,8 @@ Node SygusUnifRl::constructSol(
   }
   EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
   Node sol = itd->second.buildSol(etis->d_cons, lemmas);
-  if (sol.isNull())
-  {
-    Assert(!lemmas.empty());
-  }
+  Assert(options::sygusUnifCondIndependent() || !sol.isNull()
+         || !lemmas.empty());
   return sol;
 }
 
@@ -512,6 +510,23 @@ void SygusUnifRl::DecisionTreeInfo::setConditions(
   // set new condition values
   d_enums.insert(d_enums.end(), enums.begin(), enums.end());
   d_conds.insert(d_conds.end(), conds.begin(), conds.end());
+  // add to condition pool
+  if (options::sygusUnifCondIndependent())
+  {
+    if (Trace.isOn("sygus-unif-cond-pool"))
+    {
+      d_cond_mvs.insert(conds.begin(), conds.end());
+      for (const Node& condv : conds)
+      {
+        if (d_cond_mvs.find(condv) == d_cond_mvs.end())
+        {
+          Trace("sygus-unif-cond-pool")
+              << "  ...adding to condition pool : "
+              << d_unif->d_tds->sygusToBuiltin(condv, condv.getType()) << "\n";
+        }
+      }
+    }
+  }
 }
 
 unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const
@@ -519,8 +534,6 @@ unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const
   return d_strategy_index;
 }
 
-using UNodePair = std::pair<unsigned, Node>;
-
 Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
                                              std::vector<Node>& lemmas)
 {
@@ -532,6 +545,62 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
   Trace("sygus-unif-sol") << "Decision::buildSol with " << d_hds.size()
                           << " evaluation heads and " << d_conds.size()
                           << " conditions..." << std::endl;
+
+  return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas)
+                                             : buildSolMinCond(cons, lemmas);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
+                                                    std::vector<Node>& lemmas)
+{
+  // model values for evaluation heads
+  std::map<Node, Node> hd_mv;
+  // add conditions
+  d_conds.clear();
+  d_conds.insert(d_conds.end(), d_cond_mvs.begin(), d_cond_mvs.end());
+  unsigned num_conds = d_conds.size();
+  for (unsigned i = 0; i < num_conds; ++i)
+  {
+    d_pt_sep.d_trie.addClassifier(&d_pt_sep, i);
+  }
+  // add heads
+  for (const Node& e : d_hds)
+  {
+    Node v = d_unif->d_parent->getModelValue(e);
+    hd_mv[e] = v;
+    Node er = d_pt_sep.d_trie.add(e, &d_pt_sep, num_conds);
+    // are we in conflict?
+    if (er == e)
+    {
+      // new separation class, no conflict
+      continue;
+    }
+    Assert(hd_mv.find(er) != hd_mv.end());
+    // merged into separation class with same model value, no conflict
+    if (hd_mv[e] == hd_mv[er])
+    {
+      continue;
+    }
+    // conflict. Explanation?
+    Trace("sygus-unif-sol")
+        << "  ...can't separate " << e << " from " << er << std::endl;
+    return Node::null();
+  }
+  Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+  Node sol = d_pt_sep.extractSol(cons, hd_mv);
+  // repeated solution
+  if (options::sygusUnifCondIndNoRepeatSol()
+      && d_sols.find(sol) != d_sols.end())
+  {
+    return Node::null();
+  }
+  d_sols.insert(sol);
+  return sol;
+}
+
+Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
+                                                    std::vector<Node>& lemmas)
+{
   NodeManager* nm = NodeManager::currentNM();
   // model values for evaluation heads
   std::map<Node, Node> hd_mv;
@@ -749,13 +818,20 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
   }
 
   Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+  return d_pt_sep.extractSol(cons, hd_mv);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::PointSeparator::extractSol(
+    Node cons, std::map<Node, Node>& hd_mv)
+{
   // 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);
+  IndTriePair root = IndTriePair(0, &d_trie.d_trie);
   visit.push_back(root);
   while (!visit.empty())
   {
@@ -772,10 +848,10 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
       {
         Assert(hd_mv.find(trie->d_lazy_child) != hd_mv.end());
         cache[cur] = hd_mv[trie->d_lazy_child];
-        Trace("sygus-unif-sol-debug")
-            << "......leaf, build "
-            << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
-            << "\n";
+        Trace("sygus-unif-sol-debug") << "......leaf, build "
+                                      << d_dt->d_unif->d_tds->sygusToBuiltin(
+                                             cache[cur], cache[cur].getType())
+                                      << "\n";
         continue;
       }
       cache[cur] = Node::null();
@@ -791,7 +867,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
     Assert(trie->d_children.size() == 1 || trie->d_children.size() == 2);
     std::vector<Node> children(4);
     children[0] = cons;
-    children[1] = d_conds[index];
+    children[1] = d_dt->d_conds[index];
     unsigned i = 0;
     for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
     {
@@ -805,8 +881,12 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
     {
       cache[cur] = children[i];
       Trace("sygus-unif-sol-debug")
-          << "......no cond, build "
-          << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+          << "......no need for cond "
+          << d_dt->d_unif->d_tds->sygusToBuiltin(d_dt->d_conds[index],
+                                                 d_dt->d_conds[index].getType())
+          << ", build "
+          << d_dt->d_unif->d_tds->sygusToBuiltin(cache[cur],
+                                                 cache[cur].getType())
           << "\n";
       continue;
     }
@@ -814,15 +894,11 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
     cache[cur] = nm->mkNode(APPLY_CONSTRUCTOR, children);
     Trace("sygus-unif-sol-debug")
         << "......build node "
-        << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+        << d_dt->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];
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index c9bdf5691..b2db53aeb 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -205,16 +205,27 @@ class SygusUnifRl : public SygusUnif
                     unsigned strategy_index);
     /** 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
+    /** builds solution, if possible, 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 by the current set of conditions.
-     *
-     * This method either returns a solution (if all points are separated).
-     * It it fails, it adds a conflict lemma to lemmas.
+     * A solution is possible when all different valued heads can be separated,
+     * i.e. the current set of conditions separates them in a decision tree
      */
     Node buildSol(Node cons, std::vector<Node>& lemmas);
+    /** bulids a solution by considering all condition values ever enumerated */
+    Node buildSolAllCond(Node cons, std::vector<Node>& lemmas);
+    /** builds a solution by incrementally adding points and conditions to DT
+     *
+     * Differently from the above method, here a condition is only added to the
+     * DT when it's necessary for resolving a separation conflict (i.e. heads
+     * with different values in the same leaf of the DT). Only one value per
+     * condition enumerated is considered.
+     *
+     * If a solution cannot be built, then there are more conflicts to be
+     * resolved than condition enumerators. A conflict lemma is added to lemmas
+     * that forces a new assigment in which the conflict is removed (heads are
+     * made equal) or a new condition is enumerated to try to separate them.
+     */
+    Node buildSolMinCond(Node cons, std::vector<Node>& lemmas);
     /** reference to parent unif util */
     SygusUnifRl* d_unif;
     /** enumerator template (if no templates, nodes in pair are Node::null()) */
@@ -223,6 +234,8 @@ class SygusUnifRl : public SygusUnif
     std::vector<Node> d_conds;
     /** gathered evaluation point heads */
     std::vector<Node> d_hds;
+    /** all enumerated model values for conditions */
+    std::unordered_set<Node, NodeHashFunction> d_cond_mvs;
     /** get condition enumerator */
     Node getConditionEnumerator() const { return d_cond_enum; }
     /** set conditions */
@@ -231,6 +244,9 @@ class SygusUnifRl : public SygusUnif
                        const std::vector<Node>& conds);
 
    private:
+    /** Accumulates solutions built when considering all enumerated condition
+     * values (which may generate repeated solutions) */
+    std::unordered_set<Node, NodeHashFunction> d_sols;
     /**
      * Conditional enumerator variables corresponding to the condition values in
      * d_conds. These are used for generating separation lemmas during
@@ -278,6 +294,8 @@ class SygusUnifRl : public SygusUnif
 
       /** the lazy trie for building the separation classes */
       LazyTrieMulti d_trie;
+      /** extracts solution from decision tree built */
+      Node extractSol(Node cons, std::map<Node, Node>& hd_mv);
 
      private:
       /** reference to parent unif util */