package libzipperposition

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

Module ClauseQueue.MakeSource

Parameters

module C : Clause.S

Signature

module C = C
Sourcemodule WeightFun : sig ... end
Sourcemodule PriorityFun : sig ... end
Sourcetype t

A priority queue.

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

Add a clause to the Queue

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

Add clauses to the queue

Sourceval length : t -> int

Number of elements

Sourceval is_empty : t -> bool

check whether the queue is empty

Sourceval take_first : t -> C.t

Take first element of the queue, or raise Not_found

Sourceval name : t -> string

Name of the implementation/role of the queue

Available Queues
Sourceval add_to_mixed_eval : ratio:int -> weight_fun:(C.t -> int * int) -> t
Sourceval bfs : unit -> t

FIFO

Sourceval almost_bfs : unit -> t

Half FIFO, half default

Sourceval explore : unit -> t

Use heuristics for selecting "small" clauses

Sourceval ground : unit -> t

Favor positive unit clauses and ground clauses

Sourceval goal_oriented : unit -> t

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

Sourceval default : unit -> t

Obtain the default queue

Sourceval of_profile : ClauseQueue_intf.profile -> t

Select the queue corresponding to the given profile

IO
Sourceval 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