Remove usages of Z3_bool, just use bool.

Z3Prover · Jul 30, 2022 · fc40e3c · fc40e3c
1 parent c682ec1
commit fc40e3c
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 6 deletions.
diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
@@ -47,7 +47,7 @@ extern "C" {
         env_params::updt_params();
     }
 
-    Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
+    bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
         memory::initialize(UINT_MAX);
         LOG_Z3_global_param_get(param_id, param_value);
         *param_value = nullptr;

diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md
@@ -103,7 +103,7 @@ function rcf_get_numerator_denominator(c: Z3_context, a: Z3_rcf_num): { n: Z3_rc
 When there is only a single out parameter, and the return value is not otherwise of interest, the parameter is not wrapped. For example, the C declaration
 
 ```c
-Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
+bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
 ```
 
 is represented in the TS bindings as

diff --git a/src/api/js/scripts/parse-api.ts b/src/api/js/scripts/parse-api.ts
@@ -16,7 +16,6 @@ const files = [
 
 const aliases = {
   __proto__: null,
-  Z3_bool: 'boolean',
   Z3_string: 'string',
   bool: 'boolean',
   signed: 'int',

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
@@ -1528,7 +1528,7 @@ extern "C" {
 
        def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING)))
     */
-    Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
+    bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
 
     /**@}*/
 
@@ -4440,7 +4440,7 @@ extern "C" {
 
         def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64)))
     */
-    Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
+    bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
 
     /**
        \brief Return the domain of the given array sort.
@@ -5413,7 +5413,7 @@ extern "C" {
 
        def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
     */
-    Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
+    bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
 
     /**
        \brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m.