package bitwuzla

  1. Overview
  2. Docs

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 =
  1. | [] : unit variadic
  2. | :: : [< `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.

OCaml

Innovation. Community. Security.