Component-based program synthesis using SBV.

Given a library of available componen functions, synthesize a program implementing a specification.

Component-based synthesis of loop-free programs

This package implements a library for synthesizing programs as described in the Component-based Synthesis Applied to Bitvector Programs paper. It uses an off-the-shelf SMT solver via sbv library.

See Examples.hs file to quickly get at how to use this. For deeper understanding of library's internals see the Haddock documentation.

The code is structured and commented in such way that it follows variable naming of the original paper.