package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
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.ttype parametrized = strict:bool -> ord:Logtk.Ordering.t -> tval no_select : tNever select literals.
val max_goal : parametrizedSelect a maximal negative literal, if any, or nothing
val except_RR_horn : parametrized -> parametrizedexcept_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 -> tDefault selection function
val e_sel :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectMaxLComplexAvoidPosPred
val e_sel2 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectCQIPrecWNTNp
val e_sel3 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectComplexG
val e_sel5 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectNDepth2OptimalLiteral
val e_sel6 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectLargestOrientable
val e_sel7 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectComplexExceptRRHorn
val e_sel8 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectCQArNTNpEqFirst
val e_sel9 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectCQArEqLast
val e_sel10 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectNegativeLits
val e_sel11 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's PSelectNewComplexAHP
val e_sel12 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectComplexExceptUniqMaxHorn
val e_sel13 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectGroundNegativeLiteral
val e_sel14 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectNewComplexAHPNS
val e_sel15 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectVGNonCR
val e_sel16 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectCQArNT
val e_sel17 :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection function identical to E's SelectUnlessUniqMaxOptimalLiteral
val ho_sel :
blocker:(int -> Logtk.Literal.t -> bool) ->
ord:Logtk.Ordering.t ->
tSelection 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 * boolselection function from string (may fail) -- returns functiona and a boolean saying whether function retains completeness