colibrilib

A library of domains and propagators proved in Why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library colibrilib
Module Colibrilib . QUtils
val floor : Q.t -> Z.t

floor a return the greatest integer smaller or equal than a

val ceil : Q.t -> Z.t

ceil a return the smallest integer greater or equal than a

val divisible_down_to : Q.t -> Q.t -> Q.t

divisible_down_to a m return the greatest multiple of m smaller or equal than a

val divisible_up_to : Q.t -> Q.t -> Q.t

divisible_down_to a m return the smallest multiple of m greater or equal than a

val divisible : Q.t -> Q.t -> bool

divisible a b test if a is divisible by b

val mult_cst_divisible : Q.t -> Q.t -> Q.t

mult_cst_divisible a b

val union_divisible : Q.t -> Q.t -> Q.t
val inter_divisible : Q.t -> Q.t -> Q.t