Module U

module U: sig  end

Congruence closure
Author(s): Harald Ruess, N. Shankar

module S: Solution.SET0

module Infsys: sig  end

A congruence closure state represents the conjunction of a set of equalities x = f(x1,...,xn) with x, xi term variables and f an uninterpreted function symbol.