package libzipperposition

  1. Overview
  2. Docs
Library for Zipperposition

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz
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.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 : blocker:(int -> Logtk.Literal.t -> bool) -> 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 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectNDepth2OptimalLiteral

val e_sel6 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectLargestOrientable

val e_sel7 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectComplexExceptRRHorn

val e_sel8 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectCQArNTNpEqFirst

val e_sel9 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectCQArEqLast

val e_sel10 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectNegativeLits

val e_sel11 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's PSelectNewComplexAHP

val e_sel12 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectComplexExceptUniqMaxHorn

val e_sel13 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectGroundNegativeLiteral

val e_sel14 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectNewComplexAHPNS

val e_sel15 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectVGNonCR

val e_sel16 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectCQArNT

val e_sel17 : blocker:(int -> Logtk.Literal.t -> bool) -> ord:Logtk.Ordering.t -> t

Selection function identical to E's SelectUnlessUniqMaxOptimalLiteral

val ho_sel : blocker:(int -> Logtk.Literal.t -> bool) -> 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 * bool

selection function from string (may fail) -- returns functiona and a boolean saying whether function retains completeness

val all : unit -> string list

available names for selection functions