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