Java API for interpreting real expr ?

[classicwuhao]

I am wondering whether Z3 java API provides a way of interpreting a real expression? Or I have to cast a real expression (a/b) externally myself?

[NikolajBjorner]

do you mean get a double or float approximation?

[classicwuhao]

I think I find the solution. I cast an expr to a RatNum and then get its float approximation, I don't know if this is the correct way of doing it.

[NikolajBjorner]

this is the current approach yes.

[classicwuhao]

Thanks.