4.4 Uninterpreted Functions
In Rosette, functions are special kinds of procedures that are pure
(have no side effects) and total (defined on every input value).
A function type is recognized by the function? predicate, and all
function types are solvable. The type of a
function specifies the function’s domain and range, which are given as solvable? non-function? types. A value of a function type is recognized by
the fv? (function value) predicate. Because
function types are solvable, they can be used in the define-symbolic[*] form
to introduce a symbolic function constant. These symbolic function constants are
technically uninterpreted functions—
> (current-bitwidth #f) ; An uninterpreted function from integers to booleans: > (define-symbolic f (~> integer? boolean?)) > (f 1) ; No built-in interpretation for 1. (app f 1)
> (define-symbolic x real?) > (f x) ; This typechecks when x is an integer, (app f (real->integer x))
> (vc) ; so Rosette emits the corresponding assertion. (vc #t (int? x))
> (define sol (solve (assert (not (equal? (f x) (f 1)))))) > (define g (evaluate f sol)) ; An interpretation of f. > g (fv integer?~>boolean?)
> (evaluate x sol) 0
> (fv? f) ; f is a function value, #t
> (fv? g) ; and so is g. #t
> (g 2) ; We can apply g to concrete values #t
> (g x) ; and to symbolic values. (ite (= 1 (real->integer x)) #f #t)
> (define t (~> integer? real? boolean? (bitvector 4))) > t integer?~>real?~>boolean?~>(bitvector 4)
> (~> t integer?) function: expected a list of primitive solvable types
domain: '(integer?~>real?~>boolean?~>(bitvector 4))
> (define-symbolic b boolean?) > (~> integer? (if b boolean? real?)) function: expected a primitive solvable type
range: (union [b boolean?] [(! b) real?])
> (~> real?) ~>: arity mismatch;
the expected number of arguments does not match the given
number
expected: at least 2
given: 1
> (define t0? (~> integer? real? boolean? (bitvector 4))) > (define t1? (~> integer? real?)) > (function? t0?) #t
> (function? t1?) #t
> (define-symbolic b boolean?) > (function? (if b t0? t1?)) ; Not a concrete type. #f
> (function? integer?) ; Not a function type. #f
> (function? 3) ; Not a type. #f
> (define-symbolic f (~> boolean? boolean?)) > (fv? f) #t
> (fv? (lambda (x) x)) #f
> (define-symbolic b boolean?) > (fv? (if b f 1)) b
> (define sol (solve (begin (assert (not (f #t))) (assert (f #f))))) > (define g (evaluate f sol)) > g ; g implements logical negation. (fv boolean?~>boolean?)
> (fv? g) #t
; Verify that g implements logical negation: > (verify (assert (equal? (g b) (not b)))) (unsat)