colibrics

A CP solver proved in Why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library colibrics
val is_cst_reif : Context.t -> Var.I.t -> Z.t -> Var.B.t -> unit
val is_cst : Context.t -> Var.I.t -> Z.t -> unit
val add_reif : Context.t -> Var.I.t -> Var.I.t -> Var.I.t -> Var.B.t -> unit
val add : Context.t -> Var.I.t -> Var.I.t -> Var.I.t -> unit
val le_reif : Context.t -> Var.I.t -> Var.I.t -> Z.t -> Var.B.t -> unit
val le : Context.t -> Var.I.t -> Var.I.t -> Z.t -> unit
val or_ : Context.t -> Var.B.t -> Var.B.t -> Var.B.t -> unit
val not_ : Context.t -> Var.B.t -> Var.B.t -> unit
val is_true : Context.t -> Var.B.t -> unit
val equiv : Context.t -> Var.B.t -> Var.B.t -> Var.B.t -> unit