module Conditions: sig
.. end
Bundles
Bundles
type
bundle
val dump : Format.formatter -> bundle -> unit
type 'a
attributed = ?descr:string ->
?stmt:Cil_types.stmt -> ?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
val empty : bundle
val occurs : Lang.F.var -> bundle -> bool
val intersect : Lang.F.pred -> bundle -> bool
val merge : bundle list -> bundle
val domain : Lang.F.pred list -> bundle -> bundle
val intros : Lang.F.pred list -> bundle -> bundle
val assume : (?init:bool -> Lang.F.pred -> bundle -> bundle)
attributed
val branch : (Lang.F.pred -> bundle -> bundle -> bundle)
attributed
val either : (bundle list -> bundle) attributed
: bundle -> Lang.F.pred list
Hypotheses
type
hypotheses
val hypotheses : bundle -> hypotheses
type
sequent = hypotheses * Lang.F.pred
Simplifier
exception Contradiction
class type simplifier = object
.. end
val clean : sequent -> sequent
val filter : sequent -> sequent
val letify : ?solvers:simplifier list ->
sequent -> sequent
val pruning : ?solvers:simplifier list ->
sequent -> sequent
val close : sequent -> Lang.F.pred
Pretty
type
linker
type
link =
val linker : unit -> linker
val get_link : linker -> string -> link
val pretty : ?linker:linker -> Format.formatter -> sequent -> unit