module Selection:sig
..end
The strict
parameter, if true, means only one negative
literal is selected (at most);
if strict=false
then all positive literals are also selected.
typet =
Logtk.Literal.t array -> CCBV.t
typeparametrized =
strict:bool -> ord:Logtk.Ordering.t -> t
val no_select : t
val max_goal : parametrized
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.val default : ord:Logtk.Ordering.t -> t
val from_string : ord:Logtk.Ordering.t -> string -> t
val all : unit -> string list