working on python make for arm

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 7, 2022 · 8c2909f · 8c2909f
1 parent 1953165
commit 8c2909f
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 18 deletions.
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
@@ -69,6 +69,7 @@ def getenv(name, default):
 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 @@ def check_eol():
 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
@@ -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) {
     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
@@ -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) {
     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
@@ -24,15 +24,14 @@ Module Name:
 
 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<unsigned>(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,22 +157,22 @@ 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 {
         svector<symbol> names;
         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<unsigned>(strlen(s));
+            std::string s = name.str();
+            unsigned n = static_cast<unsigned>(s.length());
             for (unsigned i = 0; i < n; i++) {
                 if (smt2_style && s[i] == '_')
                     out << '-';