package bitwuzla

  1. Overview
  2. Docs

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.

OCaml

Innovation. Community. Security.