6 Libraries

Chapters 1-5 introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by rosette/safe, as well as Rosette libraries that provide additional facilities for solver-aided development.

    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 Destructuring Library

      6.3.2 Value Browser Library Layout Examples