[klee-dev] Why restrict to bitvectors?

[Daniel Liew]

Hi Pablo,

The underlying constraint solver ONLY works in terms of bitvectors
(although other SMT solvers can use other types). KLEE spends a large
majority of its time running its constraint solver so it makes sense
to represent constraints in a format that is close to what the solver
needs.  So it would not be faster to keep the queries in a different
format.

There is a transformation into bitvectors as you suggest but there is
nothing wrong with thinking of variables as bitvectors. An "int" is a
bitvector and a "double" is a bitvector for example. Every data type
in a computer can be represented as a bitvector. You can only
precisely represent an int data type to the solver as a bitvector. An
Integer to the SMT solvers I know of are "mathematical" integers which
are very different fixed bit-width integers in a computer.

Hope that helps,

Dan.

On 11 April 2013 14:57, Pablo González de Aledo <pabloga at teisa.unican.es> wrote:
> Hi, I'm introducing myself into klee, and I'm wondering why does klee
> restrict queries and transforms all them into bitvectors?. Wouldn't it
> be faster and easier to keep integer expressions as is, and transform
> only what is necessary because of bitwise operations such as &.|,^ ...?
>
> Thanks
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev