package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

Library for Zipperposition

Install

Dune Dependency

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

Authors

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

2.0.tar.gz

md5=7a8e57388083ed763d12d18324c8a086

sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

doc/libzipperposition.calculi/Libzipperposition_calculi/Superposition/Make/StmQ/index.html

Module `Make.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

raises Not_found
in the guard is reached

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 pp : t CCFormat.printer

val to_string : t -> string

On This Page

Available Queues
IO