On this page:
The Rosette Guide
8.3

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 and Assumptions

      2.3 Solver-Aided Queries

        2.3.1 Verification

        2.3.2 Synthesis

        2.3.3 Angelic Execution

      2.4 Symbolic Reasoning

        2.4.1 Mixing Theories

        2.4.2 Reasoning Precision

        2.4.3 Symbolic Evaluation

    3 Syntactic Forms

      3.1 Lifted Racket Forms

      3.2 Solver-Aided Forms

        3.2.1 Symbolic Constants

        3.2.2 Assertions and Assumptions

        3.2.3 Verification

        3.2.4 Synthesis

        3.2.5 Angelic Execution

        3.2.6 Optimization

        3.2.7 Reasoning Precision

    4 Built-In Datatypes

      4.1 Equality

      4.2 Booleans, Integers, and Reals

        4.2.1 Additional Logical Operators

        4.2.2 Quantifiers

      4.3 Bitvectors

        4.3.1 Comparison Operators

        4.3.2 Bitwise Operators

        4.3.3 Arithmetic Operators

        4.3.4 Conversion Operators

        4.3.5 Additional Operators

      4.4 Uninterpreted Functions

      4.5 Procedures

      4.6 Pairs and Lists

        4.6.1 Lifted Operations on Pairs and Lists

        4.6.2 Additional Operations on Pairs and Lists

      4.7 Vectors

        4.7.1 Lifted Operations on Vectors

        4.7.2 Additional Operations on Vectors

      4.8 Boxes

      4.9 Solvers and Solutions

        4.9.1 The Solver Interface

        4.9.2 Supported Solvers

          4.9.2.1 Z3

          4.9.2.2 CVC4

          4.9.2.3 Boolector

        4.9.3 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.3 Utility Libraries

        6.3.1 Value Destructuring Library

        6.3.2 Value Browser Library

          6.3.2.1 Layout

          6.3.2.2 Examples

    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

        7.2.1 Verification Conditions

        7.2.2 Symbolic Heap

    8 Unsafe Operations

    9 Performance

      9.1 Common Performance Issues

        9.1.1 Integer and Real Theories

        9.1.2 Algorithmic Mismatch

        9.1.3 Irregular Representation

        9.1.4 Missed Concretization

      9.2 Symbolic Profiling

        9.2.1 Options and Caveats

      9.3 Walkthrough: Debugging Rosette Performance

        9.3.1 Performance Bottlenecks

    10 Debugging

      10.1 Common Bugs in Solver-Aided Code

        10.1.1 Bugs Due to Exceptions in Solver-Aided Queries

        10.1.2 Bugs Due to Exceptions in Conditionals

      10.2 Error Tracer

        10.2.1 Options and Caveats

      10.3 Walkthrough: Tracing Errors in Rosette

    11 References

    Index