Module Selection

module Selection: sig .. end

Selection functions




See "E: a brainiac theorem prover". A selection function returns a bitvector of selected literals.
type t = Literal.t array -> CCBV.t 
val no_select : t
val select_max_goal : strict:bool -> ord:Libzipperposition.Ordering.t -> t
Select a maximal negative literal, if any, or nothing
val select_diff_neg_lit : strict:bool -> ord:Libzipperposition.Ordering.t -> t
arbitrary negative literal with maximal weight difference between sides
val select_complex : strict:bool -> ord:Libzipperposition.Ordering.t -> t
x!=y, or ground negative lit, or like select_diff_neg_lit
val select_complex_except_RR_horn : strict:bool -> ord:Libzipperposition.Ordering.t -> t
if clause is a restricted range horn clause, then select nothing; otherwise, like select_complex

Global selection Functions


val default_selection : ord:Libzipperposition.Ordering.t -> t
Default selection function
val selection_from_string : ord:Libzipperposition.Ordering.t -> string -> t
selection function from string (may fail)
val available_selections : unit -> string list
available names for selection functions
val register : string -> (ord:Libzipperposition.Ordering.t -> t) -> unit
Register new selection function
Raises Failure if the name is already used