src/mdd/mdd_add.c

Go to the documentation of this file.

#include "mdd.h"

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

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);


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)
{
        mdd_t *zero;
        mdd_t   *C, *D, *E, *F,
                *G, *H, *I;

        zero = mdd_zero(mgr);   
                
        G = mdd_ite( by_ptr->node, zero , *A  ,  1, 1, 1 );
        H = mdd_ite( by_ptr->node, *A   , *B  ,  1, 1, 1 );
        I = mdd_ite( by_ptr->node, *B   , zero,  1, 1, 1 );

        C = mdd_ite( bx_ptr->node, zero, G   ,  1, 1, 1 );
        D = mdd_ite( bx_ptr->node, G   , H   ,  1, 1, 1 );
        E = mdd_ite( bx_ptr->node, H   , I   ,  1, 1, 1 );
        F = mdd_ite( bx_ptr->node, I   , zero,  1, 1, 1 );
                
        *A = mdd_ite( bz_ptr->node, D   , C   ,  1, 1, 1 );
        *B = mdd_ite( bz_ptr->node, F   , E   ,  1, 1, 1 );

        mdd_free(G);
        mdd_free(H);
        mdd_free(I);
        mdd_free(C);
        mdd_free(D);
        mdd_free(E);
        mdd_free(F);
        mdd_free(zero);

        return;
}


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 *C, *D, *E;
        mdd_t *zero;

        zero = mdd_zero(mgr);   

        C = mdd_ite( blv_ptr->node,  zero,   *A, 1, 1, 1);
        D = mdd_ite( blv_ptr->node,    *A,   *B, 1, 1, 1);
        E = mdd_ite( blv_ptr->node,    *B, zero, 1, 1, 1);

        *A = mdd_ite( bz_ptr->node,    D, C, 1, 1, 1);
        *B = mdd_ite( bz_ptr->node, zero, E, 1, 1, 1);

        mdd_free(C);
        mdd_free(D);
        mdd_free(E);

        mdd_free(zero);

        return;
}

/* in1 + in2 = sum */
mdd_t *
mdd_add_s(
  mdd_manager *mgr,
  int sum_id,
  int mvar_id1,
  int mvar_id2)
{
        mdd_t *one, *zero;
        array_t *mvar_list = mdd_ret_mvar_list(mgr);
        array_t *bvar_list = mdd_ret_bvar_list(mgr);
        int     config, 
                no_common_to_all_bits, 
                no_common_in_bits, i;

        bvar_type bx, by, bz, z_carry, blv;
        mvar_type x, y, z, long_var;
        mdd_t   *A, *B, *range_check;
        mdd_t *result = NIL(mdd_t); /* initialize for lint */
        

        
        x = array_fetch(mvar_type, mvar_list, mvar_id1);
        y = array_fetch(mvar_type, mvar_list, mvar_id2);
        z = array_fetch(mvar_type, mvar_list, sum_id);

        /* Ensures that the i_th bit of x has smaller index
           than the i_th bit of y */

        if  ( ( mdd_ret_bvar_id(&x,x.encode_length) ) >
              ( mdd_ret_bvar_id(&y,y.encode_length) )  )  {
                        y = array_fetch(mvar_type, mvar_list, mvar_id1);
                        x = array_fetch(mvar_type, mvar_list, mvar_id2);
                        }

        one = mdd_one(mgr);
        zero = mdd_zero(mgr);   
        
        no_common_in_bits = MIN(x.encode_length,y.encode_length);
        no_common_to_all_bits = MIN(no_common_in_bits, z.encode_length);

        A = mdd_dup(one);
        B = mdd_dup(zero);

        for (i = 1; i <= no_common_to_all_bits; i++){

                bx = mdd_ret_bvar(&x,x.encode_length-i,bvar_list); 
                by = mdd_ret_bvar(&y,y.encode_length-i,bvar_list);
                bz = mdd_ret_bvar(&z,z.encode_length-i,bvar_list);
                addition_block_build( mgr, &A, &B, &bx, &by, &bz);
        }


        if ( z.encode_length > no_common_to_all_bits ){
                if ( x.encode_length != y.encode_length ){
                        if ( x.encode_length == no_common_in_bits ){ 
                                long_var = y;   
                                /* short_var = x; */
                        }
                        else { 
                                long_var = x;   
                                /* short_var = y; */
                        }
                
                        if ( z.encode_length > long_var.encode_length) {
                        config = 1;      
                        }
                        else
                        {
                        config = 2;             
                        }
                }
                else 
                        config = 3;                     
        }
        else 
                config = 4;                     


        switch (config) {
                
                case 1: /* z > long_var , short_var */

                        for ( i = no_common_to_all_bits + 1; i <= long_var.encode_length; i++){

                                z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list);
                                blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list);

                                one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv);
                        }
                        
                        z_carry = mdd_ret_bvar(&z,z.encode_length - long_var.encode_length - 1, bvar_list);

                        A = mdd_ite( z_carry.node, B, A, 1, 1, 1);

                        for ( i = long_var.encode_length + 2; i <= z.encode_length; i++){
                                z_carry = mdd_ret_bvar(&z,z.encode_length-i, bvar_list);
                                A = mdd_ite( z_carry.node, zero, A, 1, 1, 1);                           
                        }
                        result = mdd_dup(A);
                        break;

                case 2: /* short_var < z < long_var */

                        for ( i = no_common_to_all_bits + 1; i <= z.encode_length; i++){

                                z_carry = mdd_ret_bvar(&z,z.encode_length-i,bvar_list);
                                blv = mdd_ret_bvar(&long_var,long_var.encode_length-i,bvar_list);

                                one_var_and_carry_add_block(mgr, &A, &B, &bz, &blv);

                        }

                        result = mdd_or(A,B,1,1);
                        break;

                case 3: /* z> long_var = short_var */ 

                        z_carry = mdd_ret_bvar(&z,z.encode_length - no_common_to_all_bits - 1,bvar_list);
                        A = mdd_ite( z_carry.node, B, A, 1, 1, 1);

                        for ( i = no_common_to_all_bits + 2; i <= z.encode_length; i++){
                                z_carry = mdd_ret_bvar(&z, z.encode_length - i, bvar_list);
                                A = mdd_ite( z_carry.node, zero, A, 1, 1, 1);
                        }       

                        result = mdd_dup(A);
                        break;

                case 4: /* z <= long_var, z <= short_var */
                        result = mdd_or(A,B,1,1);
                        break;
        }
        
        mdd_free(A);
        mdd_free(B);


        mdd_free(one);
        mdd_free(zero);
        
        range_check = build_lt_c(mgr, sum_id, z.values);
        result = mdd_and(result, range_check, 1, 1);

        mdd_free(range_check);

        return result;
}

---