Module Linear

module Linear: sig .. end
Various operations for the vector space int -> QQ


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:
val dim_of_sym : Syntax.symbol -> int
Map a dimension to symbol. The following equations hold:
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