sig
type t = Z.t Monome.monome
val const : Z.t -> Monome.Int.t
val singleton : Z.t -> Monome.term -> Monome.Int.t
val of_list : Z.t -> (Z.t * Monome.term) list -> Monome.Int.t
val of_term : Monome.term -> Monome.Int.t option
val of_term_exn : Monome.term -> Monome.Int.t
val to_term : Monome.Int.t -> Monome.term
val normalize : Monome.Int.t -> Monome.Int.t
val has_instances : Monome.Int.t -> bool
val quotient : Monome.Int.t -> Z.t -> Monome.Int.t option
val divisible : Monome.Int.t -> Z.t -> bool
val factorize : Monome.Int.t -> (Monome.Int.t * Z.t) option
val normalize_wrt_zero : Monome.Int.t -> Monome.Int.t
val reduce_same_factor :
Monome.Int.t ->
Monome.Int.t -> Monome.term -> Monome.Int.t * Monome.Int.t
val compare :
(Monome.term -> Monome.term -> Libzipperposition.Comparison.t) ->
Monome.Int.t -> Monome.Int.t -> Libzipperposition.Comparison.t
val to_multiset : Monome.Int.t -> Multisets.MT.t
module Modulo :
sig
val modulo : n:Z.t -> Z.t -> Z.t
val sum : n:Z.t -> Z.t -> Z.t -> Z.t
val uminus : n:Z.t -> Z.t -> Z.t
end
module Solve :
sig
type solution = (Monome.term * Monome.Int.t) list
val split_solution :
Monome.Int.Solve.solution ->
Libzipperposition.Substs.t * Monome.Int.Solve.solution
val diophant2 : Z.t -> Z.t -> Z.t -> Z.t * Z.t * Z.t
val diophant_l : Z.t list -> Z.t -> Z.t list * Z.t
val coeffs_n : Z.t list -> Z.t -> Monome.term list -> Monome.Int.t list
val eq_zero :
?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
Monome.Int.t -> Monome.Int.Solve.solution list
val lower_zero :
?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
strict:bool -> Monome.Int.t -> Monome.Int.Solve.solution list
val lt_zero :
?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
Monome.Int.t -> Monome.Int.Solve.solution list
val leq_zero :
?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
Monome.Int.t -> Monome.Int.Solve.solution list
val neq_zero :
?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
Monome.Int.t -> Monome.Int.Solve.solution list
end
end