package logtk

  1. Overview
  2. Docs
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
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

Add given number to constant

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.

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
val set : 'a t -> int -> ('a * term) -> 'a t
val set_term : 'a t -> int -> term -> 'a t
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

For fields (Q,R)