Assignment 1

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 stellar (we will post a link 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 Assignment1.js).

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: Node:= Num(int n).....................// numeric constant num:int | False()...........................// constant FALSE. | Var(string varname)...............// variable Var:int | Plus(Node left, Node right)......// arithmetic expressions plus and times | Times(Node left, Node right).....// Plus(int,int):int Times(int, int):int | Lt(Node left, Node right)........//less than operator Lt(int, int):bool | And(Node left, Node right).......// boolean operators And(bool,bool):bool | Not(Node left)...................// Not(bool):bool | Ite(Node cond, Node tcase, Node 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 Node, 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)

• globalBnd : A bound on the maximum depth allowed for the generated ASTs.
• intOps: A list of the integer AST nodes the generator is allowed to use.
• boolOps: A list of the boolean AST nodes the generator is allowed to use.
• vars: A list of all the variable names that can appear in the generated expressions.
• consts: A list of all the integer constants that can appear in the generated expressions.
• inputoutput: A list of inputs/outputs to the function. Each element in the list is a map from variable names to values; the variable "_out" maps to the expected output for that input.
• return value: An AST for an expression that satisfies all the input/output pairs. If none is found before reaching the globalBnd, then it should return the string "FAIL".

The interface includes a few tests that you can use to sanity check your implementation, but you should add some tests of 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:

• Multiplications can only occur between variables and constants or between two variables
• Comparisons cannot include any arithmetic, only variables and constants

Problem 2 (30 pts)

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.

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). Hints:

• Every input will be processed by exactly one term.
• For a given input, if we know what term it corresponds to, we can easily solve for the unknown in that term.
• We will give close to full credit if your solution assumes that the provided input/output pairs are sorted.
• A solution that has to iterate through the input list a large number of times is still linear time as long as the number of passes is bounded by a constant.

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.

Graduate Credit

If you are taking the class for graduate credit, you must also implement the following to get full credit for Part 1. If you are taking the class for undergraduate credit, you can complete this problem for 10 points of extra credit.

Problem 1.c

You must implement the STUN algorithm from lecture 3. The algorithm should search the arithmetic language from Problem 1.b with top level branches. You should provide an example that illustrates the ability of the algorithm to produce programs that could not be synthesized using the algorithms from 1.a and 1.b. function bottomUpFasterSTUN(globalBnd, vars, consts, inputoutput) The globalBnd parameter should now bound only the size of the arithmetic expressions, not of the overall program.

Hint: You should reuse your implementation from Problem 1.b to search for conditionals and arithmetic expressions.