Uses information gain heuristic for building better solutions from DTs (#2451)

3 files changed, 294 insertions, 42 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 1245cba1f..19b0ad717 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -435,7 +435,8 @@ void CegisUnifEnumManager::setUpEnumerator(Node e,
   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);
+  d_tds->registerEnumerator(
+      e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1);
 }
 
 void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 51b14f3e1..66639b750 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -21,6 +21,8 @@
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
+#include <math.h>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -104,14 +106,14 @@ Node SygusUnifRl::purifyLemma(Node n,
         TNode cand = n[0];
         Node tmp = n.substitute(cand, it->second);
         nv = d_tds->evaluateWithUnfolding(tmp);
-        Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << tmp
-                                      << " is " << nv << "\n";
+        Trace("sygus-unif-rl-purify")
+            << "PurifyLemma : model value for " << tmp << " is " << nv << "\n";
       }
       else
       {
         nv = d_parent->getModelValue(n);
-        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";
       }
       Assert(n != nv);
     }
@@ -138,8 +140,8 @@ Node SygusUnifRl::purifyLemma(Node n,
   {
     if (n.getMetaKind() == metakind::PARAMETERIZED)
     {
-      Trace("sygus-unif-rl-purify-debug") << "Node " << n
-                                          << " is parameterized\n";
+      Trace("sygus-unif-rl-purify-debug")
+          << "Node " << n << " is parameterized\n";
       children.insert(children.begin(), n.getOperator());
     }
     if (Trace.isOn("sygus-unif-rl-purify-debug"))
@@ -152,8 +154,8 @@ Node SygusUnifRl::purifyLemma(Node n,
       }
     }
     nb = NodeManager::currentNM()->mkNode(k, children);
-    Trace("sygus-unif-rl-purify") << "PurifyLemma : transformed " << n
-                                  << " into " << nb << "\n";
+    Trace("sygus-unif-rl-purify")
+        << "PurifyLemma : transformed " << n << " into " << nb << "\n";
   }
   else
   {
@@ -174,8 +176,8 @@ Node SygusUnifRl::purifyLemma(Node n,
                                 "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";
+      Trace("sygus-unif-rl-purify")
+          << "...new enum " << new_f << " 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_hd_to_pt[new_f] =
@@ -192,8 +194,8 @@ Node SygusUnifRl::purifyLemma(Node n,
       // replace first child and rebulid node
       Assert(children.size() > 0);
       children[0] = new_f;
-      Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children
-                                          << std::endl;
+      Trace("sygus-unif-rl-purify-debug")
+          << "Make sygus eval app " << children << std::endl;
       np = nm->mkNode(DT_SYGUS_EVAL, children);
       d_app_to_purified[nb] = np;
     }
@@ -212,15 +214,15 @@ Node SygusUnifRl::purifyLemma(Node n,
     model_guards.push_back(
         NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate());
     nb = nv;
-    Trace("sygus-unif-rl-purify") << "PurifyLemma : adding model eq "
-                                  << model_guards.back() << "\n";
+    Trace("sygus-unif-rl-purify")
+        << "PurifyLemma : adding model eq " << model_guards.back() << "\n";
   }
   nb = Rewriter::rewrite(nb);
   // 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";
+  Trace("sygus-unif-rl-purify-debug")
+      << "... caching [" << n << "] = " << nb << "\n";
   cache[BoolNodePair(ensureConst, n)] = nb;
   return nb;
 }
@@ -228,8 +230,8 @@ Node SygusUnifRl::purifyLemma(Node n,
 Node SygusUnifRl::addRefLemma(Node lemma,
                               std::map<Node, std::vector<Node>>& eval_hds)
 {
-  Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma
-                                << "\n";
+  Trace("sygus-unif-rl-purify")
+      << "Registering lemma at SygusUnif : " << lemma << "\n";
   std::vector<Node> model_guards;
   BoolNodePairMap cache;
   // cache previous sizes
@@ -270,9 +272,9 @@ Node SygusUnifRl::addRefLemma(Node lemma,
         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") << "Register point with head "
-                                    << cp.second[j] << " to strategy point "
-                                    << stratpt << "\n";
+          Trace("sygus-unif-rl-dt")
+              << "Register point with head " << cp.second[j]
+              << " to strategy point " << stratpt << "\n";
           // Register new point from new head
           d_stratpt_to_dt[stratpt].d_hds.push_back(cp.second[j]);
         }
@@ -390,8 +392,8 @@ void SygusUnifRl::registerStrategy(
 {
   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;
@@ -491,6 +493,8 @@ void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum,
   d_unif = unif;
   d_strategy = strategy;
   d_strategy_index = strategy_index;
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
   // Retrieve template
   EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum);
   d_template = NodePair(eiv.d_template, eiv.d_template_arg);
@@ -513,9 +517,9 @@ void SygusUnifRl::DecisionTreeInfo::setConditions(
   // add to condition pool
   if (options::sygusUnifCondIndependent())
   {
+    d_cond_mvs.insert(conds.begin(), conds.end());
     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())
@@ -545,7 +549,8 @@ 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;
-
+  // reset the trie
+  d_pt_sep.d_trie.clear();
   return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas)
                                              : buildSolMinCond(cons, lemmas);
 }
@@ -587,7 +592,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
     return Node::null();
   }
   Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
-  Node sol = d_pt_sep.extractSol(cons, hd_mv);
+  Node sol = extractSol(cons, hd_mv);
   // repeated solution
   if (options::sygusUnifCondIndNoRepeatSol()
       && d_sols.find(sol) != d_sols.end())
@@ -604,8 +609,6 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
   NodeManager* nm = NodeManager::currentNM();
   // model values for evaluation heads
   std::map<Node, Node> hd_mv;
-  // reset the trie
-  d_pt_sep.d_trie.clear();
   // the current explanation of why there has not yet been a separation conflict
   std::vector<Node> exp;
   // is the above explanation ready to be sent out as a lemma?
@@ -818,6 +821,17 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
   }
 
   Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+  return extractSol(cons, hd_mv);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::extractSol(Node cons,
+                                               std::map<Node, Node>& hd_mv)
+{
+  // rebuild decision tree using heuristic learning
+  if (options::sygusUnifBooleanHeuristicDt())
+  {
+    recomputeSolHeuristically(hd_mv);
+  }
   return d_pt_sep.extractSol(cons, hd_mv);
 }
 
@@ -902,6 +916,153 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::extractSol(
   return cache[root];
 }
 
+void SygusUnifRl::DecisionTreeInfo::recomputeSolHeuristically(
+    std::map<Node, Node>& hd_mv)
+{
+  // reset the trie
+  d_pt_sep.d_trie.clear();
+  // TODO workaround and not really sure this is the last condition, since I put
+  // a set here. Maybe make d_cond_mvs into a vector
+  Node backup_last_cond = d_conds.back();
+  d_conds.clear();
+  for (const Node& e : d_hds)
+  {
+    d_pt_sep.d_trie.add(e, &d_pt_sep, 0);
+  }
+  // init vector of conds
+  std::vector<Node> conds;
+  conds.insert(conds.end(), d_cond_mvs.begin(), d_cond_mvs.end());
+
+  // recursively build trie by picking best condition for respective points
+  buildDtInfoGain(d_hds, conds, hd_mv, 1);
+  // if no condition was added (i.e. points are already classified at root
+  // level), use last condition as candidate
+  if (d_conds.empty())
+  {
+    Trace("sygus-unif-dt") << "......using last condition "
+                           << d_unif->d_tds->sygusToBuiltin(
+                                  backup_last_cond, backup_last_cond.getType())
+                           << " as candidate\n";
+    d_conds.push_back(backup_last_cond);
+    d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1);
+  }
+}
+
+void SygusUnifRl::DecisionTreeInfo::buildDtInfoGain(std::vector<Node>& hds,
+                                                    std::vector<Node> conds,
+                                                    std::map<Node, Node>& hd_mv,
+                                                    int ind)
+{
+  // test if fully classified
+  if (hds.size() < 2)
+  {
+    indent("sygus-unif-dt", ind);
+    Trace("sygus-unif-dt") << "..set fully classified: "
+                           << (hds.empty() ? "empty" : "unary") << "\n";
+    return;
+  }
+  Node v1 = hd_mv[hds[0]];
+  unsigned i = 1, size = hds.size();
+  for (; i < size; ++i)
+  {
+    if (hd_mv[hds[i]] != v1)
+    {
+      break;
+    }
+  }
+  if (i == size)
+  {
+    indent("sygus-unif-dt", ind);
+    Trace("sygus-unif-dt") << "..set fully classified: " << hds.size() << " "
+                           << (d_unif->d_tds->sygusToBuiltin(v1, v1.getType())
+                                       == d_true
+                                   ? "good"
+                                   : "bad")
+                           << " points\n";
+    return;
+  }
+  // pick condition to further classify
+  double maxgain = -1;
+  unsigned picked_cond = 0;
+  std::vector<std::pair<std::vector<Node>, std::vector<Node>>> splits;
+  double current_set_entropy = getEntropy(hds, hd_mv, ind);
+  for (unsigned i = 0, size = conds.size(); i < size; ++i)
+  {
+    std::pair<std::vector<Node>, std::vector<Node>> split =
+        evaluateCond(hds, conds[i]);
+    splits.push_back(split);
+    Assert(hds.size() == split.first.size() + split.second.size());
+    double gain =
+        current_set_entropy
+        - (split.first.size() * getEntropy(split.first, hd_mv, ind)
+           + split.second.size() * getEntropy(split.second, hd_mv, ind))
+              / hds.size();
+    indent("sygus-unif-dt-debug", ind);
+    Trace("sygus-unif-dt-debug")
+        << "..gain of "
+        << d_unif->d_tds->sygusToBuiltin(conds[i], conds[i].getType()) << " is "
+        << gain << "\n";
+    if (gain > maxgain)
+    {
+      maxgain = gain;
+      picked_cond = i;
+    }
+  }
+  // add picked condition
+  indent("sygus-unif-dt", ind);
+  Trace("sygus-unif-dt") << "..picked condition "
+                         << d_unif->d_tds->sygusToBuiltin(
+                                conds[picked_cond],
+                                conds[picked_cond].getType())
+                         << "\n";
+  d_conds.push_back(conds[picked_cond]);
+  conds.erase(conds.begin() + picked_cond);
+  d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1);
+  // recurse
+  buildDtInfoGain(splits[picked_cond].first, conds, hd_mv, ind + 1);
+  buildDtInfoGain(splits[picked_cond].second, conds, hd_mv, ind + 1);
+}
+
+std::pair<std::vector<Node>, std::vector<Node>>
+SygusUnifRl::DecisionTreeInfo::evaluateCond(std::vector<Node>& pts, Node cond)
+{
+  std::vector<Node> good, bad;
+  for (const Node& pt : pts)
+  {
+    if (d_pt_sep.computeCond(cond, pt) == d_true)
+    {
+      good.push_back(pt);
+      continue;
+    }
+    Assert(d_pt_sep.computeCond(cond, pt) == d_false);
+    bad.push_back(pt);
+  }
+  return std::pair<std::vector<Node>, std::vector<Node>>(good, bad);
+}
+
+double SygusUnifRl::DecisionTreeInfo::getEntropy(const std::vector<Node>& hds,
+                                                 std::map<Node, Node>& hd_mv,
+                                                 int ind)
+{
+  double p = 0, n = 0;
+  TermDbSygus* tds = d_unif->d_tds;
+  // get number of points evaluated positively and negatively with feature
+  for (const Node& e : hds)
+  {
+    if (tds->sygusToBuiltin(hd_mv[e]) == d_true)
+    {
+      p++;
+      continue;
+    }
+    Assert(tds->sygusToBuiltin(hd_mv[e]) == d_false);
+    n++;
+  }
+  // compute entropy
+  return p == 0 || n == 0 ? 0
+                          : ((-p / (p + n)) * log2(p / (p + n)))
+                                - ((n / (p + n)) * log2(n / (p + n)));
+}
+
 void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize(
     DecisionTreeInfo* dt)
 {
@@ -914,16 +1075,29 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n,
   Assert(index < d_dt->d_conds.size());
   // Retrieve respective built_in condition
   Node cond = d_dt->d_conds[index];
+  return computeCond(cond, n);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond,
+                                                                Node hd)
+{
+  std::pair<Node, Node> cond_hd = std::pair<Node, Node>(cond, hd);
+  std::map<std::pair<Node, Node>, Node>::iterator it =
+      d_eval_cond_hd.find(cond_hd);
+  if (it != d_eval_cond_hd.end())
+  {
+    return it->second;
+  }
   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];
+  Assert(d_dt->d_unif->d_hd_to_pt.find(hd) != d_dt->d_unif->d_hd_to_pt.end());
+  std::vector<Node> pt = d_dt->d_unif->d_hd_to_pt[hd];
   // compute the result
   if (Trace.isOn("sygus-unif-rl-sep"))
   {
-    Trace("sygus-unif-rl-sep") << "Evaluate cond " << builtin_cond << " on pt "
-                               << n << " ( ";
+    Trace("sygus-unif-rl-sep")
+        << "Evaluate cond " << builtin_cond << " on pt " << hd << " ( ";
     for (const Node& pti : pt)
     {
       Trace("sygus-unif-rl-sep") << pti << " ";
@@ -939,13 +1113,14 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n,
   {
     res = templ.substitute(templ_var, res);
     res = Rewriter::rewrite(res);
-    Trace("sygus-unif-rl-sep") << "...after template res = " << res
-                               << std::endl;
+    Trace("sygus-unif-rl-sep")
+        << "...after template res = " << res << std::endl;
   }
   Assert(res.isConst());
+  d_eval_cond_hd[cond_hd] = res;
   return res;
 }
 
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index b2db53aeb..aad3c0b49 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -80,7 +80,7 @@ class SygusUnifRl : public SygusUnif
    * whether f is being synthesized with unification strategies. This can be
    * checked through wehether f has conditional or point enumerators (we use the
    * former)
-    */
+   */
   bool usingUnif(Node f) const;
   /** get condition for evaluation point
    *
@@ -244,6 +244,9 @@ class SygusUnifRl : public SygusUnif
                        const std::vector<Node>& conds);
 
    private:
+    /** true and false nodes */
+    Node d_true;
+    Node d_false;
     /** Accumulates solutions built when considering all enumerated condition
      * values (which may generate repeated solutions) */
     std::unordered_set<Node, NodeHashFunction> d_sols;
@@ -275,6 +278,63 @@ class SygusUnifRl : public SygusUnif
      * decision tree.
      */
     Node d_cond_enum;
+    /** extracts solution from decision tree built
+     *
+     * Depending on the active options, the decision tree might be rebuilt
+     * before a solution is extracted, for example to optimize size (smaller
+     * DTs) or chance of having a general solution (information gain heuristics)
+     */
+    Node extractSol(Node cons, std::map<Node, Node>& hd_mv);
+
+    /** rebuild decision tree using information gain heuristic
+     *
+     * In a scenario in which the decision tree potentially contains more
+     * conditions than necessary, it is beneficial to rebuild it in a way that
+     * "better" conditions occurr closer to the top.
+     *
+     * The information gain heuristic selects conditions that lead to a
+     * greater reduction of the Shannon entropy in the set of points
+     */
+    void recomputeSolHeuristically(std::map<Node, Node>& hd_mv);
+    /** recursively select (best) conditions to split heads
+     *
+     * At each call picks the best condition based on the information gain
+     * heuristic and splits the set of heads accordingly, then recurses on
+     * them.
+     *
+     * The base case is a set being fully classified (i.e. all heads have the
+     * same value)
+     *
+     * hds is the set of evaluation point heads we must classify with the
+     * values in conds. The classification is guided by how a condition value
+     * splits the heads through its evaluation on the points associated with
+     * the heads. The metric is based on the model values of the heads (hd_mv)
+     * in the resulting splits.
+     *
+     * ind is the current level of indentation (for debugging)
+     */
+    void buildDtInfoGain(std::vector<Node>& hds,
+                         std::vector<Node> conds,
+                         std::map<Node, Node>& hd_mv,
+                         int ind);
+    /** computes the Shannon entropy of a set of heads
+     *
+     * The entropy depends on how many positive and negative heads are in the
+     * set and in their distribution. The polarity of the evaluation heads is
+     * queried from their model values in hd_mv.
+     *
+     * ind is the current level of indentation (for debugging)
+     */
+    double getEntropy(const std::vector<Node>& hds,
+                      std::map<Node, Node>& hd_mv,
+                      int ind);
+    /** evaluates a condition on a set of points
+     *
+     * The result is two sets of points: those on which the condition holds
+     * and those on which it does not
+     */
+    std::pair<std::vector<Node>, std::vector<Node>> evaluateCond(
+        std::vector<Node>& pts, Node cond);
     /** Classifies evaluation points according to enumerated condition values
      *
      * Maintains the invariant that points evaluated in the same way in the
@@ -296,10 +356,26 @@ class SygusUnifRl : public SygusUnif
       LazyTrieMulti d_trie;
       /** extracts solution from decision tree built */
       Node extractSol(Node cons, std::map<Node, Node>& hd_mv);
+      /** computes the result of applying cond on the respective point of hd
+       *
+       * If for example cond is (\lambda xy. x < y) and hd is an evaluation head
+       * in point (hd 0 1) this function will result in true, since
+       *   (\lambda xy. x < y) 0 1 evaluates to true
+       */
+      Node computeCond(Node cond, Node hd);
 
      private:
       /** reference to parent unif util */
       DecisionTreeInfo* d_dt;
+      /** cache of conditions evaluations on heads
+       *
+       * If for example cond is (\lambda xy. x < y) and hd is an evaluation head
+       * in point (hd 0 1), then after invoking computeCond(cond, hd) this map
+       * will contain d_eval_cond_hd[<cond, hd>] = true, since
+       *
+       *   (\lambda xy. x < y) 0 1 evaluates to true
+       */
+      std::map<std::pair<Node, Node>, Node> d_eval_cond_hd;
     };
     /**
      * Utility for determining how evaluation points are separated by currently
@@ -353,8 +429,8 @@ class SygusUnifRl : public SygusUnif
                                      unsigned strategy_index);
 };
 
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */