7.1 Reflecting on Symbolic Values🔗ℹ

There are two kinds of symbolic values in Rosette: symbolic terms and symbolic unions. A Rosette program can inspect the representation of both kinds of values. This is useful for lifting additional (unlifted) Racket procedures to work on symbolic values, and for controlling the performance of Rosette’s symbolic evaluator.

7.1.1 Symbolic Terms🔗ℹ

A symbolic term is either a symbolic constant, created via define-symbolic[*], or a symbolic expression, produced by a lifted operator. Terms are strongly typed, and always belong to a solvable type. Symbolic values of all other (unsolvable) types take the form of symbolic unions.

7.1.2 Symbolic Unions🔗ℹ

Rosette represents symbolic values of an unsolvable type (e.g., list?) as symbolic unions. A symbolic union is a set of two or more guarded values. A guarded value, in turn, combines a guard, which is a symbolic boolean? term, and a (non-union) value. Rosette’s symbolic evaluator guarantees that the guards in a symbolic union are disjoint: only one of them can ever be true. For example, the symbolic vector s defined below is represented as a symbolic union of two guarded vectors:

> (define-symbolic b boolean?)

> (define v (vector 1))

> (define w (vector 2 3))

> (define s (if b v w))

> s

(union [b #(1)] [(! b) #(2 3)])

> (type-of s)

vector?

> (eq? s v)

b

> (eq? s w)

(! b)

The values that appear in a union are themselves never unions. They may, however, contain unions. They may also belong to several different types. In that case, the type of the union is the most specific type? predicate that accepts all members of the union. This will always be an unsolvable type—possibly any/c, the most general unsolvable type.

> (define-symbolic b boolean?)

> (define-symbolic c boolean?)

> (define v (if c "c" 0))

> (define u (if b (vector v) 4))

> u

(union [b #((union #:size 2 #:hash 736602544239193347))] [(! b) 4])

> (type-of u)

any/c

> (union-contents u)

(list (cons b '#((union [c c] [(! c) 0]))) (cons (! b) 4))

Symbolic unions are recognized by the union? predicate, and Rosette programs can inspect union contents using the union-contents procedure. Applications may use union? and union-contents directly to lift Racket code to work on symbolic unions, but Rosette also provides dedicated lifting constructs, described in the next section, to make this process easier and the resulting lifted code more efficient.

7.1.3 Symbolic Lifting🔗ℹ

Rosette provides a construct, for/all, for controlling how symbolic evaluation is performed. This construct is built into the language. It is used internally by Rosette to lift operations on unsolvable types. Rosette programs can also use it for this purpose, as well as for tuning the performance of symbolic evaluation.

The keyword #:exhaustive controls the decomposition of V.

When #:exhaustive is omitted, V is decomposed into (union-contents V) if it is a symbolic union. Otherwise, it is decomposed trivially into (list (cons #t V)).

When #:exhaustive is included, V is decomposed into its constituent guard-value pairs recursively if it is either a union or a conditional symbolic term. Otherwise, it is decomposed trivally.

Programs can use for/all to lift pure Racket procedures to work on symbolic values and to control the performance of Rosette’s symbolic evaluation.

For example, the following snippet shows how to use for/all to lift string-length to work on symbolic strings. This approach generalizes to all unlifted datatypes, since their symbolic representation is always a union of guarded concrete values.

(require (only-in racket [string-length racket/string-length]))

(define (string-length value)   (for/all ([str value])     (racket/string-length str)))

> (string-length "abababa")

7

> (string-length 3)

string-length: contract violation

expected: string?

given: 3

> (define-symbolic b boolean?)

> (string-length (if b "a" "abababa"))

(ite b 1 7)

> (vc)

(vc #t #t)

> (string-length (if b "a" 3))

1

> (vc)

(vc #t b)

> (clear-vc!)

Here is also an example of using for/all for performance tuning. Note that adding for/alls in too many places, or in the wrong places, will lead to worse performance. Profiling is the best way to determine whether and where to insert them.

(require (only-in racket build-list))

(define (vector-update! v idx proc)  ; v[idx] := proc(v[idx])   (vector-set! v idx (proc (vector-ref v idx))))

(define (vector-update!! v idx proc)   (for/all ([idx idx #:exhaustive])  ; Split paths based on idx.     (vector-update! v idx proc)))

> (define-symbolic a b boolean?)

> (define idx (if a 0 (if b 5 10)))

> (define limit 10000)

> (define vals (build-list limit identity)) ; '(0 1 ... 9999)

; vector-update! is 2 orders of magnitude slower than

; vector-update!! on the following tests.

; By default, Rosette treats idx as an opaque symbolic

; integer when evaluating vector-update!, so it must

; account for the possibility of idx taking on any value

; between 0 and limit. The for/all in vector-update!!

; instructs Rosette to split the index and consider only

; the values that idx can in fact take on: 0, 5, 10.

> (define v0 (list->vector vals))

> (time (vector-update! v0 idx add1))

cpu time: 389 real time: 395 gc time: 14

> (define v1 (list->vector vals))

> (time (vector-update!! v1 idx add1))

cpu time: 0 real time: 0 gc time: 0

; But the default evaluation strategry is better for indices

; that are fully symbolic conditional terms.

> (define-symbolic i0 i1 i2 i3 integer?)

> (define idx (if a (if b i0 i1) (if b i2 i3)))

> (define v2 (list->vector vals))

> (time (vector-update! v2 idx add1))

cpu time: 405 real time: 411 gc time: 16

> (define v3 (list->vector vals))

> (time (vector-update!! v3 idx add1))

cpu time: 3876 real time: 3901 gc time: 544