I am currently developing an concolic (like PEX) test data input generator for Java as part of my Master's project.
Bitvectors belong to a different theory than reals. Hence, it is impossible to compare bitvector types and real types directly. In programming languages it is possible to cast integer variables to float variables. What would be the best strategy to convert these types in the constraint solver?
Option 1:
I could use the concrete value that is collected while running the program with concrete input. For example, if an float is casted to a integer, then we would use the result of this conversion to initialize the variable in the constraint solver. However, this approach loses the `link' between the integer constraints and real constraints.
Option 2:
Alternatively, I could use a set of constraints to convert between bitvectors and reals. The following pseudo C code fragments convert between bitvectors and reals. Note that this is very similar to how integers and floats are converted.
Conversion from bitvector b to real r:
int b;real r;//this loop is unrolled:for (int i = 0; i < bvsize(b); i++) { int x_int = 1 << i; //precomputed real x_real = 1 << i; //precomputed if (b & x_int) { r += x_real; }}
Conversion from positive real r to bitvector b:
real r;int b;if (MAXVALUE(b) <= r) { r = MAXVALUE(b);}if (r <= MINVALUE(b)) { r = MINVALUE(b);}if (MINVALUE(b) < r < MAXVALUE(b)) { //this loop is unrolled: for (int i = 0; i < bvsize(b); i++) { int x_int = 1 << bvsize(b) - i; //precomputed real x_real = 1 << bvsize(b) - i; //precomputed if (r > x_real) { b = b & x_int; r = r - x_real; }
}}
- Would performance suffer considerably if I use this second approach? And are there perhaps better approaches?
I almost forgot my remarks about the C API.
First off all I would like to complement you on the quality of the documentation.
Why is it only possibe to create a real numeral from a string? Would it not be more appropiate to create a real numeral using two integers?
We expose the string-based method because it also covers the case where you pass in numbers that don't fit in 32-bit registers.Exposing a method to directly build fractions from two integers sounds like a good idea for making it easier for users who start out with fractions. I will add this to our next version.
Thanks
We don't expose convenient ways for converting between bit-vectors and integers, or bit-vector floats and reals.One reason is that there would be very limited support for this, and encodings tend to be inefficient (the ones you propose are not likely to scale).. One approach I have seen is to just encode floats directly as Reals, but don't pretend that the encoding captures the accurate semantics. We will have a built-in support for conversion from integers to reals, in case this helps. It should be available by end of June as far as our schedule seem to be progressing.
I understand that scalability is a big issue, in fact, it is probably the biggest problem in test data input generation and model checking. Nonetheless, it would be nice to have a tool that incorporates a decision procedure for floating point arithmetic to allow for exact reasoning about software programs. I also think that scalability is less of an issue in this case, because often floating point arithmetic is used only in small fractions of software.
I saw that you wrote about bit-vector floats: Are you going to support bit-vector floats in the next release? Otherwise I am considering layering my own (unoptimized) bit-vector float decision procedure on top of the z3 bit vector decision procedure.
As for the C api, I currently have written a function that converts a float or double in a fraction. However the resulting string can be very big. Perhaps it is better to add a api function that transforms a float / double in a fraction?
The next release will not have specific floating point support. It will contain some additional conversion functions between integers and reals that can potentially be of use. The conversion of a float to a fraction can be architecture dependent and we don't plan to expose such functionality at this point.
There are interesting problems in handling floating points in the context of SMT solvers. As you notice, the scope of floating point constraints ends up being somewhat limited, however.
Thanks for helping! I am looking forward to the next release...