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 likep
, 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 e_sel : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectMaxLComplexAvoidPosPred
val e_sel2 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectCQIPrecWNTNp
val e_sel3 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectComplexG
val e_sel5 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectNDepth2OptimalLiteral
val e_sel6 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectLargestOrientable
val e_sel7 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectComplexExceptRRHorn
val e_sel8 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectCQArNTNpEqFirst
val ho_sel : ord:Logtk.Ordering.t -> t
Selection function that tries to take into account the number of nested applied variables.
The assumption is that they are hard for unification.
val from_string : ord:Logtk.Ordering.t -> string -> t
selection function from string (may fail)