Introduction to Program Synthesis

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

Assignment 1

Clarifications: For problem 2, you can assume the inputs will be given to you in order in order to give a linear algorithm. Alternatively, we will give full credit if you can give an $n~log(n)$ algorithm.

Late submissions: Any late submission will be given a 5% penalty for every 24 hour delay. So if you turn in $n$ days late, your grade will be multiplied by $.95^n$.

Submission Instructions This assignment is due at 5pm on the date indicated in the class calendar. The starter code for the assignment can be found here. In order to submit your code, pack your Assignment1.js, default.html, question3.sk and question3c.sk files into a tar file and submit through this form. The form asks for the URL from where you can download your code. We will be downloading from all the URLs people submit shortly after 5pm on the due date.

Problem 1 (40 pts)

The goal of this assignment is for you to experiment with some of the different inductive synthesis approaches discussed in class. All the starter code for this assignment is in a file called Assignment1.js; there is also a file default.html that you can use to run the code. We have defined a simple language for the following expressions: expr:= num(int n).....................// numeric constant num:int | flse()...........................// constant FALSE. Unfortunately ,we can't call it false | vr(string varname)...............// variable var:int | plus(expr left, expr right)......// arithmetic expressions plus and times | times(expr left, expr right).....// plus(int,int):int times(int, int):int | lt(expr left, expr right)........//less than operator lt(int, int):int | and(expr left, expr right).......// boolean operators and(bool,bool):bool | not(expr left)...................// not(bool):bool | ite(expr cond, expr tcase, expr fcase)...// if-then-else; ite(bool, int, int):int As part of the starter code for this project, we have included constructors for all the different AST nodes, as well as a basic interpreter that you can use to evaluate expressions in this language. Note that even though all the AST nodes are of type expr, the language they represent has a not-quite-trivial type system on top of it.

Problem 1a

One of the shortcomings of the bottom-up algorithm as described in class is that it fails to properly account for the types of expressions. In assembling expressions from sub-expressions, it is important to make sure that only valid expressions are ever constructed. Your goal for this first exercise is to implement a version of the algorithm that properly accounts for the types of sub-expressions when assembling new expressions. Your synthesis function should have the following interface: function bottomUp(globalBnd, intOps, boolOps, vars, consts, inputoutput) The interface includes a few tests that you can use to sanity check your implementation. It's a good idea to add your own.

Problem 1b

Your goal is now to implement a new function. function bottomUpFaster(globalBnd, intOps, boolOps, vars, consts, inputoutput) that exploits the following additional constraints:

Problem 2 (30 pts)

Clarification: you can assume the inputs will be given to you in order in order to give a linear algorithm. Alternatively, we will give full credit if you can give an $n~log(n)$ algorithm. Consider the following grammar for a problem: term:= 2*x + ?? | x*x + ?? | 3*x + ?? prog:= if(x < ??){ return term; } else if(x < ??){ return term; } else if(x < ??){ return term; } else { return term; } The question marks ?? indicate unknown constants. You should assume the function operates only over the integers. Even though the space of potential expression is very large, the search space has a lot of structure. Our goal for this problem is to come up with a representation of the search space and a search strategy that exploits this structure and allows us to efficiently solve for a program in this space given a set of input/output pairs. In particular, the goal is to find a way to factor the search so it is possible to solve for the unknowns without having to search the exponentially large space.

Hints:

So your goal is to implement a function with the interface below. function structured(inputoutputs) Where inputoutputs is a list of input output pairs (each input/output pair represented as a list of size 2). The function should return an AST for the synthesized program using the same AST nodes from Problem 1. The key requirement is that your function should execute in linear time with respect to the size of this input list. Your code should be well commented to clearly explain why your algorithm is linear time and complete (guaranteed to find a solution if one exists).

Problem 3 (30 pts)

For this problem, you will be using Sketch to answer some of the questions from problem 1. You should download the latest version of sketch from here . You will find the sketch language reference useful. Starter code for this assignment is provided in question3.sk

Problem 3.a

Encode the grammar from problem 1 as a generator in Sketch.

Problem 3.b

Use your generator to synthesize expressions for 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

Problem 3.c

Write a generator that imposes the restrictions from problem 1b and run 3.b again. How do the results compare? (this should be submitted as a separate file question3c.sk).

Problem 3.d

Experiment with different flags to speed up the search. Your submitted code should use the pragma options directive to include the flags that give you the best performance.