Module `Logtk.Monome`

Polynomes of order 1, over several variables

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
val compare : 'n t -> 'n t -> int
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

constant

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

raises Not_found: if not present

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

Add term with coefficient. Sums coeffs.

Add given number to constant

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

Add given number to constant

Remove the term

val remove_const : 'a t -> 'a t

Remove the term

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

Product with constant

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 Sequence.t

val matching : ?⁠subst:Subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> Subst.t Sequence.t
val unify : ?⁠subst:Unif_subst.t -> 'a t Scoped.t -> 'a t Scoped.t -> Unif_subst.t Sequence.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