▼The Rosette Guide
On this page:
The Rosette Guide
7.7
  top  ← prev  up  next → 

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.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.7 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.2.4 Yices

          4.9.2.5 CPLEX

        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.2.3 Debugging Library

      6.3 Utility Libraries

        6.3.1 Value Browser Library

          6.3.1.1 Layout

          6.3.1.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

    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 References

    Index

  top  ← prev  up  next →