mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #13234 from msooseth/smtComp-msoos
SMTComp changes by msooseth
This commit is contained in:
commit
c429d87ba1
@ -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)
|
||||
|
@ -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)
|
||||
|
@ -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<Clause, size_t> 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<Clause, size_t> 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<uint64_t>(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<Clause>(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<size_t> 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;
|
||||
|
@ -129,30 +129,30 @@ private:
|
||||
#endif
|
||||
|
||||
// Var activity
|
||||
Heap<VarOrderLt> order;
|
||||
std::vector<double> activity;
|
||||
double var_inc_vsids = 1;
|
||||
double var_decay = 0.95;
|
||||
Heap<VarOrderLt> m_order;
|
||||
std::vector<double> 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
|
||||
|
Loading…
Reference in New Issue
Block a user