module Eligible: sig .. end
type int -> Logtk.Literal.t -> bool
Eligibility criterion for a literal
val res : Clause_intf.S.clause -> t
Only literals that are eligible for resolution
val param : Clause_intf.S.clause -> t
Only literals that are eligible for paramodulation
val eq : t
Equations
val arith : t
val filter : (Logtk.Literal.t -> bool) -> t
val max : Clause_intf.S.clause -> t
Maximal literals of the clause
val pos : t
Only positive literals
val neg : t
Only negative literals
val always : t
All literals
val combine : t list -> t
Logical "and" of the given eligibility criteria. A literal is
eligible only if all elements of the list say so.
val ( ** ) : t ->
t -> t
Logical "and"
val (++) : t ->
t -> t
Logical "or"
val (~~) : t -> t
Logical "not"