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 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