"/>

Module `Term.Uf`

Uninterpreted function

type ('a, 'b) t = ('a, 'b) fn term constraint 'b = [< bv ]: A function term which maps 'a to 'b.

val lambda : 'a Sort.variadic -> ('a variadic -> [< bv ] as 'b term) -> ('a, 'b) t

lambda sorts f create a function definition.

parameter sorts: The argument sorts.

parameter f: A function that take the function formal parameters and return a term.

returns: a function definition

val apply : ('a, [< bv ] as 'b) t -> 'a variadic -> 'b term

apply t args create a function application.

parameter t: The function term.

parameter args: The argument terms.

returns: a function application

type !'a variadic = | ([]) : unit variadic | (::) : [< `Bv | `Fp | `Rm ] as 'c value * 'b variadic -> ('c -> 'b) variadic: Statically typed list of function argument values.

val assignment : ('a, [< bv ] as 'b) fn value -> ('a variadic * 'b value) array

assignment t get the current model value of given function term.

The value of arguments and values can be queried via Bv.assignment and Fp.assignment.

parameter t: The term to query a model value for.

returns: An array of associations between `arity` arguments and a value.