This is the code developed for the paper "Generating and Searching Families of FFT Algorithms." This code depends on Python (www.python.org) and SciPy (www.scipy.org). Boolector (http://fmv.jku.at/boolector/) is required to extract a witness FFT algorithm. This code has been tested under Linux, but should work on Windows and Mac OS X platforms. 

To generate benchmarks in SMT-LIB 2.0 format:

 * Make sure you have installed python and scipy
 * If necessary, edit the file fftlia and fftbv so that the first line points to your installed python
 * To generate QF_BV, execute: ./fftbv Sz32_456
 * To generate QF_LIA, execute: ./fftlia Sz32_lia
 
Multiple files, for all partitions required to search the FFT, will be generated with suffix .smt2. Execute the scripts ./fftbv or ./fftlia with no arguments to see valid templates and usage.


To generate and test a witness FFT algorithm if possible:

 * Make sure you have installed python, scipy and boolector.
 * Make sure that boolector is in your path.
 * Edit the file fftsearch so that the first line points to your installed python.
 * Execute: ./fftsearch Sz32_456
 
The following files should be generated:
 * Sz32_456_*.smt (SMTLIB 1.2 files for all partitions searched in the FFT)
 * Sz32_456_*.txt (Solutions from the Boolector run for each partition)
 
If all partitions were SAT, the file Sz32_456.py will also be generated and executed. This is a witness instance for the searched FFT.
 
Execute ./fftsearch with no arguments to see valid templates and usage.

For those interested in more details or help with using this code, please contact the authors at steve@softerhardware.com.







