Retrieving parameters from z3::expr in C++

[SJulianS]

Hi,

I am trying to retrieve parameters stored in a z3::expr in C++. For example,

auto ctx = z3::context();
auto e   = ctx.bv_const("A", 16).extract(6, 3);
std::cout << e << std::endl;

prints ((_ extract 6 3) A). Now I would like to retrieve the parameters 6 and 3 from the expression. By digging through the z3 source code, I found that these parameters are stored in the func_decl_info object associated with the func_decl of the expression. However, I could not find a way to access the func_decl_info from the C++ API. Is there anything I am missing here or is there simply no way to get to these parameters? Any help is appreciated :)

Thanks!

[NikolajBjorner]

You can extract e.lo() and e.hi().
Generally the C API exposes a Z3_get_decl_parameter to retrieve auxiliary parameters of declarations. I didn't add a corresponding C++ wrapper for these functions.

[SJulianS]

e.lo() and e.hi() did the trick, thanks a lot!