Index of values

mult

Same as mult.

power

Same as power.

mult_scalar

Same as mult_scalar.

Const

Const

scalar

const

scalar

add

Same as add.

sub

Same as sub.

p / c is equivaent to mult_scalar (Coeff.div Coeff.one c) p.

c1 /. c2 is equivaent to !c1 / c2.

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

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

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

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

Unary minus, ~- p is syntactic sugar for sub zero p.

Same as minus.

Same as transpose.

transpose

var

Matrix addition.

block a returns the block matrix corresponding to the array a.

If check ?options e ?values (v, Q) returns true, then e is SOS.

Takes as input a square matrix of Q.t of size nxn and returns 1 if it manages to prove that the matrix is symmetric positive definite and 0 otherwise (i.e.

If check ?options e ?values returns true, then e is positive semi-definite (PSD).

Same as check_complete but returns true iff the input is positive *semi*definite (rather than positive definite).

Same as check but complete (returns true iff the input is positive definite).

Takes as input a square interval matrix m of size nxn.

TODO: doc (

Returns one of the (non zero) coefficients in the linear expression (if any).

compose p [q_1;...; q_n] returns the polynomial p' such that p'(x_1,..., x_m) = p(q_1(x_1,..., x_m),..., q_n(x_1,..., x_m)).

const c is equivalent to var ~c ~d:0 0.

Same as LinExpr.S.of_list with an empty list.

Create a new unique identificator.

Default values above.

Default values above.

Default values above.

Default values above.

Default values above.

Default values above.

-1 for the null polynomial.

degree_list p returns a list of length nb_vars p with the maximal degree for each variable in p.

derive p i returns the derivative of the polynomial p with respect to variable i (indices starting from 0).

derive m i returns j_i, x_0^{j_0} ... x_i^{j_i - 1} ... x_n^{j_n}) if the degree j_i of variable i is positive in the monomial m and 0, one otherwise.

div m1 m2 divides m1 by m2.

divide m1 m2 returns true iff m1 divides m2 (i.e., when lcm m1 m2 = m2 or equivalently gcd m1 m2 = m1).

empty_values () returns an empty map of values.

eval p [x_1;...; x_n] returns p(x_1,..., x_n).

eye n builds the identity matrix of size n (i.e., a square matrix of size n with coefficients (i, j) equal to Coeff.of_int O when i != j and Coeff.of_int 1 when i = j).

filter s p returns the list of the s_i in s such that 2s_i is in the convex hull of the p_1,..., p_n in p.

float_of_q q returns a float closest to q.

gauss_split m for a matrix m of size l x c returns (n, m1, m2) where n is the rank of the input matrix (n <= l), m1 its row space, i.e., a matrix of size l' x c where l' <= l characterizing the same space as m but with no linear dependencies, and m2 a matrix of size l' x l mapping original dimensions in m to the ones of m1 (m1 = m2 x m).

gcd m1 m2 returns the Greatest Common Divisor of m1 and m2 (i.e., the minimum of degrees for each variable).

is_const p returns Some c if p is the constant polynomial c and None otherwise.

is_monomial p returns Some m if p is a monmial x_0^i_0 ...

is_success t returns true if and only if t is Success or PartialSuccess.

is_var p returns Some (c, d, i) if p is a polynomial of the form c xi^d and None otherwise.

is_var m returns Some (d, i) if m is the monomial xi^d and None otherwise.

itv_float_of_q q returns two floats l, u such that, when q is Q.undef, l and u are both nan, otherwise l <= q <= u and there is no float (either normal or subnormal) such that l < f < u.

kron n i j builds the square matrix of size n with all coefficients equal to zero (i.e., Coeff.of_int 0 except coefficients (i, j) which is one (i.e., Coeff.of_int 1).

kron_sym n i j builds the square matrix of size n with all coefficients equal to zero (i.e., Coeff.of_int 0 except coefficients (i, j) and (j, i) which are one (i.e., Coeff.of_int 1).

lcm m1 m2 returns the Least Common Multiple of m1 and m2 (i.e., the maximum of degrees for each variable).

lift_block m i j k l returns a matrix of size i x j with zeros everywhere except starting from indices k x l where matrix m is copied.

list_eq n d provides the list of all monomials with n variables of degree equal d (for instance, list_eq 3 2 can return [x0^2; x0 x1; x0 x2; x1^2; x1 x2; x2^2]).

list_le n d provides the list of all monomials with n variables of degree less or equal d (for instance, list_le 3 2 can return [1; x0; x1; x2; x0^2; x0 x1; x0 x2; x1^2; x1 x2; x2^2]).

make s creates a new parametric variable named s.

tail-recursive version of List.map (implemented using List.rev_map and List.rev)

Unary minus.

monomial m is equivalent to of_list [m, Coeff.one].

mult m1 m2 multiplies the two monomials m1 and m2.

Matrix multiplication.

mult_scalar s m multiplies matrix m by scalar s.

nb_vars p returns the largest index (starting from 0) of a variable appearing in p plus one (0 if none).

nb_vars m returns the largest index (starting from 0) of a variable appearing in m plus one (0 if none).

of_array_array a returns the matrix with lines corresponding to the elements of a.

of_list [(m_1, a_1);..; (m_n, a_n)] builds the polynomial a_1 m_1 + ...

of_list l produces the monomial corresponding to list l.

of_list [(x_1, a_1);..; (x_n, a_n)] c builds the affine expression a_1 x_1 + ...

of_list_list l returns the matrix with lines corresponding to the elements of the list l.

Equivalent to of_list [].

param_vars e returns the list of all parametric variables appearing in e.

pfeas_stop_crit (b_1,..., b_m) returns eps used as primal feasibility error stopping criteria by solver solver on a problem with given b_i (i.e., if the solver successfully terminates, |tr(A_i X) - b_i| <= eps should hold for each constraint i).

power p n computes p^n, n must be non negative.

power m n computes m^n, n must be non negative.

Printer for polynomial expressions.

Pretty printing.

Printer for LMI.

See Monomial.pp_names for details about names.

See Monomial.pp for details about names.

Pretty printing.

Printer for environment values computed by solver.

profile f executes the function f and returns both its result and the execution time in second.

Register a scalar value in value environement

Returns the same matrix, without its rows and columns containing only 0.

compose le [v_1, l_1;...; v_n, l_n] replaces each variable v_i by l_i in l.

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

Returns -1, 0 or 1 when its argument is respectively < 0, 0 or > 0.

solve obj l tries to optimise the objective obj under the constraint that each polynomial expressions in l is SOS.

solve obj constraints solves the SDP problem: max{ tr(obj X) | tr(A_1 X) = a_1,..., tr(A_n X) = a_n, X psd } with [(A_1, a_1);...; (A_n, a_n)] the constraints list.

Same as Sdp.solve_sparse with dense matrices as input.

solve obj constraints solves the SDP problem: max{ tr(obj X) | tr(A_1 X) = a_1,..., tr(A_m X) = a_m, X psd } with [(A_1, a_1);...; (A_m, a_m)] the constraints list.

solve obj l tries to optimise the objective obj under the constraint that each matrix expressions in l is positive semi-definite.

solve ?verbose obj constraints solves the SDP problem: max{ tr(obj X) | tr(A_1 X) = a_1,..., tr(A_n X) = a_n, X psd } with [(A_1, a_1);...; (A_n, a_n)] the constraints list.

Same as Sdp.solve_ext_sparse with dense matrices as input.

solve obj constraints solves the SDP problem: max{ c^T x + tr(obj X) | b_1^- <= a_1^T x + tr(A_1 X) <= a_1^+,..., b_m^- <= a_m x + tr(A_m X) <= b_m^+, d_1^- <= x_1 <= d_1^+,..., d_n^- <= x_n <= d_n^+, X psd } with [(a_1, A_1, b_1^-, b_1^+);...; (a_m, A_m, b_m^-, b_m^+)] the constraints list and [(d_1^-, d_1^+),..., (d_n^-, d_n^+)] the bounds list (missing bounds are considered as (neg_infinity, infinity), bounds about variables x_i not appearing in the objective or constraints may be ignored).

solve_ext_sparse obj constraints bounds solves the SDP problem: max{ obj | constraints, bounds, X psd }.

See Sdp.solve_ext_sparse for details.

See Sdp.solve_ext_sparse for details.

solve_sparse obj constraints solves the SDP problem: max{ tr(obj X) | constraints, X psd }.

Matrix subtraction.

The returned array is a copy that can be freely modified by the user.

Returns a list sorted in increasing order of Monomial.compare without duplicates.

Returns a list sorted in increasing order of Monomial.compare without duplicates nor zeros.

The returned list contains only non negative values and its last element is non zero (or the list is empty).

Returns a list sorted in increasing order of Ident.compare without duplicates nor zeros.

Matrix transposition.

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

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

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

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

var ?c ?d i returns c xi^d, this is equivalent to of_list [c, Monomial.var ~d i].

var ?d i returns xi^d, this is equivalent to of_list [0;...; O; d] with i zeros.

var s n creates a new variable (Var v).

Same as LinExpr.S.of_list with the list [ident, Coeff.one] and constant Coeff.zero.

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

zeros n m builds a matrix of size n x m with all coefficients equal to Coeff.of_int O.