On this page:
The Rosette Guide
6.6

The Rosette Guide

Emina Torlak

This document is intended both as an introduction to solver-aided programming with Rosette, and as a reference manual for the Rosette language. It assumes Racket programming experience, so if you are unfamiliar with Racket, you may want to start by reading The Racket Guide.

Chapters 1 and 2 introduce the Rosette system and illustrate the key concepts of solver-aided programming. Chapters 3-6 define the core Rosette language (rosette/safe) and describe its main libraries. Chapter 7 and 8 describe the advanced features of the full language (rosette). If you are new to Rosette, consider starting with the core language. The full language is richer than the core, but it can also be harder to use.

 #lang rosette/safe package: rosette
 #lang rosette

    1 Getting Started

      1.1 Installing Rosette

      1.2 Interacting with Rosette

      1.3 Rosette Dialects

    2 Rosette Essentials

      2.1 Symbolic Values

      2.2 Assertions

      2.3 Solver-Aided Queries

        2.3.1 Verification

        2.3.2 Debugging

        2.3.3 Synthesis

        2.3.4 Angelic Execution

      2.4 Symbolic Reasoning

    3 Syntactic Forms

      3.1 Lifted Racket Forms

      3.2 Solver-Aided Forms

        3.2.1 Symbolic Constants

        3.2.2 Assertions

        3.2.3 Angelic Execution

        3.2.4 Verification

        3.2.5 Synthesis

        3.2.6 Optimization

        3.2.7 Debugging

        3.2.8 Reasoning Precision

    4 Built-In Datatypes

      4.1 Equality

      4.2 Booleans, Integers, and Reals

        4.2.1 Additional Logical Operators

      4.3 Bitvectors

        4.3.1 Comparison Operators

        4.3.2 Bitwise Operators

        4.3.3 Arithmetic Operators

        4.3.4 Conversion Operators

      4.4 Uninterpreted Functions

      4.5 Procedures

      4.6 Pairs and Lists

      4.7 Vectors

      4.8 Boxes

      4.9 Solvers and Solutions

        4.9.1 The Solver Interface

        4.9.2 Solutions

    5 Structures

    6 Libraries

      6.1 Exported Racket Libraries

      6.2 Solver-Aided Libraries

        6.2.1 Synthesis Library

        6.2.2 Angelic Execution Library

        6.2.3 Debugging Library

    7 Symbolic Reflection

      7.1 Reflecting on Symbolic Values

        7.1.1 Symbolic Terms

        7.1.2 Symbolic Unions

        7.1.3 Symbolic Lifting

      7.2 Reflecting on Symbolic State

    8 Unsafe Operations

    9 References

    Index