I am using bitvector to implement efficient computing.
As we all know that adding two 8-bit numbers, we need a 9-bit width;
whereas multiplying two 8-bit numbers, we need a 16-bit width.
Is there any methods to switch the bit-width of each bitvectors?
Because I have tried:
A = BV(240,9)
B = BV(200,9)
Upper_bound = BV(255,8)
C = BVAdd(A,B)
C = BV(C,8)
C = max(C,Upper_bound) # To ensure the upper bound is 255 in 8-bit
Then it shows:
pysmt.exceptions.PysmtTypeError: Invalid type in constant. The type was:<class 'pysmt.fnode.FNode'>
which refers that C = BV(C,8) is illegal