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 (often stored internally as 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:
A DAG is usually represented as an alist from node numbers to their corresponding expresspions. Nodes 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)).
This can be seen by calling the function
(dag-to-term '((4 foo 1 3) (3 bar '2 2) (2 . y) (1 binary-* '2 0) (0 . x)))
but note that the term representation can blow up for DAGs with extensive sharing!
(dag-info '((4 foo 1 3) (3 bar '2 2) (2 . y) (1 binary-* '2 0) (0 . x)))
(DAG info: Unique nodes: 5 2 Variables: x y Functions and counts: binary-*: 1 bar: 1 foo: 1)
Often Axe stores DAGs in named constants, since the DAGs themselves may be large. For example, if the DAG above were stored in the constant