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

• 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 (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:

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

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

.