Library for reasoning about and computing with integer-encoded truth tables.
A Boolean function of n variables can be represented using a
bit vector of 2^n bits. Operators such as AND/OR/XOR can then be computed
using logand, logior, and logxor, respectively. This library
provides utilities for using this encoding of Boolean functions and reasoning
about them. It is particularly useful in the aignet::rewrite AIG
transformation.
Checks whether the given truth table is the xor of variable n with something.
If so, the other input to the xor is the negative cofactor of the truth
table with n.
