osdp 1.1.1 (latest) · OCaml Package

Matrix expressions.

module Mat = Matrix.Float

type var

Scalar or symmetric matrix variables.

type matrix_expr =

| Const of Mat.t
| Var of var
(*
All variables are symmetric square matrices.
*)
| Zeros of int * int
| Eye of int
| Kron of int * int * int
| Kron_sym of int * int * int
| Block of matrix_expr array array
| Lift_block of matrix_expr * int * int * int * int
| Transpose of matrix_expr
| Minus of matrix_expr
| Add of matrix_expr * matrix_expr
| Sub of matrix_expr * matrix_expr
| Mult of matrix_expr * matrix_expr
(*
mult_scalar or mult, according to he size of the first argument.
*)
| 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 add : matrix_expr -> matrix_expr -> matrix_expr

val sub : matrix_expr -> matrix_expr -> matrix_expr

val mult : matrix_expr -> 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

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

scalar

val (~:) : matrix_expr -> matrix_expr

transpose

val (*.) : Mat.Coeff.t -> matrix_expr -> matrix_expr

val (~-) : matrix_expr -> matrix_expr

val (+) : matrix_expr -> matrix_expr -> matrix_expr

val (-) : matrix_expr -> matrix_expr -> matrix_expr

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

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

val (>=) : matrix_expr -> matrix_expr -> matrix_expr

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

val (<=) : matrix_expr -> matrix_expr -> matrix_expr

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

LMI.

type options = {

sdp : Sdp.options;
(*
default: Sdp.default
*)
verbose : int;
(*
verbosity level, non negative integer, 0 (default) means no output (but see sdp.verbose just above)
*)
pad : float;
(*
padding factor (default: 2.), 0. means no padding
*)

}

val default : options

Default values above.

type obj =

| Minimize of matrix_expr
| Maximize of matrix_expr
| 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.

raises Dimension_error
if e is not a scalar.

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

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 : Format.formatter -> matrix_expr -> unit

Printer for LMI.

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

Printer for environment values computed by solver.

package osdp

Matrix expressions.

Various operations.

Prefix and infix operators.

LMI.

Printing function.