package osdp

  1. Overview
  2. Docs

Matrix expressions.

module Mat : Matrix.S
type var

Scalar or symmetric matrix variables.

type matrix_expr =
  1. | Const of Mat.t
  2. | Var of var
    (*

    All variables are symmetric square matrices.

    *)
  3. | Zeros of int * int
  4. | Eye of int
  5. | Kron of int * int * int
  6. | Kron_sym of int * int * int
  7. | Block of matrix_expr array array
  8. | Lift_block of matrix_expr * int * int * int * int
  9. | Transpose of matrix_expr
  10. | Minus of matrix_expr
  11. | Add of matrix_expr * matrix_expr
  12. | Sub of matrix_expr * matrix_expr
  13. | Mult of matrix_expr * matrix_expr
    (*

    mult_scalar or mult, according to he size of the first argument.

    *)
  14. | Power of matrix_expr * int

Constructors. See the module Matrix.S for details.

val var : string -> int -> matrix_expr

var s n creates a new variable (Var v). n is the size of the variable (scalars and matrices of size 1 are considered the same). It must be positive.

val var_var : string -> int -> var * matrix_expr

TODO: renamed (to discuss: this breaks the interface)

Functions for above constructors.

val const : Mat.t -> matrix_expr
val scalar : Mat.Coeff.t -> matrix_expr

scalar s returns Const (Mat.of_list_list [[s]]).

val zeros : int -> int -> matrix_expr
val eye : int -> matrix_expr
val kron : int -> int -> int -> matrix_expr
val kron_sym : int -> int -> int -> matrix_expr
val block : matrix_expr array array -> matrix_expr
val lift_block : matrix_expr -> int -> int -> int -> int -> matrix_expr
val transpose : matrix_expr -> matrix_expr
val minus : matrix_expr -> matrix_expr
val power : matrix_expr -> int -> matrix_expr

Various operations.

val nb_lines : matrix_expr -> int
val nb_cols : matrix_expr -> int
val is_symmetric : matrix_expr -> bool

Prefix and infix operators.

To use this operators, it's convenient to use local opens. For instance to write the matrix operations m1 * m2 + I_3x3:

let module M = Osdp.Matrix.Float in
M.(m1 * m2 + eye 3)

See the module Matrix.S for details.

val (!!) : Mat.t -> matrix_expr

Const

scalar

val (~:) : matrix_expr -> matrix_expr

transpose

val (~-) : matrix_expr -> matrix_expr
val (**) : matrix_expr -> int -> matrix_expr

e1 >= e2 is just syntactic sugar for e1 - e2.

e1 <= e2 is just syntactic sugar for e2 - e1.

LMI.

type options = {
  1. sdp : Sdp.options;
    (*

    default: Sdp.default

    *)
  2. verbose : int;
    (*

    verbosity level, non negative integer, 0 (default) means no output (but see sdp.verbose just above)

    *)
  3. pad : float;
    (*

    padding factor (default: 2.), 0. means no padding

    *)
}
val default : options

Default values above.

type obj =
  1. | Minimize of matrix_expr
  2. | Maximize of matrix_expr
  3. | Purefeas

Minimize e or Maximize e or Purefeas (just checking feasibility). e must be a scalar (i.e., a matrix of size 1).

type values
exception Dimension_error of string
exception Not_linear
exception Not_symmetric
val solve : ?options:options -> ?solver:Sdp.solver -> obj -> matrix_expr list -> SdpRet.t * (float * float) * values

solve obj l tries to optimise the objective obj under the constraint that each matrix expressions in l is positive semi-definite. If solver is provided, it will supersed the solver given in options. Returns a tuple ret, (pobj, dobj), values. If SdpRet.is_success ret, then the following holds. pobj (resp. dobj) is the achieved primal (resp. dual) objective value. values contains values for each variable appearing in l (to be retrieved through following functions value and value_mat).

If ret is SdpRet.Success, then all LMI constraints in l are indeed satisfied by the values returned in values (this is checked through the function check below).

  • raises Dimension_error

    with an explanatory message in case something inconsistent is found in a LMI.

  • raises Not_linear

    if the objective obj is not a scalar (1x1 matrix) or one of the input matrix expressions in l is non linear.

  • raises Not_symmetric

    if one of the input matrix expressions in l is non symmetric.

val empty_values : unit -> values

empty_values () returns an empty map of values. Useful when using references.

val value : matrix_expr -> values -> Mat.Coeff.t

value e values returns the evaluation of matrix expression e, replacing all Var by the corresponding value in values.

  • raises Not_found

    if one of the variables appearing in e has no corresponding value in values.

val value_mat : matrix_expr -> values -> Mat.t

value_mat e values returns the evaluation of matrix expression e, replacing all Var by the correspoding value in values.

  • raises Not_found

    if one of the variables appearing in e has no corresponding value in values.

val register_value : var -> Mat.Coeff.t -> values -> values

Register a scalar value in value environement

val check : ?options:options -> ?values:values -> matrix_expr -> bool

If check ?options e ?values returns true, then e is positive semi-definite (PSD). Otherwise, either e is not PSD or it is not positive definite enough for the proof to succeed. If e contains variables, they are replaced by the corresponding value in values (values is empty by default).

  • raises Not_found

    if e contains a variable not present in values.

Printing function.

val pp : Stdlib.Format.formatter -> matrix_expr -> unit

Printer for LMI.

val pp_values : Stdlib.Format.formatter -> values -> unit

Printer for environment values computed by solver.