package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Monome.IntSource

Sourcetype t = Z.t monome
Sourceval const : Z.t -> t

Empty monomial, from constant (decides type)

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

One term.

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

try to get a monome from a term.

  • raises NotLinear

    if the term is not a proper monome.

Sourceval to_term : t -> term

convert back to a term

Sourceval 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.

Sourceval 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)

Sourceval 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

Sourceval 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

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval to_multiset : t -> Multisets.MT.t

Multiset of terms with multiplicity

Modular Computations

Sourcemodule Modulo : sig ... end

Find Solutions

Sourcemodule Solve : sig ... end
OCaml

Innovation. Community. Security.