The graph structure, used to keep global information about elements and implement interpretation. Only elements from the graph can be related.

Handle to an equivalence class

Create a new graph.

fresh gr x creates a new equivalence class in graph gr with associated value x

assume_equal x y adds the equation x = y

assume_application f x ~equal:y adds the equation y = f x

propagate graph updates the congruence closure to account for all added equations.

same x y returns true iff x and y are in the same congruence. New equations are propagated if necessary.

find_app f x returns Some z if any node is already equal to f x (added via assume_application), or None otherwise.

get_tag n returns the tag associated with the class of n (not the node).

Warning: this function doesn't propagate equation. Call propagate before if necessary.

set_tag n x changes the tag associated with the class of n (not the node).

Warning: this function doesn't propagate equation. Call propagate before if necessary.

set_root_tag n x changes the tag associated with the node n. This function should be called before any equation is added about n. The root tag is not backed up (it won't be restored by restore).

The purpose of this function is to change the tag of a fresh node, immediately after its creation. This is useful if the tag needs to reference the node (to create a recursion between a node and its tag).

get_id node returns an integer identifying node (unique for the graph). This function is constant: the integer identify the node and not the equivalence class.

compare a b compares two nodes by their id.

get_repr node returns the node that is the representative of the equivalence class of node in the current state. The representative can change when new equations are propagated.

Warning: this function doesn't propagate equations. Call propagate before if necessary.

An 'a var is like a 'a ref, but its contents is backed up and restored when using snapshot and restore.

var graph x creates a new variable with initial value x, which contents is backed up and restored when snapshotting and restoring graph.

get_var v retrieves the current value of the variable, like !

set_var v x changes the current value of the variable, like :=

A snapshot (efficiently) stores the state of the congruence closure (and its associated variables) at a specific point in time.

snapshot graph takes a snapshot of the current state.

restore sn restores the congruence closure to the exact same state it had when sn = snapshot graph was called.

Precondition: snapshot must be valid, see is_valid.

A snapshot becomes invalid when an earlier snapshot is restored. This only applies to the descendants: a snapshot that is restored remains valid, and can be restored multiple times. For instance, the following holds: let s1 = snapshot graph in let s2 = snapshot graph in restore s1; assert (is_valid s1); assert (not (is_valid s2))

invalid_snapshot for which is_valid is always false. It cannot be restored. Its purpose is to be used as a placeholder in places where a snapshot is expected but doesn't have to be valid.