Module `Int.Solve`

type solution = (term * t) list: List of constraints (term = monome). It means that if all those constraints are satisfied, then a solution to the given problem has been found

val split_solution : solution -> Subst.t * solution: Split the solution into a variable substitution, and a list of constraints on non-variable terms

val diophant2 : Z.t -> Z.t -> Z.t -> Z.t * Z.t * Z.t

Find the solution vector for this diophantine equation, or fails.

returns: a triple u, v, gcd such that for all int k, u + b * k, v - a * k is solution of equation a * x + b * y = const.

raises Failure: if the equation is unsolvable

val diophant_l : Z.t list -> Z.t -> Z.t list * Z.t

generalize diophantine equation solving to a list of at least two coefficients.

returns: a list of Bezout coefficients, and the GCD of the input list, or fails

raises Failure: if the equation is not solvable

val coeffs_n : Z.t list -> Z.t -> term list -> t list

coeffs_n l gcd, if length l = n, returns a function that takes a list of n-1 terms k1, ..., k(n-1) and returns a list of monomes m1, ..., mn that depend on k1, ..., k(n-1) such that the sum l1 * m1 + l2 * m2 + ... + ln * mn = 0.

Note that the input list of the solution must have n-1 elements, but that it returns a list of n elements!

parameter gcd: is the gcd of all members of l.

parameter l: is a list of at least 2 elements, none of which should be 0

val eq_zero : ?⁠fresh_var:(Type.t -> term) -> t -> solution list

Returns substitutions that make the monome always equal to zero. Fresh variables may be generated using fresh_var, for diophantine equations. Returns the empty list if no solution is found.

For instance, on the monome 2X + 3Y - 7, it may generate a new variable Z and return the substitution X -> 3Z - 7, Y -> 2Z + 7

val lower_zero : ?⁠fresh_var:(Type.t -> term) -> strict:bool -> t -> solution list

Solve for the monome to be always lower than zero (strict determines whether the inequality is strict or not). This may not return all solutions, but a subspace of it

parameter fresh_var: see solve_eq_zero

val lt_zero : ?⁠fresh_var:(Type.t -> term) -> t -> solution list: Shortcut for lower_zero when strict = true

val leq_zero : ?⁠fresh_var:(Type.t -> term) -> t -> solution list: Shortcut for lower_zero when strict = false

val neq_zero : ?⁠fresh_var:(Type.t -> term) -> t -> solution list: Find some solutions that negate the equation. For now it just takes solutions to m < 0.