This tutorial is a short introduction to using Rosette for program synthesis. You should start by following the Getting Started part of the guide. You will be required to install Racket (version > 7.0) and use the package manager of Racket to install Rosette. To interact with Rosette, we will have to write Racket programs, which you might have learned to do in CSC324. But don't worry if you haven't, our use of Racket will be limited and you only need to know how to write simple functions and expressions.
This short video is meant to be an introduction to the syntax of the language used in the tutorial. You do not need an advanced knowledge of Racket to understand the tutorial, only an understanding of the syntax, and a basic understanding of what being a functional language means. If you have taken CSC324 before, you can safely skip this.
The video is also available on MyMedia for UofT students.
Now we can focus on progam synthesis. In the video tutorial below, we intrdouce you to syntax-guided synthesis using Rosette. In order to follow this tutorial, you need to have Rosette installed. The editor used in the demo is Emacs, but feel free to use your editor of choice. If you use DrRacket, you can directly run the examples from your editor.
The video is also available on MyMedia for UofT students.
Note: in the tutorial I used a version of Rosette installed before May 2020. In the current version, the first example of the tutorial does not seem to work. You can get around that problem by replacing one of the (??) by a 3.
Rosette has an excellent documentation, the Rosette Guide. We are interested in the synthesis part (Sections 2.3.3, 3.2.5 and 6.2.2) but the section defining the built-in datatypes will also be useful to you.
You can also have a look at last year's tutorial on Github. However, be cautious with the example used here. Because of the use of non-linear arithmetic, the synthesis times can increase dramatically for seemingly innocuous changes in the expression grammar.