package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Linear/Space/Matrix/index.html

Module `Space.Matrix`

val pretty : Stdlib.Format.formatter -> ('n, 'm) matrix -> unit

val id : 'n Nat.succ Nat.nat -> ('n Nat.succ, 'n Nat.succ) matrix

The call id n returns the identity matrix in 𝕂ⁿˣⁿ.

val zero : 
  'n Nat.succ Nat.nat ->
  'm Nat.succ Nat.nat ->
  ('n Nat.succ, 'm Nat.succ) matrix

The call zero n m returns the 0 matrix in 𝕂ⁿˣᵐ.

val shift : 'n Nat.succ Nat.nat -> ('n Nat.succ, 'n Nat.succ) matrix

The call shift n returns a square matrix in 𝕂ⁿˣⁿ such as the first row and the last column is all zero, and the remaining is the identity.

val get : 'n Finite.finite -> 'm Finite.finite -> ('n, 'm) matrix -> scalar

The call get i j m returns the coefficient of the i-th row and the j-th column.

val set : 
  'n Finite.finite ->
  'm Finite.finite ->
  scalar ->
  ('n, 'm) matrix ->
  ('n, 'm) matrix

The call set i j x m returns a new matrix of the same linear space as m, and with the same coefficients, except for the one of the i-th row and the j-th column, which is set to the scalar x.

val norm_inf : ('n, 'm) matrix -> scalar

The call norm_inf m computes the ∞-norm of m, i.e the maximum of the absolute sums of the rows of m.

val norm_one : ('n, 'm) matrix -> scalar

The call norm_one m computes the 1-norm of m, i.e the maximum of the absolute sums of the columns of m.

val transpose : ('n, 'm) matrix -> ('m, 'n) matrix

The call transpose m for m in 𝕂ⁿˣᵐ returns a new matrix in 𝕂ᵐˣⁿ with all the coefficients transposed.

val dimensions : ('m, 'n) matrix -> 'm Nat.nat * 'n Nat.nat

The call dimensions m for m in 𝕂ⁿˣᵐ returns the pair (n, m).

val (+) : ('n, 'm) matrix -> ('n, 'm) matrix -> ('n, 'm) matrix

Matrices addition. The dimensions compatibility is statically ensured.

val (-) : ('n, 'm) matrix -> ('n, 'm) matrix -> ('n, 'm) matrix

Matrices substraction. As for the addition, the dimensions compatibility is statically ensured.

val (*) : ('n, 'm) matrix -> ('m, 'p) matrix -> ('n, 'p) matrix

Matrices multiplication. The dimensions compatibility is statically ensured.

val (**) : scalar -> ('n, 'm) matrix -> ('n, 'm) matrix

Scalar multiplication.

val power : ('n, 'n) matrix -> int -> ('n, 'n) matrix

Matrix exponentiation. The call power m returns a memoized function. When one needs to compute several exponentiations of the same matrix, one should perform the call power m once and used the returned function each times one needs it.

val inverse : ('n, 'n) matrix -> ('n, 'n) matrix option

Matrix inverse. Returns None if the input matrix is singular.

val abs : ('n, 'm) matrix -> ('n, 'm) matrix

The call abs m returns a matrix for which each coordinate is the absolute value of the corresponding coordinate of m.