[13] | 1 | /* |
---|
| 2 | * $Id: mdd_mod.c,v 1.5 2002/08/27 16:30:26 fabio Exp $ |
---|
| 3 | * |
---|
| 4 | */ |
---|
| 5 | |
---|
| 6 | #include "mdd.h" |
---|
| 7 | |
---|
| 8 | static void mod_block_build (mdd_t ****, int, bvar_type *, bvar_type *); |
---|
| 9 | static void assert_zero (mdd_manager *, mdd_t **, bvar_type *); |
---|
| 10 | static void single_var_block_build (mdd_t ****, bvar_type *, int); |
---|
| 11 | |
---|
| 12 | int |
---|
| 13 | getbit(int number, int position) |
---|
| 14 | { |
---|
| 15 | return ( (number >> position) & 1); |
---|
| 16 | } |
---|
| 17 | |
---|
| 18 | static void |
---|
| 19 | assert_zero( |
---|
| 20 | mdd_manager *mgr, |
---|
| 21 | mdd_t **PINS_00_ptr, |
---|
| 22 | bvar_type *a_bit_i_ptr) |
---|
| 23 | { |
---|
| 24 | mdd_t *zero; |
---|
| 25 | |
---|
| 26 | zero = mdd_zero(mgr); |
---|
| 27 | |
---|
| 28 | (*PINS_00_ptr) = mdd_ite( a_bit_i_ptr->node, zero, (*PINS_00_ptr) , 1, 1, 1); |
---|
| 29 | |
---|
| 30 | mdd_free(zero); |
---|
| 31 | |
---|
| 32 | return; |
---|
| 33 | } |
---|
| 34 | |
---|
| 35 | static void |
---|
| 36 | single_var_block_build( |
---|
| 37 | mdd_t ****PINS_ptr, |
---|
| 38 | bvar_type *b_bit_i_ptr, |
---|
| 39 | int M) |
---|
| 40 | { |
---|
| 41 | int i; |
---|
| 42 | |
---|
| 43 | for (i=0; i < M; i++) |
---|
| 44 | (*PINS_ptr)[0][i] = mdd_ite( b_bit_i_ptr->node, (*PINS_ptr)[0][(2*i+1)%M], (*PINS_ptr)[0][(2*i)%M], 1, 1, 1); |
---|
| 45 | |
---|
| 46 | } |
---|
| 47 | |
---|
| 48 | /* a = b (mod M) */ |
---|
| 49 | static void |
---|
| 50 | mod_block_build( |
---|
| 51 | mdd_t ****PINS_ptr, |
---|
| 52 | int M /* modulus */, |
---|
| 53 | bvar_type *a_bit_i_ptr, |
---|
| 54 | bvar_type *b_bit_i_ptr) |
---|
| 55 | { |
---|
| 56 | int i, j; |
---|
| 57 | mdd_t *THEN, *ELSE; |
---|
| 58 | |
---|
| 59 | for(i=0; i<M; i++) |
---|
| 60 | for (j=0; j<M; j++){ |
---|
| 61 | THEN = mdd_ite(b_bit_i_ptr->node, (*PINS_ptr)[(2*i+1)%M][(2*j+1)%M], |
---|
| 62 | (*PINS_ptr)[(2*i+1)%M][(2*j)%M], 1, 1, 1); |
---|
| 63 | |
---|
| 64 | ELSE = mdd_ite(b_bit_i_ptr->node, (*PINS_ptr)[(2*i)%M][(2*j+1)%M], |
---|
| 65 | (*PINS_ptr)[(2*i)%M][(2*j)%M], 1, 1, 1); |
---|
| 66 | |
---|
| 67 | (*PINS_ptr)[i][j] = mdd_ite(a_bit_i_ptr->node, THEN, ELSE, 1, 1, 1); |
---|
| 68 | } |
---|
| 69 | } |
---|
| 70 | |
---|
| 71 | /* a = b (mod M) */ |
---|
| 72 | mdd_t * |
---|
| 73 | mdd_mod( |
---|
| 74 | mdd_manager *mgr, |
---|
| 75 | int a_mvar_id, |
---|
| 76 | int b_mvar_id, |
---|
| 77 | int M /* Modulus */ ) |
---|
| 78 | { |
---|
| 79 | mdd_t ***PINS; /* Two dimensional array of mdd_t*'s used in forming the mdd */ |
---|
| 80 | int i, j; |
---|
| 81 | mvar_type a, b; |
---|
| 82 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 83 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 84 | bvar_type a_bit_i, b_bit_i; |
---|
| 85 | mdd_t *result, *less_than; |
---|
| 86 | |
---|
| 87 | a = array_fetch ( mvar_type, mvar_list, a_mvar_id); |
---|
| 88 | b = array_fetch ( mvar_type, mvar_list, b_mvar_id); |
---|
| 89 | |
---|
| 90 | /* Allocate two dimensional array PINS[0..M-1][0..M-1] of mdd_t *'s */ |
---|
| 91 | PINS = ALLOC(mdd_t **, M); |
---|
| 92 | for(i=0; i<M; i++) PINS[i] = ALLOC(mdd_t *, M); |
---|
| 93 | |
---|
| 94 | for(i=0; i< M; i++) |
---|
| 95 | for(j=0; j< M; j++) PINS[i][j] = mdd_zero(mgr); |
---|
| 96 | |
---|
| 97 | for(i=0; i< M; i++) PINS[i][i] = mdd_one(mgr); |
---|
| 98 | |
---|
| 99 | for( i = 1 ; i <= (MIN(a.encode_length, b.encode_length)); i++){ |
---|
| 100 | a_bit_i = mdd_ret_bvar( &a, (a.encode_length - i), bvar_list); |
---|
| 101 | b_bit_i = mdd_ret_bvar( &b, (b.encode_length - i), bvar_list); |
---|
| 102 | |
---|
| 103 | mod_block_build(&PINS, M, &a_bit_i, &b_bit_i); |
---|
| 104 | } |
---|
| 105 | |
---|
| 106 | if ( a.encode_length > b.encode_length ) |
---|
| 107 | for ( i = MIN(a.encode_length, b.encode_length)+1; i <= a.encode_length; i++){ |
---|
| 108 | a_bit_i = mdd_ret_bvar( &a, (a.encode_length - i), bvar_list); |
---|
| 109 | assert_zero( mgr, &(PINS[0][0]), &a_bit_i); |
---|
| 110 | } |
---|
| 111 | |
---|
| 112 | if ( b.encode_length > a.encode_length ) |
---|
| 113 | for ( i = MIN(a.encode_length, b.encode_length)+1; i <= b.encode_length; i++){ |
---|
| 114 | b_bit_i = mdd_ret_bvar( &b, (b.encode_length - i), bvar_list); |
---|
| 115 | single_var_block_build( &PINS, &b_bit_i, M); |
---|
| 116 | } |
---|
| 117 | |
---|
| 118 | less_than = build_lt_c(mgr, a_mvar_id, M); |
---|
| 119 | |
---|
| 120 | result = mdd_and(PINS[0][0], less_than, 1, 1); |
---|
| 121 | |
---|
| 122 | return result; |
---|
| 123 | |
---|
| 124 | |
---|
| 125 | } |
---|
| 126 | |
---|
| 127 | /*---------------------------------------------------------------------------*/ |
---|
| 128 | /* Static function prototypes */ |
---|
| 129 | /*---------------------------------------------------------------------------*/ |
---|
| 130 | |
---|