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.
(interpret (square (plus y 2)))
; So we can search for a `y` that makes (y+2)^2 = 25
(= (interpret (square (plus y 2))) 25)))
; Find values for `x` and `c` such that c*x = x+x.
; This is our first synthesis attempt, but it doesn't do what we want,
; which is to find a `c` that works for *every* x.
(define-symbolic x c integer?)
(= (interpret (mul c x)) (+ x x))))
; Find a `c` such that c*x = x+x for *every* x.
#:forall (list x)
#:guarantee (assert (= (interpret (mul c x)) (+ x x))))
; Create an unknown expression -- one that can evaluate to several
; possible values.
(define (??expr terminals)
(define a (apply choose* terminals))
(define b (apply choose* terminals))
(choose* (plus a b)
(mul a b)
(square a)
; 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 (list x p q)) (??expr (list x p q))))
; Solve the sketch to find a program equivalent to 10*x,
; but of the form (plus ?? ??). Save the resulting model.
(define M
#:forall (list x)
#:guarantee (assert (= (interpret sketch) (interpret (mul 10 x))))))
; 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