logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . UnionFind

Imperative Union-Find structure

This structure operates on arbitrary objects as long as they are hashable. It maps keys to values (values belong to a monoid, if they are not needed, unit makes for a simple implementation) and each equivalence class' representative maps to the monoid merge of all the class' elements values. One also can iterate on the representative elements.

module type PAIR = sig ... end

We need to be able to hash and compare keys, and values need to form a monoid

module Make (P : PAIR) : sig ... end

Build a union-find module from a key/value specification