6.2 Solver-Aided Libraries
In principle, solver-aided programming requires only symbolic values and the basic constructs described in Chapter 3. In practice, however, it is often convenient to work with richer constructs, which are built on top of these primitives. Rosette ships with three libraries that provide such constructs, as well as utility procedures for turning the results of synthesis and debugging queries into code.
6.2.1 Synthesis Library
| (require rosette/lib/synthax) | package: rosette |
syntax
(?? maybe-type)
maybe-type =
| type-expr
type-expr : (and/c solvable? type? (not/c function?))
syntax
(choose expr ...+)
syntax
(define-synthax id ([pattern expr] ...+))
(define-synthax (id terminal ... k) #:base base-expr #:else else-expr)
The first form, (define-synthax id ([pattern expr] ...+)), works like Racket’s syntax-rules macro: it fills the hole (id e ...) with the expression expr that corresponds to the first pattern matching the hole. The second form, (define-synthax (id terminal ... k) #:base base-expr #:else else-expr), defines a recursive grammar that is inlined a finite number of times to fill a hole. The base-expr usually chooses among the provided terminals, while the else-expr chooses among the terminals and a set of productions. The hole (id e ... k) must specify the inlining bound k as an integer literal.
; Defines a grammar for boolean expressions ; in negation normal form (NNF). (define-synthax (nnf x y depth) #:base (choose x (! x) y (! y)) #:else (choose x (! x) y (! y) ((choose && ||) (nnf x y (- depth 1)) (nnf x y (- depth 1)))))
; The body of nnf=> is a hole to be filled with an ; expression of depth (up to) 1 from the NNF grammar. (define (nnf=> x y) (nnf x y 1))
> (define-symbolic a b boolean?)
> (print-forms (synthesize #:forall (list a b) #:guarantee (assert (equal? (=> a b) (nnf=> a b))))) '(define (nnf=> x y) (|| (! x) y))
Since define-synthax uses macros to implement recursive grammars, instantiating a recursive grammar with a large limit (e.g., k > 3) can cause long compilation times, especially if else-expr contains many recursive instantiations of the grammar.
Note also that the ... transformer cannot be used to create multiple ?? or choose holes within a define-synthax form. In particular, a given syntactic occurrence of ?? or choose always refers to the same hole, as shown below.
; A grammar for linear arithmetic. (define-synthax LA ([(_ e ...) (+ (* e (??)) ...)])) ; The following query has no solution because (??) in ; (LA e ...) generates a single integer hole that is ; shared by all e passed to LA, in this case x and y. (define-symbolic* x y integer?) (define sol (synthesize #:forall (list x y) #:guarantee (assert (= (LA x y) (+ (* 2 x) y)))))
> sol (unsat)
; The following query has a solution because the second ; clause of LA2 creates two independent (??) holes. (define-synthax LA2 ([(_ e) (* e (??))] [(_ e1 e2) (+ (* e1 (??)) (* e2 (??)))])) (define sol2 (synthesize #:forall (list x y) #:guarantee (assert (= (LA2 x y) (+ (* 2 x) y)))))
> (print-forms sol2)
'(define sol
(synthesize
#:forall
(list x y)
#:guarantee
(assert (= (+ (* x 2) (* y 1)) (+ (* 2 x) y)))))
procedure
(generate-forms solution) → (listof syntax?)
solution : solution?
procedure
(print-forms solution) → void?
solution : solution?
6.2.2 Angelic Execution Library
| (require rosette/lib/angelic) | package: rosette |
> (define (static) (choose 1 2 3)) > (define (dynamic) (choose* 1 2 3)) > (static) (ite 0$choose:eval:27:0 1 (ite 1$choose:eval:27:0 2 3))
> (static) (ite 0$choose:eval:27:0 1 (ite 1$choose:eval:27:0 2 3))
> (dynamic) (ite xi?$0 1 (ite xi?$1 2 3))
> (dynamic) (ite xi?$2 1 (ite xi?$3 2 3))
> (equal? (static) (static)) #t
> (equal? (dynamic) (dynamic)) (= (ite xi?$4 1 (ite xi?$5 2 3)) (ite xi?$6 1 (ite xi?$7 2 3)))
6.2.3 Debugging Library
| (require rosette/lib/render) | package: rosette |