Module Monome

module Monome: sig .. end

Polynomes of order 1, over several variables

.

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 = Libzipperposition.FOTerm.t 
type 'a t 
A monome over terms, with coefficient of type 'a
type 'a monome = 'a t 
val eq : 'n t -> 'n t -> bool
val compare : 'n t -> 'n t -> int
val hash : 'a t -> int
val hash_fun : 'a t CCHash.hash_fun
val ty : 'a t -> Libzipperposition.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 : 'a 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 : 'a t -> bool
Returns true if the monome is only a constant
val is_zero : 'a t -> bool
return true if the monome is the constant 0
val sign : 'a 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 : 'a t -> int
Number of distinct terms. 0 means that the monome is a constant
val terms : 'a t -> term list
List of terms that occur in the monome with non-nul coefficients
val var_occurs : var:Libzipperposition.FOTerm.var -> 'a 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 -> Libzipperposition.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.
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 : renaming:Libzipperposition.Substs.Renaming.t ->
Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t -> 'a t
Apply a substitution to the monome's terms
val apply_subst_no_renaming : Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t -> 'a t
Apply a substitution but doesn't rename free variables. Careful with the collisions
val variant : ?subst:Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t ->
'a t Libzipperposition.Scoped.t ->
Libzipperposition.Substs.t Sequence.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:Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t ->
'a t Libzipperposition.Scoped.t ->
Libzipperposition.Substs.t Sequence.t
val unify : ?subst:Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t ->
'a t Libzipperposition.Scoped.t ->
Libzipperposition.Substs.t Sequence.t
val is_ground : 'a 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:Libzipperposition.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 : 'a t CCFormat.printer
val to_string : 'a t -> string
val pp_tstp : 'a t CCFormat.printer
exception NotLinear
module Int: sig .. end

For fields (Q,R)