Use fast enumeration by default for Boolean predicate synthesis (#6440)

This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals.

This significantly improves run time on a challenge benchmark from @makaimann.

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 41b4c27f42d9fa16dd4b79ba6028da4c468aaff8..b18a7c796d950e5b78953cea1124bfafdbf370b1 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -507,17 +507,16 @@ void TermDbSygus::registerEnumerator(Node e,
       if (options::sygusActiveGenMode() == options::SygusActiveGenMode::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,
+        // have ITE and does not have Boolean connectives. 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 DType& dt = et.getDType();
         if (options::sygusStream()
-            || (!eti.hasIte() && !dt.getSygusType().isBoolean()))
+            || (!eti.hasIte() && !eti.hasBoolConnective()))
         {
           isActiveGen = true;
         }

diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index c8a86e32abb0ec60f016724dc0eae8cea73d8175..f9aa5bdc3d5ac65b52335aaa8a326ee930567b7d 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -31,6 +31,7 @@ namespace quantifiers {
 
 SygusTypeInfo::SygusTypeInfo()
     : d_hasIte(false),
+      d_hasBoolConnective(false),
       d_min_term_size(0),
       d_sym_cons_any_constant(-1),
       d_has_subterm_sym_cons(false)
@@ -150,11 +151,6 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     {
       d_kinds[builtinKind] = i;
       d_arg_kind[i] = builtinKind;
-      if (builtinKind == ITE)
-      {
-        // mark that this type has an ITE
-        d_hasIte = true;
-      }
     }
     // symbolic constructors
     if (sop.getAttribute(SygusAnyConstAttribute()))
@@ -179,6 +175,21 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
         << "Sygus datatype " << dt.getName()
         << " encodes terms that are not of type " << btn << std::endl;
     Trace("sygus-db") << "...done register Operator #" << i << std::endl;
+    Kind gk = g.getKind();
+    if (gk == ITE)
+    {
+      // mark that this type has an ITE
+      d_hasIte = true;
+      if (g.getType().isBoolean())
+      {
+        d_hasBoolConnective = true;
+      }
+    }
+    else if (gk == AND || gk == OR || gk == IMPLIES || gk == XOR
+             || (gk == EQUAL && g[0].getType().isBoolean()))
+    {
+      d_hasBoolConnective = true;
+    }
   }
   // compute minimum type depth information
   computeMinTypeDepthInternal(tn, 0);
@@ -375,6 +386,7 @@ int SygusTypeInfo::getOpConsNum(Node n) const
 
 bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
 bool SygusTypeInfo::hasIte() const { return d_hasIte; }
+bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; }
 bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
 bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }
 

diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h
index 7b22f826c6b2190e5f679be52093db27fd458c52..3c0fbf30e9c66ffa9f312b273c1b2f17a0cfb797 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.h
+++ b/src/theory/quantifiers/sygus/type_info.h
@@ -81,6 +81,11 @@ class SygusTypeInfo
    * ITE, or is a lambda whose body is ITE.
    */
   bool hasIte() const;
+  /**
+   * Returns true if this sygus type has a constructor whose sygus operator is
+   * a Boolean connective.
+   */
+  bool hasBoolConnective() const;
   /**
    * Get the builtin kind for the i^th constructor of this sygus type. If the
    * i^th constructor does not encode an application of a builtin kind, this
@@ -196,6 +201,11 @@ class SygusTypeInfo
    * or is a lambda whose body is ITE.
    */
   bool d_hasIte;
+  /**
+   * Whether this sygus type has a constructor whose sygus operator is a
+   * Boolean connective.
+   */
+  bool d_hasBoolConnective;
   /**
    * Maps constructor indices to the constant that they encode, if any.
    */