4.1 Equality
Rosette supports two generic equality predicates, eq? and equal?. The equal? predicate follows the Racket semantics, extended to work with symbolic values. In particular, two values are equal? only when they are eq?, unless a more permissive notion of equal? is specified for a particular datatype.
> (equal? 1 #t) #f
> (equal? 1 1.0) #t
> (equal? (list 1) (list 1.0)) #t
> (equal? (box 1) (box 1)) #t
> (equal? (list (box 1)) (list (box 1))) #t
> (define-symbolic n integer?) > (equal? n 1) (= 1 n)
> (equal? (box n) (box 1)) (= 1 n)
> (define-symbolic f g (~> integer? integer?)) > (equal? f g) ; f and g are different procedures. #f
The eq? predicate follows the Racket semantics for opaque or mutable datatypes, such as procedures or vectors, but not for transparent immutable datatypes, such as lists, or transparent solvable types, such as reals. Rosette treats these transparent types as value types, while Racket does not. Racket’s eq? may therefore return #f when given two instances of such a transparent type, regardless of their contents. Rosette’s eq?, in contrast, returns true when given two transparent solvable values that are equal?, or two transparent immutable values with eq? contents.
> (eq? 1 #t) #f
> (eq? 1 1.0) ; equal? transparent solvable values. #t
> (eq? (list 1) (list 1.0)) ; Transparent immutable values with eq? contents. #t
> (eq? (box 1) (box 1)) ; But boxes are mutable, so eq? follows Racket, #f
> (eq? (list (box 1)) (list (box 1))) #f
> (define-symbolic n integer?) > (eq? n 1) (= 1 n)
> (eq? (box n) (box 1)) #f
> (define-symbolic f g (~> integer? integer?)) > (eq? f g) ; and procedures are opaque, so eq? follows Racket. #f
> (eq? f f) #t
In addition to lifting Racket’s equality predicates, Rosette also provides a distinct? predicate that returns true iff all of its arguments are distinct from each other. Invoking this predicate on arbitrary values has the effect of performing O(N2) equality comparisons. But when applied to symbolic values of a primitive solvable type, distinct? will produce a compact symbolic value that can be directly solved by the underlying solver.