[13] | 1 | /* |
---|
| 2 | * $Id: mdd_ineq_s.c,v 1.4 2002/08/27 16:30:26 fabio Exp $ |
---|
| 3 | * |
---|
| 4 | */ |
---|
| 5 | |
---|
| 6 | #include "mdd.h" |
---|
| 7 | |
---|
| 8 | static int |
---|
| 9 | mdd_is_care_bit( |
---|
| 10 | mvar_type mvar, |
---|
| 11 | int index) |
---|
| 12 | { |
---|
| 13 | return ( getbit( ( (int) pow(2.0, (double)mvar.encode_length) ) - mvar.values, mvar.encode_length-index-1)); |
---|
| 14 | } |
---|
| 15 | |
---|
| 16 | |
---|
| 17 | mdd_t * |
---|
| 18 | mdd_ineq_template_s( |
---|
| 19 | mdd_manager *mgr, |
---|
| 20 | int mvar1, |
---|
| 21 | int mvar2, |
---|
| 22 | int zero_then_val /* J in Tim's thesis */, |
---|
| 23 | int one_else_val /* K */, |
---|
| 24 | int bottom_val /* A and B */) |
---|
| 25 | { |
---|
| 26 | mvar_type x, y; |
---|
| 27 | bvar_type bx, by; |
---|
| 28 | mdd_t *one_top, *zero_top, *zero_then, *one_else, |
---|
| 29 | *one_top_else = mdd_one(mgr); |
---|
| 30 | mdd_t *one_top_then = mdd_one(mgr); |
---|
| 31 | mdd_t *zero_top_else = mdd_one(mgr); |
---|
| 32 | mdd_t *zero_top_then = mdd_one(mgr); |
---|
| 33 | mdd_t *compare; |
---|
| 34 | int i; |
---|
| 35 | |
---|
| 36 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 37 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 38 | |
---|
| 39 | if (zero_then_val == 0) |
---|
| 40 | zero_then = mdd_zero(mgr); |
---|
| 41 | else |
---|
| 42 | zero_then = mdd_one(mgr); |
---|
| 43 | |
---|
| 44 | |
---|
| 45 | if (one_else_val == 0) |
---|
| 46 | one_else = mdd_zero(mgr); |
---|
| 47 | else |
---|
| 48 | one_else = mdd_one(mgr); |
---|
| 49 | |
---|
| 50 | if (bottom_val == 0) { |
---|
| 51 | one_top = mdd_zero(mgr); |
---|
| 52 | zero_top = mdd_zero(mgr); |
---|
| 53 | } |
---|
| 54 | else { |
---|
| 55 | one_top = mdd_one(mgr); |
---|
| 56 | zero_top = mdd_one(mgr); |
---|
| 57 | } |
---|
| 58 | |
---|
| 59 | |
---|
| 60 | x = array_fetch(mvar_type, mvar_list, mvar1); |
---|
| 61 | y = array_fetch(mvar_type, mvar_list, mvar2); |
---|
| 62 | |
---|
| 63 | if (x.values != y.values) |
---|
| 64 | fail("mdd_ineq: 2 mvars have incompatible value ranges\n"); |
---|
| 65 | |
---|
| 66 | if (x.status == MDD_BUNDLED) { |
---|
| 67 | (void) fprintf(stderr, |
---|
| 68 | "\nWarning: mdd_ineq, bundled variable %s is used\n", x.name); |
---|
| 69 | fail(""); |
---|
| 70 | } |
---|
| 71 | |
---|
| 72 | if (y.status == MDD_BUNDLED) { |
---|
| 73 | (void) fprintf(stderr, |
---|
| 74 | "\nWarning: mdd_ineq, bundled variable %s is used\n", y.name); |
---|
| 75 | fail(""); |
---|
| 76 | } |
---|
| 77 | |
---|
| 78 | |
---|
| 79 | for (i=(x.encode_length-1); i>=0; i--) { |
---|
| 80 | |
---|
| 81 | bx = mdd_ret_bvar(&x, i, bvar_list); |
---|
| 82 | by = mdd_ret_bvar(&y, i, bvar_list); |
---|
| 83 | |
---|
| 84 | mdd_free(zero_top_else); |
---|
| 85 | zero_top_else = mdd_ite(by.node, zero_then, zero_top, 1, 1, 1); |
---|
| 86 | mdd_free(zero_top_then); |
---|
| 87 | zero_top_then = mdd_ite(by.node, zero_top, one_else, 1, 1, 1); |
---|
| 88 | |
---|
| 89 | if (mdd_is_care_bit(x,i) == 0) { |
---|
| 90 | |
---|
| 91 | mdd_free(one_top_else); |
---|
| 92 | one_top_else = mdd_ite(by.node, zero_then, zero_top, 1, 1, 1); |
---|
| 93 | mdd_free(one_top_then); |
---|
| 94 | one_top_then = mdd_ite(by.node, one_top, one_else, 1, 1, 1); |
---|
| 95 | |
---|
| 96 | mdd_free(one_top); |
---|
| 97 | |
---|
| 98 | one_top = mdd_ite(bx.node, one_top_then, one_top_else, 1, 1, 1); |
---|
| 99 | } |
---|
| 100 | |
---|
| 101 | mdd_free(zero_top); |
---|
| 102 | zero_top = mdd_ite(bx.node, zero_top_then, zero_top_else, 1, 1, 1); |
---|
| 103 | |
---|
| 104 | } |
---|
| 105 | |
---|
| 106 | mdd_free(zero_then); |
---|
| 107 | mdd_free(one_else); |
---|
| 108 | |
---|
| 109 | mdd_free(zero_top_else); |
---|
| 110 | mdd_free(zero_top_then); |
---|
| 111 | mdd_free(one_top_else); |
---|
| 112 | mdd_free(one_top_then); |
---|
| 113 | |
---|
| 114 | mdd_free(zero_top); |
---|
| 115 | |
---|
| 116 | compare = mdd_eq(mgr, mvar1, mvar2); |
---|
| 117 | |
---|
| 118 | if ( ( bdd_equal(compare, one_top) == 0) && (zero_then_val == 0) && (one_else_val == 0) && (bottom_val == 1) ) |
---|
| 119 | printf("Error \n"); |
---|
| 120 | |
---|
| 121 | mdd_free(compare); |
---|
| 122 | |
---|
| 123 | return one_top; |
---|
| 124 | } |
---|
| 125 | |
---|
| 126 | /*---------------------------------------------------------------------------*/ |
---|
| 127 | /* Static function prototypes */ |
---|
| 128 | /*---------------------------------------------------------------------------*/ |
---|
| 129 | |
---|
| 130 | |
---|