Tool for synthesizing programs that meet some requirement

Requirements:
-------------
1. Yices2 -- EFSMT solver
   Send email to bruno@csl.sri.com for obtaining the EFSMT Yices2 solver
   
   The publicly available Yices2 release (yices.csl.sri.com)
   does not contain the EFSMT solver component yet.  
   
   The toplevel pythons program invokes yices using the command:
     "yices_main --mode=ef"
   Hence, yices2 must be properly installed so that the above 
   command works.

2. Python 
   With pyparsing installed
   Also need the s-expression parser sexpParser.py


How to run the tool:
--------------------
1. Create a sketch
   For example, see file oeap.sketch
   A second example can be found in ot.sketch

2. Run the program thus:
   python prog_synth.py oeap.sketch na=4 nb=4 answers=8
   or
   python prog_synth.py ot.sketch nite1=2 nc=2 answers=1

Details:
--------
prog_synth.py: Converts input <filename.sketch> into a 
 EF-Yices formula (stored as synth.ys)
 It then calls the yices ef-solver on synth.ys
 Output is stored in synth.yout


Documentation:
--------------
See report.pdf