Infer when sygus operators are equivalent to builtin kinds (#4140)

The V2 parser always turns sygus operators into lambdas for consistency. This PR ensures that we nevertheless infer when a sygus operator is equivalent to a builtin operator, e.g.
(lambda x y. (+ x y)) is equivalent to +.

The main reason this is required is to ensure that solution reconstruction heuristics work optimally when we make the switch SyGuS V1 -> V2 (see 5 failing benchmarks due to --cegqi-si=all on #4136).

diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index a17a60927fd06281303f7163f3e13078315664a2..7235fd65c9420ff2e6c2b1f5de7d1a8673bb2d86 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -97,17 +97,11 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
     Node sop = dt[i].getSygusOp();
     Assert(!sop.isNull());
     Trace("sygus-db") << "  Operator #" << i << " : " << sop;
+    Kind builtinKind = UNDEFINED_KIND;
     if (sop.getKind() == kind::BUILTIN)
     {
-      Kind sk = NodeManager::operatorToKind(sop);
-      Trace("sygus-db") << ", kind = " << sk;
-      d_kinds[sk] = i;
-      d_arg_kind[i] = sk;
-      if (sk == ITE)
-      {
-        // mark that this type has an ITE
-        d_hasIte = true;
-      }
+      builtinKind = NodeManager::operatorToKind(sop);
+      Trace("sygus-db") << ", kind = " << builtinKind;
     }
     else if (sop.isConst() && dt[i].getNumArgs() == 0)
     {
@@ -128,7 +122,32 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
             << "In sygus datatype " << dt.getName()
             << ", argument to a lambda constructor is not " << lat << std::endl;
       }
-      if (sop[0].getKind() == ITE)
+      // See if it is a builtin kind, possible if the operator is of the form:
+      // lambda x1 ... xn. f( x1, ..., xn ) and f is not a parameterized kind
+      // (e.g. APPLY_UF is a parameterized kind).
+      if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED)
+      {
+        size_t nchild = sop[0].getNumChildren();
+        if (nchild == sop[1].getNumChildren())
+        {
+          builtinKind = sop[1].getKind();
+          for (size_t j = 0; j < nchild; j++)
+          {
+            if (sop[0][j] != sop[1][j])
+            {
+              // arguments not in order
+              builtinKind = UNDEFINED_KIND;
+              break;
+            }
+          }
+        }
+      }
+    }
+    if (builtinKind != UNDEFINED_KIND)
+    {
+      d_kinds[builtinKind] = i;
+      d_arg_kind[i] = builtinKind;
+      if (builtinKind == ITE)
       {
         // mark that this type has an ITE
         d_hasIte = true;