From d6f99b015e8879229b8599316e19b5467863db2f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Mar 2020 21:20:32 -0500 Subject: [PATCH] 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 . --- .../quantifiers/sygus/sygus_grammar_red.cpp | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) 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 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]; -- 2.30.2