sig
  type t
  module V = Linear.QQVector
  val enum :
    Polyhedron.t ->
    [ `EqZero of V.t | `LeqZero of V.t | `LtZero of V.t ] BatEnum.t
  val pp : 'a CoordinateSystem.t -> Format.formatter -> Polyhedron.t -> unit
  val conjoin : Polyhedron.t -> Polyhedron.t -> Polyhedron.t
  val top : Polyhedron.t
  val of_formula :
    ?admit:bool -> 'a CoordinateSystem.t -> 'a Syntax.formula -> Polyhedron.t
  val to_formula : 'a CoordinateSystem.t -> Polyhedron.t -> 'a Syntax.formula
  val to_apron :
    'a CoordinateSystem.t ->
    'a SrkApron.Env.t ->
    'abs Apron.Manager.t -> Polyhedron.t -> ('a, 'abs) SrkApron.property
  val mem : (int -> QQ.t) -> Polyhedron.t -> bool
  val of_implicant :
    ?admit:bool ->
    'a CoordinateSystem.t -> 'a Syntax.formula list -> Polyhedron.t
  val implicant_of :
    'a CoordinateSystem.t -> Polyhedron.t -> 'a Syntax.formula list
  val local_project :
    (int -> QQ.t) -> int list -> Polyhedron.t -> Polyhedron.t
  val project : int list -> Polyhedron.t -> Polyhedron.t
  val try_fourier_motzkin :
    'a CoordinateSystem.t ->
    (Syntax.symbol -> bool) -> Polyhedron.t -> Polyhedron.t
end