Module `Libzipperposition.Selection`

Selection functions

type t = Logtk.Literal.t array -> CCBV.t
type parametrized = strict:bool -> ord:Logtk.Ordering.t -> t

val no_select : t: Never select literals.

val max_goal : parametrized: Select a maximal negative literal, if any, or nothing

val except_RR_horn : parametrized -> parametrized: except_RR_horn p behaves like p, except if the clause is a range-restricted Horn clause. In that case, we assume the clause is a (conditional) rewrite rule and we don't prevent using it as an active clause.

Global selection Functions

val default : ord:Logtk.Ordering.t -> t: Default selection function

val from_string : ord:Logtk.Ordering.t -> string -> t: selection function from string (may fail)

val all : unit -> string list: available names for selection functions