Module Monome.Int.Solve

module Solve: sig .. end

type solution = (Monome.term * Monome.Int.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 ->
       Libzipperposition.Substs.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.
Raises Failure if the equation is unsolvable
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.

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.
Raises Failure if the equation is not solvable
Returns a list of Bezout coefficients, and the GCD of the input list, or fails

val coeffs_n : Z.t list -> Z.t -> Monome.term list -> Monome.Int.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!

val eq_zero : ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
       Monome.Int.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:(Libzipperposition.Type.t -> Monome.term) ->
       strict:bool -> Monome.Int.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

fresh_var : see solve_eq_zero

val lt_zero : ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
       Monome.Int.t -> solution list

Shortcut for Monome.Int.Solve.lower_zero when strict = true

val leq_zero : ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
       Monome.Int.t -> solution list

Shortcut for Monome.Int.Solve.lower_zero when strict = false

val neq_zero : ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
       Monome.Int.t -> solution list

Find some solutions that negate the equation. For now it just takes solutions to m < 0.