Tau
-
|
This question was originally posted by LEARN TAU: |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment
-
|
We have several base Boolean algebras at hand: the sbf (simple Boolean functions) and the Tau Boolean algebra (dealing with specs over specs and sbf's). We are including the bit-vectors as a new base Boolean algebra. This new base Boolean algebra would deal with bit-vector types (each bit-vector variable would have its own fixed bit-width size). Bit-vectors are represented as Z3 bit-vectors and the formulas related to them are solved using Z3. The rest is done using current algorithms for atomless Boolean algebras. Boolean functions are another one, being tables one of its incarnations. |
Beta Was this translation helpful? Give feedback.
We have several base Boolean algebras at hand: the sbf (simple Boolean functions) and the Tau Boolean algebra (dealing with specs over specs and sbf's). We are including the bit-vectors as a new base Boolean algebra. This new base Boolean algebra would deal with bit-vector types (each bit-vector variable would have its own fixed bit-width size). Bit-vectors are represented as Z3 bit-vectors and the formulas related to them are solved using Z3. The rest is done using current algorithms for atomless Boolean algebras.
Boolean functions are another one, being tables one of its incarnations.