Cegis unif defaults to cegis when no unif (#1942)

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 57c4c1ad3964692c7a2f3f67058902619ec0388e..5a383a17af38319aa51f6f7a1ff9a00bb9a831d1 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -53,9 +53,11 @@ bool CegisUnif::processInitialize(Node n,
     {
       Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
       d_tds->registerEnumerator(f, f, d_parent);
+      d_non_unif_candidates.push_back(f);
     }
     else
     {
+      d_unif_candidates.push_back(f);
       Trace("cegis-unif") << "* unification candidate : " << f
                           << " with strategy points:" << std::endl;
       std::vector<Node>& enums = d_cand_to_strat_pt[f];
@@ -80,14 +82,11 @@ bool CegisUnif::processInitialize(Node n,
 void CegisUnif::getTermList(const std::vector<Node>& candidates,
                             std::vector<Node>& enums)
 {
-  for (const Node& c : candidates)
+  // Non-unif candidate are themselves the enumerators
+  enums.insert(
+      enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end());
+  for (const Node& c : d_unif_candidates)
   {
-    // Non-unif candidate are themselves the enumerators
-    if (!d_sygus_unif.usingUnif(c))
-    {
-      enums.push_back(c);
-      continue;
-    }
     // Collect heads of candidates
     for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
     {
@@ -105,6 +104,12 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
                                            bool satisfiedRl,
                                            std::vector<Node>& lems)
 {
+  if (d_unif_candidates.empty())
+  {
+    Assert(d_non_unif_candidates.size() == candidates.size());
+    return Cegis::processConstructCandidates(
+        enums, enum_values, candidates, candidate_values, satisfiedRl, lems);
+  }
   if (!satisfiedRl)
   {
     // if we didn't satisfy the specification, there is no way to repair
@@ -117,7 +122,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   Node cost_lit = d_u_enum_manager.getCurrentLiteral();
   std::map<Node, std::vector<Node>> unif_enums[2];
   std::map<Node, std::vector<Node>> unif_values[2];
-  for (const Node& c : candidates)
+  for (const Node& c : d_unif_candidates)
   {
     // for each decision tree strategy allocated for c (these are referenced
     // by strategy points in d_cand_to_strat_pt[c])
@@ -196,7 +201,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
     return false;
   }
   // set the conditions
-  for (const Node& c : candidates)
+  for (const Node& c : d_unif_candidates)
   {
     for (const Node& e : d_cand_to_strat_pt[c])
     {

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 80c11f82dd77cc2ec4c62fac298997292b604db0..ec338a8b2bbe29c5c88c161882b0490b1e6cde89 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -277,6 +277,10 @@ class CegisUnif : public Cegis
   CegisUnifEnumManager d_u_enum_manager;
   /* The null node */
   Node d_null;
+  /** the unification candidates */
+  std::vector<Node> d_unif_candidates;
+  /** the non-unification candidates */
+  std::vector<Node> d_non_unif_candidates;
   /** list of strategy points per candidate */
   std::map<Node, std::vector<Node>> d_cand_to_strat_pt;
   /** map from conditional enumerators to their strategy point */

diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index d26edffd2ee919abfb98f117dcd9c6c81045926b..0fe8dd05e88e5a3b2f388542fe978980e77817b4 100644 (file)
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,6 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int