projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 591b704) | patch
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)
commitd6f99b015e8879229b8599316e19b5467863db2f
tree1d913fea831b02f466afb738f194ecc343434286tree
parent591b704fa2e02adf2f192c3480e7b0393ed5daf9commit | diff
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 .
src/theory/quantifiers/sygus/sygus_grammar_red.cpp diff | blob | history