module Logic_simplification:sig
..end
Basic simplification over Promelaast.typed_condition
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 and returns an equivalent DNF form together with the simplified version
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 transition list, this function returns the same transition list with simplifyCond done on each cross condition. Uncrossable transition are removed.
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
Given a DNF condition, it returns a condition in Promelaast.condition form. WARNING : empty lists not supported
val simplifyDNFwrtCtx : Promelaast.typed_condition list list ->
Cil_types.kernel_function ->
Promelaast.funcStatus -> Promelaast.typed_condition
Given a DNF condition, it returns the same condition simplified according to the context (function name and status). Hence, the returned condition is without any Call/Return stmts.