8.12

3.1 Lifted Racket Forms🔗ℹ

Rosette lifts the following Racket forms:

Lifted forms have the same meaning in Rosette programs as they do in Racket programs. For example, the Racket expression (if test-expr then-expr else-expr) evaluates test-expr first and then, depending on the outcome, it returns the result of evaluating either then-expr or else-expr. Rosette preserves this interpretation of if for concrete values, and also extends it to work with symbolic values:
> (let ([y 0])
    (if #t (void) (set! y 3))
    (printf "y unchanged: ~a\n" y)
    (if #f (set! y 3) (void))
    (printf "y unchanged: ~a\n" y)
    (define-symbolic x boolean?)
    (if x (void) (set! y 3))
    (printf "y symbolic: ~a\n" y))

y unchanged: 0

y unchanged: 0

y symbolic: (ite x 0 3)