Module Monome.Int

module Int: sig .. end

type t = Z.t Monome.monome

val const : Z.t -> t

Empty monomial, from constant (decides type)

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

One term.

val of_list : Z.t -> (Z.t * Monome.term) list -> t

val of_term : Monome.term -> t option

val of_term_exn : Monome.term -> t

try to get a monome from a term.
Raises NotLinear if the term is not a proper monome.

val to_term : t -> Monome.term

convert back to a term

val normalize : t -> t

Normalize the monome, which means that if some terms are integer constants, they are moved to the constant part (e.g after apply X->3 in 2.X+1, one gets 2.3 +1. Normalization reduces this to 7).

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 -> Monome.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.
Raises Invalid_argument if t does not belong to m1 or m2

val compare : (Monome.term -> Monome.term -> Libzipperposition.Comparison.t) ->
       t -> t -> Libzipperposition.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