1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** 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
(** [var] is the type of variables *)
type var = int
(** [id] are used to identify equations in a system *)
type id = int
(** An equation [eqn] is of the form a1.x1 + ... + an.xn = a0
where the ai are integer coefficients and xi are variables.
*)
type eqn
(** [output_equations o l] prints the list of equations *)
val output_equations : out_channel -> eqn list -> unit
(** [empty] is the system with no equation *)
val empty : system
(** [set_constant i c s] returns the equation [i]
of the system [s] where the constant a0 is set to [c] *)
val set_constant : id -> int -> system -> eqn
(** [make_mon i x a s] augments the system [s]
with the equation a.x = 0 indexed by i *)
val make_mon : id -> var -> int -> 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
*)
val merge : system -> system -> system
(** [solution] assigns a value to each variable *)
type solution = (var * int) list
(** [output_solutions o l] outputs the list of solutions *)
val output_solutions : out_channel -> solution list -> unit
(** [solve_and_enum l] solves the system of equations
and enumerate all the solutions *)
val solve_and_enum : eqn list -> solution list
|
