mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

uct forget and minisat restarts added

Browse source
This commit is contained in:
Andreas Froehlich 2014-03-20 15:58:53 +00:00 committed by Christoph M. Wintersteiger
parent a6227d5446
commit 1e55b3bfb5
2 changed files with 1402 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1417
src/tactic/sls/sls_tactic.cpp
View file

File diff suppressed because it is too large Load diff

22
src/tactic/sls/sls_tracker.h
View file

@ -276,6 +276,20 @@ public:
} }
#endif #endif
void uct_forget(goal_ref const & g) {
expr * e;
unsigned touched_old, touched_new;
for (unsigned i = 0; i < g->size(); i++)
{
e = g->form(i);
touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new;
m_touched += touched_new - touched_old;
}
}
void initialize(app * n) { void initialize(app * n) {
// Build score table // Build score table
if (!m_scores.contains(n)) { if (!m_scores.contains(n)) {
@ -1195,6 +1209,8 @@ public:
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched)/vscore.touched); double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched)/vscore.touched);
#elif _UCT_ == 2 #elif _UCT_ == 2
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
#elif _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif #endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
} }
@ -1202,7 +1218,7 @@ public:
if (pos == static_cast<unsigned>(-1)) if (pos == static_cast<unsigned>(-1))
return m_temp_constants; return m_temp_constants;
#if _UCT_ == 1 #if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++; m_scores.find(g->form(pos)).touched++;
m_touched++; m_touched++;
#elif _UCT_ == 2 #elif _UCT_ == 2
@ -1343,6 +1359,8 @@ public:
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched); double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched);
#elif _UCT_ == 2 #elif _UCT_ == 2
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
#elif _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif #endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
} }
@ -1350,7 +1368,7 @@ public:
if (pos == static_cast<unsigned>(-1)) if (pos == static_cast<unsigned>(-1))
return 0; return 0;
#if _UCT_ == 1 #if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++; m_scores.find(g->form(pos)).touched++;
m_touched++; m_touched++;
#elif _UCT_ == 2 #elif _UCT_ == 2