sig
val enabled : unit -> bool
val args : (Arg.key * Arg.spec * Arg.doc) list
type ga_node
val new_node : Assertions.cform -> Genarith.ga_node
val put_edge_skip : Genarith.ga_node -> Genarith.ga_node -> unit
val put_edge_implication :
Genarith.ga_node -> Exp.subst -> Pure.t -> Genarith.ga_node -> unit
val pp_function : Format.formatter -> string * Genarith.ga_node -> unit
type eform = Genarith.ga_node
type eprop = Genarith.eform list
val cform_of_eform : Genarith.eform -> Assertions.cform
val eprop_of_cprop : Assertions.cprop -> Genarith.eprop
val eprop_of_cprop_at_start_node :
Assertions.cprop -> Genarith.ga_node * Genarith.eprop
val eprop_false : Genarith.eprop
val eprop_star : Assertions.cprop -> Genarith.eprop -> Genarith.eprop
val eprop_star_assume :
Assertions.cprop -> Genarith.eprop -> Genarith.eprop
val eprop_or : Genarith.eprop -> Genarith.eprop -> Genarith.eprop
val ext_append_return : Genarith.eprop -> unit
val ext_append_comment :
(unit -> string) -> Genarith.eprop -> Genarith.eprop
val ext_append_assign :
(Exp.Id.t * Exp.exp option) list -> Genarith.eprop -> Genarith.eprop
val ext_append_case_split :
Genarith.eprop -> Genarith.eprop * Genarith.eprop
val ext_opt_transform1 :
(Assertions.cform -> Assertions.cform list option) ->
Genarith.eform -> Genarith.eform list option
val plain_ext_transform :
(Assertions.cform -> Assertions.cprop) ->
Genarith.eprop -> Genarith.eprop
val ext_transform :
(Assertions.cform -> Assertions.cprop) ->
Genarith.eprop -> Genarith.eprop
val remove_eform_duplicates : Genarith.eform list -> Genarith.eform list
val map_eprop : (Exp.exp -> Exp.exp) -> Genarith.eprop -> Genarith.eprop
val naive_map_eprop :
(Exp.exp -> Exp.exp) -> Genarith.eprop -> Genarith.eprop
val pp_eprop : Format.formatter -> Genarith.eprop -> unit
type udom = Assertions.uform list * Assertions.uform list
val udom_of_uform_list : Assertions.uform list -> Genarith.udom
val uform_list_of_udom : Genarith.udom -> Assertions.uform list
type abstraction = {
uform_abs : bool -> Assertions.uform list -> Assertions.uform list;
uform_join :
Genarith.udom ->
Assertions.uform list -> Genarith.udom * Assertions.uform list;
prop_abs : Genarith.eprop -> Genarith.eprop;
prop_join :
Genarith.eprop ->
Genarith.eprop ->
Genarith.eprop -> Genarith.eprop * Genarith.eprop * Genarith.eprop;
set_abs : Exp.IdSet.t -> Exp.exp list list -> Exp.subst;
list_abs : Exp.exp list list -> Exp.subst;
}
end