- Notifications
You must be signed in to change notification settings - Fork1
SyGuS solver for programming-by-example
License
NotificationsYou must be signed in to change notification settings
sygus-tools/tychon
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
An enumerative SyGuS solver for programming-by-example (PBE).
Tychon (currently e3solver) builds on the original enumerativesolver andcontributes several features. Our main addition is an optimized mode forprogramming-by-example. In this mode, we use decision tree unification in orderto incrementally find an expression consistent with all examples.
More details can be found in thisreportandslides.
The project has three main branches:
original-esolver. Where we keep the original esolver.constraint-unified. Where we apply basic fixes to esolver in order to make itsolve PBE problems.master. Where we merged our latest improved version for PBE.
We have the following dependencies:
- Boost libraries
systemandprogram_options - z3 library
- Our version of synthlib2parser which can be foundhere