mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Remove usages of Z3_bool, just use bool.

Browse source
This commit is contained in:
Bruce Mitchener 2022-07-30 02:06:53 +07:00 • committed by Nikolaj Bjorner
parent c682ec1135
commit fc40e3c510
4 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_config_params.cpp
View file

@ -47,7 +47,7 @@ extern "C" {
env_params::updt_params(); 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); memory::initialize(UINT_MAX);
LOG_Z3_global_param_get(param_id, param_value); LOG_Z3_global_param_get(param_id, param_value);
*param_value = nullptr; *param_value = nullptr;

2
src/api/js/PUBLISHED_README.md
View file

@ -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 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 ```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 is represented in the TS bindings as

1
src/api/js/scripts/parse-api.ts
View file

@ -16,7 +16,6 @@ const files = [
const aliases = { const aliases = {
__proto__: null, __proto__: null,
Z3_bool: 'boolean',
Z3_string: 'string', Z3_string: 'string',
bool: 'boolean', bool: 'boolean',
signed: 'int', signed: 'int',

6
src/api/z3_api.h
View file

@ -1528,7 +1528,7 @@ extern "C" {
def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING))) 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))) 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. \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))) 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. \brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m.