Restrict cases of sygus grammar reduction based on argument variants (#4131)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 24 Mar 2020 02:20:32 +0000 (21:20 -0500)
committerGitHub <noreply@github.com>
Tue, 24 Mar 2020 02:20:32 +0000 (21:20 -0500)
An assertion is triggered for some V2 versions of SyGuS V1 benchmarks during sygus grammar reduction. This PR updates this technique so that it only applies to sygus constructors whose sygus operators are lambdas of the form
lambda x1 ... xn. f( x1 ... xn ).

FYI @abdoo8080 .

src/theory/quantifiers/sygus/sygus_grammar_red.cpp

index d9ce08d49645c4d04c3d91443038c645b3f3960a..d865457c3fca290f3610f6237dcb2d9696f8bcb8 100644 (file)
@@ -56,11 +56,30 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
     Node g = tds->mkGeneric(dt, i, pre, false);
     Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
     d_gen_terms[i] = g;
+    // is the operator a lambda of the form (lambda x1...xn. f(x1...xn))?
+    bool lamInOrder = false;
+    if (sop.getKind() == LAMBDA && sop[0].getNumChildren() == sop[1].getNumChildren())
+    {
+      Assert(g.getNumChildren()==sop[0].getNumChildren());
+      lamInOrder = true;
+      for (size_t j = 0, nchild = sop[1].getNumChildren(); j < nchild; j++)
+      {
+        if (sop[0][j] != sop[1][j])
+        {
+          // arguments not in order
+          lamInOrder = false;
+          break;
+        }
+      }
+    }
     // a list of variants of the generic term (see getGenericList).
     std::vector<Node> glist;
-    if (sop.isConst() || sop.getKind() == LAMBDA)
+    if (lamInOrder)
     {
-      Assert(g.getNumChildren() == dt[i].getNumArgs());
+      // If it is a lambda whose arguments are one-to-one with the datatype
+      // arguments, then we can add variants of this operator by permuting
+      // the argument list (see getGenericList).
+      Assert(g.getNumChildren()==dt[i].getNumArgs());
       for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
       {
         pre[j] = g[j];