Excerpts from The Rosette Guide.
(define-symbolic b boolean?)
(define (check-mid impl lo hi) ; Assuming that (assume (bvsle (int32 0) lo)) ; 0 ≤ lo and (assume (bvsle lo hi)) ; lo ≤ hi, (define mi (impl lo hi)) ; and letting mi = impl(lo, hi) and (define diff ; diff = (hi - mi) - (mi - lo), (bvsub (bvsub hi mi) (bvsub mi lo))) ; we require that (assert (bvsle lo mi)) ; lo ≤ mi, (assert (bvsle mi hi)) ; mi ≤ hi, (assert (bvsle (int32 0) diff)) ; 0 ≤ diff, and (assert (bvsle diff (int32 1)))) ; diff ≤ 1.
(define-symbolic l h int32?) (define cex (verify (check-mid bvmid l h)))
(require rosette/lib/synthax) ; Require the sketching library. (define-grammar (fast-int32 x y) ; Grammar of int32 expressions over two inputs: [expr (choose x y (?? int32?) ; <expr> := x | y | <32-bit integer constant> | ((bop) (expr) (expr)) ; (<bop> <expr> <expr>) | ((uop) (expr)))] ; (<uop> <expr>) [bop (choose bvadd bvsub bvand ; <bop> := bvadd | bvsub | bvand | bvor bvxor bvshl ; bvor | bvxor | bvshl | bvlshr bvashr)] ; bvlshr | bvashr [uop (choose bvneg bvnot)]) ; <uop> := bvneg | bvnot
(let () (define-symbolic id int32?) id)
(choose bvneg bvnot):
(if (?? boolean?) bvneg bvnot)
(define sol (synthesize #:forall (list l h) #:guarantee (check-mid bvmid-fast l h))) (print-forms sol)
(define (bvmid-fast lo hi) (bvlshr (bvadd hi lo) (bv 1 32))) (define sol (solve (begin (assume (not (equal? l h))) (assume (bvsle (int32 0) l)) (assume (bvsle l h)) (assert (equal? (bvand l h) (bvmid-fast l h))))))
With this setting, integers (and reals) are treated as infinite precision values during evaluation, but when solving queries, they are translated to bitvectors of length
k for better performance.
In general, recursion terminates under symbolic evaluation only when the stopping condition is reached with concrete values.
define-symbolic*: creates a stream of distinct symbolic constants
Assertions and Assumptions
VC: track of all assertions and assumptions
(verify expr) searches for a model of the formula
(vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ ¬ (vc-asserts Q)
P is the verification condition before the call to verify,
Q is the verification condition generated by evaluating
(synthesize input expr)
(solve expr) searches for a model of the formula
(vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ (vc-asserts Q)
(solve+) Returns a stateful procedure that uses a fresh
solver? instance to incrementally solve a sequence of constraints.
> (define-symbolic x y integer?) > (define inc (solve+)) > (inc (< x y)) ; Push (< x y) and solve. (model [x 0] [y 1]) > (inc (> x 5)) ; Push (> x 5) and solve. (model [x 6] [y 7]) > (inc (< y 4)) ; Push (< y 4) and solve. (unsat) > (inc 1) ; Pop (< y 4) and solve. (model [x 6] [y 7])
(define-symbolic x y integer?) ; This query maximizes x + y while ensuring that y - x < 1 whenever x < 2: (optimize #:maximize (list (+ x y)) #:guarantee (begin (assume (< x 2)) (assert (< (- y x) 1))))