The bit-width transformation of bit vectors

[陳宏毅]

Hello Everyone!

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

[Andrea Micheli]

Hi!

in SMT the width of each BV variable must be fixed, there is no way to dynamically extend it to avoid overflows. Moreover the arithmetic operations (such as BVAdd) take in input two bit-vectors of size w and return a bit vector of size w. Of course, there is the possibility of overflow or underflow in the operations, but those are well-defined in the logic and expected. You can think of BV as a logic that allows to express formulae over the computation of microprocessors or hardware in general.

If you want to represent numeric operations without overflows or underflows and you can limit your encoding to a linear formula, you should try to use the Linear Integer Arithmetic (LIA) logic instead of BV.

Otherwise you need to over-approximate the bit-width necessary for your problem and the use this bit width for all your variables.

HTH

Andrea

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/2c0b3ca8-18b5-4eaf-80de-56a407451d8b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.