diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b1d44bfad..d5c6f1f22 100644 --- a/scripts/mk_util.py +++ b/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,7 +492,10 @@ def find_ml_lib(): def is64(): global LINUX_X64 - return LINUX_X64 and sys.maxsize >= 2**32 + if is_sunos() and sys.version_info.major < 3: + return LINUX_X64 + else: + return LINUX_X64 and sys.maxsize >= 2**32 def check_ar(): if is_verbose(): @@ -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' diff --git a/src/ast/value_generator.cpp b/src/ast/value_generator.cpp index 8b17c84cb..ef21f2444 100644 --- a/src/ast/value_generator.cpp +++ b/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(8*z + 1)) - 1)/2; unsigned t = (unsigned)(w*w + w)/2; y = z - t; x = w - y; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index c78e7995c..83e5b9ca5 100644 --- a/src/sat/sat_lookahead.cpp +++ b/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(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(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(nonfixed)) * to_add / nonfixed; break; } case heule_unit_reward: - m_lookahead_reward += pow(0.5, nonfixed); + m_lookahead_reward += pow(0.5, static_cast(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(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(sz)) * to_add / sz; break; } case heule_unit_reward: - m_lookahead_reward += pow(0.5, sz); + m_lookahead_reward += pow(0.5, static_cast(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(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(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(depth))); m_cube_state.m_freevars_threshold *= dec; m_cube_state.m_psat_threshold *= 2.0 - dec; set_conflict(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 93942e21e..8ba4ba41b 100644 --- a/src/sat/sat_solver.cpp +++ b/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(age)); set_activity(v, static_cast(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(m_activity[next] * pow(0.95, age))); + set_activity(next, static_cast(m_activity[next] * pow(0.95, static_cast(age)))); m_canceled[next] = m_stats.m_conflict; next = m_case_split_queue.min_var(); age = m_stats.m_conflict - m_canceled[next]; diff --git a/src/sat/smt/ba_card.cpp b/src/sat/smt/ba_card.cpp index 51e996ce2..277a53fe3 100644 --- a/src/sat/smt/ba_card.cpp +++ b/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(slack - k + 1)) * to_add; } std::ostream& card::display(std::ostream& out) const { diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp index 191b03e49..8de3f2f34 100644 --- a/src/smt/smt_lookahead.cpp +++ b/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(nu)); } } return score; diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index c32648a44..ef2356678 100644 --- a/src/solver/parallel_tactic.cpp +++ b/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(pow(exp, m_depth - 1)); + unsigned mult = static_cast(pow(exp, static_cast(m_depth - 1))); unsigned max_conflicts = pp.simplify_max_conflicts(); if (max_conflicts < 1000000) max_conflicts *= std::max(m_depth, 1u);