On this page:
6.2.1 Synthesis Library
??
choose
define-grammar
define-simple-grammar
current-grammar-depth
generate-forms
print-forms
6.2.2 Angelic Execution Library
choose*
8.12

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 two libraries that provide such constructs, as well as utility procedures for turning the results of synthesis 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?))
Introduces a constant hole into a program—a placeholder for a concrete constant of the given type. The default value for type-expr, if one is not provided, is integer?. The ?? construct creates and returns a distinct symbolic constant of type type-expr.

When used in a recursive grammar definition, a ?? hole generates a fresh constant every time it is evaluated, similarly to define-symbolic*. Otherwise, a ?? hole always generates the same constant, similarly to define-symbolic.

See also define-grammar.

Examples:
; Uses a ?? hole to sketch a procedure for multiplying
; an 8-bit number by 2 using a constant left shift.
(define (bvmul2_?? x)
  (bvshl x (?? (bitvector 8))))

; bvmul2_?? hole always returns the same constant:
> (bvmul2_?? (bv 1 8))

(bvshl (bv #x01 8) ??:bvmul2:9:12)

> (bvmul2_?? (bv 3 8))

(bvshl (bv #x03 8) ??:bvmul2:9:12)

> (define-symbolic x (bitvector 8))
> (bvmul2_?? x)

(bvshl x ??:bvmul2:9:12)

> (equal? (bvmul2_?? x) (bvmul2_?? x))

#t

; Use synthesis to fill the hole with a constant:
> (define sol
    (synthesize
     #:forall (list x)
     #:guarantee (assert (equal? (bvmul2_?? x) (bvmul x (bv 2 8))))))
> sol

(model

 [??:bvmul2:9:12 (bv #x01 8)])

; Save bvmul2_?? to a file before calling print-forms.
> (print-forms sol)

(define (bvmul2_?? x) (bvshl x (bv #x01 8)))

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 distinct boolean constants and uses them to conditionally select one of the n provided expressions.

When used in a recursive grammar definition, a choose hole generates fresh selector constants and may select a different expression every time it is evaluated. Otherwise, a choose hole generates the same constants and makes the same selection every time.

See also choose* and define-grammar.

Examples:
; Uses a chooose hole to sketch a procedure for multiplying
; an 8-bit number by 2 using a constant shift.
(define (bvmul2_choose x)
  ((choose bvshl bvashr bvlshr) x (?? (bitvector 8))))

; bvmul2_choose holes always generate the same constants:
> (define-symbolic x (bitvector 8))
> (bvmul2_choose x)

(ite*

 (⊢ 0$choose:bvmul2:12:4 (bvshl x ??:bvmul2:12:35))

 (⊢

  (&& 1$choose:bvmul2:12:4 (! 0$choose:bvmul2:12:4))

  (bvashr x ??:bvmul2:12:35))

 (⊢

  (&& (! 0$choose:bvmul2:12:4) (! 1$choose:bvmul2:12:4))

  (bvlshr x ??:bvmul2:12:35)))

> (equal? (bvmul2_choose x) (bvmul2_choose x))

#t

; Use synthesis to fill the holes:
> (define sol
    (synthesize
     #:forall (list x)
     #:guarantee (assert (equal? (bvmul2_choose x) (bvmul x (bv 2 8))))))
> sol

(model

 [0$choose:bvmul2:12:4 #t]

 [1$choose:bvmul2:12:4 #f]

 [??:bvmul2:12:35 (bv #x01 8)])

; Save bvmul2_choose to a file before calling print-forms.
> (print-forms sol)

(define (bvmul2_choose x) (bvshl x (bv #x01 8)))

syntax

(define-grammar (id arg-id ...)
  [rule-id rule-expr] ...+)
Defines a macro for creating and filling grammar holes. The macro uses (id arg-id ...) as the pattern for creating holes and [rule-id rule-expr] ...+ as the rules for filling these holes with expressions. In particular, writing (id arg-expr ...) creates a hole for an expression derived from the grammar [rule-id rule-expr] ...+, where the pattern variables arg-id are instantianted with the hole arguments arg-expr.

Each hole defines a local scope that binds the rule names rule-id to procedures of the form (lambda () ... rule-expr). This scope behaves like letrec, so rules can refer to themselves and each other via (rule-id) to specify a recursive grammar.

For example, the following definition specifies a grammar of fast bitvector expressions over one input:

(define-grammar (bitfast y)
  [expr                            ; <expr> :=
   (choose y (?? (bitvector 8))    ;  y | <8-bit constant> |
           ((bop) (expr) (expr)))] ;  ((bop) <expr> <expr>)
  [bop                             ; <bop> :=
   (choose bvshl bvashr bvlshr     ;  bvshl | bvashr | bvlshr |
           bvand bvor bvxor        ;  bvand | bvor | bvxor |
           bvadd bvsub)])          ;  bvadd | bvsub

By default, a grammar hole is filled by evaluating the first grammar rule (rule-id0) in the hole’s local scope, and limiting the call stack to include at most (current-grammar-depth) applications of the grammar rules. Holes can override these defaults by providing the optional arguments #:depth n and #:start rule-idk, which control the call stack depth and the starting rule, respectively.

; Uses a bitfast hole to sketch a procedure consisting
; of a fast bitvector expression over x, created by at
; most 2 applications of the bitfast grammar rules,
; following the initial application of the (expr) rule.
(define (bvmul2_bitfast x)
  (bitfast x #:depth 2))

Whenever a grammar hole is evaluated, its constituent choose and ?? holes generate the same set of constants, with each rule application generating a distinct subset of this set. This allows different applications of the same rule to produce different components of the unique expression that fills a grammar hole.

; The choose and ?? holes that are part of the same bitfast
; hole always generate the same set of constants:
> (define-symbolic x (bitvector 8))
> (equal? (bvmul2_bitfast x) (bvmul2_bitfast x))

#t

> (define sol
     (synthesize
      #:forall (list x)
      #:guarantee (assert (equal? (bvmul2_bitfast x) (bvmul x (bv 2 8))))))
; Save bvmul2_bitfast to a file before calling print-forms.
> (print-forms sol)

(define (bvmul2_bitfast x) (bvshl x (bv #x01 8)))

Grammar rules can include grammar holes as part of their definition. An included grammar hole behaves just like an included choose or ?? hole: it can be filled with different expressions in different applications of the enclosing rule.

; Specifies a grammar of signed and unsigned
; comparisons of bitfast expressions.
(define-grammar (bitcmp y)
  [cmp
   (choose                         ; <cmp> :=
    ((op) (bitfast y) (bitfast y)) ;  (<op> <bitfast y> <bitfast y>) |
    (and (cmp) (cmp)))]            ;  (and <cmp> <cmp>)
  [op
   (choose                         ; <op> :=
    bvult bvule                    ;  bvult | bvule |
    bvslt bvsle)])                 ;  bvslt | bvsle
; Uses bitcmp and bitfast holes to sketch
; a procedure with a conditional, intended
; to implement fast signed division by 2.
(define (bvsdiv2_bitcmp x)
  (if (bitcmp x)
      (bitfast x)
      (bitfast x)))
> (define-symbolic x (bitvector 8))
> (current-grammar-depth 2) ; Set the grammar depth.
> (define sol
    (synthesize
     #:forall (list x)
     #:guarantee (assert (equal? (bvsdiv2_bitcmp x) (bvsdiv x (bv 2 8))))))
; Save bvsdiv2_bitcmp to a file before calling print-forms.
; Note that the solver can return any correct solution.
; In this case, there is a shorter solution that omits the
; trivially true right child from the test expression.
> (print-forms sol)

(define (bvsdiv2_bitcmp x)

  (if (and (bvult x (bv #x81 8)) (bvsle (bv #x23 8) (bv #x72 8)))

    (bvashr x (bv #x01 8))

    (bvadd (bvashr x (bv #x01 8)) (bvand (bv #x01 8) x))))

Finally, grammar holes can accept other holes as arguments. Unlike included holes, argument holes are shared within the same rule. If an argument arg-id is bound to a hole arg-expr, then all occurrences of arg-id in a given rule refer to one shared arg-expr hole, which can be filled with different expressions in different applications of the rule. In contrast, if a rule explicitly includes arg-expr multiple times, then each occurrence of arg-expr creates a distinct hole. The following examples illustrate the difference and show how to structure grammars to avoid unwanted sharing of argument holes.

; This grammar is intended to take a hole xs
; as an argument and use it to define the space
; of signed and unsigned comparisons over the xs
; expressions. The grammar is the same as bitcmp
; except that it uses xs instead of (bitfast y)
; in the cmp rule.
(define-grammar (bvcmp xs)
 [cmp
  (choose              ; Both occurrences of xs
   ((op) xs xs)        ; refer to a single shared
   (and (cmp) (cmp)))] ; hole in this rule.
 [op
  (choose
   bvult bvule
   bvslt bvsle)])
; This sketch is the same as bvsdiv2_bitcmp except
; that it replaces bitcmp with (bvcmp (bitfast x)).
(define (bvsdiv2_bvcmp x)
  (if (bvcmp (bitfast x))
      (bitfast x)
      (bitfast x)))
> (define-symbolic x (bitvector 8))
> (current-grammar-depth 2)
; There is no solution because the two xs in the
; cmp rule of the bvcmp grammar refer to the same
; hole, so it is not possible for the rule to
; create a comparison expression with different left
; and right children (comparing x to a constant).
> (synthesize
    #:forall (list x)
    #:guarantee (assert (equal? (bvsdiv2_bvcmp x) (bvsdiv x (bv 2 8)))))

(unsat)

; To avoid the sharing, we refactor bvcmp to place xs into
; its own rule, arg, which is then called by cmp.
; This works because every application of the arg rule
; can fill its sole xs hole with a different expression.
(define-grammar (bvcmp* xs)
 [cmp
  (choose
   ((op) (arg) (arg))
   (and (cmp) (cmp)))]
 [op
  (choose
   bvult bvule
   bvslt bvsle)]
 [arg xs])
; This sketch is the same as bvsdiv2_bitcmp except
; that it replaces bitcmp with (bvcmp* (bitfast x)).
(define (bvsdiv2_bvcmp* x)
  (if (bvcmp* (bitfast x))
      (bitfast x)
      (bitfast x)))

> (define-symbolic x (bitvector 8))
> (current-grammar-depth 2)
; A solution exists now because the arg rule produces
; different left and right children for the comparison
; operator used in the bvsdiv2_bvcmp* conditional test.
> (define sol
    (synthesize
     #:forall (list x)
     #:guarantee (assert (equal? (bvsdiv2_bvcmp* x) (bvsdiv x (bv 2 8))))))
; Save bvsdiv2_bvcmp* to a file before calling print-forms.
> (print-forms sol)

(define (bvsdiv2_bvcmp* x)

  (if (bvult x (bv #x81 8))

    (bvashr (bvashr x (bv #x01 8)) (bv #x00 8))

    (bvashr (bvadd x (bv #x01 8)) (bvsub (bv #x49 8) (bv #x48 8)))))

syntax

(define-simple-grammar (id arg-id ...) body)

Defines a grammar with a single (possibly recursive) rule. Equivalent to
(define-grammar (id param ...)
  [id body])

parameter

(current-grammar-depth)  natural?

(current-grammar-depth n)  void?
  n : natural?
 = 0
A parameter that controls the evaluation of grammar holes. Evaluating a grammar hole involves evaluating the rules of its grammar. The (current-grammar-depth) parameter controls how many of these rules can appear on the call stack after the start rule is evaluated. The default value of 0 allows only the start rule to be evaluated, and a value of n > 0 allows at most n additional rules to be added to the call stack. For best performance, keep the value of this parameter as low as possible.

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.

This procedure cooperates with the constructs in the rosette/lib/synthax library to turn solutions into code. It works by scanning program files for constant, choice, and grammar holes, and replacing all identified holes with code. The code for a hole is computed from the solution bindings for the symbolic constants generated by the hole. Holes are identified by their original names: ??, choose, and any id introduced by define-grammar or define-simple-grammar. If a program uses different names for these holes (e.g., by renaming them in a require clause), generate-forms will not recognize or replace them, even if the given solution has bindings for their symbolic constants.

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.2 Angelic Execution Library🔗ℹ

 (require rosette/lib/angelic) package: rosette

procedure

(choose* v ...+)  any/c

  v : any/c

Symbolically chooses one of the provided values. The procedure creates n-1 fresh symbolic boolean constants every time it is evaluated, and uses these constants to conditionally select one of the n provided expressions.

The choose* procedure is related to the choose construct from the synthesis library. Semantically, the difference between choose* and choose is analogous to the difference between define-symbolic* and define-symbolic.

They also differ in how they are typically used: choose is used primarily for synthesis, while choose* is suitable for both synthesis (via the synthesize query) and angelic execution (via the solve query).

In the context of synthesis, choose is used to sketch programs in (a subset of) the Rosette language, and choose* can be used to sketch programs in any language that has a Rosette-based interpreter.

Examples:
(require rosette/lib/angelic rosette/lib/destruct)
(define BV (bitvector 8))
; A toy language for programs that manipulate a
; a single storage cell by adding a constant to
; it, multiplying it by constant, and squaring it.
(struct Add (arg) #:transparent)
(struct Mul (arg) #:transparent)
(struct Sqr ()    #:transparent)
(define (interpret prog [acc (bv 0 BV)])
  (if (null? prog)
      acc
      (interpret
       (cdr prog)
       (destruct (car prog)
         [(Add v) (bvadd acc v)]
         [(Mul v) (bvmul acc v)]
         [(Sqr)   (bvmul acc acc)]
         [_       acc]))))
; Creates a symbolic instruction (a hole) in the toy language.
(define (inst*)
 (define-symbolic* arg BV)
 (choose* (Add arg) (Mul arg) (Sqr)))
; Creates a toy program consisting of n symbolic instructions.
(define (prog* n)
 (if (<= n 0)
     (list)
     (cons (inst*) (prog* (- n 1)))))

> (define-symbolic acc BV)
> (define prog (prog* 3))
> prog

'((union

   [xi?$1 #(struct:Add arg$0)]

   [(&& xi?$2 (! xi?$1)) #(struct:Mul arg$0)]

   [(&& (! xi?$1) (! xi?$2)) #(struct:Sqr)])

  (union

   [xi?$4 #(struct:Add arg$3)]

   [(&& xi?$5 (! xi?$4)) #(struct:Mul arg$3)]

   [(&& (! xi?$4) (! xi?$5)) #(struct:Sqr)])

  (union

   [xi?$7 #(struct:Add arg$6)]

   [(&& xi?$8 (! xi?$7)) #(struct:Mul arg$6)]

   [(&& (! xi?$7) (! xi?$8)) #(struct:Sqr)]))

; Complete prog so that it implements 3 * acc^2 - 1 for all acc.
> (define sol
   (synthesize
    #:forall (list acc)
    #:guarantee
    (assert
     (equal? (interpret prog acc)
             (bvsub (bvmul (bv 3 BV) acc acc) (bv 1 BV))))))
> (evaluate prog sol)

(list (Sqr) (Add (bv #x55 8)) (Mul (bv #x03 8)))