From 6bbe8e2619c83e6a0403931aee06fdeabe5c738b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 7 Jul 2019 15:30:32 +0100 Subject: [PATCH] add some static --- src/api/api_bv.cpp | 12 ++---------- src/api/api_numeral.cpp | 2 +- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index e56371bb5..7f0888d45 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -67,7 +67,7 @@ extern "C" { MK_BV_BINARY(Z3_mk_ext_rotate_left, OP_EXT_ROTATE_LEFT); MK_BV_BINARY(Z3_mk_ext_rotate_right, OP_EXT_ROTATE_RIGHT); - Z3_ast mk_extract_core(Z3_context c, unsigned high, unsigned low, Z3_ast n) { + static Z3_ast mk_extract_core(Z3_context c, unsigned high, unsigned low, Z3_ast n) { expr * _n = to_expr(n); parameter params[2] = { parameter(high), parameter(low) }; expr * a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_EXTRACT, 2, params, 1, &_n); @@ -174,18 +174,10 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_CATCH_RETURN(nullptr); } - Z3_ast Z3_mk_bvsmin(Z3_context c, Z3_sort s) { + static Z3_ast Z3_mk_bvsmin(Z3_context c, Z3_sort s) { return Z3_mk_bvmsb(c, s); } - Z3_ast Z3_mk_bvsmax(Z3_context c, Z3_sort s) { - return Z3_mk_bvnot(c, Z3_mk_bvmsb(c, s)); - } - - Z3_ast Z3_mk_bvumax(Z3_context c, Z3_sort s) { - return Z3_mk_int(c, -1, s); - } - Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) { Z3_TRY; RESET_ERROR_CODE(); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 90d5998f3..a09e33cf6 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -38,7 +38,7 @@ bool is_numeral_sort(Z3_context c, Z3_sort ty) { return true; } -bool check_numeral_sort(Z3_context c, Z3_sort ty) { +static bool check_numeral_sort(Z3_context c, Z3_sort ty) { bool is_num = is_numeral_sort(c, ty); if (!is_num) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);