package libzipperposition

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

Parameters

module C : Clause.S

Signature

module C = C
module WeightFun : sig ... end
type t

A priority queue.

val add : t -> C.t -> unit

Add a clause to the Queue

val add_seq : t -> C.t Iter.t -> unit

Add clauses to the queue

val length : t -> int

Number of elements

val is_empty : t -> bool

check whether the queue is empty

val take_first : t -> C.t

Take first element of the queue, or raise Not_found

val name : t -> string

Name of the implementation/role of the queue

Available Queues
val make : ratio:int -> weight:(C.t -> int) -> string -> t

Bring your own implementation of queue.

  • parameter ratio

    pick-given ratio. One in ratio calls to take_first, the returned clause comes from a FIFO; the other times it comes from a priority queue that uses weight to sort clauses

  • parameter name

    the name of this clause queue

val bfs : unit -> t

FIFO

val almost_bfs : unit -> t

Half FIFO, half default

val explore : unit -> t

Use heuristics for selecting "small" clauses

val ground : unit -> t

Favor positive unit clauses and ground clauses

val goal_oriented : unit -> t

custom weight function that favors clauses that are "close" to initial conjectures. It is fair.

val default : unit -> t

Obtain the default queue

val of_profile : ClauseQueue_intf.profile -> t

Select the queue corresponding to the given profile

IO
val to_string : t -> string
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