Module Libzipperposition_calculi.Hlt_elim

module T = Logtk.Term
module Ty = Logtk.Type
module Lits = Logtk.Literals
module Lit = Logtk.Literal
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_reduce_tautologies : bool Logtk.Flex_state.key
val k_delete_lits : 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
val k_heartbeat_steps : int option Logtk.Flex_state.key
val k_heartbeat_disabled_hlbe : bool Logtk.Flex_state.key
val k_max_imp_entries : int Logtk.Flex_state.key
val k_basic_rules : bool Logtk.Flex_state.key
val k_penalize_tautologies : bool Logtk.Flex_state.key
module type S = sig ... end
module Make (E : Libzipperposition.Env.S) : S with module Env = E
val max_depth_ : int ref
val enabled_ : bool ref
val simpl_new_ : bool ref
val clauses_to_track_ : [ `Active | `All | `Passive ] ref
val max_self_impls_ : int ref
val max_tracked_clauses : int ref
val propagated_hle : bool ref
val hte_ : bool ref
val hle_ : bool ref
val track_eq_ : bool ref
val insert_ordered_ : bool ref
val heartbeat_steps : int option ref
val max_imp_ : int ref
val basic_rules_ : bool ref
val penalize_tautologies_ : bool ref