Module Conditions

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
val extract : 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 = 
| Lstmt of Cil_types.stmt
| Lprop of Property.t
val linker : unit -> linker
val get_link : linker -> string -> link
val pretty : ?linker:linker -> Format.formatter -> sequent -> unit