• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Axe
      • R1cs-verification-with-axe
      • Prove-equal-with-axe
      • Dags
      • Stp
      • Lifters
      • Read-jar
      • Read-class
    • Execloader
  • Math
  • Testing-utilities

• Axe

Dags

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 variable (a symbol), or
• A quoted constant, or
• The application of a function symbol (almost always a defined ACL2 function) to a list of arguments. Each argument (or "darg" = "DAG argument") should be either a quoted constant or the number of a DAG node, which must be smaller than the number of the node that contains this expression. Since the expression for a given node can only refer to nodes with smaller numbers, the DAG is acyclic.

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 x and y, and the functions it calls are foo, bar, and binary-+. Node 4 represents a call of the function foo whose two arguments are nodes 1 and 3. Node 3 represents a call of the function bar whose two arguments are the constant 2 and node 2. The term represented by this DAG is:

(foo (binary-* '2 x) (bar '2 y))

.

This can be seen by calling the function dag-to-term on the DAG, like this:

(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!

The function dag-info can be used to print information about a DAG. For example,

(dag-info '((4 foo 1 3) (3 bar '2 2) (2 . y) (1 binary-* '2 0) (0 . x)))

prints:

(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 *my-dag*, then one could do:

(dag-to-term *my-dag*)

and

(dag-info *my-dag*)

.