4 Built-In Datatypes

The previous chapter describes the Racket syntax forms that are lifted by Rosette to work on symbolic values. This chapter describes the lifted datatypes and their corresponding operations. Most lifted operations retain their Racket semantics, with the exception of equality predicates (Section 4.1) and numeric operations (Section 4.2).

Rosette distinguishes between two kinds of built-in datatypes: solvable and unsolvable. Solvable types are (efficiently) supported by SMT solvers, and they include booleans, integers, reals, bitvectors, and uninterpreted functions. All other built-in types are unsolvable—that is, not as well supported by SMT solvers.

Every lifted type is equipped with a predicate (e.g., boolean?) that recognizes values of that type. Solvable types are themselves recognized by the solvable? predicate. Lifted types include both concrete Racket values and symbolic Rosette values, but only solvable types include symbolic constants, as introduced by define-symbolic[*].