package logtk

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

Module Logtk.MonomeSource

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

Sourcetype term = Term.t
Sourcetype 'a t

A monome over terms, with coefficient of type 'a

Sourcetype 'a monome = 'a t
Sourceval equal : 'n t -> 'n t -> bool

structural equality

Sourceval compare : 'n t -> 'n t -> int

arbitrary total order on monomes

Sourceval hash : _ t -> int
Sourceval ty : _ t -> Type.t

type of the monome (int or rat)

Sourceval const : 'a t -> 'a

constant

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

coefficients

Sourceval find : 'a t -> term -> 'a option
Sourceval find_exn : 'a t -> term -> 'a
Sourceval mem : _ t -> term -> bool

Is the term in the monome?

Sourceval add : 'a t -> 'a -> term -> 'a t

Add term with coefficient. Sums coeffs.

Sourceval add_const : 'a t -> 'a -> 'a t

Add given number to constant

Sourceval remove : 'a t -> term -> 'a t

Remove the term

Sourceval remove_const : 'a t -> 'a t

Remove the constant

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

Returns true if the monome is only a constant

Sourceval is_zero : _ t -> bool

return true if the monome is the constant 0

Sourceval sign : _ t -> int

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

Sourceval size : _ t -> int

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

Sourceval terms : _ t -> term list

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

Sourceval var_occurs : var:Term.var -> _ t -> bool

Does the variable occur in the monome?

Sourceval sum : 'a t -> 'a t -> 'a t
Sourceval difference : 'a t -> 'a t -> 'a t
Sourceval uminus : 'a t -> 'a t
Sourceval product : 'a t -> 'a -> 'a t

Product with constant

Sourceval succ : 'a t -> 'a t

+1

Sourceval pred : 'a t -> 'a t

-1

Sourceval sum_list : 'a t list -> 'a t

Sum of a list.

  • raises Failure

    if the list is empty

Sourceval 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

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

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

Sourceval 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

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

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

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

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

Are there no variables in the monome?

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

Fold over terms

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

Fold over terms that are maximal in the given ordering.

Sourceval nth : 'a t -> int -> 'a * term
Sourceval set : 'a t -> int -> ('a * term) -> 'a t
Sourceval set_term : 'a t -> int -> term -> 'a t
Sourcemodule Focus : sig ... end

Focus on a specific term

Sourceval to_string : _ t -> string
Sourceval pp_tstp : _ t CCFormat.printer
Sourceexception NotLinear
Sourcemodule Int : sig ... end
Sourcemodule Rat : sig ... end

For fields (Q,R)