search

muraliadithya / mini-sygus

a constraint-based syntax-guided synthesis (SyGuS) engine
9 stars 0 forks source link

Making cleanup branch functional #12

Closed muraliadithya closed 3 years ago

muraliadithya commented 3 years ago

The cleanup branch has all the necessary modules for creating a sygus solver. This needs to be combined with (i) reading a sygus file (ii) finding and replacing the synth-fun commands and then (iii) running the file using an SMT solver, getting valuations for boolean variables and finally (iv) using them to output a yield of the grammar satisfying the synthesis constraints.

eionblanc commented 3 years ago

A current example of full functionality is shown via the following terminal command: python3 -m src.engine 'data/out_sdlist-dlist-and-slist.sy'