Module Micromega_plugin.Linsolve
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 equationi
of the systems
where the constant a0 is set toc
val make_mon : id -> var -> int -> system -> system
make_mon i x a s
augments the systems
with the equation a.x = 0 indexed by i
val merge : system -> system -> system
merge s1 s2
returns a systems
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