Introduction to Program Synthesis

© Armando Solar-Lezama. 2018. All rights reserved.

Assignment 2

Submission Instructions This assignment is due at 5pm on the date indicated in the class calendar. In order to submit your code, pack each requested file into a tar file and submit through Canvas (we will create a Canvas assignment as the deadline approaches).

Collaboration policy You are allowed to consult with at most one other student while working on the pset, but every student is responsible for writing their own code and submitting their own work. If you do consult with another student, you should explicitly acknowledge them in your submission (you can do that in a comment in question1a.sk).

Problem 1 (30 pts)

For this problem, you will be encoding an arithmetic language in Sketch to synthesize expressions matching input output examples. You should download the latest version of sketch from here. Note: unless you run into issues, do not follow the build instructions. Just unzip the file, and then run the binary located at sketch-frontend/sketch. On some operating systems (e.g. one TA's M1 Mac) you may need to follow the build instructions. To test that your installation is working, you may find it useful to ensure that the first example sketch (doubleSketch) from the manual works.

Consider the following simple arithmetic language:

Int := | n.................................// numeric constant | x.................................// variable | Plus(int, int):int................// addition | Times(int, int):int...............// multiplication | ITE(bool, int, int):int...........// if-then-else Bool := | false.............................// constant false | true..............................// constant true | Lt(int, int):bool.................// less than | Not(bool):bool....................// boolean negation | And(bool, bool):bool..............// boolean conjunction

Problem 1.a

Encode the arithmetic grammar from above as a generator in Sketch, using it to synthesize functions solving the following examples: x=5, y=5, out=15; x=8, y=3, out=14; x=1234, y=227, out=1688; And x=10, y=7, out=17 x=4, y=7, out=-7 x=10, y=3, out=13 x=1, y=-7, out=-6 x=1, y=8, out=-8 Starter code for this problem can be found here. You will find the sketch language reference useful. Submit your code as question1a.sk.

Problem 1.b

In a copy of the file, add the following constraints: Submit your code as question1b.sk.

Problems 2-3

Apologies for the delay, we will post the remaining problems shortly.