Module Dpll_literal.Variable_queue

module Variable_queue: Index.PriorityQueue  with type elt = Variable.t

Priorities queues of variables.

type elt

Type of elements.

type t

Type of priority queues of elements.

val create : elt -> t

An empty queue.

val length : t -> int

length q is the number of elements in the queue.

val is_empty : t -> bool

is_empty q is true iff there are no elements enqueued in q.

val mem : t -> elt -> bool

mem q e is true iff e is enqueued in q.

val head : t -> elt

head q is the highest priority element of q.

val enqueue : t -> elt -> unit

enqueue q e enqueues the element e. The position of e in q is determined by its priority.

Note: The default priority of elements is 0.0.

val dequeue : t -> elt

dequeue q removes the highest priority element from q.
Returns The element removed.

val drop : t -> unit

drop q removes the highest priority element from q.

val priority : t -> elt -> float

The priority of an element.

Note: The default priority of elements is 0.0.

val inc_priority : t -> elt -> float -> unit

inc_priority q e x adds x to the priority of element e. If e is enqueued, it will move up the queue as necessary.

val scale : t -> float -> unit

scale q x multiplies the priority of every element by the constant factor x. The ordering of elements in the queue is unchanged.

Hosted by the

^* web site.
^*Other names and brands may be claimed as the property of others.