package bitwuzla

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Term.Ar`Source

Array

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

An array term which maps 'a to 'b.

Sourceval make : ('a, 'b) ar sort -> 'b term -> ('a, 'b) t

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

Sourceval select : ('a, 'b) t -> 'a term -> 'b term

select t i create an array access.

Sourceval store : ('a, 'b) t -> 'a term -> 'b term -> ('a, 'b) t

store t i e create an array write.

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