7.9

#### 6.2Solver-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.1Synthesis Library

 (require rosette/lib/synthax) package: rosette

syntax

(?? maybe-type)

maybe-type =
| type-expr

 type-expr : (and/c solvable? type? (not/c function?))
Introduces a hole into a program—a placeholder for a concrete constant of the given type. The default type for holes, if one is not provided, is integer?. Chapter 2.3.3 shows an example of using integer holes to sketch a factored polynomial function, which is then completed with the help of a synthesize query. The (??) construct creates and returns a fresh symbolic constant of type type-expr (or integer?).

 syntax(choose expr ...+)
Introduces a choice hole into a program—a placeholder to be filled with one of the given expressions. This construct defines n-1 fresh boolean constants and uses them to conditionally select one of the n provided expressions.

Examples:
 > (define (div2 x) ([choose bvshl bvashr bvlshr bvadd bvsub bvmul] x (?? (bitvector 8))))
> (define-symbolic i (bitvector 8))
 > (print-forms (synthesize #:forall (list i) #:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8))))))

'(define (div2 x) (bvlshr x (bv 1 8)))

syntax

 (define-synthax id ([pattern expr] ...+))
 (define-synthax (id terminal ... k) #:base base-expr #:else else-expr)
Defines a grammar of expressions that can be used to fill holes of the form (id e ...). That is, writing (id e ...) introduces a hole that is to be filled with an expression from the id grammar.

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.

Examples:
 ; 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.

Examples:
 ; 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?
Given a satisfiable solution? to a synthesize query, returns a list of sketch completions for that query. Sketch completions can only be generated for programs that have been saved to disk.

 procedure(print-forms solution) → void? solution : solution?
Pretty-prints the result of applying generate-forms to the given solution. Sketch completions can only be generated and printed for programs that have been saved to disk.

##### 6.2.2Angelic Execution Library

 (require rosette/lib/angelic) package: rosette

 procedure(choose* v ...+) → any/c v : any/c
Non-determinstically chooses between the provided values. The difference between choose* and choose is analogous to the difference between define-symbolic* and define-symbolic: the former is dynamic and the latter is static.

Examples:
 > (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.3Debugging Library

 (require rosette/lib/render) package: rosette

 procedure(render solution [font-size]) → pict? solution : solution? font-size : natural/c = 16
Given an unsatisfiable solution? to a debug query, returns a pict? visualization of that solution. The visualization displays the debugged code, highlighting the faulty expressions (i.e., those in the solution’s core) in red. The optional font-size parameter controls the size of the font used to typeset the code. Visualizations can only be constructed for programs that have been saved to disk. See Chapter 2.3.2 for an example of using render.