Module Conditions

module Conditions: sig .. end
Sequent


Sequent
type step = private {
   size : int;
   vars : Lang.F.Vars.t;
   stmt : Cil_types.stmt option;
   descr : string option;
   deps : Property.t list;
   warn : Warning.Set.t;
   condition : condition;
}
type condition = 
| Type of Lang.F.pred
| Have of Lang.F.pred
| When of Lang.F.pred
| Core of Lang.F.pred
| Init of Lang.F.pred
| Branch of Lang.F.pred * sequence * sequence
| Either of sequence list
type sequence 
List of steps
type sequent = sequence * Lang.F.pred 
val step : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Warning.Set.t -> condition -> step
val is_empty : sequence -> bool
val vars_hyp : sequence -> Lang.F.Vars.t
val vars_seq : sequent -> Lang.F.Vars.t
val empty : sequence
val seq_list : step list -> sequence
val seq_branch : ?stmt:Cil_types.stmt ->
Lang.F.pred ->
sequence -> sequence -> sequence
val append : sequence -> sequence -> sequence
val concat : sequence list -> sequence
val iter : (step -> unit) -> sequence -> unit
val iteri : ?from:int -> (int -> step -> unit) -> sequence -> unit
val condition : sequence -> Lang.F.pred
With free variables kept.
val close : sequent -> Lang.F.pred
With free variables quantified.

Bundles

Bundles are mergeable pre-sequences. This the key structure for merging hypotheses with linerar complexity during backward weakest pre-condition calculus.

type bundle 
type 'a attributed = ?descr:string ->
?stmt:Cil_types.stmt -> ?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
val nil : 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
val sequence : bundle -> sequence

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