sig
  type 'a t
  type cs_term =
      [ `App of Syntax.symbol * Linear.QQVector.t list
      | `Floor of Linear.QQVector.t
      | `Inv of Linear.QQVector.t
      | `Mod of Linear.QQVector.t * Linear.QQVector.t
      | `Mul of Linear.QQVector.t * Linear.QQVector.t ]
  val pp : Format.formatter -> 'a CoordinateSystem.t -> unit
  val pp_vector :
    'a CoordinateSystem.t -> Format.formatter -> Linear.QQVector.t -> unit
  val pp_cs_term :
    'a CoordinateSystem.t ->
    Format.formatter -> CoordinateSystem.cs_term -> unit
  val mk_empty : 'a Syntax.context -> 'a CoordinateSystem.t
  val get_context : 'a CoordinateSystem.t -> 'a Syntax.context
  val copy : 'a CoordinateSystem.t -> 'a CoordinateSystem.t
  val admit_term : 'a CoordinateSystem.t -> 'a Syntax.term -> unit
  val admit_cs_term :
    'a CoordinateSystem.t -> CoordinateSystem.cs_term -> unit
  val const_id : int
  val dim : 'a CoordinateSystem.t -> int
  val int_dim : 'a CoordinateSystem.t -> int
  val real_dim : 'a CoordinateSystem.t -> int
  val destruct_coordinate :
    'a CoordinateSystem.t -> int -> CoordinateSystem.cs_term
  val term_of_coordinate : 'a CoordinateSystem.t -> int -> 'a Syntax.term
  val term_of_vec :
    'a CoordinateSystem.t -> Linear.QQVector.t -> 'a Syntax.term
  val cs_term_id :
    ?admit:bool -> 'a CoordinateSystem.t -> CoordinateSystem.cs_term -> int
  val vec_of_term :
    ?admit:bool ->
    'a CoordinateSystem.t -> 'a Syntax.term -> Linear.QQVector.t
  val type_of_id : 'a CoordinateSystem.t -> int -> [ `TyInt | `TyReal ]
  val polynomial_of_term :
    'a CoordinateSystem.t -> 'a Syntax.term -> Polynomial.Mvp.t
  val polynomial_of_vec :
    'a CoordinateSystem.t -> Linear.QQVector.t -> Polynomial.Mvp.t
  val polynomial_of_coordinate :
    'a CoordinateSystem.t -> int -> Polynomial.Mvp.t
  val term_of_polynomial :
    'a CoordinateSystem.t -> Polynomial.Mvp.t -> 'a Syntax.term
  val admits : 'a CoordinateSystem.t -> 'a Syntax.term -> bool
  val project_ideal :
    'a CoordinateSystem.t ->
    Polynomial.Mvp.t list ->
    ?subterm:(Syntax.symbol -> bool) ->
    (Syntax.symbol -> bool) ->
    (int * 'a Syntax.term * 'a Syntax.formula) list
  val subcoordinates : 'a CoordinateSystem.t -> int -> SrkUtil.Int.Set.t
  val direct_subcoordinates :
    'a CoordinateSystem.t -> int -> SrkUtil.Int.Set.t
end