From 8c2909f52bda61ce2422f6fb6484fa69a651e59d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Apr 2022 13:36:23 +0200 Subject: [PATCH] working on python make for arm Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 ++++ src/ast/pb_decl_plugin.cpp | 10 +++++----- src/ast/special_relations_decl_plugin.cpp | 10 +++++----- src/util/params.cpp | 17 +++++++++-------- 4 files changed, 23 insertions(+), 18 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1fca64f29..78c983ec4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -69,6 +69,7 @@ IS_WINDOWS=False IS_LINUX=False IS_HURD=False IS_OSX=False +IS_OS_ARM64=False IS_FREEBSD=False IS_NETBSD=False IS_OPENBSD=False @@ -598,6 +599,9 @@ if os.name == 'nt': elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True + print("setting Darwin", os.uname()[4]) + if os.uname()[4] == 'arm64': + IS_OS_ARM64 = True elif os.uname()[0] == 'Linux': IS_LINUX=True elif os.uname()[0] == 'GNU': diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index d4797b507..10e6c694c 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -90,11 +90,11 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") { - op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); - op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K)); - op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE)); - op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE)); - op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ)); + op_names.push_back(builtin_name(m_at_most_sym.str(), OP_AT_MOST_K)); + op_names.push_back(builtin_name(m_at_least_sym.str(), OP_AT_LEAST_K)); + op_names.push_back(builtin_name(m_pble_sym.str(), OP_PB_LE)); + op_names.push_back(builtin_name(m_pbge_sym.str(), OP_PB_GE)); + op_names.push_back(builtin_name(m_pbeq_sym.str(), OP_PB_EQ)); } } diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index 5dc5f32fe..7ed5e8346 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -61,11 +61,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl( void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol::null) { - op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO)); - op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO)); - op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO)); - op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); - op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC)); + op_names.push_back(builtin_name(m_po.str(), OP_SPECIAL_RELATION_PO)); + op_names.push_back(builtin_name(m_lo.str(), OP_SPECIAL_RELATION_LO)); + op_names.push_back(builtin_name(m_plo.str(), OP_SPECIAL_RELATION_PLO)); + op_names.push_back(builtin_name(m_to.str(), OP_SPECIAL_RELATION_TO)); + op_names.push_back(builtin_name(m_tc.str(), OP_SPECIAL_RELATION_TC)); } } diff --git a/src/util/params.cpp b/src/util/params.cpp index aefe4e074..1745e56fd 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -24,15 +24,14 @@ Notes: params_ref params_ref::g_empty_params_ref; -std::string norm_param_name(char const * n) { - if (n == nullptr) - return "_"; +std::string norm_param_name(char const* n) { if (*n == ':') n++; std::string r = n; unsigned sz = static_cast(r.size()); if (sz == 0) return "_"; + for (unsigned i = 0; i < sz; i++) { char curr = r[i]; if ('A' <= curr && curr <= 'Z') @@ -44,6 +43,8 @@ std::string norm_param_name(char const * n) { } std::string norm_param_name(symbol const & n) { + if (n.is_null()) + return "_"; return norm_param_name(n.bare_str()); } @@ -156,8 +157,8 @@ struct param_descrs::imp { return m_names[idx]; } - struct lt { - bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; } + struct symlt { + bool operator()(symbol const & s1, symbol const & s2) const { return ::lt(s1, s2); } }; void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { @@ -165,13 +166,13 @@ struct param_descrs::imp { for (auto const& kv : m_info) { names.push_back(kv.m_key); } - std::sort(names.begin(), names.end(), lt()); + std::sort(names.begin(), names.end(), symlt()); for (symbol const& name : names) { for (unsigned i = 0; i < indent; i++) out << " "; if (smt2_style) out << ':'; - char const * s = name.bare_str(); - unsigned n = static_cast(strlen(s)); + std::string s = name.str(); + unsigned n = static_cast(s.length()); for (unsigned i = 0; i < n; i++) { if (smt2_style && s[i] == '_') out << '-';