module Monome:sig
..end
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".
typeterm =
Libzipperposition.FOTerm.t
type 'a
t
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
val const : 'a t -> 'a
val coeffs : 'a t -> ('a * term) list
val find : 'a t -> term -> 'a option
val find_exn : 'a t -> term -> 'a
Not_found
if not presentval mem : 'a t -> term -> bool
val add : 'a t -> 'a -> term -> 'a t
val add_const : 'a t -> 'a -> 'a t
val remove : 'a t -> term -> 'a t
val remove_const : 'a t -> 'a t
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
true
if the monome is only a constantval is_zero : 'a t -> bool
true
if the monome is the constant 0val sign : 'a t -> int
is_constant m
, sign m
returns the sign of m
.Invalid_argument
if the monome is not a constantval size : 'a t -> int
val terms : 'a t -> term list
val var_occurs : var:Libzipperposition.FOTerm.var -> 'a t -> bool
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
val succ : 'a t -> 'a t
val pred : 'a t -> 'a t
val sum_list : 'a t list -> 'a t
Failure
if the list is emptyval comparison : 'a t -> 'a t -> Libzipperposition.Comparison.t
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.m1, m2
such that m = m1 - m2
and m1,m2
both have positive
coefficientsval apply_subst : renaming:Libzipperposition.Substs.Renaming.t ->
Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t -> 'a t
val apply_subst_no_renaming : Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t -> 'a t
val variant : ?subst:Libzipperposition.Substs.t ->
'a t Libzipperposition.Scoped.t ->
'a t Libzipperposition.Scoped.t ->
Libzipperposition.Substs.t Sequence.t
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
val fold : ('a -> int -> 'b -> term -> 'a) -> 'a -> 'b t -> 'a
val fold_max : ord:Libzipperposition.Ordering.t ->
('a -> int -> 'b -> term -> 'a) -> 'a -> 'b t -> 'a
val nth : 'a t -> int -> 'a * term
Invalid_argument
if the index is invalidval set : 'a t -> int -> 'a * term -> 'a t
Invalid_argument
if the index is invalidval set_term : 'a t -> int -> term -> 'a t
Invalid_argument
if the index is invalidmodule Focus:sig
..end
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