Module `Libzipperposition_calculi.Hlt_elim`

module T = Logtk.Term

module Ty = Logtk.Type

module Lits = Logtk.Literals

module Lit = Logtk.Literal

module A = Libzipperposition_avatar

val section : Logtk.Util.Section.t
val k_enabled : bool Logtk.Flex_state.key
val k_max_depth : int Logtk.Flex_state.key
val k_simpl_new : bool Logtk.Flex_state.key
val k_clauses_to_track : [ `Active | `All | `Passive ] Logtk.Flex_state.key
val k_max_self_impls : int Logtk.Flex_state.key
val k_unit_propagated_hle : bool Logtk.Flex_state.key
val k_unit_htr : bool Logtk.Flex_state.key
val k_hte : bool Logtk.Flex_state.key
val k_hle : bool Logtk.Flex_state.key
val k_max_tracked_clauses : int Logtk.Flex_state.key
val k_track_eq : bool Logtk.Flex_state.key
val k_insert_only_ordered : bool Logtk.Flex_state.key

module type S = sig ... end

module Make : functor (E : Libzipperposition.Env.S) -> S with module Env = E

val max_depth_ : int Stdlib.ref
val enabled_ : bool Stdlib.ref
val simpl_new_ : bool Stdlib.ref
val clauses_to_track_ : [ `Active | `All | `Passive ] Stdlib.ref
val max_self_impls_ : int Stdlib.ref
val max_tracked_clauses : int Stdlib.ref
val propagated_hle : bool Stdlib.ref
val unit_htr_ : bool Stdlib.ref
val hte_ : bool Stdlib.ref
val hle_ : bool Stdlib.ref
val track_eq_ : bool Stdlib.ref
val insert_ordered_ : bool Stdlib.ref
val extension : Libzipperposition.Extensions.t