Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
#lang rosette/safe
(require rosette/lib/angelic ; provides `choose*`
rosette/lib/match) ; provides `match`
; 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.
(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)
(match 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
(= (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.
#: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
#: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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.