package libzipperposition

  1. Overview
  2. Docs

Module Libzipperposition.ClauseQueue

Priority Queue of clauses

Heuristic selection of clauses, using a priority queue. Only one queue is used, but the priority of a clause is determined by a combination of criteria that should include at least one fair criterion (e.g. the age of the clause, so that older clauses are more likely to be chosen).

val profile_of_string : string -> profile
val get_profile : unit -> profile
val set_profile : profile -> unit
val ignoring_orphans : unit -> bool
val disable_ignoring_orphans : unit -> unit
module type S = ClauseQueue_intf.S
module Make (C : Clause.S) : S with module C = C