		Search-engine friendly clone of the ACL2 documentation.

Aig-other

Aig-random-sim

Functions for randomly vector simulations of Hons aigs.

Simulating AIGs on random vectors is useful in algorithms such as fraiging, to look for nodes that are probably equivalent and might be merged.

Our hons-based aig representation is not especially efficient or well-suited for carrying out random simulations, and nowadays aignet is a much faster alternative. Nevertheless, we have developed various routines for vector-simulations of Hons AIGs.

Note that some of these routines make use of 60-bit natural numbers, which are fixnums on 64-bit CCL and SBCL. They may perform quite badly on other Lisps with smaller fixnum ranges.

Subtopics

Aig-vecsim60: Do a 60-bit wide evaluation of an AIG.
60-bit-fix: Coerce an object to a 60-bit natural.
Logbitp-env60: Given an ALST binding variables to 60-bit integers as in aig-vecsim60, we extract an ordinary, Boolean-valued alist by using the Ith bit of each variable.
Init-random-state: Create a fast alist binding each variable to a random 60-bit natural.
N-random-60-bit-nats: Generate a list of 60-bit naturals.
*60-bit-mask*: The largest 60-bit natural, all ones.