Crate congruence 

An implementation of congruence closure, CongruenceClosure, which drives modifications to an arbitrary union-find ADT implementing the UnionFind trait. Based on Nieuwenhuis and Oliveras Proof-producing Congruence Closure, except without the proof production.

A minimal disjoint set forest implementation with dense usize nodes, DisjointSetForest, is also provided.

Structs

CongruenceClosure

An implementation of congruence closure, parametric over an arbitrary disjoint set forest implementation.

DisjointSetForest

A minimal disjoint set forest with dense usize nodes, implementing the UnionFind trait.

Equate

A simple equation of the form term = ix

Pending

A list of pending equalities for congruence closure

UseSet

A set of (used, user) pairs, where used is an index in a context and user is an equation hash modulo that context

Traits

ConstLanguage

An type within which, when taken as a language, all objects have constant class

EqMod

A type which can be compared to another modulo some equivalence context over a type I

Equation

An object which can be used as an equation between a term L and an index x of the form L = x

HashMod

A type which can be hashed modulo some equivalence context over a type I

Language

An object which can be used as a language for congruence closure with indices of type I given a context of type C.

UnionFind

A trait implemented by data-structures implementing the union-find ADT.