package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.EligibleSource

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

Eligibility criterion for a literal

Sourceval res : clause -> t

Only literals that are eligible for resolution

Sourceval param : clause -> t

Only literals that are eligible for paramodulation

Sourceval eq : t

Equations

Sourceval arith : t
Sourceval filter : (Logtk.Literal.t -> bool) -> t
Sourceval max : clause -> t

Maximal literals of the clause

Sourceval pos : t

Only positive literals

Sourceval pos_eq : t

Only positive equational literals

Sourceval neg : t

Only negative literals

Sourceval always : t

All literals

Sourceval combine : t list -> t

Logical "and" of the given eligibility criteria. A literal is eligible only if all elements of the list say so.

Sourceval (**) : t -> t -> t

Logical "and"

Sourceval (++) : t -> t -> t

Logical "or"

Sourceval (~~) : t -> t

Logical "not"