Module `Micromega_plugin.Linsolve`

type system
type var = int: var is the type of variables

type id = int: id are used to identify equations in a system

type eqn: An equation eqn is of the form a1.x1 + ... + an.xn = a0 where the ai are integer coefficients and xi are variables.

val output_equations : Stdlib.out_channel -> eqn list -> unit: output_equations o l prints the list of equations

val empty : system: empty is the system with no equation

val set_constant : id -> int -> system -> eqn: set_constant i c s returns the equation i of the system s where the constant a0 is set to c

val make_mon : id -> var -> int -> system -> system: make_mon i x a s augments the system s with the equation a.x = 0 indexed by i

val merge : system -> system -> system: merge s1 s2 returns a system s such that the equation i is obtained by adding of the equations s1(i) and s2(i) i.e. s(i) = s1(i) + s2(i) NB: the operation is only well-defined if the variables in s1(i) and s2(i) is disjoint

type solution = (var * int) list: solution assigns a value to each variable

val output_solutions : Stdlib.out_channel -> solution list -> unit: output_solutions o l outputs the list of solutions

val solve_and_enum : eqn list -> solution list: solve_and_enum l solves the system of equations and enumerate all the solutions