"/>

Module `Term.Uf`

Uninterpreted function

type ('a, 'b) t = ('a, 'b) fn term: A function term which maps 'a to 'b.

val lambda : 'a Sort.variadic -> ('a variadic -> '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, '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 | rm | fp ] as 'a value * 'b variadic -> ('a -> 'b) variadic: Statically typed list of function argument values.

val assignment : ('a, '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.