add warning messages for #7100

Z3Prover · Jan 31, 2024 · 738c5b6 · 738c5b6
1 parent 50deece
commit 738c5b6
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 6 deletions.
diff --git 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<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) {
             // 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
@@ -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<unsigned>(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
@@ -70,5 +70,10 @@ class context_params {
     */
     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;
+
 
 };