Add support of the SunOS platform (Solaris, OpenSolaris, OpenIndiana) (#4757)

* Add support of the SunOS plateform (OpenSolaris, OpenIndiana) in scripts/mk_util.py

* Add missing casts for the SunOS plateform (OpenSolaris, OpenIndiana) for the pow function

scripts/mk_util.py

@@ -72,6 +72,7 @@ IS_OSX=False
 IS_FREEBSD=False
 IS_NETBSD=False
 IS_OPENBSD=False
+IS_SUNOS=False
 IS_CYGWIN=False
 IS_CYGWIN_MINGW=False
 IS_MSYS2=False
@@ -154,6 +155,9 @@ def is_netbsd():
 def is_openbsd():
     return IS_OPENBSD
 
+def is_sunos():
+    return IS_SUNOS
+
 def is_osx():
     return IS_OSX
 
@@ -488,6 +492,9 @@ def find_ml_lib():
 
 def is64():
     global LINUX_X64
+    if is_sunos() and sys.version_info.major < 3: 
+        return LINUX_X64
+    else:
         return LINUX_X64 and sys.maxsize >= 2**32
 
 def check_ar():
@@ -598,6 +605,8 @@ elif os.name == 'posix':
         IS_NETBSD=True
     elif os.uname()[0] == 'OpenBSD':
         IS_OPENBSD=True
+    elif os.uname()[0] == 'SunOS':
+        IS_SUNOS=True
     elif os.uname()[0][:6] == 'CYGWIN':
         IS_CYGWIN=True
         if (CC != None and "mingw" in CC):
@@ -1768,6 +1777,8 @@ class JavaDLLComponent(Component):
                 t = t.replace('PLATFORM', 'netbsd')
             elif IS_OPENBSD:
                 t = t.replace('PLATFORM', 'openbsd')
+            elif IS_SUNOS:
+                t = t.replace('PLATFORM', 'SunOS')
             elif IS_CYGWIN:
                 t = t.replace('PLATFORM', 'cygwin')
             elif IS_MSYS2:
@@ -2514,6 +2525,12 @@ def mk_config():
             OS_DEFINES     = '-D_OPENBSD_'
             SO_EXT         = '.so'
             SLIBFLAGS      = '-shared'
+        elif sysname  == 'SunOS':
+            CXXFLAGS       = '%s -D_SUNOS_' % CXXFLAGS
+            OS_DEFINES     = '-D_SUNOS_'
+            SO_EXT         = '.so'
+            SLIBFLAGS      = '-shared'
+            SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS
         elif sysname.startswith('CYGWIN'):
             CXXFLAGS       = '%s -D_CYGWIN' % CXXFLAGS
             OS_DEFINES     = '-D_CYGWIN'

src/ast/value_generator.cpp

@@ -31,7 +31,7 @@
   bigger (and only equal for values 0, 1).
 */
 static void inverse_cantor(unsigned z, unsigned& x, unsigned& y) {
-    unsigned w = ((unsigned)sqrt(8*z + 1) - 1)/2;
+    unsigned w = ((unsigned)sqrt(static_cast<double>(8*z + 1)) - 1)/2;
     unsigned t = (unsigned)(w*w + w)/2;
     y = z - t;
     x = w - y;

src/sat/sat_lookahead.cpp

@@ -553,7 +553,7 @@ namespace sat {
                 }
             }
             unsigned len = n->size();
-            sum += pow(0.5, len) * to_add / len;            
+            sum += pow(0.5, static_cast<double>(len)) * to_add / len;
         }
         return sum;
     } 
@@ -575,7 +575,7 @@ namespace sat {
         unsigned sz = m_nary_count[(~l).index()];
         for (nary * n : m_nary[(~l).index()]) {
             if (sz-- == 0) break;
-            sum += pow(0.5, n->size());
+            sum += pow(0.5, static_cast<double>(n->size()));
         }
         return sum;
     }
@@ -1490,14 +1490,14 @@ namespace sat {
                             to_add += literal_occs(lit);
                         }                        
                     }
-                    m_lookahead_reward += pow(0.5, nonfixed) * to_add / nonfixed;                    
+                    m_lookahead_reward += pow(0.5, static_cast<double>(nonfixed)) * to_add / nonfixed;
                     break;
                 }
                 case heule_unit_reward:
-                    m_lookahead_reward += pow(0.5, nonfixed);
+                    m_lookahead_reward += pow(0.5, static_cast<double>(nonfixed));
                     break;
                 case march_cu_reward:
-                    m_lookahead_reward += nonfixed >= 2 ? 3.3 * pow(0.5, nonfixed - 2) : 0.0;
+                    m_lookahead_reward += nonfixed >= 2 ? 3.3 * pow(0.5, static_cast<double>(nonfixed - 2)) : 0.0;
                     break;
                 case ternary_reward:
                     UNREACHABLE();
@@ -1615,14 +1615,14 @@ namespace sat {
                     to_add += literal_occs(l);
                 } 
             }
-            m_lookahead_reward += pow(0.5, sz) * to_add / sz;
+            m_lookahead_reward += pow(0.5, static_cast<double>(sz)) * to_add / sz;
             break;
         }
         case heule_unit_reward:
-            m_lookahead_reward += pow(0.5, sz);
+            m_lookahead_reward += pow(0.5, static_cast<double>(sz));
             break;
         case march_cu_reward:
-            m_lookahead_reward += 3.3 * pow(0.5, sz - 2);
+            m_lookahead_reward += 3.3 * pow(0.5, static_cast<double>(sz - 2));
             break;
         case ternary_reward:
             m_lookahead_reward = (double)0.001;            
@@ -2125,7 +2125,7 @@ namespace sat {
             }
         }
         for (nary * n : m_nary_clauses) {
-            h += 1.0 / pow(m_config.m_cube_psat_clause_base, n->size() - 1);
+            h += 1.0 / pow(m_config.m_cube_psat_clause_base, static_cast<double>(n->size() - 1));
         }
         h /= pow(m_freevars.size(), m_config.m_cube_psat_var_exp);
         IF_VERBOSE(10, verbose_stream() << "(sat-cube-psat :val " << h << ")\n";);
@@ -2189,7 +2189,7 @@ namespace sat {
             backtrack_level = UINT_MAX;
             depth = m_cube_state.m_cube.size();
             if (should_cutoff(depth)) {
-                double dec = (1.0 - pow(m_config.m_cube_fraction, depth));
+                double dec = (1.0 - pow(m_config.m_cube_fraction, static_cast<double>(depth)));
                 m_cube_state.m_freevars_threshold *= dec;
                 m_cube_state.m_psat_threshold *= 2.0 - dec;
                 set_conflict();

src/sat/sat_solver.cpp

@@ -958,7 +958,7 @@ namespace sat {
         if (m_config.m_anti_exploration) {
             uint64_t age = m_stats.m_conflict - m_canceled[v];
             if (age > 0) {
-                double decay = pow(0.95, age);
+                double decay = pow(0.95, static_cast<double>(age));
                 set_activity(v, static_cast<unsigned>(m_activity[v] * decay));
                 // NB. MapleSAT does not update canceled.
                 m_canceled[v] = m_stats.m_conflict;
@@ -1640,7 +1640,7 @@ namespace sat {
                 next = m_case_split_queue.min_var();
                 auto age = m_stats.m_conflict - m_canceled[next];
                 while (age > 0) {
-                    set_activity(next, static_cast<unsigned>(m_activity[next] * pow(0.95, age)));
+                    set_activity(next, static_cast<unsigned>(m_activity[next] * pow(0.95, static_cast<double>(age))));
                     m_canceled[next] = m_stats.m_conflict;
                     next = m_case_split_queue.min_var();
                     age = m_stats.m_conflict - m_canceled[next];                    

src/sat/smt/ba_card.cpp

@@ -78,7 +78,7 @@ namespace ba {
             }
         }
         if (k >= slack) return 1;
-        return pow(0.5, slack - k + 1) * to_add;
+        return pow(0.5, static_cast<double>(slack - k + 1)) * to_add;
     }
 
     std::ostream& card::display(std::ostream& out) const {

src/smt/smt_lookahead.cpp

@@ -49,7 +49,7 @@ namespace smt {
                 }
             }
             if (!is_taut && nf > 0) {
-                score += pow(0.5, nu);
+                score += pow(0.5, static_cast<double>(nu));
             }
         }
         return score;

src/solver/parallel_tactic.cpp

@@ -327,7 +327,7 @@ class parallel_tactic : public tactic {
             p.copy(m_params);
             double exp = pp.simplify_exp();
             exp = std::max(exp, 1.0);
-            unsigned mult = static_cast<unsigned>(pow(exp, m_depth - 1));
+            unsigned mult = static_cast<unsigned>(pow(exp, static_cast<double>(m_depth - 1)));
             unsigned max_conflicts = pp.simplify_max_conflicts();
             if (max_conflicts < 1000000)
                 max_conflicts *= std::max(m_depth, 1u);