8.12

7 Symbolic Reflection🔗ℹ

This chapter describes symbolic reflection, a mechanism for manipulating the representation of symbolic values (Section 7.1) and the state of the symbolic evaluation from within a Rosette program (Section 7.2). Symbolic reflection has three main applications: (1) lifting additional Racket constructs to work with symbolic values; (2) guiding Rosette’s symbolic virtual machine to achieve better performance; and (3) implementing advanced solver-aided functionality.

    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