In fact, looking at this code is how I recently learned that Z3 also supports an exponentiation operator (^), which can be used with types Int -> Int -> Real or Real -> Real -> Real. It has a curious definition where it considers 0^0 to be undefined but 0^n is defined to be zero when n is negative (which strikes me as a bit inconsistent).
If I recall correctly, it also has a very curious property where it considers (-3.0) ^ (-0.5) to be equal to (-1/3) ^ 0.5, which is kinda weird because in the “usual” definition of exponentiation 1) those two expressions are complex numbers, 2) those two expressions are not equal – only their real parts are equal, and 3) Z3 doesn’t even support complex numbers (or at least, not directly, although it’s possible to map them to a pair of real numbers).
I’ve never used floats in an SMT solver, much less looked at their internal representation, so I’m not sure I can answer this accurately. From a quick glance at the theory for floating points defined in the SMT-LIB standard, it seems to suggest that they are represented as bit vectors.
Just in case it isn’t clear, however, note that the floats are different from the reals that I mentioned in my comment in several ways. For one, floats have limited precision, while the reals have infinite. Floats have a +infinity and a -infinity representation, two different “zero” representations (plus and minus zero) and also have the concept of a NaN, which has multiple representations. Rounding is necessary for many operations.
The reals as defined in the SMT-LIB standard basically have none of that. It more closely corresponds to the set of real numbers used in math, but as far as irrational numbers are concerned, the SMT-LIB standard doesn’t seem to support transcendental numbers, only algebraic numbers.
That said, it appears that Z3 has some support for transcendental numbers, as evidenced by the support for the π and e constants and the trigonometric functions in the code that I referenced. I could be entirely wrong, but my understanding is that Z3 simply represents real numbers internally as AST nodes, which is something that might look like mk_sin(mk_div(pi,rational_literal(2, 1))), which would represent the sin(π/2) expression. As part of the solving mechanism, this expression could later be arithmetically simplified/rewritten into the literal value 1, which like the number 2 in the former expression, is probably represented as a rational literal, i.e. a pair of bignums. I think Z3 might also have some special support for representing algebraic numbers, but I’m not sure about this. In fact, don’t take my word for any of this, this is just my understanding from very small pieces of code that I’ve read when I was investigating some issues that I ran into. Note that Z3 stands at ~500,000 lines of code, so as you can imagine I’m not even close to having scratched the surface… :)
I’ve never used them, but I believe Z3 actually does have them for at least 12 years (although it might not be documented): see this code where these trigonometric functions are declared.
In fact, looking at this code is how I recently learned that Z3 also supports an exponentiation operator (
^), which can be used with typesInt -> Int -> RealorReal -> Real -> Real. It has a curious definition where it considers0^0to be undefined but0^nis defined to be zero when n is negative (which strikes me as a bit inconsistent).If I recall correctly, it also has a very curious property where it considers
(-3.0) ^ (-0.5)to be equal to(-1/3) ^ 0.5, which is kinda weird because in the “usual” definition of exponentiation 1) those two expressions are complex numbers, 2) those two expressions are not equal – only their real parts are equal, and 3) Z3 doesn’t even support complex numbers (or at least, not directly, although it’s possible to map them to a pair of real numbers).How are floats represented inside a SMT solver?
I’ve never used floats in an SMT solver, much less looked at their internal representation, so I’m not sure I can answer this accurately. From a quick glance at the theory for floating points defined in the SMT-LIB standard, it seems to suggest that they are represented as bit vectors.
Just in case it isn’t clear, however, note that the floats are different from the reals that I mentioned in my comment in several ways. For one, floats have limited precision, while the reals have infinite. Floats have a +infinity and a -infinity representation, two different “zero” representations (plus and minus zero) and also have the concept of a NaN, which has multiple representations. Rounding is necessary for many operations.
The reals as defined in the SMT-LIB standard basically have none of that. It more closely corresponds to the set of real numbers used in math, but as far as irrational numbers are concerned, the SMT-LIB standard doesn’t seem to support transcendental numbers, only algebraic numbers.
That said, it appears that Z3 has some support for transcendental numbers, as evidenced by the support for the
πandeconstants and the trigonometric functions in the code that I referenced. I could be entirely wrong, but my understanding is that Z3 simply represents real numbers internally as AST nodes, which is something that might look likemk_sin(mk_div(pi,rational_literal(2, 1))), which would represent thesin(π/2)expression. As part of the solving mechanism, this expression could later be arithmetically simplified/rewritten into the literal value1, which like the number 2 in the former expression, is probably represented as a rational literal, i.e. a pair of bignums. I think Z3 might also have some special support for representing algebraic numbers, but I’m not sure about this. In fact, don’t take my word for any of this, this is just my understanding from very small pieces of code that I’ve read when I was investigating some issues that I ran into. Note that Z3 stands at ~500,000 lines of code, so as you can imagine I’m not even close to having scratched the surface… :)