mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

working on python make for arm

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-07 13:36:23 +02:00
parent 1953165422
commit 8c2909f52b
4 changed files with 23 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
scripts/mk_util.py
View file

@ -69,6 +69,7 @@ IS_WINDOWS=False
IS_LINUX=False IS_LINUX=False
IS_HURD=False IS_HURD=False
IS_OSX=False IS_OSX=False
IS_OS_ARM64=False
IS_FREEBSD=False IS_FREEBSD=False
IS_NETBSD=False IS_NETBSD=False
IS_OPENBSD=False IS_OPENBSD=False
@ -598,6 +599,9 @@ if os.name == 'nt':
elif os.name == 'posix': elif os.name == 'posix':
if os.uname()[0] == 'Darwin': if os.uname()[0] == 'Darwin':
IS_OSX=True IS_OSX=True
print("setting Darwin", os.uname()[4])
if os.uname()[4] == 'arm64':
IS_OS_ARM64 = True
elif os.uname()[0] == 'Linux': elif os.uname()[0] == 'Linux':
IS_LINUX=True IS_LINUX=True
elif os.uname()[0] == 'GNU': elif os.uname()[0] == 'GNU':

10
src/ast/pb_decl_plugin.cpp
View file

@ -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<builtin_name> & op_names, symbol const & logic) { void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") { 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_most_sym.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_at_least_sym.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_pble_sym.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_pbge_sym.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_pbeq_sym.str(), OP_PB_EQ));
} }
} }

10
src/ast/special_relations_decl_plugin.cpp
View file

@ -61,11 +61,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) { void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null) { 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_po.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_lo.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_plo.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_to.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_tc.str(), OP_SPECIAL_RELATION_TC));
} }
} }

17
src/util/params.cpp
View file

@ -24,15 +24,14 @@ Notes:
params_ref params_ref::g_empty_params_ref; params_ref params_ref::g_empty_params_ref;
std::string norm_param_name(char const * n) { std::string norm_param_name(char const* n) {
if (n == nullptr)
return "_";
if (*n == ':') if (*n == ':')
n++; n++;
std::string r = n; std::string r = n;
unsigned sz = static_cast<unsigned>(r.size()); unsigned sz = static_cast<unsigned>(r.size());
if (sz == 0) if (sz == 0)
return "_"; return "_";
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
char curr = r[i]; char curr = r[i];
if ('A' <= curr && curr <= 'Z') 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) { std::string norm_param_name(symbol const & n) {
if (n.is_null())
return "_";
return norm_param_name(n.bare_str()); return norm_param_name(n.bare_str());
} }
@ -156,8 +157,8 @@ struct param_descrs::imp {
return m_names[idx]; return m_names[idx];
} }
struct lt { struct symlt {
bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; } 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 { 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) { for (auto const& kv : m_info) {
names.push_back(kv.m_key); 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 (symbol const& name : names) {
for (unsigned i = 0; i < indent; i++) out << " "; for (unsigned i = 0; i < indent; i++) out << " ";
if (smt2_style) if (smt2_style)
out << ':'; out << ':';
char const * s = name.bare_str(); std::string s = name.str();
unsigned n = static_cast<unsigned>(strlen(s)); unsigned n = static_cast<unsigned>(s.length());
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {
if (smt2_style && s[i] == '_') if (smt2_style && s[i] == '_')
out << '-'; out << '-';