On this page:

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 functionsthey have no fixed meaning. Their meaning (or interpretation) is determined by the underlying solver as the result of a solver-aided query.

> (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))

> (asserts) ; so Rosette emits the corresponding assertion

'((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)


> (fv? f)   ; f is a function value


> (fv? g)   ; and so is g


> (g 2)     ; we can apply g to concrete values


> (g x)     ; and to symbolic values

(ite (= 1 (real->integer x)) #t (ite (= 0 (real->integer x)) #f #t))


(~> d ...+ r)  function?

  d : (and/c solvable? (not/c function?))
  r : (and/c solvable? (not/c function?))
Returns a type predicate for recognizing functions that take as input values of types d...+ and produce values of type r. The domain and range arguments must be concrete solvable? types that are not themselves functions. Note that ~> expects at least one domain type to be given, disallowing zero-argument functions.

> (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: {[b boolean?] [(! b) real?]}

> (~> real?)

~>: arity mismatch;

 the expected number of arguments does not match the given


  given: 1




(function? v)  boolean?

  v : any/c
Returns true if v is a concrete type predicate that recognizes function values.

> (define t0? (~> integer? real? boolean? (bitvector 4)))
> (define t1? (~> integer? real?))
> (function? t0?)


> (function? t1?)


> (define-symbolic b boolean?)
> (function? (if b t0? t1?)) ; not a concrete type


> (function? integer?)       ; not a function type


> (function? 3)              ; not a type



(fv? v)  boolean?

  v : any/c
Returns true if v is a concrete or symbolic function value.

> (define-symbolic f (~> boolean? boolean?))
> (fv? f)


> (fv? (lambda (x) x))


> (define-symbolic b boolean?)
> (fv? (if b f 1))


> (define sol
       (assert (not (f #t)))
       (assert (f #f)))))
> (define g (evaluate f sol))
> g ; g implements logical negation

(fv boolean?~>boolean?)

> (fv? g)


; verify that g implements logical negation:
> (verify (assert (equal? (g b) (not b))))