rosette.rkt

#lang rosette/safe


(require rosette/lib/angelic    ; provides `choose*`
         rosette/lib/destruct)  ; provides `destruct`
; Tell Rosette we really do want to use integers.
(current-bitwidth #f)



; Compute the absolute value of `x`.
(define (absv x)
  (if (< x 0) (- x) x))

; Define a symbolic variable called y of type integer.
(define-symbolic y integer?)

; Solve a constraint saying |y| = 5.
(solve
 (assert (= (absv y) 5)))


; Try to outsmart Rosette by asking for the impossible:
(solve (assert (< (absv y) 0)))


; Syntax for our simple DSL
(struct plus (left right) #:transparent)
(struct mul (left right) #:transparent)
(struct square (arg) #:transparent)


; A simple program
(define prog (plus (square 7) 3))


; Interpreter for our DSL.
; We just recurse on the program's syntax using pattern matching.
(define (interpret p)
  (destruct p
    [(plus a b)  (+ (interpret a) (interpret b))]
    [(mul a b)   (* (interpret a) (interpret b))]
    [(square a)  (expt (interpret a) 2)]
    [_ p]))


; (plus (square 7) 3) evaluates to 52.
(interpret prog)


; Our interpreter works on symbolic values, too.
(define-symbolic z integer?)
(interpret (square (plus z 2)))


; So we can search for a `z` that makes (z+2)^2 = 25
(solve 
  (assert 
    (= (interpret (square (plus z 2))) 25)))


; Our intepreter works even if the expression itself is symbolic
(define-symbolic b boolean?)
(define expr (if b (plus z z) (mul z z)))
(interpret expr)


; Find a program equivalent to `(square z)` for *every* z.
(synthesize
 #:forall (list z)
 #:guarantee (assert (= (interpret expr) (interpret (square z)))))


; Create an unknown expression -- one that can evaluate to several
; possible values.
(define (??expr a b c)
  (define left (choose* a b c))
  (define right (choose* a b c))
  (choose* (plus left right) (mul left right) left))


; Create a sketch representing all programs of the form (plus ?? ??),
; where the ??s are unknown expressions created by ??expr.
(define-symbolic p q integer?)
(define sketch
  (plus (??expr z p q) (??expr z p q)))


; Solve the sketch to find a program equivalent to 10*z,
; but of the form (plus ?? ??). Save the resulting model.
(define M
  (synthesize
   #:forall (list z)
   #:guarantee (assert (= (interpret sketch) (interpret (mul 10 z))))))


; Substitute the bindings in M into the sketch to get back the
; synthesized program.
(evaluate sketch M)