5 Structures🔗ℹ

In addition to lifting many built-in datatypes to work with symbolic values, Rosette also lifts Racket’s structures. As in Racket, a structure is an instance of a structure type—a record datatype with zero or more fields. Structure types are defined using the struct syntax. Defining a structure type in this way also defines the necessary procedures for creating instances of that type and for accessing their fields.

> (struct point (x y) #:transparent)

; Immutable transparent type.

> (struct pt (x y))

; Opaque immutable type.

> (struct pnt (x y) #:mutable #:transparent)

; Mutable transparent type.

Rosette structures can be concrete or symbolic. Their semantics matches that of Racket, with one important exception: immutable transparent structures are treated as values rather than references. This means that two such structures are eq? if they belong to the same type and their corresponding field values are eq?. Structures of opaque or mutable types are treated as references. Two such structures are eq? only if the point to the same instance of the same type.

> (eq? (point 1 2) (point 1 2))  ; point structures are values.

#t

> (eq? (pt 1 2) (pt 1 2))        ; pt structures are references.

#f

> (eq? (pnt 1 2) (pnt 1 2))      ; pnt structures are references.

#f

Like unsolvable built-in datatypes, symbolic structures cannot be created using define-symbolic. Instead, they are created implicitly, by, for example, using an if expression together with a symbolic value.

> (define-symbolic b boolean?)

> (define p (if b (point 1 2) (point 3 4))) ; p holds a symbolic structure.

> (point-x p)

(ite b 1 3)

> (point-y p)

(ite b 2 4)

> (define sol (solve (assert (= (point-x p) 3))))

> (evaluate p sol)

(point 3 4)

Lifted generics work as expected with symbolic values:

> (define-generics viewable (view viewable))

> (struct square (side)     #:methods gen:viewable     [(define (view self) (square-side self))])

> (struct circle (radius)     #:transparent     #:methods gen:viewable     [(define (view self) (circle-radius self))])

> (define-symbolic b boolean?)

> (define p (if b (square 2) (circle 3))) ; p holds a symbolic structure.

> (view p)

(ite b 2 3)

> (define sol (solve (assert (= (view p) 3))))

> (evaluate p sol)

(circle 3)