mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
true is true, false is not true, it is false
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f21162960e
commit
5a825d7ac3
|
@ -83,7 +83,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_algebraic_is_value(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
return Z3_algebraic_is_value_core(c, a) ? true : false;
|
||||
return Z3_algebraic_is_value_core(c, a);
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
@ -283,7 +283,7 @@ extern "C" {
|
|||
r = _am.IRAT_PRED(av, bv); \
|
||||
} \
|
||||
} \
|
||||
return r ? true : false;
|
||||
return r;
|
||||
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
|
|
|
@ -121,7 +121,7 @@ extern "C" {
|
|||
|
||||
Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) {
|
||||
LOG_Z3_is_algebraic_number(c, a);
|
||||
return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? true : false;
|
||||
return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a));
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) {
|
||||
|
|
|
@ -166,7 +166,7 @@ extern "C" {
|
|||
CHECK_IS_EXPR(t, false);
|
||||
model * _m = to_model_ref(m);
|
||||
expr_ref result(mk_c(c)->m());
|
||||
model::scoped_model_completion _scm(*_m, model_completion == true);
|
||||
model::scoped_model_completion _scm(*_m, model_completion);
|
||||
result = (*_m)(to_expr(t));
|
||||
mk_c(c)->save_ast_trail(result.get());
|
||||
*v = of_ast(result.get());
|
||||
|
|
|
@ -188,7 +188,7 @@ extern "C" {
|
|||
CHECK_IS_EXPR(a, "");
|
||||
rational r;
|
||||
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
|
||||
if (ok == true) {
|
||||
if (ok) {
|
||||
return mk_c(c)->mk_external_string(r.to_string());
|
||||
}
|
||||
else {
|
||||
|
@ -252,8 +252,8 @@ extern "C" {
|
|||
am.display_decimal(buffer, n, precision);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
}
|
||||
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
|
||||
if (ok == true) {
|
||||
bool ok = Z3_get_numeral_rational(c, a, r);
|
||||
if (ok) {
|
||||
return mk_c(c)->mk_external_string(r.to_string());
|
||||
}
|
||||
else {
|
||||
|
@ -271,7 +271,7 @@ extern "C" {
|
|||
CHECK_IS_EXPR(a, false);
|
||||
rational r;
|
||||
Z3_bool ok = Z3_get_numeral_rational(c, a, r);
|
||||
if (ok == true) {
|
||||
if (ok) {
|
||||
rational n = numerator(r);
|
||||
rational d = denominator(r);
|
||||
if (n.is_int64() && d.is_int64()) {
|
||||
|
@ -340,7 +340,7 @@ extern "C" {
|
|||
rational r;
|
||||
Z3_bool ok = Z3_get_numeral_rational(c, v, r);
|
||||
SASSERT(u);
|
||||
if (ok == true && r.is_uint64()) {
|
||||
if (ok && r.is_uint64()) {
|
||||
*u = r.get_uint64();
|
||||
return ok;
|
||||
}
|
||||
|
@ -360,7 +360,7 @@ extern "C" {
|
|||
}
|
||||
rational r;
|
||||
Z3_bool ok = Z3_get_numeral_rational(c, v, r);
|
||||
if (ok == true && r.is_int64()) {
|
||||
if (ok && r.is_int64()) {
|
||||
*i = r.get_int64();
|
||||
return ok;
|
||||
}
|
||||
|
|
|
@ -347,7 +347,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_quantifier_forall(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
return ::is_forall(to_ast(a)) ? true : false;
|
||||
return ::is_forall(to_ast(a));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
@ -355,7 +355,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_quantifier_exists(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
return ::is_exists(to_ast(a)) ? true : false;
|
||||
return ::is_exists(to_ast(a));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
@ -363,7 +363,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_lambda(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
return ::is_lambda(to_ast(a)) ? true : false;
|
||||
return ::is_lambda(to_ast(a));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
|
|
@ -69,8 +69,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_seq_sort(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
bool result = mk_c(c)->sutil().is_seq(to_sort(s));
|
||||
return result?true:false;
|
||||
return mk_c(c)->sutil().is_seq(to_sort(s));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
@ -78,8 +77,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_re_sort(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
bool result = mk_c(c)->sutil().is_re(to_sort(s));
|
||||
return result?true:false;
|
||||
return mk_c(c)->sutil().is_re(to_sort(s));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
@ -87,8 +85,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_string_sort(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
bool result = mk_c(c)->sutil().is_string(to_sort(s));
|
||||
return result?true:false;
|
||||
return mk_c(c)->sutil().is_string(to_sort(s));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
@ -96,8 +93,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_is_string(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
bool result = mk_c(c)->sutil().str.is_string(to_expr(s));
|
||||
return result?true:false;
|
||||
return mk_c(c)->sutil().str.is_string(to_expr(s));
|
||||
Z3_CATCH_RETURN(false);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue