package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

Dune Dependency

alt-ergo.ocamlpro.com Readme LicenseRef-OCamlPro-Non-Commercial-Purpose-License-Version-1 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

O

OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.0.tar.gz

sha256=7f1906900272125315833b9f0a6abc3c5af7b836d604fdb10a98a9079c1b99f9

md5=d99bfaf748f7c640222e59677e6afd7c

doc/alt-ergo-lib/AltErgoLib/Hconsing/Make/argument-1-H/index.html

Parameter `Make.H`

Hashed values.

This signature defines the interface required for values to be hashconsed.

type elt

The type of hashed elements

val eq : elt -> elt -> bool

Equality predicate on values.

val hash : elt -> int

Hash function on values. Must be compatible with the equality function, i.e: equality of values imply that hashes are equal.

val set_id : int -> elt -> elt

Set an id to the given value. This id should not be considered by the equality function when comparing values. Should not mutate the given value for the hashconsing to be correct.

val initial_size : int

Initial size for the hashconsing table.

val disable_weaks : unit -> bool

Values hashconsed when this returns true are treated as always reachable by the gc and thus will not be collected.