Change default sygus enumeration mode to auto (#2689)

6 files changed, 147 insertions, 57 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 79bec60ee..6aca71ca3 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -69,17 +69,10 @@ bool Cegis::processInitialize(Node n,
 {
   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 isActiveGen =
-      options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1;
+  // The role of enumerators is to be either the single solution or part of
+  // a solution involving multiple enumerators.
+  EnumeratorRole erole =
+      csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION;
   // initialize an enumerator for each candidate
   for (unsigned i = 0; i < csize; i++)
   {
@@ -98,13 +91,8 @@ bool Cegis::processInitialize(Node n,
       }
     }
     Trace("cegis") << std::endl;
-    // variable agnostic enumerators require an active guard
-    d_tds->registerEnumerator(candidates[i],
-                              candidates[i],
-                              d_parent,
-                              isActiveGen,
-                              do_repair_const,
-                              isActiveGen);
+    d_tds->registerEnumerator(
+        candidates[i], candidates[i], d_parent, erole, do_repair_const);
   }
   return true;
 }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index dbde79aae..18e313bf0 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -44,7 +44,12 @@ bool CegisUnif::processInitialize(Node n,
   std::map<Node, Node> pt_to_cond;
   // strategy lemmas for each strategy point
   std::map<Node, std::vector<Node>> strategy_lemmas;
-  // Initialize strategies for all functions-to-synhesize
+  // Initialize strategies for all functions-to-synthesize
+  // The role of non-unification enumerators is to be either the single solution
+  // or part of a solution involving multiple enumerators.
+  EnumeratorRole eroleNonUnif = candidates.size() == 1
+                                    ? ROLE_ENUM_SINGLE_SOLUTION
+                                    : ROLE_ENUM_MULTI_SOLUTION;
   for (const Node& f : candidates)
   {
     // Init UNIF util for this candidate
@@ -53,7 +58,7 @@ bool CegisUnif::processInitialize(Node n,
     if (!d_sygus_unif.usingUnif(f))
     {
       Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
-      d_tds->registerEnumerator(f, f, d_parent);
+      d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif);
       d_non_unif_candidates.push_back(f);
     }
     else
@@ -462,7 +467,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
                                                                exclude_cons,
                                                                term_irrelevant);
       d_virtual_enum = nm->mkSkolem("_ve", vtn);
-      d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
+      d_tds->registerEnumerator(
+          d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
     }
     // if new_size is a power of two, then isPow2 returns log2(new_size)+1
     // otherwise, this returns 0. In the case it returns 0, we don't care
@@ -606,20 +612,17 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   }
   // register the enumerator
   si.d_enums[index].push_back(e);
-  bool mkActiveGuard = false;
-  bool isActiveGen = false;
+  EnumeratorRole erole = ROLE_ENUM_CONSTRAINED;
   // if we are using a single independent enumerator for conditions, then we
   // allocate an active guard, and are eligible to use variable-agnostic
   // enumeration.
   if (options::sygusUnifCondIndependent() && index == 1)
   {
-    mkActiveGuard = true;
-    isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
+    erole = ROLE_ENUM_POOL;
   }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
-  d_tds->registerEnumerator(
-      e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen);
+  d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false);
 }
 
 void CegisUnifEnumDecisionStrategy::registerEvalPts(
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index b49c29c53..f91dd5d30 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -179,7 +179,6 @@ bool SygusPbe::initialize(Node n,
       return false;
     }
   }
-  bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
   for (const Node& c : candidates)
   {
     Assert(d_examples.find(c) != d_examples.end());
@@ -203,7 +202,7 @@ bool SygusPbe::initialize(Node n,
     for (const Node& e : d_candidate_to_enum[c])
     {
       TypeNode etn = e.getType();
-      d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen);
+      d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false);
       d_enum_to_candidate[e] = c;
       TNode te = e;
       // initialize static symmetry breaking lemmas for it
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 03344d2e7..2bfde2d80 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -703,13 +703,13 @@ class EnumValGeneratorBasic : public EnumValGenerator
    */
   bool increment() override
   {
+    ++d_te;
     if (d_te.isFinished())
     {
       d_currTerm = Node::null();
       return false;
     }
     d_currTerm = *d_te;
-    ++d_te;
     if (options::sygusSymBreakDynamic())
     {
       Node nextb = d_tds->sygusToBuiltin(d_currTerm);
@@ -773,15 +773,18 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
     else
     {
       // Actively-generated enumerators are currently either variable agnostic
-      // or basic.
+      // or basic. The auto mode always prefers the optimized enumerator over
+      // the basic one.
       Assert(d_tds->isBasicEnumerator(e));
-      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM)
+      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC)
       {
-        d_evg[e].reset(new SygusEnumerator(d_tds, this));
+        d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
       }
       else
       {
-        d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+        Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM
+               || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO);
+        d_evg[e].reset(new SygusEnumerator(d_tds, this));
       }
     }
     Trace("sygus-active-gen")
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 9af990086..5cf230820 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -58,6 +58,19 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
   }
 }
 
+std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
+{
+  switch (r)
+  {
+    case ROLE_ENUM_POOL: os << "POOL"; break;
+    case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break;
+    case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break;
+    case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break;
+    default: os << "enum_" << static_cast<unsigned>(r); break;
+  }
+  return os;
+}
+
 TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
     : d_quantEngine(qe),
       d_syexp(new SygusExplain(this)),
@@ -454,9 +467,8 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
 void TermDbSygus::registerEnumerator(Node e,
                                      Node f,
                                      SynthConjecture* conj,
-                                     bool mkActiveGuard,
-                                     bool useSymbolicCons,
-                                     bool isActiveGen)
+                                     EnumeratorRole erole,
+                                     bool useSymbolicCons)
 {
   if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
   {
@@ -470,13 +482,6 @@ void TermDbSygus::registerEnumerator(Node e,
   d_enum_to_conjecture[e] = conj;
   d_enum_to_synth_fun[e] = f;
   NodeManager* nm = NodeManager::currentNM();
-  if( mkActiveGuard ){
-    // make the guard
-    Node ag = nm->mkSkolem("eG", nm->booleanType());
-    // must ensure it is a literal immediately here
-    ag = d_quantEngine->getValuation().ensureLiteral(ag);
-    d_enum_to_active_guard[e] = ag;
-  }
 
   Trace("sygus-db") << "  registering symmetry breaking clauses..."
                     << std::endl;
@@ -554,6 +559,66 @@ void TermDbSygus::registerEnumerator(Node e,
   }
   Trace("sygus-db") << "  ...finished" << std::endl;
 
+  // determine if we are actively-generated
+  bool isActiveGen = false;
+  if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
+  {
+    if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
+    {
+      // If the enumerator is a solution for a conjecture with multiple
+      // functions, we do not use active generation. If we did, 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, and if these enumerators generated:
+      // e_f -> t1, ..., tn
+      // e_g -> s1, ..., sm
+      // The sygus module in charge of this conjecture would expect
+      // constructCandidates calls of the form
+      //   (e_f,e_g) -> (ti, sj)
+      // for each i,j. We instead use passive enumeration in this case.
+      //
+      // If the enumerator is constrained, it cannot be actively generated.
+    }
+    else if (erole == ROLE_ENUM_POOL)
+    {
+      // If the enumerator is used for generating a pool of values, we always
+      // use active generation.
+      isActiveGen = true;
+    }
+    else if (erole == ROLE_ENUM_SINGLE_SOLUTION)
+    {
+      // If the enumerator is the single function-to-synthesize, if auto is
+      // enabled, we infer whether it is better to enable active generation.
+      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
+      {
+        // We use active generation if the grammar of the enumerator does not
+        // have ITE and is not Boolean. Experimentally, it is better to
+        // use passive generation for these cases since it enables useful
+        // search space pruning techniques, e.g. evaluation unfolding,
+        // conjecture-specific symmetry breaking. Also, if sygus-stream is
+        // enabled, we always use active generation, since the use cases of
+        // sygus stream are to find many solutions to an easy problem, where
+        // the bottleneck often becomes the large number of "exclude the current
+        // solution" clauses.
+        const Datatype& dt = et.getDatatype();
+        if (options::sygusStream()
+            || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean()))
+        {
+          isActiveGen = true;
+        }
+      }
+      else
+      {
+        isActiveGen = true;
+      }
+    }
+    else
+    {
+      Unreachable("Unknown enumerator mode in registerEnumerator");
+    }
+  }
+  Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
+                    << " returned " << isActiveGen << std::endl;
   // Currently, actively-generated enumerators are either basic or variable
   // agnostic.
   bool isVarAgnostic =
@@ -607,6 +672,18 @@ void TermDbSygus::registerEnumerator(Node e,
   }
   d_enum_active_gen[e] = isActiveGen;
   d_enum_basic[e] = isActiveGen && !isVarAgnostic;
+
+  // We make an active guard if we will be explicitly blocking solutions for
+  // the enumerator. This is the case if the role of the enumerator is to
+  // populate a pool of terms, or (some cases) of when it is actively generated.
+  if (isActiveGen || erole == ROLE_ENUM_POOL)
+  {
+    // make the guard
+    Node ag = nm->mkSkolem("eG", nm->booleanType());
+    // must ensure it is a literal immediately here
+    ag = d_quantEngine->getValuation().ensureLiteral(ag);
+    d_enum_to_active_guard[e] = ag;
+  }
 }
 
 bool TermDbSygus::isEnumerator(Node e) const
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 713e322a4..2e8604411 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -48,6 +48,23 @@ class TypeNodeIdTrie
   void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
 };
 
+/** role for registering an enumerator */
+enum EnumeratorRole
+{
+  /** The enumerator populates a pool of terms (e.g. for PBE). */
+  ROLE_ENUM_POOL,
+  /** The enumerator is the single solution of the problem. */
+  ROLE_ENUM_SINGLE_SOLUTION,
+  /**
+   * The enumerator is part of the solution of the problem (e.g. multiple
+   * functions to synthesize).
+   */
+  ROLE_ENUM_MULTI_SOLUTION,
+  /** The enumerator must satisfy some set of constraints */
+  ROLE_ENUM_CONSTRAINED,
+};
+std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
+
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
  public:
@@ -80,29 +97,32 @@ class TermDbSygus {
   //------------------------------enumerators
   /**
    * Register a variable e that we will do enumerative search on.
+   *
    * conj : the conjecture that the enumeration of e is for.
-   * f : the synth-fun that the enumeration of e is for.
-   * mkActiveGuard : whether we want to make an active guard for e
-   * (see d_enum_to_active_guard),
-   * useSymbolicCons : whether we want model values for e to include symbolic
-   * constructors like the "any constant" variable.
-   * isActiveGen : if this flag is true, the enumerator will be
-   * actively-generated based on the mode specified by --sygus-active-gen.
+   *
+   * f : the synth-fun that the enumeration of e is for.Notice that enumerator
+   * e may not be one-to-one with f in synthesis-through-unification approaches
+   * (e.g. decision tree construction for PBE synthesis).
+   *
+   * erole : the role of this enumerator (see definition of EnumeratorRole).
+   * Depending on this and the policy for actively-generated enumerators
+   * (--sygus-active-gen), the enumerator may be "actively-generated".
    * For example, if --sygus-active-gen=var-agnostic, then the enumerator will
    * only generate values whose variables are in canonical order (only x1-x2
    * and not x2-x1 will be generated, assuming x1 and x2 are in the same
    * "subclass", see getSubclassForVar).
    *
-   * Notice that enumerator e may not be one-to-one with f in
-   * synthesis-through-unification approaches (e.g. decision tree construction
-   * for PBE synthesis).
+   * useSymbolicCons : whether we want model values for e to include symbolic
+   * constructors like the "any constant" variable.
+   *
+   * An "active guard" may be allocated by this method for e based on erole
+   * and the policies for active generation.
    */
   void registerEnumerator(Node e,
                           Node f,
                           SynthConjecture* conj,
-                          bool mkActiveGuard = false,
-                          bool useSymbolicCons = false,
-                          bool isActiveGen = false);
+                          EnumeratorRole erole,
+                          bool useSymbolicCons = false);
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */