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

6 files changed, 840 insertions, 42 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 01cf41518..a4fca6d3c 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -984,6 +984,14 @@ header = "options/quantifiers_options.h"
   help       = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
 
 [[option]]
+  name       = "sygusUnifBooleanHeuristicDt"
+  category   = "regular"
+  long       = "sygus-unif-boolean-heuristic-dt"
+  type       = "bool"
+  default    = "false"
+  help       = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
+
+[[option]]
   name       = "sygusUnifCondIndNoRepeatSol"
   category   = "regular"
   long       = "sygus-unif-cond-indpendent-no-repeat-sol"
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 */
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 8b690f3e1..45385f9c6 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1545,6 +1545,7 @@ REG1_TESTS = \
 	regress1/sygus/array_search_5-Q-easy.sy \
 	regress1/sygus/array_sum_2_5.sy \
 	regress1/sygus/bvudiv-by-2.sy \
+	regress1/sygus/car_3.lus.sy \
 	regress1/sygus/cegar1.sy \
 	regress1/sygus/cegis-unif-inv-eq-fair.sy \
 	regress1/sygus/cegisunif-depth1.sy \
diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy
new file mode 100755
index 000000000..b572622f7
--- /dev/null
+++ b/test/regress/regress1/sygus/car_3.lus.sy
@@ -0,0 +1,537 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt
+
+(set-logic LIA)
+
+(define-fun
+  __node_init_Sofar_0 (
+    (Sofar.usr.X_a_0 Bool)
+    (Sofar.usr.Sofar_a_0 Bool)
+    (Sofar.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and (= Sofar.usr.Sofar_a_0 Sofar.usr.X_a_0) Sofar.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_Sofar_0 (
+    (Sofar.usr.X_a_1 Bool)
+    (Sofar.usr.Sofar_a_1 Bool)
+    (Sofar.res.init_flag_a_1 Bool)
+    (Sofar.usr.X_a_0 Bool)
+    (Sofar.usr.Sofar_a_0 Bool)
+    (Sofar.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and
+   (= Sofar.usr.Sofar_a_1 (and Sofar.usr.X_a_1 Sofar.usr.Sofar_a_0))
+   (not Sofar.res.init_flag_a_1))
+)
+
+(define-fun
+  __node_init_excludes2_0 (
+    (excludes2.usr.X1_a_0 Bool)
+    (excludes2.usr.X2_a_0 Bool)
+    (excludes2.usr.excludes_a_0 Bool)
+    (excludes2.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and
+   (=
+    excludes2.usr.excludes_a_0
+    (not (and excludes2.usr.X1_a_0 excludes2.usr.X2_a_0)))
+   excludes2.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_excludes2_0 (
+    (excludes2.usr.X1_a_1 Bool)
+    (excludes2.usr.X2_a_1 Bool)
+    (excludes2.usr.excludes_a_1 Bool)
+    (excludes2.res.init_flag_a_1 Bool)
+    (excludes2.usr.X1_a_0 Bool)
+    (excludes2.usr.X2_a_0 Bool)
+    (excludes2.usr.excludes_a_0 Bool)
+    (excludes2.res.init_flag_a_0 Bool)
+  ) Bool
+
+  (and
+   (=
+    excludes2.usr.excludes_a_1
+    (not (and excludes2.usr.X1_a_1 excludes2.usr.X2_a_1)))
+   (not excludes2.res.init_flag_a_1))
+)
+
+(define-fun
+  __node_init_voiture_0 (
+    (voiture.usr.m_a_0 Bool)
+    (voiture.usr.s_a_0 Bool)
+    (voiture.usr.toofast_a_0 Bool)
+    (voiture.usr.stop_a_0 Bool)
+    (voiture.usr.bump_a_0 Bool)
+    (voiture.usr.dist_a_0 Int)
+    (voiture.usr.speed_a_0 Int)
+    (voiture.usr.time_a_0 Int)
+    (voiture.usr.move_a_0 Bool)
+    (voiture.usr.second_a_0 Bool)
+    (voiture.usr.meter_a_0 Bool)
+    (voiture.res.init_flag_a_0 Bool)
+    (voiture.res.abs_0_a_0 Bool)
+  ) Bool
+
+  (and
+   (= voiture.usr.speed_a_0 0)
+   (= voiture.usr.toofast_a_0 (>= voiture.usr.speed_a_0 3))
+   (= voiture.usr.move_a_0 true)
+   (= voiture.usr.time_a_0 0)
+   (= voiture.usr.dist_a_0 0)
+   (= voiture.usr.bump_a_0 (= voiture.usr.dist_a_0 10))
+   (= voiture.usr.stop_a_0 (>= voiture.usr.time_a_0 4))
+   (=
+    voiture.res.abs_0_a_0
+    (and
+     (and
+      (and voiture.usr.move_a_0 (not voiture.usr.stop_a_0))
+      (not voiture.usr.toofast_a_0))
+     (not voiture.usr.bump_a_0)))
+   (= voiture.usr.second_a_0 false)
+   (= voiture.usr.meter_a_0 false)
+   voiture.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_voiture_0 (
+    (voiture.usr.m_a_1 Bool)
+    (voiture.usr.s_a_1 Bool)
+    (voiture.usr.toofast_a_1 Bool)
+    (voiture.usr.stop_a_1 Bool)
+    (voiture.usr.bump_a_1 Bool)
+    (voiture.usr.dist_a_1 Int)
+    (voiture.usr.speed_a_1 Int)
+    (voiture.usr.time_a_1 Int)
+    (voiture.usr.move_a_1 Bool)
+    (voiture.usr.second_a_1 Bool)
+    (voiture.usr.meter_a_1 Bool)
+    (voiture.res.init_flag_a_1 Bool)
+    (voiture.res.abs_0_a_1 Bool)
+    (voiture.usr.m_a_0 Bool)
+    (voiture.usr.s_a_0 Bool)
+    (voiture.usr.toofast_a_0 Bool)
+    (voiture.usr.stop_a_0 Bool)
+    (voiture.usr.bump_a_0 Bool)
+    (voiture.usr.dist_a_0 Int)
+    (voiture.usr.speed_a_0 Int)
+    (voiture.usr.time_a_0 Int)
+    (voiture.usr.move_a_0 Bool)
+    (voiture.usr.second_a_0 Bool)
+    (voiture.usr.meter_a_0 Bool)
+    (voiture.res.init_flag_a_0 Bool)
+    (voiture.res.abs_0_a_0 Bool)
+  ) Bool
+
+  (and
+   (= voiture.usr.meter_a_1 (and voiture.usr.m_a_1 (not voiture.usr.s_a_1)))
+   (= voiture.usr.second_a_1 voiture.usr.s_a_1)
+   (= voiture.usr.move_a_1 voiture.res.abs_0_a_0)
+   (=
+    voiture.usr.speed_a_1
+    (ite
+     (or (not voiture.usr.move_a_1) voiture.usr.second_a_1)
+     0
+     (ite
+      (and voiture.usr.move_a_1 voiture.usr.meter_a_1)
+      (+ voiture.usr.speed_a_0 1)
+      voiture.usr.speed_a_0)))
+   (= voiture.usr.toofast_a_1 (>= voiture.usr.speed_a_1 3))
+   (=
+    voiture.usr.time_a_1
+    (ite voiture.usr.second_a_1 (+ voiture.usr.time_a_0 1) voiture.usr.time_a_0))
+   (=
+    voiture.usr.dist_a_1
+    (ite
+     (and voiture.usr.move_a_1 voiture.usr.meter_a_1)
+     (+ voiture.usr.dist_a_0 1)
+     voiture.usr.dist_a_0))
+   (= voiture.usr.bump_a_1 (= voiture.usr.dist_a_1 10))
+   (= voiture.usr.stop_a_1 (>= voiture.usr.time_a_1 4))
+   (=
+    voiture.res.abs_0_a_1
+    (and
+     (and
+      (and voiture.usr.move_a_1 (not voiture.usr.stop_a_1))
+      (not voiture.usr.toofast_a_1))
+     (not voiture.usr.bump_a_1)))
+   (not voiture.res.init_flag_a_1))
+)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.m_a_0 Bool)
+    (top.usr.s_a_0 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+    (top.res.abs_0_a_0 Bool)
+    (top.res.abs_1_a_0 Bool)
+    (top.res.abs_2_a_0 Bool)
+    (top.res.abs_3_a_0 Int)
+    (top.res.abs_4_a_0 Int)
+    (top.res.abs_5_a_0 Int)
+    (top.res.abs_6_a_0 Bool)
+    (top.res.abs_7_a_0 Bool)
+    (top.res.abs_8_a_0 Bool)
+    (top.res.abs_9_a_0 Bool)
+    (top.res.abs_10_a_0 Bool)
+    (top.res.inst_3_a_0 Bool)
+    (top.res.inst_2_a_0 Bool)
+    (top.res.inst_1_a_0 Bool)
+    (top.res.inst_0_a_0 Bool)
+  ) Bool
+
+  (let
+   ((X1 Bool top.res.abs_10_a_0))
+   (let
+    ((X2 Int top.res.abs_4_a_0))
+    (and
+     (= top.usr.OK_a_0 (=> X1 (< X2 4)))
+     (__node_init_voiture_0
+      top.usr.m_a_0
+      top.usr.s_a_0
+      top.res.abs_0_a_0
+      top.res.abs_1_a_0
+      top.res.abs_2_a_0
+      top.res.abs_3_a_0
+      top.res.abs_4_a_0
+      top.res.abs_5_a_0
+      top.res.abs_6_a_0
+      top.res.abs_7_a_0
+      top.res.abs_8_a_0
+      top.res.inst_3_a_0
+      top.res.inst_2_a_0)
+     (__node_init_Sofar_0 top.res.abs_9_a_0 top.res.abs_10_a_0 top.res.inst_1_a_0)
+     (__node_init_excludes2_0
+      top.usr.m_a_0
+      top.usr.s_a_0
+      top.res.abs_9_a_0
+      top.res.inst_0_a_0)
+     top.res.init_flag_a_0)))
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.m_a_1 Bool)
+    (top.usr.s_a_1 Bool)
+    (top.usr.OK_a_1 Bool)
+    (top.res.init_flag_a_1 Bool)
+    (top.res.abs_0_a_1 Bool)
+    (top.res.abs_1_a_1 Bool)
+    (top.res.abs_2_a_1 Bool)
+    (top.res.abs_3_a_1 Int)
+    (top.res.abs_4_a_1 Int)
+    (top.res.abs_5_a_1 Int)
+    (top.res.abs_6_a_1 Bool)
+    (top.res.abs_7_a_1 Bool)
+    (top.res.abs_8_a_1 Bool)
+    (top.res.abs_9_a_1 Bool)
+    (top.res.abs_10_a_1 Bool)
+    (top.res.inst_3_a_1 Bool)
+    (top.res.inst_2_a_1 Bool)
+    (top.res.inst_1_a_1 Bool)
+    (top.res.inst_0_a_1 Bool)
+    (top.usr.m_a_0 Bool)
+    (top.usr.s_a_0 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+    (top.res.abs_0_a_0 Bool)
+    (top.res.abs_1_a_0 Bool)
+    (top.res.abs_2_a_0 Bool)
+    (top.res.abs_3_a_0 Int)
+    (top.res.abs_4_a_0 Int)
+    (top.res.abs_5_a_0 Int)
+    (top.res.abs_6_a_0 Bool)
+    (top.res.abs_7_a_0 Bool)
+    (top.res.abs_8_a_0 Bool)
+    (top.res.abs_9_a_0 Bool)
+    (top.res.abs_10_a_0 Bool)
+    (top.res.inst_3_a_0 Bool)
+    (top.res.inst_2_a_0 Bool)
+    (top.res.inst_1_a_0 Bool)
+    (top.res.inst_0_a_0 Bool)
+  ) Bool
+
+  (let
+   ((X1 Bool top.res.abs_10_a_1))
+   (let
+    ((X2 Int top.res.abs_4_a_1))
+    (and
+     (= top.usr.OK_a_1 (=> X1 (< X2 4)))
+     (__node_trans_voiture_0
+      top.usr.m_a_1
+      top.usr.s_a_1
+      top.res.abs_0_a_1
+      top.res.abs_1_a_1
+      top.res.abs_2_a_1
+      top.res.abs_3_a_1
+      top.res.abs_4_a_1
+      top.res.abs_5_a_1
+      top.res.abs_6_a_1
+      top.res.abs_7_a_1
+      top.res.abs_8_a_1
+      top.res.inst_3_a_1
+      top.res.inst_2_a_1
+      top.usr.m_a_0
+      top.usr.s_a_0
+      top.res.abs_0_a_0
+      top.res.abs_1_a_0
+      top.res.abs_2_a_0
+      top.res.abs_3_a_0
+      top.res.abs_4_a_0
+      top.res.abs_5_a_0
+      top.res.abs_6_a_0
+      top.res.abs_7_a_0
+      top.res.abs_8_a_0
+      top.res.inst_3_a_0
+      top.res.inst_2_a_0)
+     (__node_trans_Sofar_0
+      top.res.abs_9_a_1
+      top.res.abs_10_a_1
+      top.res.inst_1_a_1
+      top.res.abs_9_a_0
+      top.res.abs_10_a_0
+      top.res.inst_1_a_0)
+     (__node_trans_excludes2_0
+      top.usr.m_a_1
+      top.usr.s_a_1
+      top.res.abs_9_a_1
+      top.res.inst_0_a_1
+      top.usr.m_a_0
+      top.usr.s_a_0
+      top.res.abs_9_a_0
+      top.res.inst_0_a_0)
+     (not top.res.init_flag_a_1))))
+)
+
+
+
+(synth-inv str_invariant(
+  (top.usr.m Bool)
+  (top.usr.s Bool)
+  (top.usr.OK Bool)
+  (top.res.init_flag Bool)
+  (top.res.abs_0 Bool)
+  (top.res.abs_1 Bool)
+  (top.res.abs_2 Bool)
+  (top.res.abs_3 Int)
+  (top.res.abs_4 Int)
+  (top.res.abs_5 Int)
+  (top.res.abs_6 Bool)
+  (top.res.abs_7 Bool)
+  (top.res.abs_8 Bool)
+  (top.res.abs_9 Bool)
+  (top.res.abs_10 Bool)
+  (top.res.inst_3 Bool)
+  (top.res.inst_2 Bool)
+  (top.res.inst_1 Bool)
+  (top.res.inst_0 Bool)
+))
+
+
+(declare-primed-var top.usr.m Bool)
+(declare-primed-var top.usr.s Bool)
+(declare-primed-var top.usr.OK Bool)
+(declare-primed-var top.res.init_flag Bool)
+(declare-primed-var top.res.abs_0 Bool)
+(declare-primed-var top.res.abs_1 Bool)
+(declare-primed-var top.res.abs_2 Bool)
+(declare-primed-var top.res.abs_3 Int)
+(declare-primed-var top.res.abs_4 Int)
+(declare-primed-var top.res.abs_5 Int)
+(declare-primed-var top.res.abs_6 Bool)
+(declare-primed-var top.res.abs_7 Bool)
+(declare-primed-var top.res.abs_8 Bool)
+(declare-primed-var top.res.abs_9 Bool)
+(declare-primed-var top.res.abs_10 Bool)
+(declare-primed-var top.res.inst_3 Bool)
+(declare-primed-var top.res.inst_2 Bool)
+(declare-primed-var top.res.inst_1 Bool)
+(declare-primed-var top.res.inst_0 Bool)
+
+(define-fun
+  init (
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+
+  (let
+   ((X1 Bool top.res.abs_10))
+   (let
+    ((X2 Int top.res.abs_4))
+    (and
+     (= top.usr.OK (=> X1 (< X2 4)))
+     (__node_init_voiture_0
+      top.usr.m
+      top.usr.s
+      top.res.abs_0
+      top.res.abs_1
+      top.res.abs_2
+      top.res.abs_3
+      top.res.abs_4
+      top.res.abs_5
+      top.res.abs_6
+      top.res.abs_7
+      top.res.abs_8
+      top.res.inst_3
+      top.res.inst_2)
+     (__node_init_Sofar_0 top.res.abs_9 top.res.abs_10 top.res.inst_1)
+     (__node_init_excludes2_0
+      top.usr.m
+      top.usr.s
+      top.res.abs_9
+      top.res.inst_0)
+     top.res.init_flag)))
+)
+
+(define-fun
+  trans (
+
+    ;; Current state.
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+
+    ;; Next state.
+    (top.usr.m! Bool)
+    (top.usr.s! Bool)
+    (top.usr.OK! Bool)
+    (top.res.init_flag! Bool)
+    (top.res.abs_0! Bool)
+    (top.res.abs_1! Bool)
+    (top.res.abs_2! Bool)
+    (top.res.abs_3! Int)
+    (top.res.abs_4! Int)
+    (top.res.abs_5! Int)
+    (top.res.abs_6! Bool)
+    (top.res.abs_7! Bool)
+    (top.res.abs_8! Bool)
+    (top.res.abs_9! Bool)
+    (top.res.abs_10! Bool)
+    (top.res.inst_3! Bool)
+    (top.res.inst_2! Bool)
+    (top.res.inst_1! Bool)
+    (top.res.inst_0! Bool)
+
+  ) Bool
+
+  (let
+   ((X1 Bool top.res.abs_10!))
+   (let
+    ((X2 Int top.res.abs_4!))
+    (and
+     (= top.usr.OK! (=> X1 (< X2 4)))
+     (__node_trans_voiture_0
+      top.usr.m!
+      top.usr.s!
+      top.res.abs_0!
+      top.res.abs_1!
+      top.res.abs_2!
+      top.res.abs_3!
+      top.res.abs_4!
+      top.res.abs_5!
+      top.res.abs_6!
+      top.res.abs_7!
+      top.res.abs_8!
+      top.res.inst_3!
+      top.res.inst_2!
+      top.usr.m
+      top.usr.s
+      top.res.abs_0
+      top.res.abs_1
+      top.res.abs_2
+      top.res.abs_3
+      top.res.abs_4
+      top.res.abs_5
+      top.res.abs_6
+      top.res.abs_7
+      top.res.abs_8
+      top.res.inst_3
+      top.res.inst_2)
+     (__node_trans_Sofar_0
+      top.res.abs_9!
+      top.res.abs_10!
+      top.res.inst_1!
+      top.res.abs_9
+      top.res.abs_10
+      top.res.inst_1)
+     (__node_trans_excludes2_0
+      top.usr.m!
+      top.usr.s!
+      top.res.abs_9!
+      top.res.inst_0!
+      top.usr.m
+      top.usr.s
+      top.res.abs_9
+      top.res.inst_0)
+     (not top.res.init_flag!))))
+)
+
+(define-fun
+  prop (
+    (top.usr.m Bool)
+    (top.usr.s Bool)
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    (top.res.abs_0 Bool)
+    (top.res.abs_1 Bool)
+    (top.res.abs_2 Bool)
+    (top.res.abs_3 Int)
+    (top.res.abs_4 Int)
+    (top.res.abs_5 Int)
+    (top.res.abs_6 Bool)
+    (top.res.abs_7 Bool)
+    (top.res.abs_8 Bool)
+    (top.res.abs_9 Bool)
+    (top.res.abs_10 Bool)
+    (top.res.inst_3 Bool)
+    (top.res.inst_2 Bool)
+    (top.res.inst_1 Bool)
+    (top.res.inst_0 Bool)
+  ) Bool
+
+  top.usr.OK
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)