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 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 Blog 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