package alt-ergo-lib

  1. Overview
  2. Docs
On This Page
  1. Integer heaps
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. O
    OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.3.tar.gz
sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388
md5=3b060044767d16d1de3416944abd2dd5

doc/alt-ergo-lib/AltErgoLib/Iheap/index.html

Module AltErgoLib.IheapSource

Integer heaps

This modules define priority heaps over integers.

Integer heaps

Sourcetype t

The type of heaps.

Sourceval init : int -> t

Create a heap with the given initial size.

Sourceval in_heap : t -> int -> bool

Heap membership function.

Sourceval decrease : (int -> int -> bool) -> t -> int -> unit

Decrease activity of the given integer. TODO: document the comparison function !

Sourceval increase : (int -> int -> bool) -> t -> int -> unit

Increase activity of the given integer. TODO: document the comparison function !

Sourceval size : t -> int

Returns the current size of the heap.

Sourceval is_empty : t -> bool

Is the heap empty ?

Sourceval insert : (int -> int -> bool) -> t -> int -> unit

Inset a new element in the heap. TODO: document comparison function.

Sourceval grow_to_by_double : t -> int -> unit

Grow the size of the heap by multiplying it by 2 until it is at least the size specified.

Sourceval remove_min : (int -> int -> bool) -> t -> int

Remove the minimum element from the heap and return it.

Sourceval filter : t -> (int -> bool) -> (int -> int -> bool) -> unit

Filter elements in the heap. TODO: document comparison function !