1 files changed, 29 insertions, 14 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index db9af10b4..9706e3732 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -68,8 +68,19 @@ bool Cegis::processInitialize(Node n,
                               std::vector<Node>& lemmas)
 {
   Trace("cegis") << "Initialize cegis..." << std::endl;
+  unsigned csize = candidates.size();
+  // We only can use actively-generated enumerators if there is only one
+  // function-to-synthesize. Otherwise, we would have to generate a "product" of
+  // two actively-generated enumerators. That is, given a conjecture with two
+  // functions-to-synthesize with enumerators e_f and e_g, if:
+  // e_f -> t1, ..., tn
+  // e_g -> s1, ..., sm
+  // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj)
+  // for each i,j. We do not do this and revert to the default behavior of
+  // this module instead.
+  bool isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1;
   // initialize an enumerator for each candidate
-  for (unsigned i = 0; i < candidates.size(); i++)
+  for (unsigned i = 0; i < csize; i++)
   {
     Trace("cegis") << "...register enumerator " << candidates[i];
     bool do_repair_const = false;
@@ -86,8 +97,13 @@ bool Cegis::processInitialize(Node n,
       }
     }
     Trace("cegis") << std::endl;
-    d_tds->registerEnumerator(
-        candidates[i], candidates[i], d_parent, false, do_repair_const);
+    // variable agnostic enumerators require an active guard
+    d_tds->registerEnumerator(candidates[i],
+                              candidates[i],
+                              d_parent,
+                              isVarAgnostic,
+                              do_repair_const,
+                              isVarAgnostic);
   }
   return true;
 }
@@ -99,7 +115,8 @@ void Cegis::getTermList(const std::vector<Node>& candidates,
 }
 
 bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
-                          const std::vector<Node>& candidate_values)
+                          const std::vector<Node>& candidate_values,
+                          std::vector<Node>& lems)
 {
   // First, decide if this call will apply "conjecture-specific refinement".
   // In other words, in some settings, the following method will identify and
@@ -144,13 +161,14 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     }
     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"))
       {
-        if (d_qe->addLemma(lem))
+        for (const Node& lem : cre_lems)
         {
           Trace("cegqi-lemma")
               << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
-          addedEvalLemmas = true;
         }
       }
       /* we could, but do not return here. experimentally, it is better to
@@ -178,12 +196,9 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     {
       Node lem = nm->mkNode(
           OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
-      if (d_qe->addLemma(lem))
-      {
-        Trace("cegqi-lemma")
-            << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl;
-        addedEvalLemmas = true;
-      }
+      lems.push_back(lem);
+      Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
+                           << std::endl;
     }
   }
   return addedEvalLemmas;
@@ -258,7 +273,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
   }
 
   // evaluate on refinement lemmas
-  bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
+  bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems);
 
   // try to construct candidates
   if (!processConstructCandidates(enums,