"/>

Module Term.Ar

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.

parameter sort

The sort of the array.

parameter value

The value to initialize the elements of the array with.

returns

A term representing a constant array of given sort.

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

select t i create an array access.

parameter t

The array term.

parameter i

The index term.

returns

SMT-LIB: select

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.

parameter t

The array term.

parameter i

The index term.

parameter e

The element term.

returns

SMT-LIB: store

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.

parameter t

The term to query a model value for.

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.