package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = Z.t monome
val const : Z.t -> t

Empty monomial, from constant (decides type)

val singleton : Z.t -> term -> t

One term.

val of_list : Z.t -> (Z.t * term) list -> t
val of_term : term -> t option
val of_term_exn : term -> t

try to get a monome from a term.

  • raises NotLinear

    if the term is not a proper monome.

val to_term : t -> term

convert back to a term

val has_instances : t -> bool

For real or rational, always true. For integers, returns true iff g divides m.constant, where g is the GCD of c for c in m.coeffs.

The intuition is that this returns true iff the monome actually has some instances in its type. Trivially true in reals or rationals, this is only the case for integers if m.coeffs + m.constant = 0 is a satisfiable diophantine equation.

val quotient : t -> Z.t -> t option

quotient e c tries to divide e by c, returning e/c if it is still an integer expression. For instance, quotient (2x + 4y) 2 will return Some (x + 2y)

val divisible : t -> Z.t -> bool

divisible e n returns true if all coefficients of e are divisible by n and n is an int >= 2

val factorize : t -> (t * Z.t) option

Factorize e into Some (e',s) if e = e' x s, None otherwise (ie if s=1). In case it returns Some (e', s), s > 1 holds

val normalize_wrt_zero : t -> t

Allows to multiply or divide by any positive number since we consider that the monome is equal to (or compared with) zero. For integer monomes, the result will have co-prime coefficients.

val reduce_same_factor : t -> t -> term -> t * t

reduce_same_factor m1 m2 t multiplies m1 and m2 by some constants, so that their coefficient for t is the same.

val compare : (term -> term -> Comparison.t) -> t -> t -> Comparison.t

Compare monomes as if they were multisets of terms, the coefficient in front of a term being its multiplicity.

val to_multiset : t -> Multisets.MT.t

Multiset of terms with multiplicity

Modular Computations

module Modulo : sig ... end

Find Solutions

module Solve : sig ... end