# package logtk

Legend:
Library
Module
Module type
Parameter
Class
Class type

## Polynomes of order 1, over several variables

.

A monome is a linear expression on several "variables".

We parametrize modules over some class of number (typically, Z or Q) that need to provide some operations. The `'a` parameter is the type of numbers (`Z.t` or `Q.t` from the library Zarith).

Variables, in this module, are non-arithmetic terms, i.e. non-interpreted functions and predicates, that occur immediately under an arithmetic operator. For instance, in the term "f(X) + 1 + 3 × a", the variables are "f(X)" and "a", with coefficients "1" and "3".

`type term = Term.t`
`type 'a t`

A monome over terms, with coefficient of type 'a

`type 'a monome = 'a t`
`val equal : 'n t -> 'n t -> bool`

structural equality

`val compare : 'n t -> 'n t -> int`

arbitrary total order on monomes

`val hash : _ t -> int`
`val ty : _ t -> Type.t`

type of the monome (int or rat)

`val const : 'a t -> 'a`

constant

`val coeffs : 'a t -> ('a * term) list`

coefficients

`val find : 'a t -> term -> 'a option`
`val find_exn : 'a t -> term -> 'a`
• raises Not_found

if not present

`val mem : _ t -> term -> bool`

Is the term in the monome?

`val add : 'a t -> 'a -> term -> 'a t`

Add term with coefficient. Sums coeffs.

`val add_const : 'a t -> 'a -> 'a t`

`val remove : 'a t -> term -> 'a t`

Remove the term

`val remove_const : 'a t -> 'a t`

Remove the constant

`val add_list : 'a t -> ('a * term) list -> 'a t`
`val map : (term -> term) -> 'a t -> 'a t`
`val map_num : ('a -> 'a) -> 'a t -> 'a t`
`module Seq : sig ... end`
`val is_const : _ t -> bool`

Returns `true` if the monome is only a constant

`val is_zero : _ t -> bool`

return `true` if the monome is the constant 0

`val sign : _ t -> int`

Assuming `is_constant m`, `sign m` returns the sign of `m`.

• raises Invalid_argument

if the monome is not a constant

`val size : _ t -> int`

Number of distinct terms. 0 means that the monome is a constant

`val terms : _ t -> term list`

List of terms that occur in the monome with non-nul coefficients

`val var_occurs : var:Term.var -> _ t -> bool`

Does the variable occur in the monome?

`val sum : 'a t -> 'a t -> 'a t`
`val difference : 'a t -> 'a t -> 'a t`
`val uminus : 'a t -> 'a t`
`val product : 'a t -> 'a -> 'a t`

Product with constant

`val succ : 'a t -> 'a t`

+1

`val pred : 'a t -> 'a t`

-1

`val sum_list : 'a t list -> 'a t`

Sum of a list.

• raises Failure

if the list is empty

`val comparison : 'a t -> 'a t -> Comparison.t`

Try to compare two monomes. They may not be comparable (ie on some points, or in some models, one will be bigger), but some pairs of monomes are: for instance, 2X + 1 < 2X + 4 is always true

`val dominates : strict:bool -> 'a t -> 'a t -> bool`

`dominates ~strict m1 m2` is true if `m1` is always greater than `m2`, in any model or variable valuation. if `dominates ~strict:false m1 m2 && dominates ~strict:false m2 m1`, then `m1 = m2`. @argument strict if true, use "greater than", else "greater or equal".

`val normalize : 'a t -> 'a t`

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

`val split : 'a t -> 'a t * 'a t`

`split m` splits into a monome with positive coefficients, and one with negative coefficients.

• returns

`m1, m2` such that `m = m1 - m2` and `m1,m2` both have positive coefficients

`val apply_subst : Subst.Renaming.t -> Subst.t -> 'a t Scoped.t -> 'a t`

Apply a substitution to the monome's terms. This does not preserve positions in the monome.

`val apply_subst_no_simp : Subst.Renaming.t -> Subst.t -> 'a t Scoped.t -> 'a t`

Apply a substitution to the monome's terms, without renormalizing. This preserves positions.

```val variant : ?subst:Subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> Subst.t Iter.t```

Matching and unification aren't complete in the presence of variables occurring directly under the sum, for this would require the variable to be bound to sums (monomes) itself in the general case. Instead, such variables are only bound to atomic terms, excluding constants (ie X+1 = a+1 will bind X to a without problem, but will X+a=a+1 will fail to bind X to 1)

```val matching : ?subst:Subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> Subst.t Iter.t```
```val unify : ?subst:Unif_subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> Unif_subst.t Iter.t```
`val is_ground : _ t -> bool`

Are there no variables in the monome?

`val fold : ('a -> int -> 'b -> term -> 'a) -> 'a -> 'b t -> 'a`

Fold over terms

```val fold_max : ord:Ordering.t -> ('a -> int -> 'b -> term -> 'a) -> 'a -> 'b t -> 'a```

Fold over terms that are maximal in the given ordering.

`val nth : 'a t -> int -> 'a * term`
• raises Invalid_argument

if the index is invalid

`val set : 'a t -> int -> ('a * term) -> 'a t`
• raises Invalid_argument

if the index is invalid

`val set_term : 'a t -> int -> term -> 'a t`
• raises Invalid_argument

if the index is invalid

`module Focus : sig ... end`

Focus on a specific term

`val pp : _ t CCFormat.printer`
`val to_string : _ t -> string`
`val pp_tstp : _ t CCFormat.printer`
`val pp_zf : _ t CCFormat.printer`
`exception NotLinear`
`module Int : sig ... end`
`module Rat : sig ... end`