sig
  module Poly : Polynomial.S
  type var
  type polynomial_expr =
      Const of Poly.t
    | Var of Sos.S.var
    | Mult_scalar of Poly.Coeff.t * Sos.S.polynomial_expr
    | Add of Sos.S.polynomial_expr * Sos.S.polynomial_expr
    | Sub of Sos.S.polynomial_expr * Sos.S.polynomial_expr
    | Mult of Sos.S.polynomial_expr * Sos.S.polynomial_expr
    | Power of Sos.S.polynomial_expr * int
    | Compose of Sos.S.polynomial_expr * Sos.S.polynomial_expr list
    | Derive of Sos.S.polynomial_expr * int
  val make :
    ?n:int -> ?d:int -> ?homogen:bool -> string -> Sos.S.polynomial_expr
  val const : Poly.t -> Sos.S.polynomial_expr
  val scalar : Poly.Coeff.t -> Sos.S.polynomial_expr
  val monomial : Monomial.t -> Sos.S.polynomial_expr
  val mult_scalar :
    Poly.Coeff.t -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val add :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val sub :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val mult :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val power : Sos.S.polynomial_expr -> int -> Sos.S.polynomial_expr
  val compose :
    Sos.S.polynomial_expr ->
    Sos.S.polynomial_expr list -> Sos.S.polynomial_expr
  val derive : Sos.S.polynomial_expr -> int -> Sos.S.polynomial_expr
  val of_list :
    (Monomial.t * Sos.S.polynomial_expr) list -> Sos.S.polynomial_expr
  exception Dimension_error
  val to_list :
    Sos.S.polynomial_expr -> (Monomial.t * Sos.S.polynomial_expr) list
  val nb_vars : Sos.S.polynomial_expr -> int
  val degree : Sos.S.polynomial_expr -> int
  val is_homogeneous : Sos.S.polynomial_expr -> bool
  val param_vars : Sos.S.polynomial_expr -> Sos.S.var list
  val ( !! ) : Poly.t -> Sos.S.polynomial_expr
  val ( ?? ) : int -> Sos.S.polynomial_expr
  val ( ! ) : Poly.Coeff.t -> Sos.S.polynomial_expr
  val ( *. ) : Poly.Coeff.t -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val ( ~- ) : Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val ( + ) :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val ( - ) :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val ( * ) :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val ( / ) : Sos.S.polynomial_expr -> Poly.Coeff.t -> Sos.S.polynomial_expr
  val ( /. ) : Poly.Coeff.t -> Poly.Coeff.t -> Sos.S.polynomial_expr
  val ( ** ) : Sos.S.polynomial_expr -> int -> Sos.S.polynomial_expr
  val ( >= ) :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val ( <= ) :
    Sos.S.polynomial_expr -> Sos.S.polynomial_expr -> Sos.S.polynomial_expr
  val pp : Stdlib.Format.formatter -> Sos.S.polynomial_expr -> unit
  val pp_names :
    string list -> Stdlib.Format.formatter -> Sos.S.polynomial_expr -> unit
  type options = {
    sdp : Sdp.options;
    verbose : int;
    scale : bool;
    trace_obj : bool;
    dualize : bool;
    monoms : Monomial.t list list;
    pad : float;
    pad_list : float list;
  }
  val default : Sos.S.options
  type obj =
      Minimize of Sos.S.polynomial_expr
    | Maximize of Sos.S.polynomial_expr
    | Purefeas
  type values
  type 'a witness = Monomial.t array * 'a array array
  exception Not_linear
  val solve :
    ?options:Sos.S.options ->
    ?solver:Sdp.solver ->
    Sos.S.obj ->
    Sos.S.polynomial_expr list ->
    SdpRet.t * (float * float) * Sos.S.values * float Sos.S.witness list
  val value : Sos.S.polynomial_expr -> Sos.S.values -> Poly.Coeff.t
  val value_poly : Sos.S.polynomial_expr -> Sos.S.values -> Poly.t
  val check :
    ?options:Sos.S.options ->
    ?values:Sos.S.values ->
    Sos.S.polynomial_expr -> float Sos.S.witness -> bool
  val check_round :
    ?options:Sos.S.options ->
    ?values:Sos.S.values ->
    Sos.S.polynomial_expr list ->
    float Sos.S.witness list ->
    (Sos.S.values * Scalar.Q.t Sos.S.witness list) option
end