Module Libzipperposition_calculi.Pure_literal_elim

val section : Logtk.Util.Section.t
type id_sgn = Logtk.ID.t * bool
module IDMap : sig ... end
module IntSet = Logtk.Util.Int_set
module TST = Logtk.TypedSTerm
exception AppVarFound
val _enabled : bool Stdlib.ref
val total_clauses : Logtk.Util.stat
val removed_clauses : Logtk.Util.stat
val pp_key : (Logtk.ID.t * CCBool.t) CCPair.printer
val cl_syms : Logtk__TypedSTerm.t Logtk.SLiteral.t list -> Logtk.ID.Set.t
val compute_occurence_map : (TST.t Logtk.SLiteral.t list, TST.t, TST.t) Logtk.Statement.t Iter.t -> Logtk.ID.Set.t * IntSet.t Logtk.ID.Map.t * int IDMap.t list
val get_pure_symbols : Logtk.ID.Set.t -> IntSet.t Logtk.ID.Map.t -> int IDMap.t list -> Logtk.ID.Set.t
val remove_pure_clauses : (TST.t Logtk.SLiteral.t list, TST.t, TST.t) Logtk.Statement.t Iter.t -> (TST.t Logtk.SLiteral.t CCList.t, TST.t, TST.t) Logtk.Statement.t Iter.t
val extension : Libzipperposition.Extensions.t