|
|
|---|
|
|
|
|---|
Symbolic versions of the SV functions that operate on a4vecs instead of 4vecs.
These operations form the core of our support for bit-blasting SV expressions.
Our basic goal here is to provide efficient ACL2::aig-based implementations of all of the SV functions. It is generally important for these functions to produce small AIGs so that we will produce simpler, smaller problems for back-end tools like SAT solvers and BDD packages to process.
These are many functions to implement, but most of this is straightforward and we can substantially reuse our functions for aig-symbolic-arithmetic, extending them as appropriate to deal with our four-valued logic.
A few functions with fancier implementations include a4vec-concat, which is reused in a4vec-zero-ext and a4vec-sign-ext, and also the shifting operations a4vec-rsh and a4vec-lsh. Each of these take some special measures to try to avoid creating catastrophically large vectors.