package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

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)

val all : unit -> string list

available names for selection functions

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct