diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 93d4e27e1..d463b1fb7 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -98,7 +98,10 @@ extern "C" { LOG_Z3_set_param_value(c, param_id, param_value); try { ast_context_params * p = reinterpret_cast(c); - p->set(param_id, param_value); + if (p->is_shell_only_parameter(param_id)) + warning_msg("parameter %s can only be set for the shell, not binary API", param_id); + else + p->set(param_id, param_value); } catch (z3_exception & ex) { // The error handler is only available for contexts @@ -111,7 +114,10 @@ extern "C" { Z3_TRY; LOG_Z3_update_param_value(c, param_id, param_value); RESET_ERROR_CODE(); - mk_c(c)->params().set(param_id, param_value); + if (mk_c(c)->params().is_shell_only_parameter(param_id)) + warning_msg("parameter %s can only be set for the shell, not binary API", param_id); + else + mk_c(c)->params().set(param_id, param_value); Z3_CATCH; } diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index fbdd90b8c..1d5d10b39 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -51,15 +51,18 @@ void context_params::set_uint(unsigned & opt, char const * param, char const * v } } -void context_params::set(char const * param, char const * value) { - std::string p = param; - unsigned n = static_cast(p.size()); - for (unsigned i = 0; i < n; i++) { +static void lower_case(std::string& p) { + for (size_t i = 0; i < p.size(); i++) { if (p[i] >= 'A' && p[i] <= 'Z') p[i] = p[i] - 'A' + 'a'; else if (p[i] == '-') p[i] = '_'; } +} + +void context_params::set(char const * param, char const * value) { + std::string p = param; + lower_case(p); if (p == "timeout") { set_uint(m_timeout, param, value); } @@ -195,5 +198,15 @@ void context_params::get_solver_params(params_ref & p, bool & proofs_enabled, bo p.set_bool("auto_config", false); } +bool context_params::is_shell_only_parameter(char const* _p) const { + std::string p(_p); + lower_case(p); + if (p == "dump_models" || p == "well_sorted_check" || + p == "model_validate" || p == "smtlib2_compliant" || + p == "stats") + return true; + + return false; +} diff --git a/src/params/context_params.h b/src/params/context_params.h index ad4cee31d..1f169a5bd 100644 --- a/src/params/context_params.h +++ b/src/params/context_params.h @@ -70,5 +70,10 @@ public: */ params_ref merge_default_params(params_ref const & p); + /** + \brief Is this a parameter that can only be set for the shell. + */ + bool is_shell_only_parameter(char const* p) const; + };