module Poly = Polynomial.Floattype polynomial_expr = | Const of Poly.t| Var of var| Mult_scalar of Poly.Coeff.t * polynomial_expr| Add of polynomial_expr * polynomial_expr| Sub of polynomial_expr * polynomial_expr| Mult of polynomial_expr * polynomial_expr| Power of polynomial_expr * int| Compose of polynomial_expr * polynomial_expr list| Derive of polynomial_expr * intConstructors. See the module Polynomial.S for details.
val make : ?n:int -> ?d:int -> ?homogen:bool -> string -> polynomial_exprmake s creates a new parametric variable named s. For instance, make "lambda" creates a new scalar parametric variable and make ~n:1 ~d:2 "p" creates a new polynomial parametric variable (p_0 + p_1 x0 + p_2 x0^2 with p_0, p_1 and p_2 scalar parametric variables).
Functions for above constructors.
val const : Poly.t -> polynomial_exprval scalar : Poly.Coeff.t -> polynomial_exprval monomial : Monomial.t -> polynomial_exprval mult_scalar : Poly.Coeff.t -> polynomial_expr -> polynomial_exprval add : polynomial_expr -> polynomial_expr -> polynomial_exprval sub : polynomial_expr -> polynomial_expr -> polynomial_exprval mult : polynomial_expr -> polynomial_expr -> polynomial_exprval power : polynomial_expr -> int -> polynomial_exprval compose : polynomial_expr -> polynomial_expr list -> polynomial_exprval derive : polynomial_expr -> int -> polynomial_exprval of_list : (Monomial.t * polynomial_expr) list -> polynomial_exprval to_list : polynomial_expr -> (Monomial.t * polynomial_expr) listReturns a list sorted in increasing order of Monomial.compare without duplicates. All polynomial_expr in the returned list are scalars (i.e., functions nb_vars and degree below both return 0).
See the module Polynomial.S for details. Beware that the returned values correspond to the polynomial_expression and can be larger than the result after solving. For instance, considering the expression v x_1^3 + x_0^2 with v a variable, nb_vars and degree will respectively return 2 and 3. Although, when asking the expression to be SOS, v will be 0 and then nb_vars and degree will become respectively 1 and 2 in the result.
val nb_vars : polynomial_expr -> intval degree : polynomial_expr -> intval is_homogeneous : polynomial_expr -> boolval param_vars : polynomial_expr -> var listparam_vars e returns the list of all parametric variables appearing in e.
To use this operators, it's convenient to use local opens. For instance to write the polynomial 2.3 x0^3 x2^2 + x1 + 0.5:
let module Sos = Osdp.Sos.Float in
Sos.(2.3 *. ??0**3 * ??2**2 + ??1 + !0.5)See the module Polynomial.S for details.
val (!!) : Poly.t -> polynomial_exprval (??) : int -> polynomial_exprval (!) : Poly.Coeff.t -> polynomial_exprval (*.) : Poly.Coeff.t -> polynomial_expr -> polynomial_exprval (~-) : polynomial_expr -> polynomial_exprval (+) : polynomial_expr -> polynomial_expr -> polynomial_exprval (-) : polynomial_expr -> polynomial_expr -> polynomial_exprval (*) : polynomial_expr -> polynomial_expr -> polynomial_exprval (/) : polynomial_expr -> Poly.Coeff.t -> polynomial_exprval (/.) : Poly.Coeff.t -> Poly.Coeff.t -> polynomial_exprval (**) : polynomial_expr -> int -> polynomial_exprval (>=) : polynomial_expr -> polynomial_expr -> polynomial_expre1 >= e2 is just syntactic sugar for e1 - e2.
val (<=) : polynomial_expr -> polynomial_expr -> polynomial_expre1 <= e2 is just syntactic sugar for e2 - e1.
val pp : Format.formatter -> polynomial_expr -> unitPrinter for polynomial expressions.
val pp_names : string list -> Format.formatter -> polynomial_expr -> unitSee Monomial.pp_names for details about names.
type options = {sdp : Sdp.options;verbose : int;verbosity level, non negative integer, 0 (default) means no output (but see sdp.verbose just above)
*)scale : bool;scale (default: true)
*)trace_obj : bool;When no objective is set (Purefeas below), minimize the trace of the SOS constraints instead of no objective (default: false).
*)dualize : bool;solve using the dual representation, can be slower but more robust (default: false)
*)monoms : Monomial.t list list;monomials (default: []) for each constraint (automatically determined when list shorter than constraints list)
*)pad : float;padding factor (default: 2.), 0. means no padding
*)pad_list : float list;padding factors (dafault: []) for each constraint (pad used when list shorter than constraints list)
}val default : optionsDefault values above.
Minimize e or Maximize e or Purefeas (just checking feasibility). e must be an affine combination of scalar variables (obtained from var).
type 'a witness = Monomial.t array * 'a array arrayval solve :
?options:options ->
?solver:Sdp.solver ->
obj ->
polynomial_expr list ->
SdpRet.t * (float * float) * values * float witness listsolve obj l tries to optimise the objective obj under the constraint that each polynomial expressions in l is SOS. If solver is provided, it will supersed the solver given in options. Returns a tuple ret, (pobj, dobj), values,
witnesses. 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_poly). witnesses is a list with the same length than l containing pairs v, Q such that Q is a square matrix and v a vector of monomials of the same size and the polynomial v^T Q v should be close from the corresponding polynomial in l.
If ret is SdpRet.Success, then all SOS constraints in l are indeed satisfied by the values returned in values (this is checked through the function check below with witnesses).
val value : polynomial_expr -> values -> Poly.Coeff.tvalue e values returns the evaluation of polynomial expression e, replacing all Var by the correspoding value in values.
val value_poly : polynomial_expr -> values -> Poly.tvalue_poly e values returns the evaluation of polynomial expression e, replacing all Var by the correspoding value in values.
val check :
?options:options ->
?values:values ->
polynomial_expr ->
float witness ->
boolIf check ?options e ?values (v, Q) returns true, then e is SOS. Otherwise, either e is not SOS or the difference between e and v^T Q v is too large or Q is not positive definite enough for the proof to succeed. The witness (v, Q) is typically obtained from the above function solve. If e contains variables, they are replaced by the corresponding value in values (values is empty by default).
Here is how it works. e is expected to be the polynomial v^T Q v modulo numerical errors. To prove that e is SOS despite these numerical errors, we first check that the polynomial e can be expressed as v^T Q' v for some Q' (i.e. that the monomial base v contains enough monomials). Then e can be expressed as v^T (Q + R) v where R is a matrix with all coefficients bounded by the maximum difference between the coefficients of the polynomials e and v^T Q v. If all such matrices Q + R are positive definite, then e is SOS.
val check_round :
?options:options ->
?values:values ->
polynomial_expr list ->
float witness list ->
(values * Scalar.Q.t witness list) optionTODO: doc