grenier 0.15 (latest) · OCaml Package

Creations of equality graph

type 'a graph

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

type 'a node

Handle to an equivalence class

type 'a merger = repr:'a node -> 'a node -> unit

Create a new graph.

val make : ?on_merge:'a merger -> unit -> 'a graph

val set_on_merge : 'a graph -> 'a merger -> unit

val fresh : 'a graph -> 'a -> 'a node

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

Assume properties on classes

val assume_equal : 'a node -> 'a node -> unit

assume_equal x y adds the equation x = y

val assume_application : 'a node -> 'a node -> equal:'a node -> unit

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

Observe equivalence structure

val propagate : 'a graph -> unit

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

val same : 'a node -> 'a node -> bool

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

val find_app : 'a node -> 'a node -> 'a node option

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

Associating values with classes

val get_tag : 'a node -> 'a

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.

val set_tag : 'a node -> 'a -> unit

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.

val set_root_tag : 'a node -> 'a -> unit

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).

val get_id : 'a node -> int

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.

val compare : 'a node -> 'a node -> int

compare a b compares two nodes by their id.

val get_repr : 'a node -> 'a node

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.

Variables

type 'a var

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

val var : _ graph -> 'a -> 'a var

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

val get_var : 'a var -> 'a

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

val set_var : 'a var -> 'a -> unit

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

Snapshots

type snapshot

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

val snapshot : 'a graph -> snapshot

snapshot graph takes a snapshot of the current state.

val restore : snapshot -> unit

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.

val is_valid : snapshot -> bool

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))

val invalid_snapshot : snapshot

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.

package grenier

Assume properties on classes

Observe equivalence structure

Associating values with classes

Variables

Snapshots