package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63
doc/libzipperposition/Libzipperposition/Selection/index.html
Module Libzipperposition.Selection
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 e_sel :
?blocker:(int -> Logtk.Literal.t -> bool) ->
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 :
?blocker:(int -> Logtk.Literal.t -> bool) ->
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 e_sel9 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectCQArEqLast
val e_sel10 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectNegativeLits
val e_sel11 : ord:Logtk.Ordering.t -> t
Selection function identical to E's PSelectNewComplexAHP
val e_sel12 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectComplexExceptUniqMaxHorn
val e_sel13 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectGroundNegativeLiteral
val e_sel14 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectNewComplexAHPNS
val e_sel15 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectVGNonCR
val e_sel16 : ord:Logtk.Ordering.t -> t
Selection function identical to E's SelectCQArNT
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)