package logtk

Empty monomial, from constant (decides type)

One term.

try to get a monome from a term.

• raises NotLinear

  if the term is not a proper monome.

convert back to a term

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.

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)

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

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

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.

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

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

Multiset of terms with multiplicity