mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

removed dependency of bvsls on goal_refs

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-28 12:27:06 +00:00
parent e9797c3922
commit 71fdb59747
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -276,13 +276,13 @@ public:
}
#endif
void uct_forget(goal_ref const & g) {
void uct_forget(ptr_vector<expr> & as) {
expr * e;
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_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new;