Use example evaluation cache instead of sygus PBE (#3733)

11 files changed, 125 insertions, 598 deletions

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 890b8b2b9..1e593a664 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1054,16 +1054,16 @@ Node SygusExtension::registerSearchValue(Node a,
       Node bad_val_bvr;
       bool by_examples = false;
       if( itsv==d_cache[a].d_search_val[tn].end() ){
-        // TODO (github #1210) conjecture-specific symmetry breaking
-        // this should be generalized and encapsulated within the
-        // SynthConjecture class.
         // Is it equivalent under examples?
         Node bvr_equiv;
         if (options::sygusSymBreakPbe())
         {
-          if (aconj->getPbe()->hasExamples(a))
+          // If the enumerator has examples, see if it is equivalent up to its
+          // examples with a previous term.
+          quantifiers::ExampleEvalCache* eec = aconj->getExampleEvalCache(a);
+          if (eec != nullptr)
           {
-            bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr);
+            bvr_equiv = eec->addSearchVal(bvr);
           }
         }
         if( !bvr_equiv.isNull() ){
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index f7d0e7b7e..3ef3a3edc 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -17,6 +17,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "theory/quantifiers/sygus/example_min_eval.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers_engine.h"
@@ -143,30 +144,36 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
                                     : "")
                           << "..." << std::endl;
     // see if any refinement lemma is refuted by evaluation
-    std::vector<Node> cre_lems;
-    bool ret =
-        getRefinementEvalLemmas(candidates, candidate_values, cre_lems, doGen);
-    if (ret && !doGen)
+    if (doGen)
     {
-      Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
-                               "refinement lemma evaluation."
-                            << std::endl;
-      return true;
-    }
-    if (!cre_lems.empty())
-    {
-      lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
-      addedEvalLemmas = true;
-      if (Trace.isOn("cegqi-lemma"))
+      std::vector<Node> cre_lems;
+      getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
+      if (!cre_lems.empty())
       {
-        for (const Node& lem : cre_lems)
+        lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
+        addedEvalLemmas = true;
+        if (Trace.isOn("cegqi-lemma"))
         {
-          Trace("cegqi-lemma")
-              << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
+          for (const Node& lem : cre_lems)
+          {
+            Trace("cegqi-lemma")
+                << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
+          }
         }
+        /* we could, but do not return here. experimentally, it is better to
+          add the lemmas below as well, in parallel. */
+      }
+    }
+    else
+    {
+      // just check whether the refinement lemmas are satisfied, fail if not
+      if (checkRefinementEvalLemmas(candidates, candidate_values))
+      {
+        Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
+                                 "refinement lemma evaluation."
+                              << std::endl;
+        return true;
       }
-      /* we could, but do not return here. experimentally, it is better to
-         add the lemmas below as well, in parallel. */
     }
   }
   // we only do evaluation unfolding for passive enumerators
@@ -481,8 +488,7 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
 bool Cegis::usingRepairConst() { return true; }
 bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
                                     const std::vector<Node>& ms,
-                                    std::vector<Node>& lems,
-                                    bool doGen)
+                                    std::vector<Node>& lems)
 {
   Trace("sygus-cref-eval") << "Cref eval : conjecture has "
                            << d_refinement_lemma_unit.size() << " unit and "
@@ -496,6 +502,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
   Node nfalse = nm->mkConst(false);
   Node neg_guard = d_parent->getGuard().negate();
   bool ret = false;
+
   for (unsigned r = 0; r < 2; r++)
   {
     std::unordered_set<Node, NodeHashFunction>& rlemmas =
@@ -519,11 +526,6 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
           << "...after unfolding is : " << lemcsu << std::endl;
       if (lemcsu.isConst() && !lemcsu.getConst<bool>())
       {
-        if (!doGen)
-        {
-          // we are not generating the lemmas, instead just return
-          return true;
-        }
         ret = true;
         std::vector<Node> msu;
         std::vector<Node> mexp;
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 2c21257b9..bebb91fa3 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -185,13 +185,11 @@ class Cegis : public SygusModule
    * to lems based on evaluating the conjecture, instantiated for ms, on lemmas
    * for previous refinements (d_refinement_lemmas).
    *
-   * Returns true if any such lemma exists. If doGen is false, then the
-   * lemmas are not generated or added to lems.
+   * Returns true if any such lemma exists.
    */
   bool getRefinementEvalLemmas(const std::vector<Node>& vs,
                                const std::vector<Node>& ms,
-                               std::vector<Node>& lems,
-                               bool doGen);
+                               std::vector<Node>& lems);
   /** Check refinement evaluation lemmas
    *
    * This method is similar to above, but does not perform any generalization
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp
index a7dd59900..2a43335d7 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.cpp
+++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp
@@ -51,17 +51,17 @@ Node ExampleEvalCache::addSearchVal(Node bv)
     return Node::null();
   }
   std::vector<Node> vals;
-  evaluateVec(bv, vals, false);
+  evaluateVec(bv, vals, true);
   Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
   Node ret = d_trie.addOrGetTerm(bv, vals);
   Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
   // Only save the cache data if necessary: if the enumerated term
   // is redundant, its cached data will not be used later and thus should
-  // be discarded.
-  if (ret == bv)
+  // be discarded. This applies also to the case where the evaluation
+  // was cached prior to this call.
+  if (ret != bv)
   {
-    std::vector<Node>& eocv = d_exOutCache[bv];
-    eocv.insert(eocv.end(), vals.begin(), vals.end());
+    clearEvaluationCache(bv);
   }
   Assert(ret.getType().isComparableTo(bv.getType()));
   return ret;
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 99f8eee2c..63a61b818 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -17,6 +17,7 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
 
 using namespace CVC4::kind;
 
@@ -143,7 +144,7 @@ Node SygusEnumerator::getCurrent()
 
 SygusEnumerator::TermCache::TermCache()
     : d_tds(nullptr),
-      d_pbe(nullptr),
+      d_eec(nullptr),
       d_isSygusType(false),
       d_numConClasses(0),
       d_sizeEnum(0),
@@ -151,15 +152,19 @@ SygusEnumerator::TermCache::TermCache()
       d_sampleRrVInit(false)
 {
 }
-void SygusEnumerator::TermCache::initialize(
-    SygusStatistics* s, Node e, TypeNode tn, TermDbSygus* tds, SygusPbe* pbe)
+
+void SygusEnumerator::TermCache::initialize(SygusStatistics* s,
+                                            Node e,
+                                            TypeNode tn,
+                                            TermDbSygus* tds,
+                                            ExampleEvalCache* eec)
 {
   Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
   d_stats = s;
   d_enum = e;
   d_tn = tn;
   d_tds = tds;
-  d_pbe = pbe;
+  d_eec = eec;
   d_sizeStartIndex[0] = 0;
   d_isSygusType = false;
 
@@ -334,11 +339,11 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
       return false;
     }
     // if we are doing PBE symmetry breaking
-    if (d_pbe != nullptr)
+    if (d_eec != nullptr)
     {
       ++(d_stats->d_enumTermsExampleEval);
       // Is it equivalent under examples?
-      Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
+      Node bne = d_eec->addSearchVal(bnr);
       if (!bne.isNull())
       {
         if (bnr != bne)
@@ -533,17 +538,13 @@ void SygusEnumerator::TermEnumSlave::validateIndexNextEnd()
 void SygusEnumerator::initializeTermCache(TypeNode tn)
 {
   // initialize the term cache
-  // see if we use sygus PBE for symmetry breaking
-  SygusPbe* pbe = nullptr;
+  // see if we use an example evaluation cache for symmetry breaking
+  ExampleEvalCache* eec = nullptr;
   if (options::sygusSymBreakPbe())
   {
-    pbe = d_parent->getPbe();
-    if (!pbe->hasExamples(d_enum))
-    {
-      pbe = nullptr;
-    }
+    eec = d_parent->getExampleEvalCache(d_enum);
   }
-  d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, pbe);
+  d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec);
 }
 
 SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index 7e5add299..9803cd962 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -103,7 +103,7 @@ class SygusEnumerator : public EnumValGenerator
                     Node e,
                     TypeNode tn,
                     TermDbSygus* tds,
-                    SygusPbe* pbe = nullptr);
+                    ExampleEvalCache* ece = nullptr);
     /** get last constructor class index for weight
      *
      * This returns a minimal index n such that all constructor classes at
@@ -152,8 +152,11 @@ class SygusEnumerator : public EnumValGenerator
     TypeNode d_tn;
     /** pointer to term database sygus */
     TermDbSygus* d_tds;
-    /** pointer to the PBE utility (used for symmetry breaking) */
-    SygusPbe* d_pbe;
+    /**
+     * Pointer to the example evaluation cache utility (used for symmetry
+     * breaking).
+     */
+    ExampleEvalCache* d_eec;
     //-------------------------static information about type
     /** is d_tn a sygus type? */
     bool d_isSygusType;
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index b494e085e..9d20e1c3c 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -91,15 +91,14 @@ void EquivSygusInvarianceTest::init(
 {
   // compute the current examples
   d_bvr = bvr;
-  if (aconj->getPbe()->hasExamples(e))
+  Assert(tds != nullptr);
+  ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
+  if (eec != nullptr)
   {
+    // get the result of evaluating bvr on the examples of enumerator e.
+    eec->evaluateVec(bvr, d_exo, false);
     d_conj = aconj;
     d_enum = e;
-    unsigned nex = aconj->getPbe()->getNumExamples(e);
-    for (unsigned i = 0; i < nex; i++)
-    {
-      d_exo.push_back(d_conj->getPbe()->evaluateBuiltin(tn, bvr, e, i));
-    }
   }
 }
 
@@ -149,9 +148,11 @@ bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
     if (!d_enum.isNull())
     {
       bool ex_equiv = true;
-      for (unsigned j = 0; j < d_exo.size(); j++)
+      ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
+      Assert(eec != nullptr);
+      for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
       {
-        Node nbvr_ex = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, j);
+        Node nbvr_ex = eec->evaluate(nbvr, j);
         if (nbvr_ex != d_exo[j])
         {
           ex_equiv = false;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index ae019e50f..dc290d4ba 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/example_infer.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -38,114 +39,6 @@ SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p)
 
 SygusPbe::~SygusPbe() {}
 
-//--------------------------------- collecting finite input/output domain information
-
-bool SygusPbe::collectExamples(Node n,
-                               std::map<Node, bool>& visited,
-                               bool hasPol,
-                               bool pol)
-{
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    Node neval;
-    Node n_output;
-    bool neval_is_evalapp = false;
-    if (n.getKind() == DT_SYGUS_EVAL)
-    {
-      neval = n;
-      if( hasPol ){
-        n_output = pol ? d_true : d_false;
-      }
-      neval_is_evalapp = true;
-    }
-    else if (n.getKind() == EQUAL && hasPol && pol)
-    {
-      for( unsigned r=0; r<2; r++ ){
-        if (n[r].getKind() == DT_SYGUS_EVAL)
-        {
-          neval = n[r];
-          if( n[1-r].isConst() ){
-            n_output = n[1-r];
-          }
-          neval_is_evalapp = true;
-        }
-      }
-    }
-    // is it an evaluation function?
-    if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
-    {
-      Trace("sygus-pbe-debug")
-          << "Process head: " << n << " == " << n_output << std::endl;
-      // If n_output is null, then neval does not have a constant value
-      // If n_output is non-null, then neval is constrained to always be
-      // that value.
-      if (!n_output.isNull())
-      {
-        std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
-        if (itet == d_exampleTermMap.end())
-        {
-          d_exampleTermMap[neval] = n_output;
-        }
-        else if (itet->second != n_output)
-        {
-          // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
-          // the conjecture is infeasible.
-          return false;
-        }
-      }
-      // get the evaluation head
-      Node eh = neval[0];
-      std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
-      if (itx == d_examples_invalid.end())
-      {
-        // collect example
-        bool success = true;
-        std::vector<Node> ex;
-        for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
-        {
-          if (!neval[j].isConst())
-          {
-            success = false;
-            break;
-          }
-          ex.push_back(neval[j]);
-        }
-        if (success)
-        {
-          d_examples[eh].push_back(ex);
-          d_examples_out[eh].push_back(n_output);
-          d_examples_term[eh].push_back(neval);
-          if (n_output.isNull())
-          {
-            d_examples_out_invalid[eh] = true;
-          }
-          else
-          {
-            Assert(n_output.isConst());
-            // finished processing this node if it was an I/O pair
-            return true;
-          }
-        }
-        else
-        {
-          d_examples_invalid[eh] = true;
-          d_examples_out_invalid[eh] = true;
-        }
-      }
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      bool newHasPol;
-      bool newPol;
-      QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
-      if (!collectExamples(n[i], visited, newHasPol, newPol))
-      {
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
 bool SygusPbe::initialize(Node conj,
                           Node n,
                           const std::vector<Node>& candidates,
@@ -154,51 +47,6 @@ bool SygusPbe::initialize(Node conj,
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
 
-  for (unsigned i = 0; i < candidates.size(); i++)
-  {
-    Node v = candidates[i];
-    d_examples[v].clear();
-    d_examples_out[v].clear();
-    d_examples_term[v].clear();
-  }
-
-  std::map<Node, bool> visited;
-  // n is negated conjecture
-  if (!collectExamples(n, visited, true, false))
-  {
-    Trace("sygus-pbe") << "...conflicting examples" << std::endl;
-    Node infeasible = d_parent->getGuard().negate();
-    lemmas.push_back(infeasible);
-    return false;
-  }
-
-  for (unsigned i = 0; i < candidates.size(); i++)
-  {
-    Node v = candidates[i];
-    Trace("sygus-pbe") << "  examples for " << v << " : ";
-    if (d_examples_invalid.find(v) != d_examples_invalid.end())
-    {
-      Trace("sygus-pbe") << "INVALID" << std::endl;
-    }
-    else
-    {
-      Trace("sygus-pbe") << std::endl;
-      for (unsigned j = 0; j < d_examples[v].size(); j++)
-      {
-        Trace("sygus-pbe") << "    ";
-        for (unsigned k = 0; k < d_examples[v][j].size(); k++)
-        {
-          Trace("sygus-pbe") << d_examples[v][j][k] << " ";
-        }
-        if (!d_examples_out[v][j].isNull())
-        {
-          Trace("sygus-pbe") << " -> " << d_examples_out[v][j];
-        }
-        Trace("sygus-pbe") << std::endl;
-      }
-    }
-  }
-
   if (!options::sygusUnifPbe())
   {
     // we are not doing unification
@@ -206,11 +54,12 @@ bool SygusPbe::initialize(Node conj,
   }
 
   // check if all candidates are valid examples
+  ExampleInfer* ei = d_parent->getExampleInfer();
   d_is_pbe = true;
   for (const Node& c : candidates)
   {
-    if (d_examples[c].empty()
-        || d_examples_out_invalid.find(c) != d_examples_out_invalid.end())
+    // if it has no examples or the output of the examples is invalid
+    if (ei->getNumExamples(c) == 0 || !ei->hasExamplesOut(c))
     {
       d_is_pbe = false;
       return false;
@@ -218,11 +67,12 @@ bool SygusPbe::initialize(Node conj,
   }
   for (const Node& c : candidates)
   {
-    Assert(d_examples.find(c) != d_examples.end());
+    Assert(ei->hasExamples(c));
+    d_sygus_unif[c].reset(new SygusUnifIo(d_parent));
     Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
                        << std::endl;
     std::map<Node, std::vector<Node>> strategy_lemmas;
-    d_sygus_unif[c].initializeCandidate(
+    d_sygus_unif[c]->initializeCandidate(
         d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
     Assert(!d_candidate_to_enum[c].empty());
     Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
@@ -288,163 +138,10 @@ bool SygusPbe::initialize(Node conj,
         d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
       }
     }
-    Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
-                       << " example points for " << c << "..." << std::endl;
-    // initialize the examples
-    for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++)
-    {
-      d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]);
-    }
   }
   return true;
 }
 
-Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector<Node>& exOut)
-{
-  PbeTrie* curr = this;
-  for (const Node& eo : exOut)
-  {
-    curr = &(curr->d_children[eo]);
-  }
-  if (!curr->d_children.empty())
-  {
-    return curr->d_children.begin()->first;
-  }
-  curr->d_children.insert(std::pair<Node, PbeTrie>(b, PbeTrie()));
-  return b;
-}
-
-bool SygusPbe::hasExamples(Node e)
-{
-  e = d_tds->getSynthFunForEnumerator(e);
-  if (e.isNull())
-  {
-    // enumerator is not associated with synthesis function?
-    return false;
-  }
-  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
-  if (itx == d_examples_invalid.end())
-  {
-    return d_examples.find(e) != d_examples.end();
-  }
-  return false;
-}
-
-unsigned SygusPbe::getNumExamples(Node e)
-{
-  e = d_tds->getSynthFunForEnumerator(e);
-  Assert(!e.isNull());
-  std::map<Node, std::vector<std::vector<Node> > >::iterator it =
-      d_examples.find(e);
-  if (it != d_examples.end()) {
-    return it->second.size();
-  } else {
-    return 0;
-  }
-}
-
-void SygusPbe::getExample(Node e, unsigned i, std::vector<Node>& ex)
-{
-  e = d_tds->getSynthFunForEnumerator(e);
-  Assert(!e.isNull());
-  std::map<Node, std::vector<std::vector<Node> > >::iterator it =
-      d_examples.find(e);
-  if (it != d_examples.end()) {
-    Assert(i < it->second.size());
-    ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
-  } else {
-    Assert(false);
-  }
-}
-
-Node SygusPbe::getExampleOut(Node e, unsigned i)
-{
-  e = d_tds->getSynthFunForEnumerator(e);
-  Assert(!e.isNull());
-  std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e);
-  if (it != d_examples_out.end()) {
-    Assert(i < it->second.size());
-    return it->second[i];
-  } else {
-    Assert(false);
-    return Node::null();
-  }
-}
-
-Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
-{
-  Assert(!e.isNull());
-  if (d_tds->isVariableAgnosticEnumerator(e))
-  {
-    // we cannot apply conjecture-specific symmetry breaking on variable
-    // agnostic enumerators
-    return Node::null();
-  }
-  Node ee = d_tds->getSynthFunForEnumerator(e);
-  Assert(!e.isNull());
-  std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
-  if (itx == d_examples_invalid.end()) {
-    std::vector<Node> vals;
-    Trace("sygus-pbe-debug")
-        << "Compute examples " << bvr << "..." << std::endl;
-    if (d_is_pbe)
-    {
-      // Compute example values with the I/O utility, which ensures they are
-      // not later recomputed when the enumerated term is given the I/O utility.
-      d_sygus_unif[ee].computeExamples(e, bvr, vals);
-    }
-    else
-    {
-      // If the I/O utility is not enabled (if the conjecture is not PBE),
-      // compute them separately. This handles the case when all applications
-      // of a function-to-synthesize are applied to constant arguments but
-      // the conjecture is not PBE.
-      TypeNode etn = e.getType();
-      std::vector<std::vector<Node>>& exs = d_examples[ee];
-      for (size_t i = 0, esize = exs.size(); i < esize; i++)
-      {
-        Node res = d_tds->evaluateBuiltin(etn, bvr, exs[i]);
-        vals.push_back(res);
-      }
-    }
-    Assert(vals.size() == d_examples[ee].size());
-    Trace("sygus-pbe-debug") << "...got " << vals << std::endl;
-    Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
-    Node ret = d_pbe_trie[e][tn].addTerm(bvr, vals);
-    Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
-    if (d_is_pbe)
-    {
-      // Clean up the cache data if necessary: if the enumerated term
-      // is redundant, its cached data will not be used later and thus should
-      // be cleared now.
-      if (ret != bvr)
-      {
-        Trace("sygus-pbe-debug") << "...clear example cache" << std::endl;
-        d_sygus_unif[ee].clearExampleCache(e, bvr);
-      }
-    }
-    Assert(ret.getType().isComparableTo(bvr.getType()));
-    return ret;
-  }
-  return Node::null();
-}
-
-Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i)
-{
-  e = d_tds->getSynthFunForEnumerator(e);
-  Assert(!e.isNull());
-  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
-  if (itx == d_examples_invalid.end()) {
-    std::map<Node, std::vector<std::vector<Node> > >::iterator it =
-        d_examples.find(e);
-    if (it != d_examples.end()) {
-      Assert(i < it->second.size());
-      return d_tds->evaluateBuiltin(tn, bn, it->second[i]);
-    }
-  }
-  return Rewriter::rewrite(bn);
-}
-
 // ------------------------------------------- solution construction from enumeration
 
 void SygusPbe::getTermList(const std::vector<Node>& candidates,
@@ -526,7 +223,7 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
       Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
       Node c = d_enum_to_candidate[e];
       std::vector<Node> enum_lems;
-      d_sygus_unif[c].notifyEnumeration(e, v, enum_lems);
+      d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems);
       if (!enum_lems.empty())
       {
         // the lemmas must be guarded by the active guard of the enumerator
@@ -544,7 +241,7 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
     Node c = candidates[i];
     //build decision tree for candidate
     std::vector<Node> sol;
-    if (d_sygus_unif[c].constructSolution(sol, lems))
+    if (d_sygus_unif[c]->constructSolution(sol, lems))
     {
       Assert(sol.size() == 1);
       candidate_values.push_back(sol[0]);
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 2e6ca2659..3aa668e0d 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -34,13 +34,14 @@ class SynthConjecture;
  *
  * [EX#1] An example of a synthesis conjecture in PBE form is :
  * exists f. forall x.
- * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 )
+ * ( f( 0 ) = 2 ) ^ ( f( 5 ) = 7 ) ^ ( f( 6 ) = 8 )
  *
  * We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8.
  *
  * Internally, this class does the following for SyGuS inputs:
  *
- * (1) Infers whether the input conjecture is in PBE form or not.
+ * (1) Infers whether the input conjecture is in PBE form or not, which
+ *     is based on looking up information in the ExampleInfer utility.
  * (2) Based on this information and on the syntactic restrictions, it
  *     devises a strategy for enumerating terms and construction solutions,
  *     which is inspired by Alur et al. "Scaling Enumerative Program Synthesis
@@ -68,22 +69,11 @@ class SynthConjecture;
  * syntactic restrictions for it. The search may continue unless all enumerators
  * become inactive.
  *
- * (4) During search, the extension of quantifier-free datatypes procedure for
- *     SyGuS datatypes may ask this class whether current candidates can be
- *     discarded based on inferring when two candidate solutions are equivalent
- *     up to examples. For example, the candidate solutions:
- *     f = \x ite( x < 0, x+1, x ) and f = \x x
- *     are equivalent up to examples on the above conjecture, since they have
- * the same value on the points x = 0,5,6. Hence, we need only consider one of
- *     them. The interface for querying this is
- *       SygusPbe::addSearchVal(...).
- *     For details, see Reynolds et al. SYNT 2017.
- *
- * (5) When the extension of quantifier-free datatypes procedure for SyGuS
+ * (4) When the extension of quantifier-free datatypes procedure for SyGuS
  *     datatypes terminates with a model, the parent of this class calls
  *     SygusPbe::getCandidateList(...), where this class returns the list
  *     of active enumerators.
- * (6) The parent class subsequently calls
+ * (5) The parent class subsequently calls
  *     SygusPbe::constructValues(...), which informs this class that new
  *     values have been enumerated for active enumerators, as indicated by the
  *     current model. This call also requests that based on these
@@ -153,67 +143,6 @@ class SygusPbe : public SygusModule
                            std::vector<Node>& lems) override;
   /** is PBE enabled for any enumerator? */
   bool isPbe() { return d_is_pbe; }
-  /**
-   * Is the enumerator e associated with examples? This is true if the
-   * function-to-synthesize associated with e is only applied to concrete
-   * arguments. Notice that the conjecture need not be in PBE form for this
-   * to be the case. For example, f has examples in:
-   *   exists f. f( 1 ) = 3 ^ f( 2 ) = 4
-   *   exists f. f( 45 ) > 0 ^ f( 99 ) > 0
-   *   exists f. forall x. ( x > 5 => f( 4 ) < x )
-   * It does not have examples in:
-   *   exists f. forall x. f( x ) > 5
-   *   exists f. f( f( 4 ) ) = 5
-   * This class implements techniques for functions-to-synthesize that
-   * have examples. In particular, the method addSearchVal below can be
-   * called.
-   */
-  bool hasExamples(Node e);
-  /** get number of examples for enumerator e */
-  unsigned getNumExamples(Node e);
-  /**
-   * Get the input arguments for i^th example for e, which is added to the
-   * vector ex
-   */
-  void getExample(Node e, unsigned i, std::vector<Node>& ex);
-  /**
-   * Get the output value of the i^th example for enumerator e, or null if
-   * it does not exist (an example does not have an associate output if it is
-   * not a top-level equality).
-   */
-  Node getExampleOut(Node e, unsigned i);
-
-  /** add the search val
-   * This function is called by the extension of quantifier-free datatypes
-   * procedure for SyGuS datatypes or the SyGuS fast enumerator when we are
-   * considering a value of enumerator e of sygus type tn whose analog in the
-   * signature of builtin theory is bvr.
-   *
-   * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() )
-   * and tn is a sygus datatype that encodes a subsignature of the integers.
-   *
-   * This returns either:
-   * - A SyGuS term whose analog is equivalent to bvr up to examples
-   *   In the above example,
-   *   it may return a term t of the form Plus( One(), x() ), such that this
-   *   function was previously called with t as input.
-   * - e, indicating that no previous terms are equivalent to e up to examples.
-   *
-   * This method should only be called if hasExamples(e) returns true.
-   */
-  Node addSearchVal(TypeNode tn, Node e, Node bvr);
-  /** evaluate builtin
-  * This returns the evaluation of bn on the i^th example for the
-  * function-to-synthesis
-  * associated with enumerator e. If there are not at least i examples, it
-  * returns the rewritten form of bn.
-  * For example, if bn = x+5, e is an enumerator for f in the above example
-  * [EX#1], then
-  *   evaluateBuiltin( tn, bn, e, 0 ) = 7
-  *   evaluateBuiltin( tn, bn, e, 1 ) = 9
-  *   evaluateBuiltin( tn, bn, e, 2 ) = 10
-  */
-  Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i);
 
  private:
   /** true and false nodes */
@@ -221,31 +150,12 @@ class SygusPbe : public SygusModule
   Node d_false;
   /** is this a PBE conjecture for any function? */
   bool d_is_pbe;
-  /** for each candidate variable f (a function-to-synthesize), whether the
-  * conjecture is purely PBE for that variable
-  * In other words, all occurrences of f are guarded by equalities that
-  * constraint its arguments to constants.
-  */
-  std::map<Node, bool> d_examples_invalid;
-  /** for each candidate variable (function-to-synthesize), whether the
-  * conjecture is purely PBE for that variable.
-  * An example of a conjecture for which d_examples_invalid is false but
-  * d_examples_out_invalid is true is:
-  *   exists f. forall x. ( x = 0 => f( x ) > 2 )
-  * another example is:
-  *   exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) )
-  * since the formula is not a conjunction (the example values are not
-  * entailed).
-  * However, the domain of f in both cases is finite, which can be used for
-  * search space pruning.
-  */
-  std::map<Node, bool> d_examples_out_invalid;
   /**
    * Map from candidates to sygus unif utility. This class implements
    * the core algorithm (e.g. decision tree learning) that this module relies
    * upon.
    */
-  std::map<Node, SygusUnifIo> d_sygus_unif;
+  std::map<Node, std::unique_ptr<SygusUnifIo> > d_sygus_unif;
   /**
    * map from candidates to the list of enumerators that are being used to
    * build solutions for that candidate by the above utility.
@@ -253,63 +163,6 @@ class SygusPbe : public SygusModule
   std::map<Node, std::vector<Node> > d_candidate_to_enum;
   /** reverse map of above */
   std::map<Node, Node> d_enum_to_candidate;
-  /** for each candidate variable (function-to-synthesize), input of I/O
-   * examples */
-  std::map<Node, std::vector<std::vector<Node> > > d_examples;
-  /** for each candidate variable (function-to-synthesize), output of I/O
-   * examples */
-  std::map<Node, std::vector<Node> > d_examples_out;
-  /** the list of example terms
-   * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
-   */
-  std::map<Node, std::vector<Node> > d_examples_term;
-  /**
-   * Map from example input terms to their output, for example [EX#1] above,
-   * this is { f( 0 ) -> 2, f( 5 ) -> 7, f( 6 ) -> 8 }.
-   */
-  std::map<Node, Node> d_exampleTermMap;
-  /** collect the PBE examples in n
-   * This is called on the input conjecture, and will populate the above
-   * vectors, where hasPol/pol denote the polarity of n in the conjecture. This
-   * function returns false if it finds two examples that are contradictory.
-   */
-  bool collectExamples(Node n,
-                       std::map<Node, bool>& visited,
-                       bool hasPol,
-                       bool pol);
-
-  //--------------------------------- PBE search values
-  /**
-   * This class is an index of candidate solutions for PBE synthesis and their
-   * (concrete) evaluation on the set of input examples. For example, if the
-   * set of input examples for (x,y) is (0,1), (1,3), then:
-   *   term x is indexed by 0,1
-   *   term x+y is indexed by 1,4
-   *   term 0 is indexed by 0,0.
-   */
-  class PbeTrie
-  {
-   public:
-    PbeTrie() {}
-    ~PbeTrie() {}
-    /** the children for this node in the trie */
-    std::map<Node, PbeTrie> d_children;
-    /** clear this trie */
-    void clear() { d_children.clear(); }
-    /**
-     * Add term b whose value on examples is exOut to the trie. Return
-     * the first term registered to this trie whose evaluation was exOut.
-     */
-    Node addTerm(Node b, const std::vector<Node>& exOut);
-  };
-  /** trie of candidate solutions tried
-  * This stores information for each (enumerator, type),
-  * where type is a type in the grammar of the space of solutions for a subterm
-  * of e. This is used for symmetry breaking in quantifier-free reasoning
-  * about SyGuS datatypes.
-  */
-  std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
-  //--------------------------------- end PBE search values
 };
 
 } /* namespace CVC4::theory::quantifiers */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index d423b1777..e3e94ba44 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -16,8 +16,11 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/evaluator.h"
+#include "theory/quantifiers/sygus/example_infer.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 
 #include <math.h>
@@ -495,8 +498,9 @@ void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
   getLeavesInternal(vals, pol, v, 0, -2);
 }
 
-SygusUnifIo::SygusUnifIo()
-    : d_check_sol(false),
+SygusUnifIo::SygusUnifIo(SynthConjecture* p)
+    : d_parent(p),
+      d_check_sol(false),
       d_cond_count(0),
       d_sol_term_size(0),
       d_sol_cons_nondet(false),
@@ -507,53 +511,36 @@ SygusUnifIo::SygusUnifIo()
 }
 
 SygusUnifIo::~SygusUnifIo() {}
+
 void SygusUnifIo::initializeCandidate(
     QuantifiersEngine* qe,
     Node f,
     std::vector<Node>& enums,
     std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
+  d_candidate = f;
+  // copy the examples from the parent
+  ExampleInfer* ei = d_parent->getExampleInfer();
   d_examples.clear();
   d_examples_out.clear();
+  // copy the examples
+  if (ei->hasExamples(f))
+  {
+    for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
+    {
+      std::vector<Node> input;
+      ei->getExample(f, i, input);
+      Node output = ei->getExampleOut(f, i);
+      d_examples.push_back(input);
+      d_examples_out.push_back(output);
+    }
+  }
   d_ecache.clear();
-  d_candidate = f;
   SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
   // learn redundant operators based on the strategy
   d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
 }
 
-void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
-{
-  d_examples.push_back(input);
-  d_examples_out.push_back(output);
-}
-
-void SygusUnifIo::computeExamples(Node e, Node bv, std::vector<Node>& exOut)
-{
-  std::map<Node, std::vector<Node>>& eoc = d_exOutCache[e];
-  std::map<Node, std::vector<Node>>::iterator it = eoc.find(bv);
-  if (it != eoc.end())
-  {
-    exOut.insert(exOut.end(), it->second.begin(), it->second.end());
-    return;
-  }
-  TypeNode xtn = e.getType();
-  std::vector<Node>& eocv = eoc[bv];
-  for (size_t j = 0, size = d_examples.size(); j < size; j++)
-  {
-    Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
-    exOut.push_back(res);
-    eocv.push_back(res);
-  }
-}
-
-void SygusUnifIo::clearExampleCache(Node e, Node bv)
-{
-  std::map<Node, std::vector<Node>>& eoc = d_exOutCache[e];
-  Assert(eoc.find(bv) != eoc.end());
-  eoc.erase(bv);
-}
-
 void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
 {
   Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v
@@ -573,9 +560,13 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   bv = d_tds->getExtRewriter()->extendedRewrite(bv);
   Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl;
   // compte the results (should be cached)
-  computeExamples(e, bv, base_results);
-  // don't need it after this
-  clearExampleCache(e, bv);
+  ExampleEvalCache* eec = d_parent->getExampleEvalCache(e);
+  Assert(eec != nullptr);
+  // Evaluate, which should be cached (assuming we have performed example-based
+  // symmetry breaking on bv). Moreover don't cache the result in the case it
+  // is not there already, since we won't need this evaluation anywhere outside
+  // of this class.
+  eec->evaluateVec(bv, base_results);
   // get the results for each slave enumerator
   std::map<Node, std::vector<Node>> srmap;
   Evaluator* ev = d_tds->getEvaluator();
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 7e9c5abd2..da08044bf 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -243,19 +243,19 @@ class SubsumeTrie
                          int status);
 };
 
+class SynthConjecture;
+
 /** Sygus unification I/O utility
  *
  * This class implement synthesis-by-unification, where the specification is
- * I/O examples. With respect to SygusUnif, it's main interface function is
- * addExample, which adds an I/O example to the specification.
+ * I/O examples.
  *
  * Since I/O specifications for multiple functions can be fully separated, we
  * assume that this class is used only for a single function to synthesize.
  *
  * In addition to the base class which maintains a strategy tree, this class
  * maintains:
- * (1) A set of input/output examples that are the specification for f. This
- * can be updated via calls to resetExmaples/addExamples,
+ * (1) A set of input/output examples that are the specification for f.
  * (2) A set of terms that have been enumerated for enumerators (d_ecache). This
  * can be updated via calls to notifyEnumeration.
  */
@@ -264,11 +264,14 @@ class SygusUnifIo : public SygusUnif
   friend class UnifContextIo;
 
  public:
-  SygusUnifIo();
+  SygusUnifIo(SynthConjecture* p);
   ~SygusUnifIo();
 
   /** initialize
    *
+   * This initializes this class for solving PBE conjectures for
+   * function-to-synthesize f.
+   *
    * We only initialize for one function f, since I/O specifications across
    * multiple functions can be separated.
    */
@@ -283,29 +286,10 @@ class SygusUnifIo : public SygusUnif
   /** Construct solution */
   bool constructSolution(std::vector<Node>& sols,
                          std::vector<Node>& lemmas) override;
-
-  /** add example
-   *
-   * This adds input -> output to the specification for f. The arity of
-   * input should be equal to the number of arguments in the sygus variable
-   * list of the grammar of f. That is, if we are searching for solutions for f
-   * of the form (lambda v1...vn. t), then the arity of input should be n.
-   */
-  void addExample(const std::vector<Node>& input, Node output);
-
-  /** compute examples
-   *
-   * This adds the result of evaluating bv on the set of input examples managed
-   * by this class. Term bv is the builtin version of a term generated for
-   * enumerator e. It stores the resulting output for each example in exOut.
-   */
-  void computeExamples(Node e, Node bv, std::vector<Node>& exOut);
-
-  /** clear example cache */
-  void clearExampleCache(Node e, Node bv);
-
  protected:
-  /** the candidate */
+  /** The synthesis conjecture */
+  SynthConjecture* d_parent;
+  /** the function-to-synthesize */
   Node d_candidate;
   /**
    * Whether we will try to construct solution on the next call to
@@ -363,9 +347,6 @@ class SygusUnifIo : public SygusUnif
   /** output of I/O examples */
   std::vector<Node> d_examples_out;
 
-  /** cache for computeExamples */
-  std::map<Node, std::map<Node, std::vector<Node>>> d_exOutCache;
-
   /**
   * This class stores information regarding an enumerator, including:
   * a database of values that have been enumerated for this enumerator.