module type S = sig .. end
A priority queue of clauses, purely functional
module C: Clause.S
module WeightFun: sig .. end
Weight functions
type
A priority queue.
val add : t -> C.t -> t
Add a clause to the Queue
val adds : t -> C.t Sequence.t -> t
Add clauses to the queue
val is_empty : t -> bool
check whether the queue is empty
val take_first : t -> 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 : weight:(C.t -> int) -> string -> t
Bring your own implementation of queue. The weight function
should be fair, i.e. for any clause c, the weight of c should
eventually be the smallest one in the queue (e.g., using the age
of clauses in the weight somewhere should be enough)
val bfs : t
Strong orientation toward FIFO
val explore : t
Use heuristics for selecting "small" clauses
val ground : t
Favor positive unit clauses and ground clauses
val goal_oriented : t
custom weight function that favors clauses that are "close" to
initial conjectures. It is fair.
val default : 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