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