sig
  exception No_solution
  exception Nonlinear
  module type Vector =
    sig
      type t
      type dim
      type scalar
      val equal : Linear.Vector.t -> Linear.Vector.t -> bool
      val add : Linear.Vector.t -> Linear.Vector.t -> Linear.Vector.t
      val scalar_mul :
        Linear.Vector.scalar -> Linear.Vector.t -> Linear.Vector.t
      val negate : Linear.Vector.t -> Linear.Vector.t
      val sub : Linear.Vector.t -> Linear.Vector.t -> Linear.Vector.t
      val dot : Linear.Vector.t -> Linear.Vector.t -> Linear.Vector.scalar
      val zero : Linear.Vector.t
      val is_zero : Linear.Vector.t -> bool
      val add_term :
        Linear.Vector.scalar ->
        Linear.Vector.dim -> Linear.Vector.t -> Linear.Vector.t
      val of_term :
        Linear.Vector.scalar -> Linear.Vector.dim -> Linear.Vector.t
      val enum :
        Linear.Vector.t ->
        (Linear.Vector.scalar * Linear.Vector.dim) BatEnum.t
      val of_enum :
        (Linear.Vector.scalar * Linear.Vector.dim) BatEnum.t ->
        Linear.Vector.t
      val of_list :
        (Linear.Vector.scalar * Linear.Vector.dim) list -> Linear.Vector.t
      val coeff :
        Linear.Vector.dim -> Linear.Vector.t -> Linear.Vector.scalar
      val pivot :
        Linear.Vector.dim ->
        Linear.Vector.t -> Linear.Vector.scalar * Linear.Vector.t
    end
  module ZZVector :
    sig
      type t
      type dim = int
      type scalar = ZZ.t
      val equal : t -> t -> bool
      val add : t -> t -> t
      val scalar_mul : scalar -> t -> t
      val negate : t -> t
      val sub : t -> t -> t
      val dot : t -> t -> scalar
      val zero : t
      val is_zero : t -> bool
      val add_term : scalar -> dim -> t -> t
      val of_term : scalar -> dim -> t
      val enum : t -> (scalar * dim) BatEnum.t
      val of_enum : (scalar * dim) BatEnum.t -> t
      val of_list : (scalar * dim) list -> t
      val coeff : dim -> t -> scalar
      val pivot : dim -> t -> scalar * t
      val compare : t -> t -> int
      val pp : Format.formatter -> t -> unit
      val show : t -> string
    end
  module QQVector :
    sig
      type t
      type dim = int
      type scalar = QQ.t
      val equal : t -> t -> bool
      val add : t -> t -> t
      val scalar_mul : scalar -> t -> t
      val negate : t -> t
      val sub : t -> t -> t
      val dot : t -> t -> scalar
      val zero : t
      val is_zero : t -> bool
      val add_term : scalar -> dim -> t -> t
      val of_term : scalar -> dim -> t
      val enum : t -> (scalar * dim) BatEnum.t
      val of_enum : (scalar * dim) BatEnum.t -> t
      val of_list : (scalar * dim) list -> t
      val coeff : dim -> t -> scalar
      val pivot : dim -> t -> scalar * t
      val compare : t -> t -> int
      val pp : Format.formatter -> t -> unit
      val show : t -> string
    end
  module QQMatrix :
    sig
      type t
      type dim = int
      type scalar = QQ.t
      val equal : Linear.QQMatrix.t -> Linear.QQMatrix.t -> bool
      val add : Linear.QQMatrix.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t
      val scalar_mul :
        Linear.QQMatrix.scalar -> Linear.QQMatrix.t -> Linear.QQMatrix.t
      val mul : Linear.QQMatrix.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t
      val zero : Linear.QQMatrix.t
      val identity : Linear.QQMatrix.dim list -> Linear.QQMatrix.t
      val row : Linear.QQMatrix.dim -> Linear.QQMatrix.t -> Linear.QQVector.t
      val rowsi :
        Linear.QQMatrix.t ->
        (Linear.QQMatrix.dim * Linear.QQVector.t) BatEnum.t
      val add_row :
        Linear.QQMatrix.dim ->
        Linear.QQVector.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t
      val add_column :
        Linear.QQMatrix.dim ->
        Linear.QQVector.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t
      val add_entry :
        Linear.QQMatrix.dim ->
        Linear.QQMatrix.dim -> QQ.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t
      val pivot :
        Linear.QQMatrix.dim ->
        Linear.QQMatrix.t -> Linear.QQVector.t * Linear.QQMatrix.t
      val transpose : Linear.QQMatrix.t -> Linear.QQMatrix.t
      val entry :
        Linear.QQMatrix.dim ->
        Linear.QQMatrix.dim -> Linear.QQMatrix.t -> Linear.QQMatrix.scalar
      val entries :
        Linear.QQMatrix.t ->
        (Linear.QQMatrix.dim * Linear.QQMatrix.dim * Linear.QQMatrix.scalar)
        BatEnum.t
      val row_set : Linear.QQMatrix.t -> SrkUtil.Int.Set.t
      val column_set : Linear.QQMatrix.t -> SrkUtil.Int.Set.t
      val nb_rows : Linear.QQMatrix.t -> int
      val nb_columns : Linear.QQMatrix.t -> int
      val pp : Format.formatter -> Linear.QQMatrix.t -> unit
      val show : Linear.QQMatrix.t -> string
      val rational_eigenvalues : Linear.QQMatrix.t -> (QQ.t * int) list
    end
  module type AbelianGroup =
    sig
      type t
      val equal : Linear.AbelianGroup.t -> Linear.AbelianGroup.t -> bool
      val add :
        Linear.AbelianGroup.t ->
        Linear.AbelianGroup.t -> Linear.AbelianGroup.t
      val negate : Linear.AbelianGroup.t -> Linear.AbelianGroup.t
      val zero : Linear.AbelianGroup.t
    end
  module type Ring =
    sig
      type t
      val equal : Linear.Ring.t -> Linear.Ring.t -> bool
      val add : Linear.Ring.t -> Linear.Ring.t -> Linear.Ring.t
      val negate : Linear.Ring.t -> Linear.Ring.t
      val zero : Linear.Ring.t
      val mul : Linear.Ring.t -> Linear.Ring.t -> Linear.Ring.t
      val one : Linear.Ring.t
    end
  module RingMap :
    functor
      (M : sig
             type 'a t
             type key
             val equal :
               ('a -> 'a -> bool) ->
               'a Linear.RingMap.t -> 'a Linear.RingMap.t -> bool
             val compare :
               ('a -> 'a -> int) ->
               'a Linear.RingMap.t -> 'a Linear.RingMap.t -> int
             val enum :
               'a Linear.RingMap.t -> (Linear.RingMap.key * 'a) BatEnum.t
             val map :
               ('a -> 'b) -> 'a Linear.RingMap.t -> 'b Linear.RingMap.t
             val find : Linear.RingMap.key -> 'a Linear.RingMap.t -> 'a
             val add :
               Linear.RingMap.key ->
               'a -> 'a Linear.RingMap.t -> 'a Linear.RingMap.t
             val remove :
               Linear.RingMap.key ->
               'a Linear.RingMap.t -> 'a Linear.RingMap.t
             val empty : 'a Linear.RingMap.t
             val merge :
               (Linear.RingMap.key -> 'a option -> 'b option -> 'c option) ->
               'a Linear.RingMap.t ->
               'b Linear.RingMap.t -> 'c Linear.RingMap.t
           end) (R : Ring) ->
      sig
        type t = R.t M.t
        type dim = M.key
        type scalar = R.t
        val equal : t -> t -> bool
        val add : t -> t -> t
        val scalar_mul : scalar -> t -> t
        val negate : t -> t
        val sub : t -> t -> t
        val dot : t -> t -> scalar
        val zero : t
        val is_zero : t -> bool
        val add_term : scalar -> dim -> t -> t
        val of_term : scalar -> dim -> t
        val enum : t -> (scalar * dim) BatEnum.t
        val of_enum : (scalar * dim) BatEnum.t -> t
        val of_list : (scalar * dim) list -> t
        val coeff : dim -> t -> scalar
        val pivot : dim -> t -> scalar * t
      end
  val nullspace : Linear.QQMatrix.t -> int list -> Linear.QQVector.t list
  val solve_exn : Linear.QQMatrix.t -> Linear.QQVector.t -> Linear.QQVector.t
  val solve :
    Linear.QQMatrix.t -> Linear.QQVector.t -> Linear.QQVector.t option
  val orient :
    (int -> bool) -> Linear.QQVector.t list -> (int * Linear.QQVector.t) list
  val vector_right_mul :
    Linear.QQMatrix.t -> Linear.QQVector.t -> Linear.QQVector.t
  val intersect_rowspace :
    Linear.QQMatrix.t ->
    Linear.QQMatrix.t -> Linear.QQMatrix.t * Linear.QQMatrix.t
  val divide_right :
    Linear.QQMatrix.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t option
  val max_rowspace_projection :
    Linear.QQMatrix.t -> Linear.QQMatrix.t -> Linear.QQMatrix.t
  val rational_triangulation :
    Linear.QQMatrix.t -> Linear.QQMatrix.t * Linear.QQMatrix.t
  val evaluate_affine : (int -> QQ.t) -> Linear.QQVector.t -> QQ.t
  val sym_of_dim : int -> Syntax.symbol option
  val dim_of_sym : Syntax.symbol -> int
  val const_dim : int
  val const_linterm : QQ.t -> Linear.QQVector.t
  val const_of_linterm : Linear.QQVector.t -> QQ.t option
  val linterm_of : 'a Syntax.context -> 'a Syntax.term -> Linear.QQVector.t
  val of_linterm : 'a Syntax.context -> Linear.QQVector.t -> 'a Syntax.term
  val pp_linterm :
    'a Syntax.context -> Format.formatter -> Linear.QQVector.t -> unit
  val evaluate_linterm : (Syntax.symbol -> QQ.t) -> Linear.QQVector.t -> QQ.t
  val linterm_size : Linear.QQVector.t -> int
end