package libzipperposition

  1. Overview
  2. Docs
Library for Zipperposition

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

doc/libzipperposition.avatar/Libzipperposition_avatar/Make/argument-1-E/StmQ/index.html

Module E.StmQ

module Stm = Stm
module WeightFun : sig ... end
type t

A priority queue.

val add : t -> Stm.t -> unit

Add a stream to the Queue

val add_lst : t -> Stm.t list -> unit

Add a list of streams 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 -> Stm.C.t option

Attempts to take a clause out of the queue. Guarded recursion: can't loop forever

val take_fair_anyway : t -> Stm.C.t option list

Takes clauses from the queue in a fair manner. Unguarded recursion, may loop forever

val take_stm_nb : t -> Stm.C.t option list

Attempts to take as many clauses from the queue as there are streams in the queue. Calls take_first to do so and stops if its guard is reached

val take_stm_nb_fix_stm : t -> Stm.C.t option list

Attempts to take as many clauses from the queue as there are streams in the queue. Extract as many clauses as possible from first stream before moving to a new stream to find more clauses if necessary

val name : t -> string

Name of the implementation/role of the queue

Available Queues
val make : guard:int -> ratio:int -> weight:(Stm.t -> int) -> string -> t

Creates a priority queue that uses weight to sort streams.

  • parameter ratio

    pick-given ratio. Only one in ratio truly returns a clause if there is one available in calls to take_first_when_available and take_fair_anyway.

  • parameter name

    the name of this stream queue

val default : unit -> t

Obtain the default queue

IO
val to_string : t -> string