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 <[email protected]> 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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
