From 5844964d950ff31084a6904dc44d9cf8fb5e8adf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2020 17:17:51 -0700 Subject: [PATCH] rename temporary macro Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 20 ++++++++++---------- src/ast/seq_decl_plugin.h | 8 ++++---- src/shell/datalog_frontend.cpp | 6 +++--- src/shell/lp_frontend.cpp | 5 +++-- src/shell/opt_frontend.cpp | 5 +++-- src/util/scoped_timer.cpp | 2 ++ 6 files changed, 25 insertions(+), 21 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 23eaaa17c..cf07f2d31 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -82,7 +82,7 @@ static bool is_escape_char(char const *& s, unsigned& result) { return true; } -#if _USE_UNICODE +#if Z3_USE_UNICODE if (*(s+1) == 'u' && *(s+2) == '{') { result = 0; for (unsigned i = 0; i < 5; ++i) { @@ -606,7 +606,7 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_REPLACE_RE] = alloc(psig, m, "str.replace_re", 1, 3, seqAreAseqA, seqA); m_sigs[OP_SEQ_REPLACE_ALL] = alloc(psig, m, "str.replace_all", 1, 3, seqAseqAseqA, seqA); m_sigs[OP_STRING_CONST] = nullptr; -#if _USE_UNICODE +#if Z3_USE_UNICODE m_sigs[OP_CHAR_CONST] = nullptr; sort* charTcharT[2] = { m_char, m_char }; m_sigs[OP_CHAR_LE] = alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT); @@ -636,7 +636,7 @@ void seq_decl_plugin::init() { void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); bv_util bv(*m); -#if _USE_UNICODE +#if Z3_USE_UNICODE m_char = m->mk_sort(symbol("Unicode"), sort_info(m_family_id, _CHAR_SORT, 0, nullptr)); #else m_char = bv.mk_sort(8); @@ -674,7 +674,7 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter } return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); } -#if _USE_UNICODE +#if Z3_USE_UNICODE case _CHAR_SORT: return m_char; #endif @@ -902,7 +902,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, m_has_re = true; return mk_str_fun(k, arity, domain, range, OP_SEQ_TO_RE); -#if _USE_UNICODE +#if Z3_USE_UNICODE case OP_CHAR_LE: if (arity == 2 && domain[0] == m_char && domain[1] == m_char) { return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr)); @@ -1007,7 +1007,7 @@ app* seq_decl_plugin::mk_string(zstring const& s) { } app* seq_decl_plugin::mk_char(unsigned u) { -#if _USE_UNICODE +#if Z3_USE_UNICODE parameter param(u); func_decl* f = m_manager->mk_const_decl(m_charc_sym, m_char, func_decl_info(m_family_id, OP_CHAR_CONST, 1, ¶m)); return m_manager->mk_const(f); @@ -1079,7 +1079,7 @@ bool seq_decl_plugin::are_distinct(app* a, app* b) const { is_app_of(a, m_family_id, OP_SEQ_UNIT)) { return true; } -#if _USE_UNICODE +#if Z3_USE_UNICODE if (is_app_of(a, m_family_id, OP_CHAR_CONST) && is_app_of(b, m_family_id, OP_CHAR_CONST)) { return true; @@ -1127,7 +1127,7 @@ bv_util& seq_util::bv() const { } bool seq_util::is_const_char(expr* e, unsigned& c) const { -#if _USE_UNICODE +#if Z3_USE_UNICODE return is_app_of(e, m_fid, OP_CHAR_CONST) && (c = to_app(e)->get_parameter(0).get_int(), true); #else rational r; @@ -1137,7 +1137,7 @@ bool seq_util::is_const_char(expr* e, unsigned& c) const { } app* seq_util::mk_char(unsigned ch) const { -#if _USE_UNICODE +#if Z3_USE_UNICODE return seq.mk_char(ch); #else return bv().mk_numeral(rational(ch), 8); @@ -1145,7 +1145,7 @@ app* seq_util::mk_char(unsigned ch) const { } app* seq_util::mk_le(expr* ch1, expr* ch2) const { -#if _USE_UNICODE +#if Z3_USE_UNICODE expr* es[2] = { ch1, ch2 }; return m.mk_app(m_fid, OP_CHAR_LE, 2, es); #else diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 35a0e86a9..c0e2d1157 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -26,12 +26,12 @@ Revision History: #include "ast/ast.h" #include "ast/bv_decl_plugin.h" -#define _USE_UNICODE 0 +#define Z3_USE_UNICODE 0 enum seq_sort_kind { SEQ_SORT, RE_SORT, -#if _USE_UNICODE +#if Z3_USE_UNICODE _CHAR_SORT, // internal only #endif _STRING_SORT, @@ -87,7 +87,7 @@ enum seq_op_kind { OP_STRING_TO_CODE, OP_STRING_FROM_CODE, -#if _USE_UNICODE +#if Z3_USE_UNICODE OP_CHAR_CONST, // constant character OP_CHAR_LE, // Unicode comparison #endif @@ -247,7 +247,7 @@ public: bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); } bool is_char(expr* e) const { return is_char(m.get_sort(e)); } bool is_const_char(expr* e, unsigned& c) const; -#if _USE_UNICODE +#if Z3_USE_UNICODE bool is_char_le(expr const* e) const { return is_app_of(e, m_fid, OP_CHAR_LE); } #else bool is_char_le(expr const* e) const { return false; } diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 94a9a1537..ca0e92801 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include -#include #include #include #include "util/stopwatch.h" @@ -33,6 +32,7 @@ Revision History: #include "muz/fp/datalog_parser.h" #include "shell/datalog_frontend.h" #include "util/timeout.h" +#include "util/mutex.h" static stopwatch g_overall_time; static stopwatch g_piece_timer; @@ -43,7 +43,7 @@ static datalog::rule_set * g_orig_rules; static datalog::instruction_block * g_code; static datalog::execution_context * g_ectx; -static std::mutex *display_stats_mux = new std::mutex; +static mutex *display_stats_mux = new mutex; static void display_statistics( @@ -55,7 +55,7 @@ static void display_statistics( bool verbose ) { - std::lock_guard lock(*display_stats_mux); + lock_guard lock(*display_stats_mux); g_piece_timer.stop(); unsigned t_other = static_cast(g_piece_timer.get_seconds()*1000); g_overall_time.stop(); diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 5fb490523..8f6e6a242 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -14,16 +14,17 @@ Author: #include "util/scoped_timer.h" #include "util/rlimit.h" #include "util/gparams.h" +#include "util/mutex.h" #include #include "smt/params/smt_params_helper.hpp" namespace { -static std::mutex *display_stats_mux = new std::mutex; +static mutex *display_stats_mux = new mutex; static lp::lp_solver* g_solver = nullptr; static void display_statistics() { - std::lock_guard lock(*display_stats_mux); + lock_guard lock(*display_stats_mux); if (g_solver && g_solver->settings().print_statistics) { // TBD display relevant information about statistics } diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index b7e129145..b4e2b3f3b 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -11,6 +11,7 @@ Copyright (c) 2015 Microsoft Corporation #include "util/timeout.h" #include "util/cancel_eh.h" #include "util/scoped_timer.h" +#include "util/mutex.h" #include "ast/ast_util.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" @@ -25,7 +26,7 @@ static bool g_first_interrupt = true; static opt::context* g_opt = nullptr; static double g_start_time = 0; static unsigned_vector g_handles; -static std::mutex *display_stats_mux = new std::mutex; +static mutex *display_stats_mux = new mutex; static void display_results() { @@ -50,7 +51,7 @@ static void display_results() { } static void display_statistics() { - std::lock_guard lock(*display_stats_mux); + lock_guard lock(*display_stats_mux); if (g_display_statistics && g_opt) { ::statistics stats; g_opt->collect_statistics(stats); diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 58416289a..1d806495e 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -15,6 +15,8 @@ Author: Revision History: + Nuno Lopes (nlopes) 2019-02-04 - use C++11 goodies + --*/ #include "util/scoped_timer.h"