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
Post by Daniel LiewHi 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.
Post by Pablo González de AledoHi, 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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev