1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
bdd_ptr bddpaths[10];
/* function that updates BDD pointers floating around in user's code;
the remaining ones are kept in the sub_results list below */
void update_bddpaths(unsigned (*new_place) (unsigned node)) {
int j;
/* update the pointers in bddpaths */
for (j = 0; j < exp_count; j++)
bddpaths[j] = new_place(bddpaths[j]);
}
/* we can only update pointers that are not stored as local
variables, so values of local variables are thrown onto a stack */
DECLARE_SEQUENTIAL_LIST(sub_results, unsigned);
bdd_ptr makepath(bdd_manager *bddm, ...,
void (*update_bddpaths)
(unsigned (*new_place) (unsigned node))) {
...
bdd_ptr res, sub_res, default_state_ptr;
sub_res = makepath(bddm, n+1, leaf_value, update_bddpaths);
/* push BDD pointer sub_res on list sub_results */
PUSH_SEQUENTIAL_LIST(sub_results, unsigned, sub_res);
/* insert a new hashed node; thus potentially changing the pointer
to the node known as sub_res above, and also potentially changing
the pointers in bddpaths[10]. But bdd_find_leaf_hashed automatically
updates all pointers in the sub_results list, since it was provided
as an argument. Also, the function update_bddpaths is called when a
doubling of the table takes place and an appropriate renaming function
new_place is supplied by bdd_find_leaf_hashed */
default_state_ptr =
bdd_find_leaf_hashed(bddm,
default_state,
SEQUENTIAL_LIST(sub_results),
update_bddpaths);
/* restore the value of sub_res */
POP_SEQUENTIAL_LIST(sub_results, unsigned, sub_res);
...
}
|
