Axe's DAG data structure
Axe can represent an ACL2 term in a compact form called a "DAG" (directed acyclic graph). In a DAG, each distinct subterm is represented only once, so DAGs can be much smaller than their corresponding terms. Certain classes of terms with extensive sharing of subterms can be exponentially larger than their DAG representations. Most of Axe's algorithms operate directly on DAGs (perhaps stored in internal form in arrays).
A DAG contains a set of nodes, each of which has a node number (a natural number) and a "dag-expr" (DAG expression). A dag-expr is either:
The nodes in a DAG are listed in decreasing order, with each node number consed onto its expression. Here is an example DAG containing 5 nodes:
((4 foo 1 3) (3 bar '2 2) (2 . y) (1 binary-* '2 0) (0 . x)).
The variables in this DAG are
(foo (binary-* '2 x) (bar '2 y)).