Module Selection

module Selection: sig .. end

Selection functions

See "E: a brainiac theorem prover". A selection function returns a bitvector of selected literals.

The strict parameter, if true, means only one negative literal is selected (at most); if strict=false then all positive literals are also selected.

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