6.3 Utility Libraries

The following utility libraries facilitate the development of solver-aided programs.

6.3.1 Value Browser Library

Rosette programs often generate complex symbolic values that can be difficult to read and debug. One common problem is that the printer truncates their representation when it exceeds the threshold set by (error-print-width). This library provides an interactive value browser to help programmers navigate and read complex symbolic values.

The value browser supports displaying and navigating values of lifted datatypes. Values of other types (e.g., string or hash) are displayed as leaves in the navigation tree, labeled with the kind other. The optional argument handler can be supplied to customize the display of other values and recover the ability to navigate their structure. See layout and the examples below for more details.

6.3.1.1 Layout

A layout is an embedded DSL describing the tabular layout to display a value of an unlifted datatype in the value browser. It has the following grammar:

Here, #f means the value is atomic (and will be categorized under the kind other), '#:gap means a vertical gap, and emph means emphasis.

6.3.1.2 Examples

The value browser helps navigate values of lifted datatypes as shown below.

> (define-symbolic n integer?)

> (render-value/snip (list 1

1.2

#t

n

(bv 1 (bitvector 2))

+))

; After expanding the snip:

> (define-symbolic f (~> integer? integer?))

> (render-value/snip (list (+ n 1)

(if (= n 0) 1 2)

(f 1)))

> (struct foo [a b])

> (render-value/snip (list (list 1 2)

(foo 1 2)

(vector 1 2)

(box 1)

(if (= n 1) 2 "a")))

But when we try to display an unlifted value like a hash or a set, the browser categorizes it with the kind other, with navigation disabled.

> (render-value/snip (list (hash 1 2 3 4)

(set 1 2 3)))

To allow hash navigation, supply a handler that returns a desired layout when a hash is passed in (as the first argument). For instance, we might want (hash a b c d) to have the following layout:

`([(emph "Kind: ") "hash"]

#:gap

[,snip-a]

[,snip-b]

#:gap

[,snip-c]

[,snip-d])

In this layout, snip-a, snip-b, snip-c, and snip-d can be obtained by applying the recursive renderer to a, b, c, and d respectively.

Using the above layout, we enable hash navigation as follows:

> (render-value/snip (list (hash 1 2 3 4)

(set 1 2 3))

#:handler (λ (value rec)

(cond

[(hash? value)

(append*

'([(emph "Kind: ") "hash"])

(for/list ([(k v) (in-hash value)])

`(#:gap

[,(rec k)]

[,(rec v)])))]

[else #f])))

Note that you should use the recursive renderer (provided as the second argument) rather than calling render-value/snip directly so that the correct handler is used when rendering sub-value (e.g., a hash of hashes).