package bitwuzla

  1. Overview
  2. Docs

Module Term.ArSource

Array

Sourcetype ('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.

Sourceval 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.

Sourceval 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

Sourceval 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

Sourceval 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.