Use sygus to synthesize/verify rewrite rules (#1547)

9 files changed, 733 insertions, 4 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index a6c58e281..4720186f4 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -465,6 +465,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus_grammar_norm.h \
 	theory/quantifiers/sygus_process_conj.cpp \
 	theory/quantifiers/sygus_process_conj.h \
+	theory/quantifiers/sygus_sampler.cpp \
+	theory/quantifiers/sygus_sampler.h \
 	theory/quantifiers/symmetry_breaking.cpp \
 	theory/quantifiers/symmetry_breaking.h \
 	theory/quantifiers/term_database.cpp \
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index c6eb1cd5e..9d717c0ba 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -295,9 +295,17 @@ option sygusCRefEval --sygus-cref-eval bool :default true
 option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true
   use min explain for direct evaluation of refinement lemmas for conflict analysis
   
-option sygusStream --sygus-stream bool :default false
+option sygusStream --sygus-stream bool :read-write :default false
   enumerate a stream of solutions instead of terminating after the first one
   
+# internal uses of sygus
+option sygusRewSynth --sygus-rr-synth bool :default false
+  use sygus to enumerate candidate rewrite rules via sampling
+option sygusRewVerify --sygus-rr-verify bool :default false
+  use sygus to verify the correctness of rewrite rules via sampling
+option sygusSamples --sygus-samples=N int :read-write :default 100 :read-write
+  number of points to consider when doing sygus rewriter sample testing
+
 # CEGQI applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 11c226ee4..0c8723ff6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1885,6 +1885,11 @@ void SmtEngine::setDefaults() {
     if( !options::instNoEntail.wasSetByUser() ){
       options::instNoEntail.set( false );
     }
+    if (options::sygusRewSynth())
+    {
+      // rewrite rule synthesis implies that sygus stream must be true
+      options::sygusStream.set(true);
+    }
     if (options::sygusStream())
     {
       // PBE and streaming modes are incompatible
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index b06c96e68..7c3ab71d8 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -808,7 +808,38 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
           Trace("sygus-sb-exc") << "  ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl;
         } 
       }
-      
+
+      if (options::sygusRewVerify())
+      {
+        // add to the sampler database object
+        std::map<Node, quantifiers::SygusSampler>::iterator its =
+            d_sampler.find(a);
+        if (its == d_sampler.end())
+        {
+          d_sampler[a].initialize(d_tds, a, options::sygusSamples());
+          its = d_sampler.find(a);
+        }
+        Node sample_ret = its->second.registerTerm(bv);
+        d_cache[a].d_search_val_sample[nv] = sample_ret;
+        if (itsv != d_cache[a].d_search_val[tn].end())
+        {
+          // if the analog of this term and another term were rewritten to the
+          // same term, then they should be equivalent under examples.
+          Node prev = itsv->second;
+          Node prev_sample_ret = d_cache[a].d_search_val_sample[prev];
+          if (sample_ret != prev_sample_ret)
+          {
+            Node prev_bv = d_tds->sygusToBuiltin(prev, tn);
+            // we have detected unsoundness in the rewriter
+            Options& nodeManagerOptions =
+                NodeManager::currentNM()->getOptions();
+            std::ostream* out = nodeManagerOptions.getOut();
+            (*out) << "(unsound-rewrite " << prev_bv << " " << bv << ")"
+                   << std::endl;
+          }
+        }
+      }
+
       if( !bad_val_bvr.isNull() ){
         Node bad_val = nv;
         Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr];
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 099b45fec..1162f767f 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -30,6 +30,7 @@
 #include "expr/datatype.h"
 #include "expr/node.h"
 #include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers/term_database.h"
 
 namespace CVC4 {
@@ -80,14 +81,34 @@ private:
     SearchCache(){}
     std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms;
     std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_sb_lemmas;
-    // search values
+    /** search value
+     *
+     * For each sygus type, a map from a builtin term to a sygus term for that
+     * type that we encountered during the search whose analog rewrites to that
+     * term. The range of this map can be updated if we later encounter a sygus
+     * term that also rewrites to the builtin value but has a smaller term size.
+     */
     std::map< TypeNode, std::map< Node, Node > > d_search_val;
+    /** the size of terms in the range of d_search val. */
     std::map< TypeNode, std::map< Node, unsigned > > d_search_val_sz;
-    std::map< TypeNode, std::map< Node, Node > > d_search_val_b;
+    /** search value sample
+     *
+     * This is used for the sygusRewVerify() option. For each sygus term we
+     * register in this cache, this stores the value returned by calling
+     * SygusSample::registerTerm(...) on its analog.
+     */
+    std::map<Node, Node> d_search_val_sample;
+    /** For each term, whether this cache has processed that term */
     std::map< Node, bool > d_search_val_proc;
   };
   // anchor -> cache
   std::map< Node, SearchCache > d_cache;
+  /** a sygus sampler object for each anchor
+   *
+   * This is used for the sygusRewVerify() option to verify the correctness of
+   * the rewriter.
+   */
+  std::map<Node, quantifiers::SygusSampler> d_sampler;
   Node d_null;
   void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas );
   // register search term
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 378b26eef..74d5cef47 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -435,6 +435,12 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >&
       std::stringstream ss;
       Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
       Trace("cegqi-engine") << ss.str() << " ";
+      if (Trace.isOn("cegqi-engine-rr"))
+      {
+        Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn);
+        bv = Rewriter::rewrite(bv);
+        Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+      }
     }
     Assert( !nv.isNull() );
   }
@@ -628,6 +634,63 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
       }
       out << ")" << std::endl;
+
+      if (status != 0 && options::sygusRewSynth())
+      {
+        TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+        std::map<Node, SygusSampler>::iterator its = d_sampler.find(prog);
+        if (its == d_sampler.end())
+        {
+          d_sampler[prog].initialize(sygusDb, prog, options::sygusSamples());
+          its = d_sampler.find(prog);
+        }
+        Node solb = sygusDb->sygusToBuiltin(sol, prog.getType());
+        Node eq_sol = its->second.registerTerm(solb);
+        // eq_sol is a candidate solution that is equivalent to sol
+        if (eq_sol != solb)
+        {
+          // one of eq_sol or solb must be ordered
+          bool eqor = its->second.isOrdered(eq_sol);
+          bool sor = its->second.isOrdered(solb);
+          bool outputRewrite = false;
+          if (eqor || sor)
+          {
+            outputRewrite = true;
+            // if only one is ordered, then the ordered one must contain the
+            // free variables of the other
+            if (!eqor)
+            {
+              outputRewrite = its->second.containsFreeVariables(solb, eq_sol);
+            }
+            else if (!sor)
+            {
+              outputRewrite = its->second.containsFreeVariables(eq_sol, solb);
+            }
+          }
+
+          if (outputRewrite)
+          {
+            // Terms solb and eq_sol are equivalent under sample points but do
+            // not rewrite to the same term. Hence, this indicates a candidate
+            // rewrite.
+            out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
+                << std::endl;
+            // if the previous value stored was unordered, but this is
+            // ordered, we prefer this one. Thus, we force its addition to the
+            // sampler database.
+            if (!eqor)
+            {
+              its->second.registerTerm(solb, true);
+            }
+          }
+          else
+          {
+            Trace("sygus-synth-rr")
+                << "Alpha equivalent candidate rewrite : " << eq_sol << " "
+                << solb << std::endl;
+          }
+        }
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index 0f000bba5..e57b545e6 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus_process_conj.h"
+#include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -197,6 +198,12 @@ private:
   /** the guard for non-syntax-guided synthesis */
   Node d_nsg_guard;
   //-------------------------------- end non-syntax guided (deprecated)
+  /** sygus sampler objects for each program variable
+   *
+   * This is used for the sygusRewSynth() option to synthesize new candidate
+   * rewrite rules.
+   */
+  std::map<Node, SygusSampler> d_sampler;
 };
 
 } /* namespace CVC4::theory::quantifiers */
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
new file mode 100644
index 000000000..b5e63a6ab
--- /dev/null
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -0,0 +1,355 @@
+/*********************                                                        */
+/*! \file sygus_sampler.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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_sampler
+ **/
+
+#include "theory/quantifiers/sygus_sampler.h"
+
+#include "util/bitvector.h"
+#include "util/random.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Node LazyTrie::add(Node n,
+                   LazyTrieEvaluator* ev,
+                   unsigned index,
+                   unsigned ntotal,
+                   bool forceKeep)
+{
+  LazyTrie* lt = this;
+  while (lt != NULL)
+  {
+    if (index == ntotal)
+    {
+      // lazy child holds the leaf data
+      if (lt->d_lazy_child.isNull() || forceKeep)
+      {
+        lt->d_lazy_child = n;
+      }
+      return lt->d_lazy_child;
+    }
+    std::vector<Node> ex;
+    if (lt->d_children.empty())
+    {
+      if (lt->d_lazy_child.isNull())
+      {
+        // no one has been here, we are done
+        lt->d_lazy_child = n;
+        return lt->d_lazy_child;
+      }
+      // evaluate the lazy child
+      Node e_lc = ev->evaluate(lt->d_lazy_child, index);
+      // store at next level
+      lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
+      // replace
+      lt->d_lazy_child = Node::null();
+    }
+    // recurse
+    Node e = ev->evaluate(n, index);
+    lt = &lt->d_children[e];
+    index = index + 1;
+  }
+  return Node::null();
+}
+
+SygusSampler::SygusSampler() : d_tds(nullptr), d_is_valid(false) {}
+
+void SygusSampler::initialize(TermDbSygus* tds, Node f, unsigned nsamples)
+{
+  d_tds = tds;
+  d_is_valid = true;
+  d_ftn = f.getType();
+  Assert(d_ftn.isDatatype());
+  const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
+  Assert(dt.isSygus());
+
+  Trace("sygus-sample") << "Register sampler for " << f << std::endl;
+
+  d_var_index.clear();
+  d_type_vars.clear();
+  std::vector<TypeNode> types;
+  // get the sygus variable list
+  Node var_list = Node::fromExpr(dt.getSygusVarList());
+  if (!var_list.isNull())
+  {
+    for (const Node& sv : var_list)
+    {
+      TypeNode svt = sv.getType();
+      d_var_index[sv] = d_type_vars[svt].size();
+      d_type_vars[svt].push_back(sv);
+      types.push_back(svt);
+      Trace("sygus-sample") << "  var #" << types.size() << " : " << sv << " : "
+                            << svt << std::endl;
+    }
+  }
+
+  d_samples.clear();
+  for (unsigned i = 0; i < nsamples; i++)
+  {
+    std::vector<Node> sample_pt;
+    Trace("sygus-sample") << "Sample point #" << i << " : ";
+    for (unsigned j = 0, size = types.size(); j < size; j++)
+    {
+      Node r = getRandomValue(types[j]);
+      if (r.isNull())
+      {
+        Trace("sygus-sample") << "INVALID";
+        d_is_valid = false;
+      }
+      Trace("sygus-sample") << r << " ";
+      sample_pt.push_back(r);
+    }
+    Trace("sygus-sample") << std::endl;
+    d_samples.push_back(sample_pt);
+  }
+
+  d_trie.clear();
+}
+
+Node SygusSampler::registerTerm(Node n, bool forceKeep)
+{
+  if (d_is_valid)
+  {
+    return d_trie.add(n, this, 0, d_samples.size(), forceKeep);
+  }
+  return n;
+}
+
+bool SygusSampler::isContiguous(Node n)
+{
+  // compute free variables in n
+  std::vector<Node> fvs;
+  computeFreeVariables(n, fvs);
+  // compute contiguous condition
+  for (const std::pair<const TypeNode, std::vector<Node> >& p : d_type_vars)
+  {
+    bool foundNotFv = false;
+    for (const Node& v : p.second)
+    {
+      bool hasFv = std::find(fvs.begin(), fvs.end(), v) != fvs.end();
+      if (!hasFv)
+      {
+        foundNotFv = true;
+      }
+      else if (foundNotFv)
+      {
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar())
+      {
+        if (d_var_index.find(cur) != d_var_index.end())
+        {
+          fvs.push_back(cur);
+        }
+      }
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+  } while (!visit.empty());
+}
+
+bool SygusSampler::isOrdered(Node n)
+{
+  // compute free variables in n for each type
+  std::map<TypeNode, std::vector<Node> > fvs;
+
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar())
+      {
+        std::map<Node, unsigned>::iterator itv = d_var_index.find(cur);
+        if (itv != d_var_index.end())
+        {
+          TypeNode tn = cur.getType();
+          // if this variable is out of order
+          if (itv->second != fvs[tn].size())
+          {
+            return false;
+          }
+          fvs[tn].push_back(cur);
+        }
+      }
+      for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++)
+      {
+        visit.push_back(cur[(nchildren - j) - 1]);
+      }
+    }
+  } while (!visit.empty());
+  return true;
+}
+
+bool SygusSampler::containsFreeVariables(Node a, Node b)
+{
+  // compute free variables in a
+  std::vector<Node> fvs;
+  computeFreeVariables(a, fvs);
+
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(b);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar())
+      {
+        if (std::find(fvs.begin(), fvs.end(), cur) == fvs.end())
+        {
+          return false;
+        }
+      }
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+  } while (!visit.empty());
+  return true;
+}
+
+Node SygusSampler::evaluate(Node n, unsigned index)
+{
+  Assert(index < d_samples.size());
+  Node ev = d_tds->evaluateBuiltin(d_ftn, n, d_samples[index]);
+  Trace("sygus-sample-ev") << "( " << n << ", " << index << " ) -> " << ev
+                           << std::endl;
+  return ev;
+}
+
+Node SygusSampler::getRandomValue(TypeNode tn)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (tn.isBoolean())
+  {
+    return nm->mkConst(Random::getRandom().pickWithProb(0.5));
+  }
+  else if (tn.isBitVector())
+  {
+    unsigned sz = tn.getBitVectorSize();
+    std::stringstream ss;
+    for (unsigned i = 0; i < sz; i++)
+    {
+      ss << (Random::getRandom().pickWithProb(0.5) ? "1" : "0");
+    }
+    return nm->mkConst(BitVector(ss.str(), 2));
+  }
+  else if (tn.isString() || tn.isInteger())
+  {
+    std::vector<unsigned> vec;
+    double ext_freq = .5;
+    unsigned base = 10;
+    while (Random::getRandom().pickWithProb(ext_freq))
+    {
+      // add a digit
+      vec.push_back(Random::getRandom().pick(0, base));
+    }
+    if (tn.isString())
+    {
+      return nm->mkConst(String(vec));
+    }
+    else if (tn.isInteger())
+    {
+      Rational baser(base);
+      Rational curr(1);
+      std::vector<Node> sum;
+      for (unsigned j = 0, size = vec.size(); j < size; j++)
+      {
+        Node digit = nm->mkConst(Rational(vec[j]) * curr);
+        sum.push_back(digit);
+        curr = curr * baser;
+      }
+      Node ret;
+      if (sum.empty())
+      {
+        ret = nm->mkConst(Rational(0));
+      }
+      else if (sum.size() == 1)
+      {
+        ret = sum[0];
+      }
+      else
+      {
+        ret = nm->mkNode(kind::PLUS, sum);
+      }
+
+      if (Random::getRandom().pickWithProb(0.5))
+      {
+        // negative
+        ret = nm->mkNode(kind::UMINUS, ret);
+      }
+      ret = Rewriter::rewrite(ret);
+      Assert(ret.isConst());
+      return ret;
+    }
+  }
+  else if (tn.isReal())
+  {
+    Node s = getRandomValue(nm->integerType());
+    Node r = getRandomValue(nm->integerType());
+    if (!s.isNull() && !r.isNull())
+    {
+      Rational sr = s.getConst<Rational>();
+      Rational rr = s.getConst<Rational>();
+      if (rr.sgn() == 0)
+      {
+        return s;
+      }
+      else
+      {
+        return nm->mkConst(sr / rr);
+      }
+    }
+  }
+  return Node::null();
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
new file mode 100644
index 000000000..897931649
--- /dev/null
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -0,0 +1,237 @@
+/*********************                                                        */
+/*! \file sygus_sampler.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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_sampler
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+
+#include <map>
+#include "theory/quantifiers/term_database_sygus.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** abstract evaluator class
+ *
+ * This class is used for the LazyTrie data structure below.
+ */
+class LazyTrieEvaluator
+{
+ public:
+  virtual Node evaluate(Node n, unsigned index) = 0;
+};
+
+/** LazyTrie
+ *
+ * This is a trie where terms are added in a lazy fashion. This data structure
+ * is useful, for instance, when we are only interested in when two terms
+ * map to the same node in the trie but we need not care about computing
+ * exactly where they are.
+ *
+ * In other words, when a term n is added to this trie, we do not insist
+ * that n is placed at the maximal depth of the trie. Instead, we place n at a
+ * minimal depth node that has no children. In this case we say n is partially
+ * evaluated in this trie.
+ *
+ * This class relies on an abstract evaluator interface above, which evaluates
+ * nodes for indices.
+ *
+ * For example, say we have terms a, b, c and an evaluator ev where:
+ *   ev->evaluate( a, 0,1,2 ) = 0, 5, 6
+ *   ev->evaluate( b, 0,1,2 ) = 1, 3, 0
+ *   ev->evaluate( c, 0,1,2 ) = 1, 3, 2
+ * After adding a to the trie, we get:
+ *   root: a
+ * After adding b to the resulting trie, we get:
+ *   root: null
+ *     d_children[0]: a
+ *     d_children[1]: b
+ * After adding c to the resulting trie, we get:
+ *   root: null
+ *     d_children[0]: a
+ *     d_children[1]: null
+ *       d_children[3]: null
+ *         d_children[0] : b
+ *         d_children[2] : c
+ * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
+ */
+class LazyTrie
+{
+ public:
+  LazyTrie() {}
+  ~LazyTrie() {}
+  /** the data at this node, which may be partially evaluated */
+  Node d_lazy_child;
+  /** the children of this node */
+  std::map<Node, LazyTrie> d_children;
+  /** clear the trie */
+  void clear() { d_children.clear(); }
+  /** add n to the trie
+   *
+   * This function returns a node that is mapped to the same node in the trie
+   * if one exists, or n otherwise.
+   *
+   * ev is an evaluator which determines where n is placed in the trie
+   * index is the depth of this node
+   * ntotal is the maximal depth of the trie
+   * forceKeep is whether we wish to force that n is chosen as a representative
+   */
+  Node add(Node n,
+           LazyTrieEvaluator* ev,
+           unsigned index,
+           unsigned ntotal,
+           bool forceKeep);
+};
+
+/** SygusSampler
+ *
+ * This class can be used to test whether two expressions are equivalent
+ * by random sampling. We use this class for the following options:
+ *
+ * sygus-rr-synth: synthesize candidate rewrite rules by finding two terms
+ * t1 and t2 do not rewrite to the same term, but are identical when considering
+ * a set of sample points, and
+ *
+ * sygus-rr-verify: detect unsound rewrite rules by finding two terms t1 and
+ * t2 that rewrite to the same term, but not identical when considering a set
+ * of sample points.
+ *
+ * To use this class:
+ * (1) Call initialize( tds, f, nsamples) where f is sygus datatype term.
+ * (2) For terms n1....nm enumerated that correspond to builtin analog of sygus
+ * term f, we call registerTerm( n1 )....registerTerm( nm ). It may be the case
+ * that registerTerm( ni ) returns nj for some j < i. In this case, we have that
+ * ni and nj are equivalent under the sample points in this class.
+ *
+ * For example, say the grammar for f is:
+ *   A = 0 | 1 | x | y | A+A | ite( B, A, A )
+ *   B = A <= A
+ * If we call intialize( tds, f, 5 ), this class will generate 5 random sample
+ * points for (x,y), say (0,0), (1,1), (0,1), (1,0), (2,2). The return values
+ * of successive calls to registerTerm are listed below.
+ *   registerTerm( 0 ) -> 0
+ *   registerTerm( x ) -> x
+ *   registerTerm( x+y ) -> x+y
+ *   registerTerm( y+x ) -> x+y
+ *   registerTerm( x+ite(x <= 1+1, 0, y ) ) -> x
+ * Notice that the number of sample points can be configured for the above
+ * options using sygus-samples=N.
+ */
+class SygusSampler : public LazyTrieEvaluator
+{
+ public:
+  SygusSampler();
+  virtual ~SygusSampler() {}
+  /** initialize
+   *
+   * tds : reference to a sygus database,
+   * f : a term of some SyGuS datatype type whose (builtin) values we will be
+   * testing,
+   * nsamples : number of sample points this class will test.
+   */
+  void initialize(TermDbSygus* tds, Node f, unsigned nsamples);
+  /** register term n with this sampler database
+   *
+   * forceKeep is whether we wish to force that n is chosen as a representative
+   * value in the trie.
+   */
+  Node registerTerm(Node n, bool forceKeep = false);
+  /** is contiguous
+   *
+   * This returns whether n's free variables (terms occurring in the range of
+   * d_type_vars) are a prefix of the list of variables in d_type_vars for each
+   * type. For instance, if d_type_vars[Int] = { x, y }, then 0, x, x+y, y+x are
+   * contiguous but y is not. This is useful for excluding terms from
+   * consideration that are alpha-equivalent to others.
+   */
+  bool isContiguous(Node n);
+  /** is ordered
+   *
+   * This returns whether n's free variables are in order with respect to
+   * variables in d_type_vars for each type. For instance, if
+   * d_type_vars[Int] = { x, y }, then 0, x, x+y are ordered but y and y+x
+   * are not.
+   */
+  bool isOrdered(Node n);
+  /** contains free variables
+   *
+   * Returns true if all free variables of a are contained in b. Free variables
+   * are those that occur in the range d_type_vars.
+   */
+  bool containsFreeVariables(Node a, Node b);
+  /** evaluate n on sample point index */
+  Node evaluate(Node n, unsigned index);
+
+ private:
+  /** sygus term database of d_qe */
+  TermDbSygus* d_tds;
+  /** samples */
+  std::vector<std::vector<Node> > d_samples;
+  /** type of nodes we will be registering with this class */
+  TypeNode d_ftn;
+  /** type variables
+   *
+   * For each type, a list of variables in the grammar we are considering, for
+   * that type. These typically correspond to the arguments of the
+   * function-to-synthesize whose grammar we are considering.
+   */
+  std::map<TypeNode, std::vector<Node> > d_type_vars;
+  /**
+   * A map all variables in the grammar we are considering to their index in
+   * d_type_vars.
+   */
+  std::map<Node, unsigned> d_var_index;
+  /** constants
+   *
+   * For each type, a list of constants in the grammar we are considering, for
+   * that type.
+   */
+  std::map<TypeNode, std::vector<Node> > d_type_consts;
+  /** the lazy trie */
+  LazyTrie d_trie;
+  /** is this sampler valid?
+   *
+   * A sampler can be invalid if sample points cannot be generated for a type
+   * of an argument to function f.
+   */
+  bool d_is_valid;
+  /**
+   * Compute the variables from the domain of d_var_index that occur in n,
+   * store these in the vector fvs.
+   */
+  void computeFreeVariables(Node n, std::vector<Node>& fvs);
+  /** get random value for a type
+   *
+   * Returns a random value for the given type based on the random number
+   * generator. Currently, supported types:
+   *
+   * Bool, Bitvector : returns a random value in the range of that type.
+   * Int, String : returns a random string of values in (base 10) of random
+   * length, currently by a repeated coin flip.
+   * Real : returns the division of two random integers, where the denominator
+   * is omitted if it is zero.
+   *
+   * TODO (#1549): improve this function. Can use the grammar to generate
+   * interesting sample points.
+   */
+  Node getRandomValue(TypeNode tn);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */