New module for synthesizing functions in a data-driven SyGuS approach (#1819)

8 files changed, 535 insertions, 0 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 289ed11d4..80bd082d6 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -459,6 +459,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/skolemize.h \
 	theory/quantifiers/sygus/cegis.cpp \
 	theory/quantifiers/sygus/cegis.h \
+	theory/quantifiers/sygus/cegis_unif.cpp \
+	theory/quantifiers/sygus/cegis_unif.h \
 	theory/quantifiers/sygus/ce_guided_conjecture.cpp \
 	theory/quantifiers/sygus/ce_guided_conjecture.h \
 	theory/quantifiers/sygus/ce_guided_instantiation.cpp \
@@ -487,6 +489,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus/sygus_unif.h \
 	theory/quantifiers/sygus/sygus_unif_io.cpp \
 	theory/quantifiers/sygus/sygus_unif_io.h \
+	theory/quantifiers/sygus/sygus_unif_rl.cpp \
+	theory/quantifiers/sygus/sygus_unif_rl.h \
 	theory/quantifiers/sygus/sygus_unif_strat.cpp \
 	theory/quantifiers/sygus/sygus_unif_strat.h \
 	theory/quantifiers/sygus/term_database_sygus.cpp \
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index b8ddd6d31..2f911bdd1 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -968,6 +968,14 @@ header = "options/quantifiers_options.h"
   help       = "sygus advanced pruning based on examples"
 
 [[option]]
+  name       = "sygusUnif"
+  category   = "regular"
+  long       = "sygus-unif"
+  type       = "bool"
+  default    = "false"
+  help       = "Unification-based function synthesis"
+
+[[option]]
   name       = "sygusQePreproc"
   category   = "regular"
   long       = "sygus-qe-preproc"
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 6914fc66f..db641a82e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -42,6 +42,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
       d_ceg_pbe(new CegConjecturePbe(qe, this)),
       d_ceg_cegis(new Cegis(qe, this)),
+      d_ceg_cegisUnif(new CegisUnif(qe, this)),
       d_master(nullptr),
       d_refine_count(0),
       d_syntax_guided(false)
@@ -50,6 +51,10 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
+  if (options::sygusUnif())
+  {
+    d_modules.push_back(d_ceg_cegisUnif.get());
+  }
   d_modules.push_back(d_ceg_cegis.get());
 }
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 5d7f082d8..97cc9df1e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/cegis.h"
+#include "theory/quantifiers/sygus/cegis_unif.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
@@ -141,6 +142,8 @@ private:
   std::unique_ptr<CegConjecturePbe> d_ceg_pbe;
   /** CEGIS module */
   std::unique_ptr<Cegis> d_ceg_cegis;
+  /** CEGIS UNIF module */
+  std::unique_ptr<CegisUnif> d_ceg_cegisUnif;
   /** the set of active modules (subset of the above list) */
   std::vector<SygusModule*> d_modules;
   /** master module
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
new file mode 100644
index 000000000..f7d970ddf
--- /dev/null
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -0,0 +1,240 @@
+/*********************                                                        */
+/*! \file cegis_unif.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief implementation of class for cegis with unification techniques
+ **/
+
+#include "theory/quantifiers/sygus/cegis_unif.h"
+
+#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus/sygus_unif_rl.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
+    : SygusModule(qe, p)
+{
+  d_tds = d_qe->getTermDatabaseSygus();
+}
+
+CegisUnif::~CegisUnif() {}
+bool CegisUnif::initialize(Node n,
+                           const std::vector<Node>& candidates,
+                           std::vector<Node>& lemmas)
+{
+  Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
+  Assert(candidates.size() > 0);
+  if (candidates.size() > 1)
+  {
+    return false;
+  }
+  d_candidate = candidates[0];
+  Trace("cegis-unif") << "Initialize unif utility for " << d_candidate
+                      << "...\n";
+  d_sygus_unif.initialize(d_qe, d_candidate, d_enums, lemmas);
+  Assert(!d_enums.empty());
+  Trace("cegis-unif") << "Initialize " << d_enums.size() << " enumerators for "
+                      << d_candidate << "...\n";
+  /* initialize the enumerators */
+  for (const Node& e : d_enums)
+  {
+    d_tds->registerEnumerator(e, d_candidate, d_parent, true);
+    Node g = d_tds->getActiveGuardForEnumerator(e);
+    d_enum_to_active_guard[e] = g;
+  }
+  return true;
+}
+
+void CegisUnif::getTermList(const std::vector<Node>& candidates,
+                            std::vector<Node>& terms)
+{
+  Assert(candidates.size() == 1);
+  Valuation& valuation = d_qe->getValuation();
+  for (const Node& e : d_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 if so, then there may
+       exist more values for it, and hence we add it to terms. */
+    Node gstatus = valuation.getSatValue(g);
+    if (!gstatus.isNull() && gstatus.getConst<bool>())
+    {
+      terms.push_back(e);
+    }
+  }
+}
+
+bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
+                                    const std::vector<Node>& enum_values,
+                                    const std::vector<Node>& candidates,
+                                    std::vector<Node>& candidate_values,
+                                    std::vector<Node>& lems)
+{
+  Assert(enums.size() == enum_values.size());
+  if (enums.empty())
+  {
+    return false;
+  }
+  unsigned min_term_size = 0;
+  std::vector<unsigned> enum_consider;
+  Trace("cegis-unif-enum") << "Register new enumerated values :\n";
+  for (unsigned i = 0, size = enums.size(); i < size; ++i)
+  {
+    Trace("cegis-unif-enum") << "  " << enums[i] << " -> " << enum_values[i]
+                             << 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;
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i)
+  {
+    unsigned j = enum_consider[i];
+    Node e = enums[j];
+    Node v = enum_values[j];
+    std::vector<Node> enum_lems;
+    d_sygus_unif.notifyEnumeration(e, v, enum_lems);
+    /* the lemmas must be guarded by the active guard of the enumerator */
+    Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
+    Node g = d_enum_to_active_guard[e];
+    for (unsigned j = 0, size = enum_lems.size(); j < size; ++j)
+    {
+      enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
+    }
+    lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
+  }
+  /* build candidate solution */
+  Assert(candidates.size() == 1);
+  Node vc = d_sygus_unif.constructSolution();
+  if (vc.isNull())
+  {
+    return false;
+  }
+  candidate_values.push_back(vc);
+  return true;
+}
+
+Node CegisUnif::purifyLemma(Node n,
+                            bool ensureConst,
+                            std::vector<Node>& model_guards,
+                            BoolNodePairMap& cache)
+{
+  Trace("cegis-unif-purify") << "PurifyLemma : " << n << "\n";
+  BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n));
+  if (it != cache.end())
+  {
+    Trace("cegis-unif-purify") << "... already visited " << n << "\n";
+    return it->second;
+  }
+  /* Recurse */
+  unsigned size = n.getNumChildren();
+  Kind k = n.getKind();
+  bool fapp = k == APPLY_UF && size > 0 && n[0] == d_candidate;
+  bool childChanged = false;
+  std::vector<Node> children;
+  for (unsigned i = 0; i < size; ++i)
+  {
+    if (i == 0 && fapp)
+    {
+      children.push_back(n[0]);
+      continue;
+    }
+    Node child = purifyLemma(n[i], ensureConst || fapp, model_guards, cache);
+    children.push_back(child);
+    childChanged = childChanged || child != n[i];
+  }
+  Node nb;
+  if (childChanged)
+  {
+    if (n.hasOperator())
+    {
+      children.insert(children.begin(), n.getOperator());
+    }
+    nb = NodeManager::currentNM()->mkNode(k, children);
+    Trace("cegis-unif-purify") << "PurifyLemma : transformed " << n << " into "
+                               << nb << "\n";
+  }
+  else
+  {
+    nb = n;
+  }
+  /* get model value of non-top level applications of d_candidate */
+  if (ensureConst && fapp)
+  {
+    Node nv = d_parent->getModelValue(nb);
+    Trace("cegis-unif-purify") << "PurifyLemma : model value for " << nb
+                               << " is " << nv << "\n";
+    /* test if different, then update model_guards */
+    if (nv != nb)
+    {
+      Trace("cegis-unif-purify") << "PurifyLemma : adding model eq\n";
+      model_guards.push_back(
+          NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate());
+      nb = nv;
+    }
+  }
+  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("cegis-unif-purify") << "... caching [" << n << "] = " << nb << "\n";
+  cache[BoolNodePair(ensureConst, n)] = nb;
+  return nb;
+}
+
+void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
+                                        Node lem,
+                                        std::vector<Node>& lems)
+{
+  Node plem;
+  std::vector<Node> model_guards;
+  BoolNodePairMap cache;
+  Trace("cegis-unif") << "Registering lemma at CegisUnif : " << lem << "\n";
+  /* Make the purified lemma which will guide the unification utility. */
+  plem = purifyLemma(lem, false, model_guards, cache);
+  if (!model_guards.empty())
+  {
+    model_guards.push_back(plem);
+    plem = NodeManager::currentNM()->mkNode(OR, model_guards);
+  }
+  plem = Rewriter::rewrite(plem);
+  Trace("cegis-unif") << "Purified lemma : " << plem << "\n";
+  d_refinement_lemmas.push_back(plem);
+  /* Notify lemma to unification utility */
+  d_sygus_unif.addRefLemma(plem);
+  /* Make the refinement lemma and add it to lems. This lemma is guarded by the
+     parent's guard, which has the semantics "this conjecture has a solution",
+     hence this lemma states: if the parent conjecture has a solution, it
+     satisfies the specification for the given concrete point. */
+  /* Store lemma for external modules */
+  lems.push_back(
+      NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem));
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
new file mode 100644
index 000000000..78586cd9c
--- /dev/null
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -0,0 +1,159 @@
+/*********************                                                        */
+/*! \file cegis_unif.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief cegis with unification techinques
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+
+#include <map>
+#include <vector>
+
+#include "theory/quantifiers/sygus/sygus_module.h"
+#include "theory/quantifiers/sygus/sygus_unif_rl.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+using BoolNodePair = std::pair<bool, Node>;
+using BoolNodePairHashFunction =
+    PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
+using BoolNodePairMap =
+    std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
+
+/** Synthesizes functions in a data-driven SyGuS approach
+ *
+ * Data is derived from refinement lemmas generated through the regular CEGIS
+ * approach. SyGuS is used to generate terms for classifying the data
+ * (e.g. using decision tree learning) and thus generate a candidate for a
+ * function-to-synthesize.
+ *
+ * This approach is inspired by the divide and conquer synthesis through
+ * unification approach by Alur et al. TACAS 2017, by ICE-based invariant
+ * synthesis from Garg et al. CAV 2014 and POPL 2016, and Padhi et al. PLDI 2016
+ *
+ * This module mantains a function-to-synthesize and a set of term
+ * enumerators. When new terms are enumerated it tries to learn a new candidate
+ * function, which is verified outside this module. If verification fails a
+ * refinement lemma is generated, which this module sends to the utility that
+ * learns candidates.
+ */
+class CegisUnif : public SygusModule
+{
+ public:
+  CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
+  ~CegisUnif();
+  /** initialize this class
+   *
+   * The module takes ownership of a conjecture when it contains a single
+   * function-to-synthesize
+  */
+  bool initialize(Node n,
+                  const std::vector<Node>& candidates,
+                  std::vector<Node>& lemmas) override;
+  /** adds the candidate itself to enums */
+  void getTermList(const std::vector<Node>& candidates,
+                   std::vector<Node>& enums) override;
+  /** Tries to build a new candidate solution with new enumerated expresion
+   *
+   * This function relies on a data-driven unification-based approach for
+   * constructing a solutions for the function-to-synthesize. See SygusUnifRl
+   * for more details.
+   *
+   * Calls to this function are such that terms is the list of active
+   * enumerators (returned by getTermList), and term_values are their current
+   * model values. This function registers { terms -> terms_values } in
+   * the database of values that have been enumerated, which are in turn used
+   * for constructing candidate solutions when possible.
+   *
+   * This function also excludes models where (terms = terms_values) by adding
+   * blocking clauses to lems. For example, for grammar:
+   *   A -> A+A | x | 1 | 0
+   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
+   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
+   * to lems, where G is active guard of the enumerator d (see
+   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
+   * indicates that d should not be given the model value +( x, 1 ) anymore,
+   * since { d -> +( x, 1 ) } has now been added to the database of this class.
+   */
+  bool constructCandidates(const std::vector<Node>& enums,
+                           const std::vector<Node>& enum_values,
+                           const std::vector<Node>& candidates,
+                           std::vector<Node>& candidate_values,
+                           std::vector<Node>& lems) override;
+
+  /** Communicate refinement lemma to unification utility and external modules
+   *
+   * For the lemma to be sent to the external modules it adds a guard from the
+   * parent conjecture which establishes that if the conjecture has a solution
+   * then it must satisfy this refinement lemma
+   *
+   * For the lemma to be sent to the unification utility it purifies the
+   * arguments of the function-to-synthensize such that all of its applications
+   * are over concrete values. E.g.:
+   *   f(f(f(0))) > 1
+   * becomes
+   *   f(0) != c1 v f(c1) != c2 v f(c2) > 1
+   * in which c1 and c2 are concrete integer values
+   *
+   * Note that the lemma is in the deep embedding, which means that the above
+   * example would actually correspond to
+   *   eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1
+   * in which d is the deep embedding of the function-to-synthesize f
+  */
+  void registerRefinementLemma(const std::vector<Node>& vars,
+                               Node lem,
+                               std::vector<Node>& lems) override;
+
+ private:
+  /** sygus term database of d_qe */
+  TermDbSygus* d_tds;
+  /**
+   * Sygus unif utility. This class implements the core algorithm (e.g. decision
+   * tree learning) that this module relies upon.
+   */
+  SygusUnifRl d_sygus_unif;
+  /* Function-to-synthesize (in deep embedding) */
+  Node d_candidate;
+  /**
+   * list of enumerators being used to build solutions for candidate by the
+   * above utility.
+   */
+  std::vector<Node> d_enums;
+  /** map from enumerators to active guards */
+  std::map<Node, Node> d_enum_to_active_guard;
+  /* list of learned refinement lemmas */
+  std::vector<Node> d_refinement_lemmas;
+  /**
+  * This is called on the refinement lemma and will replace the arguments of the
+  * function-to-synthesize by their model values (constants).
+  *
+  * When the traversal hits a function application of the function-to-synthesize
+  * it will proceed to ensure that the arguments of that function application
+  * are constants (the ensureConst becomes "true"). It populates a vector of
+  * guards with the (negated) equalities between the original arguments and
+  * their model values.
+  */
+  Node purifyLemma(Node n,
+                   bool ensureConst,
+                   std::vector<Node>& model_guards,
+                   BoolNodePairMap& cache);
+
+}; /* class CegisUnif */
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
new file mode 100644
index 000000000..bac46997d
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -0,0 +1,51 @@
+/*********************                                                        */
+/*! \file sygus_unif_rl.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_unif_rl
+ **/
+
+#include "theory/quantifiers/sygus/sygus_unif_rl.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusUnifRl::SygusUnifRl() {}
+
+SygusUnifRl::~SygusUnifRl() {}
+
+void SygusUnifRl::initialize(QuantifiersEngine* qe,
+                             Node f,
+                             std::vector<Node>& enums,
+                             std::vector<Node>& lemmas)
+{
+  SygusUnif::initialize(qe, f, enums, lemmas);
+}
+
+void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
+{
+}
+
+void SygusUnifRl::addRefLemma(Node lemma) {}
+
+void SygusUnifRl::initializeConstructSol() {}
+
+Node SygusUnifRl::constructSol(Node e, NodeRole nrole, int ind)
+{
+  return Node::null();
+}
+
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
new file mode 100644
index 000000000..8dc1906fb
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file sygus_unif_rl.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_unif_rl
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+
+#include <map>
+#include "theory/quantifiers/sygus/sygus_unif.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Sygus unification Refinement Lemmas utility
+ *
+ * This class implement synthesis-by-unification, where the specification is a
+ * set of refinement lemmas. With respect to SygusUnif, it's main interface
+ * function is addExample, which adds a refinement lemma to the specification.
+ */
+class SygusUnifRl : public SygusUnif
+{
+ public:
+  SygusUnifRl();
+  ~SygusUnifRl();
+
+  /** initialize */
+  void initialize(QuantifiersEngine* qe,
+                  Node f,
+                  std::vector<Node>& enums,
+                  std::vector<Node>& lemmas) override;
+  /** Notify enumeration */
+  void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
+  /** add refinement lemma
+   *
+   * This adds a lemma to the specification for f.
+   */
+  void addRefLemma(Node lemma);
+
+ protected:
+  /** set of refinmente lemmas */
+  std::vector<Node> d_refLemmas;
+  /** initialize construct solution */
+  void initializeConstructSol() override;
+  /** construct solution */
+  Node constructSol(Node e, NodeRole nrole, int ind) override;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */