Module Micromega_plugin.Linsolve

The purpose of the solver is to generate *all* the integer solutions of a system of linear equations of the following form: 1- all the variables are positive 2- all the coefficients are positive

We expect the systems and the number of solutions to be small. This motivates a simple solver which performs 1 - interval analysis 2 - substitutions 3 - enumeration

system represents a system of equation. Each equation is indexed by a unique identifier id (an integer).

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