sig
val forall_intro : Lang.F.pred -> Lang.F.pred list * Lang.F.pred
val exist_intro : Lang.F.pred -> Lang.F.pred
type step = private {
mutable id : int;
size : int;
vars : Lang.F.Vars.t;
stmt : Cil_types.stmt option;
descr : string option;
deps : Property.t list;
warn : Warning.Set.t;
condition : Conditions.condition;
}
and 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 * Conditions.sequence * Conditions.sequence
| Either of Conditions.sequence list
| State of Mstate.state
and sequence
type sequent = Conditions.sequence * Lang.F.pred
val pretty :
(Format.formatter -> Conditions.sequent -> unit) Pervasives.ref
val step :
?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Warning.Set.t -> Conditions.condition -> Conditions.step
val update_cond :
?descr:string ->
?deps:Property.t list ->
?warn:Warning.Set.t ->
Conditions.step -> Conditions.condition -> Conditions.step
val is_true : Conditions.sequence -> bool
val is_empty : Conditions.sequence -> bool
val vars_hyp : Conditions.sequence -> Lang.F.Vars.t
val vars_seq : Conditions.sequent -> Lang.F.Vars.t
val empty : Conditions.sequence
val trivial : Conditions.sequent
val sequence : Conditions.step list -> Conditions.sequence
val seq_branch :
?stmt:Cil_types.stmt ->
Lang.F.pred ->
Conditions.sequence -> Conditions.sequence -> Conditions.sequence
val append :
Conditions.sequence -> Conditions.sequence -> Conditions.sequence
val concat : Conditions.sequence list -> Conditions.sequence
val iter : (Conditions.step -> unit) -> Conditions.sequence -> unit
val list : Conditions.sequence -> Conditions.step list
val size : Conditions.sequence -> int
val steps : Conditions.sequence -> int
val index : Conditions.sequent -> unit
val step_at : Conditions.sequence -> int -> Conditions.step
val is_trivial : Conditions.sequent -> bool
val map_condition :
(Lang.F.pred -> Lang.F.pred) ->
Conditions.condition -> Conditions.condition
val map_step :
(Lang.F.pred -> Lang.F.pred) -> Conditions.step -> Conditions.step
val map_sequence :
(Lang.F.pred -> Lang.F.pred) ->
Conditions.sequence -> Conditions.sequence
val map_sequent :
(Lang.F.pred -> Lang.F.pred) -> Conditions.sequent -> Conditions.sequent
val insert :
?at:int -> Conditions.step -> Conditions.sequent -> Conditions.sequent
val replace :
at:int -> Conditions.step -> Conditions.sequent -> Conditions.sequent
val subst :
(Lang.F.term -> Lang.F.term) -> Conditions.sequent -> Conditions.sequent
val introduction : Conditions.sequent -> Conditions.sequent option
val introduction_eq : Conditions.sequent -> Conditions.sequent
val lemma : Lang.F.pred -> Conditions.sequent
val head : Conditions.step -> Lang.F.pred
val have : Conditions.step -> Lang.F.pred
val condition : Conditions.sequence -> Lang.F.pred
val close : Conditions.sequent -> Lang.F.pred
val at_closure : (Conditions.sequent -> Conditions.sequent) -> unit
type bundle
type 'a attributed =
?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
val nil : 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 state :
?descr:string ->
?stmt:Cil_types.stmt ->
Mstate.state -> 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
val bundle : Conditions.bundle -> Conditions.sequence
val clean : Conditions.sequent -> Conditions.sequent
val filter : Conditions.sequent -> Conditions.sequent
val parasite : Conditions.sequent -> Conditions.sequent
val simplify :
?solvers:Lang.simplifier list ->
?intros:int -> Conditions.sequent -> Conditions.sequent
val pruning :
?solvers:Lang.simplifier list -> Conditions.sequent -> Conditions.sequent
end