[13] | 1 | /* BDD support routines */ |
---|
| 2 | |
---|
| 3 | |
---|
| 4 | #include "bddint.h" |
---|
| 5 | |
---|
| 6 | |
---|
| 7 | static |
---|
| 8 | int |
---|
| 9 | cmu_bdd_depends_on_step(cmu_bdd_manager bddm, bdd f, bdd_index_type var_index, int mark) |
---|
| 10 | { |
---|
| 11 | bdd_index_type f_index; |
---|
| 12 | |
---|
| 13 | BDD_SETUP(f); |
---|
| 14 | f_index=BDD_INDEX(bddm, f); |
---|
| 15 | if (f_index > var_index) |
---|
| 16 | return (0); |
---|
| 17 | if (f_index == var_index) |
---|
| 18 | return (1); |
---|
| 19 | if (BDD_MARK(f) == mark) |
---|
| 20 | return (0); |
---|
| 21 | BDD_MARK(f)=mark; |
---|
| 22 | if (cmu_bdd_depends_on_step(bddm, BDD_THEN(f), var_index, mark)) |
---|
| 23 | return (1); |
---|
| 24 | return (cmu_bdd_depends_on_step(bddm, BDD_ELSE(f), var_index, mark)); |
---|
| 25 | } |
---|
| 26 | |
---|
| 27 | |
---|
| 28 | /* cmu_bdd_depends_on(bddm, f, var) returns 1 if f depends on var and */ |
---|
| 29 | /* returns 0 otherwise. */ |
---|
| 30 | |
---|
| 31 | int |
---|
| 32 | cmu_bdd_depends_on(cmu_bdd_manager bddm, bdd f, bdd var) |
---|
| 33 | { |
---|
| 34 | if (bdd_check_arguments(2, f, var)) |
---|
| 35 | { |
---|
| 36 | BDD_SETUP(var); |
---|
| 37 | if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR) |
---|
| 38 | { |
---|
| 39 | cmu_bdd_warning("cmu_bdd_depends_on: second argument is not a positive variable"); |
---|
| 40 | if (BDD_IS_CONST(var)) |
---|
| 41 | return (1); |
---|
| 42 | } |
---|
| 43 | (void)cmu_bdd_depends_on_step(bddm, f, BDD_INDEX(bddm, var), 1); |
---|
| 44 | return (cmu_bdd_depends_on_step(bddm, f, BDD_INDEX(bddm, var), 0)); |
---|
| 45 | } |
---|
| 46 | return (0); |
---|
| 47 | } |
---|
| 48 | |
---|
| 49 | |
---|
| 50 | static |
---|
| 51 | void |
---|
| 52 | bdd_unmark_nodes(cmu_bdd_manager bddm, bdd f) |
---|
| 53 | { |
---|
| 54 | bdd temp; |
---|
| 55 | |
---|
| 56 | BDD_SETUP(f); |
---|
| 57 | if (!BDD_MARK(f) || BDD_IS_CONST(f)) |
---|
| 58 | return; |
---|
| 59 | BDD_MARK(f)=0; |
---|
| 60 | temp=BDD_IF(bddm, f); |
---|
| 61 | { |
---|
| 62 | BDD_SETUP(temp); |
---|
| 63 | BDD_MARK(temp)=0; |
---|
| 64 | } |
---|
| 65 | bdd_unmark_nodes(bddm, BDD_THEN(f)); |
---|
| 66 | bdd_unmark_nodes(bddm, BDD_ELSE(f)); |
---|
| 67 | } |
---|
| 68 | |
---|
| 69 | |
---|
| 70 | static |
---|
| 71 | bdd * |
---|
| 72 | cmu_bdd_support_step(cmu_bdd_manager bddm, bdd f, bdd *support) |
---|
| 73 | { |
---|
| 74 | bdd temp; |
---|
| 75 | |
---|
| 76 | BDD_SETUP(f); |
---|
| 77 | if (BDD_MARK(f) || BDD_IS_CONST(f)) |
---|
| 78 | return (support); |
---|
| 79 | temp=BDD_IF(bddm, f); |
---|
| 80 | { |
---|
| 81 | BDD_SETUP(temp); |
---|
| 82 | if (!BDD_MARK(temp)) |
---|
| 83 | { |
---|
| 84 | BDD_MARK(temp)=1; |
---|
| 85 | *support=temp; |
---|
| 86 | ++support; |
---|
| 87 | } |
---|
| 88 | } |
---|
| 89 | BDD_MARK(f)=1; |
---|
| 90 | support=cmu_bdd_support_step(bddm, BDD_THEN(f), support); |
---|
| 91 | return (cmu_bdd_support_step(bddm, BDD_ELSE(f), support)); |
---|
| 92 | } |
---|
| 93 | |
---|
| 94 | |
---|
| 95 | /* cmu_bdd_support(bddm, f, support) returns the support of f as a */ |
---|
| 96 | /* null-terminated array of variables. */ |
---|
| 97 | |
---|
| 98 | void |
---|
| 99 | cmu_bdd_support(cmu_bdd_manager bddm, bdd f, bdd *support) |
---|
| 100 | { |
---|
| 101 | bdd *end; |
---|
| 102 | |
---|
| 103 | if (bdd_check_arguments(1, f)) |
---|
| 104 | { |
---|
| 105 | end=cmu_bdd_support_step(bddm, f, support); |
---|
| 106 | *end=0; |
---|
| 107 | bdd_unmark_nodes(bddm, f); |
---|
| 108 | } |
---|
| 109 | else |
---|
| 110 | *support=0; |
---|
| 111 | } |
---|