Introduction to Program Synthesis

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

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 BottomUpEnumerator.jl, Question2.jl, and question3.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 BottomUpEnumerator.jl).

Setup instructions

First, you should install julia using the instructions here. Then, install the packages you will need for this assignment by running the following commands in the julia REPL: julia> import Pkg julia> Pkg.add("MLStyle") julia> Pkg.add("Images") After you have done this you should be able to run the internal tests and see that they pass, as such: $ julia test/runtests.jl internal Test Summary: | Pass Total internal | 1 1

Problem 1 (40 pts)

The goal of this assignment is for you to experiment with some of the bottom up inductive synthesis algorithm discussed in class. The code defining the language and interpreter is in the `src` directory, under `Combinata.jl` and `Interpreter.jl`. You should only modify the `BottomUpEnumerator.jl` file; you will submit only this file for Question 1. We have defined a simple language for the following expressions: Coordinate := | Coordinate(int, int)................// a coordinate in the plane. Coordinates must be between 0 and MAX_COORD shape := | Rect(Coordinate, Coordinate)........// a rectangle with the given lower left and top right coordinates | Triangle(Coordinate, Coordinate)....// the triangle represented by the bottom right half of the equivalent Rect | Circle(Coordinate, int).............// a circle with the given center and radius. Must have nonzero area | SUnion(Shape, Shape)................// the set-union of two shapes | SIntersection(Shape, Shape).........// the set-intersection of two shapes | Mirror(Shape).......................// the union of a shape with its mirror image across the line y=x 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. Make sure to use make_coord, make_rect, make_triangle, and make_circle rather than calling the constructors directly. These functions will check that the coordinates are valid and throw an error if they are not. To see examples of how to render shapes for debugging, you can look at the Render.jl file, specifically the function render_examples.

Problem 1a

As a starter task, implement the function grow in BottomUpEnumerator.jl. This function takes a list of shapes and returns a list of shapes containing - all the shapes in the input list - all the shapes that can be obtained by applying one of the constructors to two shapes in the input list You can test your implementation by running the following command on your command line: $ julia test/runtests.jl question-1a

Problem 1b

Your goal is now to implement a new the rest of the bottom up enumeration algorithm. Specifically, implement elim_equivalents, which takes a list of shapes and returns a list of shapes containing all the shapes in the input list, but with all equivalent shapes removed. Two shapes are equivalent if they have the same input/output behavior on the given points. The Dict feature in Julia will be useful for this task.

Then, implement synthesize, which takes a list of input/output pairs and returns a shape that matches the input/output pairs.

You can test your implementation by running the following command on your command line:

$ julia test/runtests.jl question-1b

Many of these tests might take several seconds, but not much longer. The entire question-1b suite takes 90 seconds on Kavi's laptop. If your tests are taking much longer than this (> 5 minutes), you should consider revising your implementation.

Hint for the test flipped_triangle: make sure that the Context independent equivalence property holds for your implementation.

Problem 2 (30 pts)

Consider the following grammar for a problem: term:= last2Digits(x + ??) || last3Digits(x + ??) || last4Digits(x + ??) || last5Digits(x + ??) prog:= term ++ term ++ term ++ term For example, the program last2Digits(x + 3) ++ last3Digits(x + 537) ++ last4Digits(x + 82) ++ last5Digits(x + 87) applied to 9928 should return 31465001010015 (31 ++ 465 ++ 0010 ++ 100015) 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 tuple of Int64, String). The function should return an AST for the synthesized program using the same format as example_lkd. 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:

You can test your implementation by running the following command on your command line: $ julia test/runtests.jl question-2

Problem 3 (30 pts)

For this problem, you will be using Sketch to answer some of the questions about a new language. You should download the latest version of sketch from here . Note: do not follow the build instructions. Just unzip the file, and then run the binary located at sketch-frontend/sketch. You will find the sketch language reference useful.

We have defined a simple arithmetic 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 Starter code for this assignment is provided in question3.sk

Problem 3.a

Encode the arithmetic grammar from above 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

We add the constraints 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.