package bitwuzla

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 f
A function that take the function formal parameters and return a term.

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

apply t args create a function application.

type !'a 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.