Module S.Eligible

type t = int -> Logtk.Literal.t -> bool

Eligibility criterion for a literal

val res : clause -> t

Only literals that are eligible for resolution

val param : 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 -> 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"