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

Array

type ('a, 'b) t = ('a, 'b) ar term constraint 'a = [< `Bv | `Fp | `Rm ] constraint 'b = [< `Bv | `Fp | `Rm ]

An array term which maps 'a to 'b.

val make : 
  ([< `Bv | `Fp | `Rm ] as 'a, [< `Bv | `Fp | `Rm ] as 'b) ar sort ->
  'b term ->
  ('a, 'b) t

make sort value create a one-dimensional constant array of given sort, initialized with given value.

val select : 
  ([< `Bv | `Fp | `Rm ] as 'a, [< `Bv | `Fp | `Rm ] as 'b) t ->
  'a term ->
  'b term

select t i create an array access.

val store : 
  ([< `Bv | `Fp | `Rm ] as 'a, [< `Bv | `Fp | `Rm ] as 'b) t ->
  'a term ->
  'b term ->
  ('a, 'b) t

store t i e create an array write.

val assignment : 
  ([< `Bv | `Fp | `Rm ] as 'a, [< `Bv | `Fp | `Rm ] as 'b) ar value ->
  ('a value * 'b value) array * 'b value option

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

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

returns
An array of associations between indices and values. The value of all other indices is Some default when base array is constant array, otherwise, it is None.