mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

add warning messages for #7100

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-30 21:30:27 -08:00
parent 50deece29e
commit 738c5b6d0d
3 changed files with 30 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_config_params.cpp
View file

@ -98,7 +98,10 @@ extern "C" {
LOG_Z3_set_param_value(c, param_id, param_value); LOG_Z3_set_param_value(c, param_id, param_value);
try { try {
ast_context_params * p = reinterpret_cast<ast_context_params*>(c); ast_context_params * p = reinterpret_cast<ast_context_params*>(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) { catch (z3_exception & ex) {
// The error handler is only available for contexts // The error handler is only available for contexts
@ -111,7 +114,10 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_update_param_value(c, param_id, param_value); LOG_Z3_update_param_value(c, param_id, param_value);
RESET_ERROR_CODE(); 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; Z3_CATCH;
} }

21
src/params/context_params.cpp
View file

@ -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) { static void lower_case(std::string& p) {
std::string p = param; for (size_t i = 0; i < p.size(); i++) {
unsigned n = static_cast<unsigned>(p.size());
for (unsigned i = 0; i < n; i++) {
if (p[i] >= 'A' && p[i] <= 'Z') if (p[i] >= 'A' && p[i] <= 'Z')
p[i] = p[i] - 'A' + 'a'; p[i] = p[i] - 'A' + 'a';
else if (p[i] == '-') else if (p[i] == '-')
p[i] = '_'; p[i] = '_';
} }
}
void context_params::set(char const * param, char const * value) {
std::string p = param;
lower_case(p);
if (p == "timeout") { if (p == "timeout") {
set_uint(m_timeout, param, value); 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); 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;
}

5
src/params/context_params.h
View file

@ -70,5 +70,10 @@ public:
*/ */
params_ref merge_default_params(params_ref const & p); 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;
}; };