source: vis_dev/glu-2.3/src/mdd/mdd_add.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 5.3 KB
Line 
1#include "mdd.h"
2
3/*---------------------------------------------------------------------------*/
4/* Static function prototypes                                                */
5/*---------------------------------------------------------------------------*/
6
7EXTERN void addition_block_build(mdd_manager *mgr, mdd_t **A, mdd_t **B, bvar_type *bx_ptr, bvar_type *by_ptr, bvar_type *bz_ptr);
8EXTERN void one_var_and_carry_add_block(mdd_manager *mgr, mdd_t **A, mdd_t **B, bvar_type *bz_ptr, bvar_type *blv_ptr);
9
10
11void
12addition_block_build(
13  mdd_manager *mgr,
14  mdd_t **A,
15  mdd_t **B,
16  bvar_type *bx_ptr,
17  bvar_type *by_ptr,
18  bvar_type *bz_ptr)
19{
20        mdd_t *zero;
21        mdd_t   *C, *D, *E, *F,
22                *G, *H, *I;
23
24        zero = mdd_zero(mgr);   
25               
26        G = mdd_ite( by_ptr->node, zero , *A  ,  1, 1, 1 );
27        H = mdd_ite( by_ptr->node, *A   , *B  ,  1, 1, 1 );
28        I = mdd_ite( by_ptr->node, *B   , zero,  1, 1, 1 );
29
30        C = mdd_ite( bx_ptr->node, zero, G   ,  1, 1, 1 );
31        D = mdd_ite( bx_ptr->node, G   , H   ,  1, 1, 1 );
32        E = mdd_ite( bx_ptr->node, H   , I   ,  1, 1, 1 );
33        F = mdd_ite( bx_ptr->node, I   , zero,  1, 1, 1 );
34               
35        *A = mdd_ite( bz_ptr->node, D   , C   ,  1, 1, 1 );
36        *B = mdd_ite( bz_ptr->node, F   , E   ,  1, 1, 1 );
37
38        mdd_free(G);
39        mdd_free(H);
40        mdd_free(I);
41        mdd_free(C);
42        mdd_free(D);
43        mdd_free(E);
44        mdd_free(F);
45        mdd_free(zero);
46
47        return;
48}
49
50
51void
52one_var_and_carry_add_block(
53  mdd_manager *mgr,
54  mdd_t **A,
55  mdd_t **B,
56  bvar_type *bz_ptr,
57  bvar_type *blv_ptr)
58{
59        mdd_t *C, *D, *E;
60        mdd_t *zero;
61
62        zero = mdd_zero(mgr);   
63
64        C = mdd_ite( blv_ptr->node,  zero,   *A, 1, 1, 1);
65        D = mdd_ite( blv_ptr->node,    *A,   *B, 1, 1, 1);
66        E = mdd_ite( blv_ptr->node,    *B, zero, 1, 1, 1);
67
68        *A = mdd_ite( bz_ptr->node,    D, C, 1, 1, 1);
69        *B = mdd_ite( bz_ptr->node, zero, E, 1, 1, 1);
70
71        mdd_free(C);
72        mdd_free(D);
73        mdd_free(E);
74
75        mdd_free(zero);
76
77        return;
78}
79
80/* in1 + in2 = sum */
81mdd_t *
82mdd_add_s(
83  mdd_manager *mgr,
84  int sum_id,
85  int mvar_id1,
86  int mvar_id2)
87{
88        mdd_t *one, *zero;
89        array_t *mvar_list = mdd_ret_mvar_list(mgr);
90        array_t *bvar_list = mdd_ret_bvar_list(mgr);
91        int     config, 
92                no_common_to_all_bits, 
93                no_common_in_bits, i;
94
95        bvar_type bx, by, bz, z_carry, blv;
96        mvar_type x, y, z, long_var;
97        mdd_t   *A, *B, *range_check;
98        mdd_t *result = NIL(mdd_t); /* initialize for lint */
99       
100
101       
102        x = array_fetch(mvar_type, mvar_list, mvar_id1);
103        y = array_fetch(mvar_type, mvar_list, mvar_id2);
104        z = array_fetch(mvar_type, mvar_list, sum_id);
105
106        /* Ensures that the i_th bit of x has smaller index
107           than the i_th bit of y */
108
109        if  ( ( mdd_ret_bvar_id(&x,x.encode_length) ) >
110              ( mdd_ret_bvar_id(&y,y.encode_length) )  )  {
111                        y = array_fetch(mvar_type, mvar_list, mvar_id1);
112                        x = array_fetch(mvar_type, mvar_list, mvar_id2);
113                        }
114
115        one = mdd_one(mgr);
116        zero = mdd_zero(mgr);   
117       
118        no_common_in_bits = MIN(x.encode_length,y.encode_length);
119        no_common_to_all_bits = MIN(no_common_in_bits, z.encode_length);
120
121        A = mdd_dup(one);
122        B = mdd_dup(zero);
123
124        for (i = 1; i <= no_common_to_all_bits; i++){
125
126                bx = mdd_ret_bvar(&x,x.encode_length-i,bvar_list); 
127                by = mdd_ret_bvar(&y,y.encode_length-i,bvar_list);
128                bz = mdd_ret_bvar(&z,z.encode_length-i,bvar_list);
129                addition_block_build( mgr, &A, &B, &bx, &by, &bz);
130        }
131
132
133        if ( z.encode_length > no_common_to_all_bits ){
134                if ( x.encode_length != y.encode_length ){
135                        if ( x.encode_length == no_common_in_bits ){ 
136                                long_var = y;   
137                                /* short_var = x; */
138                        }
139                        else { 
140                                long_var = x;   
141                                /* short_var = y; */
142                        }
143               
144                        if ( z.encode_length > long_var.encode_length) {
145                        config = 1;     
146                        }
147                        else
148                        {
149                        config = 2;             
150                        }
151                }
152                else 
153                        config = 3;                     
154        }
155        else 
156                config = 4;                     
157
158
159        switch (config) {
160               
161                case 1: /* z > long_var , short_var */
162
163                        for ( i = no_common_to_all_bits + 1; i <= long_var.encode_length; i++){
164
165                                z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list);
166                                blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list);
167
168                                one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv);
169                        }
170                       
171                        z_carry = mdd_ret_bvar(&z,z.encode_length - long_var.encode_length - 1, bvar_list);
172
173                        A = mdd_ite( z_carry.node, B, A, 1, 1, 1);
174
175                        for ( i = long_var.encode_length + 2; i <= z.encode_length; i++){
176                                z_carry = mdd_ret_bvar(&z,z.encode_length-i, bvar_list);
177                                A = mdd_ite( z_carry.node, zero, A, 1, 1, 1);                           
178                        }
179                        result = mdd_dup(A);
180                        break;
181
182                case 2: /* short_var < z < long_var */
183
184                        for ( i = no_common_to_all_bits + 1; i <= z.encode_length; i++){
185
186                                z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list);
187                                blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list);
188
189                                one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv);
190
191                        }
192
193                        result = mdd_or(A,B,1,1);
194                        break;
195
196                case 3: /* z> long_var = short_var */ 
197
198                        z_carry = mdd_ret_bvar(&z,z.encode_length - no_common_to_all_bits - 1,bvar_list);
199                        A = mdd_ite( z_carry.node, B, A, 1, 1, 1);
200
201                        for ( i = no_common_to_all_bits + 2; i <= z.encode_length; i++){
202                                z_carry = mdd_ret_bvar(&z, z.encode_length - i, bvar_list);
203                                A = mdd_ite( z_carry.node, zero, A, 1, 1, 1);
204                        }       
205
206                        result = mdd_dup(A);
207                        break;
208
209                case 4: /* z <= long_var, z <= short_var */
210                        result = mdd_or(A,B,1,1);
211                        break;
212        }
213       
214        mdd_free(A);
215        mdd_free(B);
216
217
218        mdd_free(one);
219        mdd_free(zero);
220       
221        range_check = build_lt_c(mgr, sum_id, z.values);
222        result = mdd_and(result, range_check, 1, 1);
223
224        mdd_free(range_check);
225
226        return result;
227}
228
229
Note: See TracBrowser for help on using the repository browser.