1 Getting Started
Rosette is a solver-aided programming system with two components:
A programming language that extends a subset of Racket with constructs for accessing a constraint solver. With the solver’s help, Rosette can answer interesting questions about programs—
such as, whether they are buggy and if so, how to repair them. A symbolic virtual machine (SVM) that executes Rosette programs and compiles them to logical constraints. The SVM enables Rosette to use the solver to automatically reason about program behaviors.
The name "Rosette" refers both to the language and the whole system.
1.1 Installing Rosette
To install Rosette, you will need to
Download and install Racket (version 7.0 or later).
- Use Racket’s raco tool to install Rosette:
> raco pkg install rosette
1.2 Interacting with Rosette
You can interact with Rosette programs just as you would with Racket programs: either through the DrRacket IDE or through the racket command-line interpreter. We suggest that you use DrRacket, especially at the beginning.
Example Rosette programs can be found in the rosette/sdsl folder. Most of these are implemented in solver-aided domain-specific languages (SDSLs) that are embedded in the Rosette language. To interact with an example program, open it in DrRacket and hit Run!
1.3 Rosette Dialects
The Rosette system ships with two dialects of the Rosette language:
a safe dialect, which is used throughout this guide, and
an unsafe dialect, which is briefly described in the last chapter.
To use the safe dialect, start your programs with the following line:
To use the unsafe dialect, type this line instead:
We strongly recommend that you start with the safe dialect, which includes a core subset of Racket. The unsafe dialect includes all of Racket, but unless you understand and observe the restrictions on using non-core features, your seemingly correct programs may crash or produce unexpected results.