C API: tracking function declarations

[turibe]

Hello, want to make sure that I'm not missing something in the C API:

I can make function declarations with Z3_mk_func_decl(), and add them to a parser context (Z3_parser_context_add_decl), for example.

But given, say, a function symbol and an arity, there does not seem to be a way to get the already-declared function declarations that correspond to that symbol and arity? It would be nice to have such functionality so that I don't have to keep a separate map; and perhaps even better if I could just query the context to get those declarations (to have fewer objects floating around). Thx!

[NikolajBjorner]

The functionality isn't supported.
You can retrieve all assertions from a solver object and walk all sub-expressions to get functions that are used in a solver state.