Module Lmi.Q

module Q: S  with module Mat = Matrix.Q

Matrix expressions.

module Mat: Matrix.S

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.
- Not_linear if the objective obj is not a scalar (1x1 matrix) or one of the input matrix expressions in l is non linear.
- 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.
- 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 : Stdlib.Format.formatter -> matrix_expr -> unit

Printer for LMI.

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

Printer for environment values computed by solver.