sig
type bundle
val dump : Format.formatter -> Conditions.bundle -> unit
type 'a attributed =
?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
val empty : Conditions.bundle
val occurs : Lang.F.var -> Conditions.bundle -> bool
val intersect : Lang.F.pred -> Conditions.bundle -> bool
val merge : Conditions.bundle list -> Conditions.bundle
val domain : Lang.F.pred list -> Conditions.bundle -> Conditions.bundle
val intros : Lang.F.pred list -> Conditions.bundle -> Conditions.bundle
val assume :
(?init:bool -> Lang.F.pred -> Conditions.bundle -> Conditions.bundle)
Conditions.attributed
val branch :
(Lang.F.pred ->
Conditions.bundle -> Conditions.bundle -> Conditions.bundle)
Conditions.attributed
val either :
(Conditions.bundle list -> Conditions.bundle) Conditions.attributed
val extract : Conditions.bundle -> Lang.F.pred list
type hypotheses
val hypotheses : Conditions.bundle -> Conditions.hypotheses
type sequent = Conditions.hypotheses * Lang.F.pred
exception Contradiction
class type simplifier =
object
method assume : Lang.F.pred -> unit
method copy : Conditions.simplifier
method fixpoint : unit
method infer : Lang.F.pred list
method name : string
method simplify_branch : Lang.F.pred -> Lang.F.pred
method simplify_goal : Lang.F.pred -> Lang.F.pred
method simplify_hyp : Lang.F.pred -> Lang.F.pred
method target : Lang.F.pred -> unit
end
val clean : Conditions.sequent -> Conditions.sequent
val filter : Conditions.sequent -> Conditions.sequent
val letify :
?solvers:Conditions.simplifier list ->
Conditions.sequent -> Conditions.sequent
val pruning :
?solvers:Conditions.simplifier list ->
Conditions.sequent -> Conditions.sequent
val close : Conditions.sequent -> Lang.F.pred
type linker
type link = Lstmt of Cil_types.stmt | Lprop of Property.t
val linker : unit -> Conditions.linker
val get_link : Conditions.linker -> string -> Conditions.link
val pretty :
?linker:Conditions.linker ->
Format.formatter -> Conditions.sequent -> unit
end