sig
type t
val compare : Pure.t -> Pure.t -> int
val ptrue : Pure.t
val pfalse : Pure.t
val one : Exp.exp -> Pure.t
val conj_one : Exp.exp -> Pure.t -> Pure.t
val conj : Pure.t -> Pure.t -> Pure.t
val is_true : Pure.t -> bool
val is_sat : Pure.t -> bool
val is_false : Pure.t -> bool
val has_unsat_eq : Pure.t -> bool
val has_neql : Pure.t -> bool
val identical_eq : Pure.t -> Pure.t -> bool
val to_exp : Pure.t -> Exp.exp
val to_sub : Pure.t -> Exp.subst
val only_inst_eqs : Pure.t -> Pure.t
val remove_eqs : Pure.t -> Pure.t
val no_s : string -> Pure.t -> bool
val fv : Pure.t -> Exp.IdSet.t -> Exp.IdSet.t
val exfv : Pure.t -> Exp.IdSet.t -> Exp.IdSet.t
val fhd : Pure.t -> Exp.IdSet.t -> Exp.IdSet.t
val map : (Exp.exp -> Exp.exp) -> Pure.t -> Pure.t
val kill_vars : Exp.IdSet.t -> Pure.t -> Pure.t
val kill_can_return : Pure.t -> Pure.t
val normalize : Pure.t -> Pure.t list
val normalize_aggr : Pure.t -> Pure.t list
val entails_exp_aggr : Pure.t -> Exp.exp -> bool
val entails_exp : Pure.t -> Exp.exp -> bool
val simplify : Pure.t -> Pure.t -> Pure.t
val entails : Pure.t -> Pure.t -> bool
val eq_length : Pure.t -> int
val fold : (Exp.exp -> 'a -> 'a) -> Pure.t -> 'a -> 'a
val filter : (Exp.exp -> bool) -> Pure.t -> Pure.t
val has_can_return : Pure.t -> bool
val common : Pure.t -> Pure.t -> Pure.t
val common3 : Pure.t -> Pure.t -> Pure.t * Pure.t * Pure.t
val get_set_eqs : Pure.t -> (Exp.exp list * Exp.exp list) list
val get_uneql : Exp.exp -> Pure.t -> Exp.Dset.t
val pp : Format.formatter -> Pure.t -> unit
val list_conj : Pure.t list -> Pure.t list -> Pure.t list
val lifted_list_conj : Pure.t list -> (unit -> Pure.t list) -> Pure.t list
end