Module Solution

module Solution: sig  end

Solution sets.

A solution set for theory th is a set of equalities of the form x = a, where x is term variable and a is a th-pure term application. For each such equality, a justification rho of type Jst.t is maintained.

As an invariant, solution sets s are kept in

• functional form, that is, if x = a and x = b in s, then a is identical with b, and
• solution sets are injective, that is, x = a and y = a are not in a solution set for x <> y.

Author(s): Harald Ruess, N. Shankar

val pp_index : bool Pervasives.ref

module type DEP = sig  end

Iterators over dependency index.

module type SET = sig  end

Signature for equality sets.

module type EXT = sig  end

An equality theory is specified by means of its name th,, a term map f a for replacing uninterpreted positions x of a with f x and canonizing the resulting term in theory th., side effects when updating and restricting solution sets.

module Make: functor (Ext : EXT) -> sig  end

Functor for constructing an equality set for theory specification T.

module type SET0 = sig  end

Solution set without field extension.

module Set: SET0

Functor for constructing a solution set for theory specification T0.

module Proj: functor (S : SET) -> SET0

Projecting out extensions of a solution set.