		Search-engine friendly clone of the ACL2 documentation.

Aignet-construction

Aignet-build

Macro that constructs a nested logical expression in an aignet

Usage:

 (aignet-build (and (not (:= foo (xor bar baz))) (or foo bar) baz) gatesimp strash aignet)
-->
 (mv result-literal strash aignet)

The above invocation translates to something like:

(b* (((mv foo strash aignet)
      (aignet-hash-xor bar baz gatesimp strash aignet))
     ((mv tmp0 strash aignet)
      (aignet-hash-or foo bar gatesimp strash aignet))
     ((mv tmp1 strash aignet)
      (aignet-hash-and tmp0 baz gatesimp strash aignet))
     ((mv tmp2 strash aignet)
      (aignet-hash-and (lit-negate foo) tmp1 gatesimp strash aignet)))
  (mv tmp2 strash aignet))

There is a b* binder of the same name that creates the above bindings within an existing b* form; e.g.:

(b* (((aignet-build
       (:= ans (and (not (:= foo (xor bar baz))) (or foo bar) baz))
       gatesimp strash aignet)))
   (result-form))

expands to something like:

(b* (((mv foo strash aignet)
      (aignet-hash-xor bar baz gatesimp strash aignet))
     ((mv tmp0 strash aignet)
      (aignet-hash-or foo bar gatesimp strash aignet))
     ((mv tmp1 strash aignet)
      (aignet-hash-and tmp0 baz gatesimp strash aignet))
     ((mv ans strash aignet)
      (aignet-hash-and (lit-negate foo) tmp1 gatesimp strash aignet)))
  (result-form))

Supported Operators

The operators and, or, xor, and iff produce calls of aignet-hash-and, aignet-hash-or, aignet-hash-xor, and aignet-hash-iff, respectively. Since these are all associative/commutative functions, they support variably many arguments (treated as right-associated).
The operators if and mux are synonymous and both produce a call of aignet-hash-mux.
The operator not simply uses lit-negate on the literal resulting from its argument.
The operator := must have a variable as its first argument and an expression as its second, and binds the variable to the literal resulting from the expression. That variable may be used subsequently within the operator expression, and when using the b* binder form, remains bound in the rest of the b*.