A more or less complete set of functions for doing arithmetic on a symbolic bitvector representation consisting of lists of AIGs.
See gl::symbolic-arithmetic. This is almost the same, but for AIGs instead of for gl::bfrs.