1 | /* BDD generic apply routines */ |
---|
2 | |
---|
3 | |
---|
4 | #include "bddint.h" |
---|
5 | |
---|
6 | |
---|
7 | static |
---|
8 | bdd |
---|
9 | bdd_apply2_step(cmu_bdd_manager bddm, |
---|
10 | bdd (*terminal_fn)(cmu_bdd_manager, bdd *, bdd *, pointer), |
---|
11 | long op, |
---|
12 | bdd f, |
---|
13 | bdd g, |
---|
14 | pointer env) |
---|
15 | { |
---|
16 | bdd_indexindex_type top_indexindex; |
---|
17 | bdd f1, f2; |
---|
18 | bdd g1, g2; |
---|
19 | bdd temp1, temp2; |
---|
20 | bdd result; |
---|
21 | |
---|
22 | if ((result=(*terminal_fn)(bddm, &f, &g, env))) |
---|
23 | { |
---|
24 | BDD_SETUP(result); |
---|
25 | BDD_TEMP_INCREFS(result); |
---|
26 | return (result); |
---|
27 | } |
---|
28 | if (bdd_lookup_in_cache2(bddm, op, f, g, &result)) |
---|
29 | return (result); |
---|
30 | { |
---|
31 | BDD_SETUP(f); |
---|
32 | BDD_SETUP(g); |
---|
33 | BDD_TOP_VAR2(top_indexindex, bddm, f, g); |
---|
34 | BDD_COFACTOR(top_indexindex, f, f1, f2); |
---|
35 | BDD_COFACTOR(top_indexindex, g, g1, g2); |
---|
36 | temp1=bdd_apply2_step(bddm, terminal_fn, op, f1, g1, env); |
---|
37 | temp2=bdd_apply2_step(bddm, terminal_fn, op, f2, g2, env); |
---|
38 | result=bdd_find(bddm, top_indexindex, temp1, temp2); |
---|
39 | bdd_insert_in_cache2(bddm, op, f, g, result); |
---|
40 | return (result); |
---|
41 | } |
---|
42 | } |
---|
43 | |
---|
44 | |
---|
45 | bdd |
---|
46 | bdd_apply2(cmu_bdd_manager bddm, bdd (*terminal_fn)(cmu_bdd_manager, bdd *, bdd *, pointer), bdd f, bdd g, pointer env) |
---|
47 | { |
---|
48 | long op; |
---|
49 | |
---|
50 | if (bdd_check_arguments(2, f, g)) |
---|
51 | { |
---|
52 | FIREWALL(bddm); |
---|
53 | op=bddm->temp_op--; |
---|
54 | RETURN_BDD(bdd_apply2_step(bddm, terminal_fn, op, f, g, env)); |
---|
55 | } |
---|
56 | return ((bdd)0); |
---|
57 | } |
---|
58 | |
---|
59 | |
---|
60 | static |
---|
61 | bdd |
---|
62 | bdd_apply1_step(cmu_bdd_manager bddm, bdd (*terminal_fn)(cmu_bdd_manager, bdd *, pointer), long op, bdd f, pointer env) |
---|
63 | { |
---|
64 | bdd temp1, temp2; |
---|
65 | bdd result; |
---|
66 | |
---|
67 | if ((result=(*terminal_fn)(bddm, &f, env))) |
---|
68 | { |
---|
69 | BDD_SETUP(result); |
---|
70 | BDD_TEMP_INCREFS(result); |
---|
71 | return (result); |
---|
72 | } |
---|
73 | if (bdd_lookup_in_cache1(bddm, op, f, &result)) |
---|
74 | return (result); |
---|
75 | { |
---|
76 | BDD_SETUP(f); |
---|
77 | temp1=bdd_apply1_step(bddm, terminal_fn, op, BDD_THEN(f), env); |
---|
78 | temp2=bdd_apply1_step(bddm, terminal_fn, op, BDD_ELSE(f), env); |
---|
79 | result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2); |
---|
80 | bdd_insert_in_cache1(bddm, op, f, result); |
---|
81 | return (result); |
---|
82 | } |
---|
83 | } |
---|
84 | |
---|
85 | |
---|
86 | bdd |
---|
87 | bdd_apply1(cmu_bdd_manager bddm, bdd (*terminal_fn)(cmu_bdd_manager, bdd *, pointer), bdd f, pointer env) |
---|
88 | { |
---|
89 | long op; |
---|
90 | |
---|
91 | if (bdd_check_arguments(1, f)) |
---|
92 | { |
---|
93 | FIREWALL(bddm); |
---|
94 | op=bddm->temp_op--; |
---|
95 | RETURN_BDD(bdd_apply1_step(bddm, terminal_fn, op, f, env)); |
---|
96 | } |
---|
97 | return ((bdd)0); |
---|
98 | } |
---|