From 5a825d7ac35288ddd11c43dff4691ec14e880595 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Nov 2018 09:37:23 -0800 Subject: [PATCH] true is true, false is not true, it is false Signed-off-by: Nikolaj Bjorner --- src/api/api_algebraic.cpp | 4 ++-- src/api/api_arith.cpp | 2 +- src/api/api_model.cpp | 2 +- src/api/api_numeral.cpp | 12 ++++++------ src/api/api_quant.cpp | 6 +++--- src/api/api_seq.cpp | 12 ++++-------- 6 files changed, 17 insertions(+), 21 deletions(-) diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index c6d0b179b..4ea046f1c 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -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) { diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 214a95a73..0827fd911 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -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) { diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 0cc555d3c..279cef673 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -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()); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index f90c0b4f1..718712d61 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -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; } diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 3e639f93d..306b422f1 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -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); } diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 1e9e7f277..7a9ca80a7 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -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); }