3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 14:55:25 +00:00

Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt

This commit is contained in:
Christoph M. Wintersteiger 2014-03-28 12:27:26 +00:00
commit 715ce15dec

View file

@ -276,13 +276,13 @@ public:
} }
#endif #endif
void uct_forget(goal_ref const & g) { void uct_forget(ptr_vector<expr> & as) {
expr * e; expr * e;
unsigned touched_old, touched_new; unsigned touched_old, touched_new;
for (unsigned i = 0; i < g->size(); i++) for (unsigned i = 0; i < as.size(); i++)
{ {
e = g->form(i); e = as[i];
touched_old = m_scores.find(e).touched; touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1); touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new; m_scores.find(e).touched = touched_new;