►The Rosette Guide
▼4 Built-In Datatypes
On this page:
~>
function?
fv?
7.7
  top  ← prev  up  next → 

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

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

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)) #t (ite (= 0 (real->integer x)) #f #t))

procedure

(~> 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.

Examples:
> (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

number

  expected: at least 2

  given: 1

  arguments...:

   real?

procedure

(function? v) → boolean?

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

Examples:
> (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

procedure

(fv? v) → boolean?

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

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

  top  ← prev  up  next →