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 two Rosette libraries that provide additional facilities for solver-aided synthesis and debugging.

    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