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—
> (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)
Defining Properties | |
Lifted Properties | |
Defining Generics | |
Lifted Generics |
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)