Have Z3_set_param_value indicate if a setting is being ignored

[facundominguez]

Z3_set_param_value seems to ignore global parameters, for which Z3_global_param_set should be set. Unfortunately, this is not obvious to users when they interact with Z3 through another layer (like smtlib-backends).

Would it be possible to query the API to learn if some parameter set with Z3_set_param_value has been ignored? This would allow to give users an explicit error message when things don't go as expected.

This issue surfaced when a user was trying to start a Z3 context with dump_models set to true.

Another solution could be having a way to test whether a parameter is in the domain of Z3_set_param_value ahead of making the call. There is a call Z3_get_global_param_descrs, but it requires having a Z3 context first, which isn't necessary with Z3_set_param_value.

[NikolajBjorner]

dump_models is defined two places:

• for the command-context that processes formulas from input files. Global
• for optimization. Local to optimization.

It means different things for the two uses.

• for command context it means to always display the model after check-sat when available. It is like adding a default (get-model)
• for optimization it is to display intermediary feasible, but not necessarily optimal models. You use this to glean for a best-effort result. "are we there yet".

They happen to have the same name, but may as well have been renamed apart.
If you set "dump_models" on other objects, such as a solver object, you will get an error message.

[facundominguez]

for the command-context that processes formulas from input files. Global

If this is Z3_Context in the C API, then setting dump_models with Z3_set_param_value doesn't seem to have any effect, nor does it produce an error.

If helpful, I could try writing a C program that shows this behavior.

[NikolajBjorner]

Alright, dump_models is only intended to be used from the text API.
For programmatic API you can set a callback when there is a model, Z3_optimize_register_model_eh.