package bitwuzla

  1. Overview
  2. Docs

Module Term.UfSource

Uninterpreted function

Sourcetype ('a, 'b) t = ('a, 'b) fn term

A function term which maps 'a to 'b.

Sourceval 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

Sourceval 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

Sourcetype 'a variadic =
  1. | [] : unit variadic
  2. | :: : ([< bv | rm | fp ] as 'a) value * 'b variadic -> ('a -> 'b) variadic

Statically typed list of function argument values.

Sourceval 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.