src/mdd/mdd_add.c File Reference
#include "mdd.h"
Include dependency graph for mdd_add.c:
Go to the source code of this file.
Functions | |
| EXTERN 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) |
| EXTERN void | one_var_and_carry_add_block (mdd_manager *mgr, mdd_t **A, mdd_t **B, bvar_type *bz_ptr, bvar_type *blv_ptr) |
| mdd_t * | mdd_add_s (mdd_manager *mgr, int sum_id, int mvar_id1, int mvar_id2) |
Function Documentation
| 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 | |||
| ) |
Definition at line 12 of file mdd_add.c.
00019 { 00020 mdd_t *zero; 00021 mdd_t *C, *D, *E, *F, 00022 *G, *H, *I; 00023 00024 zero = mdd_zero(mgr); 00025 00026 G = mdd_ite( by_ptr->node, zero , *A , 1, 1, 1 ); 00027 H = mdd_ite( by_ptr->node, *A , *B , 1, 1, 1 ); 00028 I = mdd_ite( by_ptr->node, *B , zero, 1, 1, 1 ); 00029 00030 C = mdd_ite( bx_ptr->node, zero, G , 1, 1, 1 ); 00031 D = mdd_ite( bx_ptr->node, G , H , 1, 1, 1 ); 00032 E = mdd_ite( bx_ptr->node, H , I , 1, 1, 1 ); 00033 F = mdd_ite( bx_ptr->node, I , zero, 1, 1, 1 ); 00034 00035 *A = mdd_ite( bz_ptr->node, D , C , 1, 1, 1 ); 00036 *B = mdd_ite( bz_ptr->node, F , E , 1, 1, 1 ); 00037 00038 mdd_free(G); 00039 mdd_free(H); 00040 mdd_free(I); 00041 mdd_free(C); 00042 mdd_free(D); 00043 mdd_free(E); 00044 mdd_free(F); 00045 mdd_free(zero); 00046 00047 return; 00048 }
| mdd_t* mdd_add_s | ( | mdd_manager * | mgr, | |
| int | sum_id, | |||
| int | mvar_id1, | |||
| int | mvar_id2 | |||
| ) |
Definition at line 82 of file mdd_add.c.
00087 { 00088 mdd_t *one, *zero; 00089 array_t *mvar_list = mdd_ret_mvar_list(mgr); 00090 array_t *bvar_list = mdd_ret_bvar_list(mgr); 00091 int config, 00092 no_common_to_all_bits, 00093 no_common_in_bits, i; 00094 00095 bvar_type bx, by, bz, z_carry, blv; 00096 mvar_type x, y, z, long_var; 00097 mdd_t *A, *B, *range_check; 00098 mdd_t *result = NIL(mdd_t); /* initialize for lint */ 00099 00100 00101 00102 x = array_fetch(mvar_type, mvar_list, mvar_id1); 00103 y = array_fetch(mvar_type, mvar_list, mvar_id2); 00104 z = array_fetch(mvar_type, mvar_list, sum_id); 00105 00106 /* Ensures that the i_th bit of x has smaller index 00107 than the i_th bit of y */ 00108 00109 if ( ( mdd_ret_bvar_id(&x,x.encode_length) ) > 00110 ( mdd_ret_bvar_id(&y,y.encode_length) ) ) { 00111 y = array_fetch(mvar_type, mvar_list, mvar_id1); 00112 x = array_fetch(mvar_type, mvar_list, mvar_id2); 00113 } 00114 00115 one = mdd_one(mgr); 00116 zero = mdd_zero(mgr); 00117 00118 no_common_in_bits = MIN(x.encode_length,y.encode_length); 00119 no_common_to_all_bits = MIN(no_common_in_bits, z.encode_length); 00120 00121 A = mdd_dup(one); 00122 B = mdd_dup(zero); 00123 00124 for (i = 1; i <= no_common_to_all_bits; i++){ 00125 00126 bx = mdd_ret_bvar(&x,x.encode_length-i,bvar_list); 00127 by = mdd_ret_bvar(&y,y.encode_length-i,bvar_list); 00128 bz = mdd_ret_bvar(&z,z.encode_length-i,bvar_list); 00129 addition_block_build( mgr, &A, &B, &bx, &by, &bz); 00130 } 00131 00132 00133 if ( z.encode_length > no_common_to_all_bits ){ 00134 if ( x.encode_length != y.encode_length ){ 00135 if ( x.encode_length == no_common_in_bits ){ 00136 long_var = y; 00137 /* short_var = x; */ 00138 } 00139 else { 00140 long_var = x; 00141 /* short_var = y; */ 00142 } 00143 00144 if ( z.encode_length > long_var.encode_length) { 00145 config = 1; 00146 } 00147 else 00148 { 00149 config = 2; 00150 } 00151 } 00152 else 00153 config = 3; 00154 } 00155 else 00156 config = 4; 00157 00158 00159 switch (config) { 00160 00161 case 1: /* z > long_var , short_var */ 00162 00163 for ( i = no_common_to_all_bits + 1; i <= long_var.encode_length; i++){ 00164 00165 z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list); 00166 blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list); 00167 00168 one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv); 00169 } 00170 00171 z_carry = mdd_ret_bvar(&z,z.encode_length - long_var.encode_length - 1, bvar_list); 00172 00173 A = mdd_ite( z_carry.node, B, A, 1, 1, 1); 00174 00175 for ( i = long_var.encode_length + 2; i <= z.encode_length; i++){ 00176 z_carry = mdd_ret_bvar(&z,z.encode_length-i, bvar_list); 00177 A = mdd_ite( z_carry.node, zero, A, 1, 1, 1); 00178 } 00179 result = mdd_dup(A); 00180 break; 00181 00182 case 2: /* short_var < z < long_var */ 00183 00184 for ( i = no_common_to_all_bits + 1; i <= z.encode_length; i++){ 00185 00186 z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list); 00187 blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list); 00188 00189 one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv); 00190 00191 } 00192 00193 result = mdd_or(A,B,1,1); 00194 break; 00195 00196 case 3: /* z> long_var = short_var */ 00197 00198 z_carry = mdd_ret_bvar(&z,z.encode_length - no_common_to_all_bits - 1,bvar_list); 00199 A = mdd_ite( z_carry.node, B, A, 1, 1, 1); 00200 00201 for ( i = no_common_to_all_bits + 2; i <= z.encode_length; i++){ 00202 z_carry = mdd_ret_bvar(&z, z.encode_length - i, bvar_list); 00203 A = mdd_ite( z_carry.node, zero, A, 1, 1, 1); 00204 } 00205 00206 result = mdd_dup(A); 00207 break; 00208 00209 case 4: /* z <= long_var, z <= short_var */ 00210 result = mdd_or(A,B,1,1); 00211 break; 00212 } 00213 00214 mdd_free(A); 00215 mdd_free(B); 00216 00217 00218 mdd_free(one); 00219 mdd_free(zero); 00220 00221 range_check = build_lt_c(mgr, sum_id, z.values); 00222 result = mdd_and(result, range_check, 1, 1); 00223 00224 mdd_free(range_check); 00225 00226 return result; 00227 }
| void one_var_and_carry_add_block | ( | mdd_manager * | mgr, | |
| mdd_t ** | A, | |||
| mdd_t ** | B, | |||
| bvar_type * | bz_ptr, | |||
| bvar_type * | blv_ptr | |||
| ) |
Definition at line 52 of file mdd_add.c.
00058 { 00059 mdd_t *C, *D, *E; 00060 mdd_t *zero; 00061 00062 zero = mdd_zero(mgr); 00063 00064 C = mdd_ite( blv_ptr->node, zero, *A, 1, 1, 1); 00065 D = mdd_ite( blv_ptr->node, *A, *B, 1, 1, 1); 00066 E = mdd_ite( blv_ptr->node, *B, zero, 1, 1, 1); 00067 00068 *A = mdd_ite( bz_ptr->node, D, C, 1, 1, 1); 00069 *B = mdd_ite( bz_ptr->node, zero, E, 1, 1, 1); 00070 00071 mdd_free(C); 00072 mdd_free(D); 00073 mdd_free(E); 00074 00075 mdd_free(zero); 00076 00077 return; 00078 }
