module Logic_simplification:sig
..end
Promelaast.typed_condition
Given a list of terms (representing a conjunction),
if a positive call or return is present,
then all negative ones are obvious and removed
val tand : Promelaast.typed_condition ->
Promelaast.typed_condition -> Promelaast.typed_condition
val tor : Promelaast.typed_condition ->
Promelaast.typed_condition -> Promelaast.typed_condition
val tnot : Promelaast.typed_condition -> Promelaast.typed_condition
val simplifyCond : Promelaast.typed_condition ->
Promelaast.typed_condition * Promelaast.typed_condition list list
Given a condition, this function does some logical simplifications.
It returns both the simplified condition and a disjunction of
conjunctions of parametrized call or return.
val simplifyTrans : Promelaast.typed_condition Promelaast.trans list ->
Promelaast.typed_condition Promelaast.trans list *
Promelaast.typed_condition list list list
Given a list of transitions, this function returns the same list of
transition with simplifyCond done on its cross condition
val dnfToCond : Promelaast.typed_condition list list -> Promelaast.typed_condition
val simplifyDNFwrtCtx : Promelaast.typed_condition list list ->
Cil_types.kernel_function ->
Promelaast.funcStatus -> Promelaast.typed_condition