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-project

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

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

Module `Space.Matrix`

val pretty : Format.formatter -> ('n Nat.succ, 'm Nat.succ) 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 of_array : 
  'n Nat.succ Nat.nat ->
  'm Nat.succ Nat.nat ->
  string array array ->
  ('n Nat.succ, 'm Nat.succ) matrix

Build a matrix from a 2 dimensional array of strings. Strings are used here to ensure that no rounding is performed prior of the ones that may be introduced by the underlying field. Raise out of bounds exceptions if the array is not well formed.

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 subtraction. 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 (/) : ('n, 'm) matrix -> ('n, 'm) matrix -> ('n, 'm) matrix

Componentwise division.

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

Scalar multiplication.

val inverse : 
  ('n Nat.succ, 'n Nat.succ) matrix ->
  ('n Nat.succ, 'n Nat.succ) 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.

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

The call all_components_lower_than l r return true if and only if each components of l are lower or equal to their counterpart in r, i.e for all i and j, get i j l is lower or equal to get i j r.