Convert SyGuS files to CHCs on the fly

SemGuS-git / Semgus-Parser

Library and tool for parsing SemGuS specifications

MIT License

4 stars 1 forks source link

Closed kjcjohnson closed 2 years ago

kjcjohnson commented 2 years ago

This is a complicated one. We want to be able to read in a SyGuS (v2) file and output as if it were a SemGuS file. The three main hurdles are:

Generating term types and CHCs on-the-fly from grammar blocks
Adding universally quantified variables (via declare-var) to constraints
Rewriting constraints to transform calls to the SyGuS function into an equivalent SemGuS relation

kjcjohnson commented 2 years ago

Merging in now. Might as well start it being used.