package logtk

  1. Overview
  2. Docs
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.