Module Linear

module Linear: sig .. end

Various operations for the vector space int -> QQ

exception No_solution

Raised for unsolvable systems of linear equations

exception Nonlinear

module type Vector = sig .. end

module ZZVector: sig .. end

module QQVector: sig .. end

module QQMatrix: sig .. end

module type AbelianGroup = sig .. end

module type Ring = sig .. end

module RingMap: functor (M : sig
type 'a t 


type key 


val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val enum : 'a t -> (key * 'a) BatEnum.t
val map : ('a -> 'b) -> 'a t -> 'b t
val find : key -> 'a t -> 'a
val add : key -> 'a -> 'a t -> 'a t
val remove : key -> 'a t -> 'a t
val empty : 'a t
val merge : (key -> 'a option -> 'b option -> 'c option) ->
       'a t -> 'b t -> 'c t
end) -> functor (R : Ring) -> Vector  with type t = R.t M.t
                         and type dim = M.key
                         and type scalar = R.t

Lift a map type over a ring to a left-module

val nullspace : QQMatrix.t -> int list -> QQVector.t list

nullspace mat dimensions computes a basis for the vector space

{ x :
    max*x = 0}

, projected on to the set of dimensions dimensions. (Note that the nullspace is not finitely generated in int -> QQ, hence the projection).

val solve_exn : QQMatrix.t -> QQVector.t -> QQVector.t

solve_exn mat b computes a rational vector x such that

mat*x =
    b

. Raises No_solution if there is no solution.

val solve : QQMatrix.t -> QQVector.t -> QQVector.t option

solve mat b computes a rational vector x such that mat*x = b, if such a vector exists. Otherwise, return None.

val orient : (int -> bool) -> QQVector.t list -> (int * QQVector.t) list

Given a predicate on dimensions and a list of terms (all implicitly equal to zero), orient the equations as rewrite rules that eliminate dimensions that don't satisfy the predicate.

val vector_right_mul : QQMatrix.t -> QQVector.t -> QQVector.t

vector_right_mul m a computes m*a

val intersect_rowspace : QQMatrix.t ->
       QQMatrix.t -> QQMatrix.t * QQMatrix.t

Given two matrices A and B, compute matrices C and D such that

CA
    = DB

is a basis for the intersection of the rowspaces of A and B.

val divide_right : QQMatrix.t -> QQMatrix.t -> QQMatrix.t option

Given two matrices A and B, compute a matrix C such that CB = A (if one exists). C exists when the rowspace of B is contained in the rowspace of A. If A and B are invertible, then C is exactly AB^-1.

val max_rowspace_projection : QQMatrix.t -> QQMatrix.t -> QQMatrix.t

Given matrices A and B, find a matrix C whose rows constitute a basis for the vector space { v : exists u. uA = vB }

val rational_triangulation : QQMatrix.t -> QQMatrix.t * QQMatrix.t

Given a matrix A, find a pair of matrices (M,T) such that MA = TM, T is lower-triangular, and the rowspace of MA is maximal.

val evaluate_affine : (int -> QQ.t) -> QQVector.t -> QQ.t

Affine terms

Various operations for manipulating affine terms over symbols, represented as rational vectors

val sym_of_dim : int -> Syntax.symbol option

Map a symbol to a dimension. The following equations hold:

sym_of_dim (dim_of_sym sym) = Some sym
sym_of_dim const_dim = None

val dim_of_sym : Syntax.symbol -> int

Map a dimension to symbol. The following equations hold:

sym_of_dim (dim_of_sym sym) = Some sym
sym_of_dim const_dim = None

val const_dim : int

Dimension for representing the coefficient of the constant 1.

val const_linterm : QQ.t -> QQVector.t

Representation of a rational number as an affine term. The equation const_of_linterm (const_linterm qq) = Some qq must hold.

val const_of_linterm : QQVector.t -> QQ.t option

Convert an affine term to a rational number, if possible. The equation const_of_linterm (const_linterm qq) = Some qq must hold.

val linterm_of : 'a Syntax.context -> 'a Syntax.term -> QQVector.t

Convert a rational vector representing an affine term. Raises Nonlinear if the input term is non-linear.

val of_linterm : 'a Syntax.context -> QQVector.t -> 'a Syntax.term

Convert a rational vector to an affine term. The equation

of_linterm srk
    (linterm_of srk t) = t

must hold.

val pp_linterm : 'a Syntax.context -> Format.formatter -> QQVector.t -> unit

Pretty-print an affine term

val evaluate_linterm : (Syntax.symbol -> QQ.t) -> QQVector.t -> QQ.t

evaluate_linterm env t evaluates the affine term t in the environment env

val linterm_size : QQVector.t -> int

Count the number of dimensions with non-zero coefficients