# package logtk

Legend:
Library
Module
Module type
Parameter
Class
Class type
`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`.