diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-23 17:12:56 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-23 17:12:56 -0500 |
| commit | 591b704fa2e02adf2f192c3480e7b0393ed5daf9 (patch) | |
| tree | 4b6904e299caaa39ce04319c930235703bb163d8 /src/options | |
| parent | df7333de4436d846da70857e61cda411d22d02ba (diff) | |
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).
Diffstat (limited to 'src/options')
0 files changed, 0 insertions, 0 deletions