setr

Abstract domain library for sets
IN THIS PACKAGE
module DS = SETr_DS
type !'sym e =
| Empty
| Universe
| DisjUnion of 'sym e * 'sym e
| Union of 'sym e * 'sym e
| Inter of 'sym e * 'sym e
| Diff of 'sym e * 'sym e
| Comp of 'sym e
| Var of 'sym
type !'sym t =
| Eq of 'sym e * 'sym e
| SubEq of 'sym e * 'sym e
| And of 'sym t * 'sym t
| Not of 'sym t
| True
| False
type !'sym q = {
get_eqs : unit -> ('sym * 'sym) list;
get_eqs_sym : 'sym -> 'sym list;
}
val prec_e : 'a e -> int
val pp_noparen_e : ?parse:bool -> ( Format.formatter -> 'a -> unit ) -> Format.formatter -> 'a e -> unit
val pp_e : ?parse:bool -> ?prec:int -> ( Format.formatter -> 'a -> unit ) -> Format.formatter -> 'a e -> unit
val pp : ?parse:bool -> ( Format.formatter -> 'a -> unit ) -> Format.formatter -> 'a t -> unit
val to_string_e : ( Format.formatter -> 'a -> unit ) -> 'a e -> string
val to_string : ( Format.formatter -> 'a -> unit ) -> 'a t -> string
val iter_sym_e : ( 'a -> unit ) -> 'a e -> unit
val iter_sym : ( 'a -> unit ) -> 'a t -> unit
val map_sym_e : ( 'a -> 'b e ) -> 'a e -> 'b e
val map_sym : ( 'a -> 'b e ) -> 'a t -> 'b t
val map_symbol_e : ( 'a -> 'b ) -> 'a e -> 'b e
val map_symbol : ( 'a -> 'b ) -> 'a t -> 'b t
val normalize_e : 'a e -> 'a e * 'a t
val normalize : 'a t -> 'a t
val to_cnf_e : int e -> DS.CNF.LSet.elt list list * DS.CNF.LSet.elt list list
val to_cnf : int t -> DS.CNF.LSet.elt list list