diff --git a/CMakeLists.txt b/CMakeLists.txt index 759f69a53..27923b1b5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -35,6 +35,14 @@ endif() option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms" OFF) option(SOLC_STATIC_STDLIBS "Link solc against static versions of libgcc and libstdc++ on supported platforms" OFF) option(STRICT_Z3_VERSION "Use the latest version of Z3" ON) +option(STATICCOMPILE "Compile to static executable" OFF) +if (STATICCOMPILE) + set(BUILD_SHARED_LIBS OFF) + set(Boost_USE_STATIC_LIBS ON) + set(SOLC_STATIC_STDLIBS ON) + set(SOLC_LINK_STATIC ON) + set(CMAKE_EXE_LINKER_FLAGS "-static") +endif() # Setup cccache. include(EthCcache) diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index ffa825446..ac08eaf9b 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -46,7 +46,7 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA # to fix warnings as they arise, so they don't accumulate "to be fixed later". add_compile_options(-Wall) add_compile_options(-Wextra) - add_compile_options(-Werror) + #add_compile_options(-Werror) add_compile_options(-pedantic) add_compile_options(-Wmissing-declarations) add_compile_options(-Wno-unknown-pragmas) diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index 0548c1d89..70770420f 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -38,7 +38,7 @@ CDCL::CDCL( m_theorySolver(_theorySolver), m_backtrackNotify(_backtrackNotify), m_variables(move(_variables)), - order(VarOrderLt(activity)) + m_order(VarOrderLt(m_activity)) { for (Clause const& clause: _clauses) addClause(clause); @@ -243,7 +243,7 @@ std::pair CDCL::analyze(Clause _conflictClause) else { //cout << " adding " << toString(literal) << " @" << variableLevel << " to learnt clause." << endl; - vsids_bump_var_act((uint32_t)literal.variable); + vsidsBumpVarAct((uint32_t)literal.variable); learntClause.push_back(literal); backtrackLevel = max(backtrackLevel, variableLevel); } @@ -278,17 +278,17 @@ std::pair CDCL::analyze(Clause _conflictClause) void CDCL::addClause(Clause _clause) { - uint64_t max_var = (uint32_t)activity.size(); + uint64_t max_var = (uint32_t)m_activity.size(); uint64_t new_max_var = 0; for(auto const& l: _clause) { new_max_var = std::max(l.variable+1, max_var); } int64_t to_add = (int64_t)new_max_var - (int64_t)max_var; if (to_add > 0) { - activity.insert(activity.end(), (uint64_t)to_add, 0.0); + m_activity.insert(m_activity.end(), (uint64_t)to_add, 0.0); } for(auto const& l: _clause) { - if (!order.inHeap((int)l.variable)) order.insert((int)l.variable); + if (!m_order.inHeap((int)l.variable)) m_order.insert((int)l.variable); } m_clauses.push_back(make_unique(move(_clause))); @@ -331,8 +331,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel) m_reason.erase(l); // TODO maybe could do without. m_levelForVariable.erase(l.variable); - if (!order.inHeap((int)l.variable)) { - order.insert((int)l.variable); + if (!m_order.inHeap((int)l.variable)) { + m_order.insert((int)l.variable); } } m_decisionPoints.resize(_backtrackLevel); @@ -344,8 +344,8 @@ void CDCL::cancelUntil(size_t _backtrackLevel) optional CDCL::nextDecisionVariable() { while(true) { - if (order.empty()) return nullopt; - size_t i = (size_t)order.removeMin(); + if (m_order.empty()) return nullopt; + size_t i = (size_t)m_order.removeMin(); if (!m_assignments.count(i)) return i; } return nullopt; diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h index 6cecd1dce..f96fe93a3 100644 --- a/libsolutil/CDCL.h +++ b/libsolutil/CDCL.h @@ -129,30 +129,30 @@ private: #endif // Var activity - Heap order; - std::vector activity; - double var_inc_vsids = 1; - double var_decay = 0.95; + Heap m_order; + std::vector m_activity; + double m_var_inc_vsids = 1; + double m_var_decay = 0.95; void vsids_decay_var_act() { - var_inc_vsids *= (1.0 / var_decay); + m_var_inc_vsids *= (1.0 / m_var_decay); } - void vsids_bump_var_act(uint32_t var) + void vsidsBumpVarAct(const uint32_t var) { - assert(activity.size() > var); - activity[var] += var_inc_vsids; + assert(m_activity.size() > var); + m_activity[var] += m_var_inc_vsids; bool rescaled = false; - if (activity[var] > 1e100) { + if (m_activity[var] > 1e100) { // Rescale - for (auto& a: activity) a *= 1e-100; + for (auto& a: m_activity) a *= 1e-100; rescaled = true; - var_inc_vsids *= 1e-100; + m_var_inc_vsids *= 1e-100; } // Update order_heap with respect to new activity: - if (order.inHeap((int)var)) order.decrease((int)var); - if (rescaled) assert(order.heap_property()); + if (m_order.inHeap((int)var)) m_order.decrease((int)var); + if (rescaled) assert(m_order.heap_property()); } // TODO group those into a class