[klee-dev] Why restrict to bitvectors?

[Pablo González de Aledo]

Hi Dan. Thanks for your help and quick answer :-).

Although STP solver only works with bitvectors, I think now it exists 
more advanced solvers like z3 that support more logics. About the 
disadvantages of using bitvectors, my humble opinion is that, even if 
they have enough expressive power to represent any type on a computer, 
they represent it in the 'most general way'. Disadvantages in such 
generality might be speed ( I believe integer solvers are faster than 
bit-vector ones ), or larger queries.

I'm currently starting a PhD in verification. Do you (for all) think 
integrating an integer --or real-- solver in klee would be an 
interesting subject?.

Thanks


On 04/11/2013 02:02 PM, Daniel Liew wrote:
> 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