From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 24 Mar 2020 02:20:32 +0000 (-0500)
Subject: Restrict cases of sygus grammar reduction based on argument variants (#4131)
X-Git-Tag: cvc5-1.0.0~3451
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6f99b015e8879229b8599316e19b5467863db2f;p=cvc5.git

Restrict cases of sygus grammar reduction based on argument variants (#4131)

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 .
---

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index d9ce08d49..d865457c3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -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];