Module type ClauseQueue.S

module type S = ClauseQueue_intf.S

module C: Clause_intf.S 
module WeightFun: sig .. end
Weight functions
type t 
A priority queue.
val add : t -> C.t -> unit
Add a clause to the Queue
val add_seq : t -> C.t Sequence.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.
ratio : pick-given ratio. One in ratio calls to ClauseQueue_intf.S.take_first, the returned clause comes from a FIFO; the other times it comes from a priority queue that uses weight to sort clauses
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 pp : t CCFormat.printer
val to_string : t -> string