Pure_literal_elim (p.libzipperposition.2.0.doc.libzipperposition.calculi.Libzipperposition_calculi.Pure_literal

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 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