src/mdd/mdd_mod.c File Reference

#include "mdd.h"

Include dependency graph for mdd_mod.c:

Go to the source code of this file.

Functions
static void	mod_block_build (mdd_t ****, int, bvar_type *, bvar_type *)
static void	assert_zero (mdd_manager *, mdd_t **, bvar_type *)
static void	single_var_block_build (mdd_t ****, bvar_type *, int)
int	getbit (int number, int position)
mdd_t *	mdd_mod (mdd_manager *mgr, int a_mvar_id, int b_mvar_id, int M)

---

Function Documentation

static void assert_zero	(	mdd_manager *	mgr,
		mdd_t **	PINS_00_ptr,
		bvar_type *	a_bit_i_ptr
	)			[static]

Definition at line 19 of file mdd_mod.c.

{
        mdd_t *zero;

        zero = mdd_zero(mgr);

        (*PINS_00_ptr) = mdd_ite( a_bit_i_ptr->node,  zero, (*PINS_00_ptr) , 1, 1, 1);          

        mdd_free(zero);

        return;
}

int getbit	(	int	number,
		int	position
	)

Definition at line 13 of file mdd_mod.c.

{
return ( (number >> position) & 1);
}

mdd_t* mdd_mod	(	mdd_manager *	mgr,
		int	a_mvar_id,
		int	b_mvar_id,
		int	M
	)

Definition at line 73 of file mdd_mod.c.

{
        mdd_t ***PINS;          /* Two dimensional array of mdd_t*'s used in forming the mdd */
        int i, j;
        mvar_type a, b;
        array_t *mvar_list = mdd_ret_mvar_list(mgr);
        array_t *bvar_list = mdd_ret_bvar_list(mgr);
        bvar_type a_bit_i, b_bit_i;
        mdd_t *result, *less_than;

        a = array_fetch ( mvar_type, mvar_list, a_mvar_id);
        b = array_fetch ( mvar_type, mvar_list, b_mvar_id);

        /* Allocate two dimensional array PINS[0..M-1][0..M-1] of mdd_t *'s */
        PINS = ALLOC(mdd_t **, M);              
        for(i=0; i<M; i++) PINS[i] = ALLOC(mdd_t *, M);
        
        for(i=0; i< M; i++) 
                for(j=0; j< M; j++) PINS[i][j] = mdd_zero(mgr);

        for(i=0; i< M; i++) PINS[i][i] = mdd_one(mgr);

        for( i = 1 ; i <= (MIN(a.encode_length, b.encode_length)); i++){ 
                a_bit_i = mdd_ret_bvar( &a, (a.encode_length - i), bvar_list);
                b_bit_i = mdd_ret_bvar( &b, (b.encode_length - i), bvar_list);

                mod_block_build(&PINS, M,  &a_bit_i, &b_bit_i);  
        }

        if ( a.encode_length > b.encode_length ) 
                for ( i = MIN(a.encode_length, b.encode_length)+1; i <= a.encode_length; i++){
                        a_bit_i = mdd_ret_bvar( &a, (a.encode_length - i), bvar_list);
                        assert_zero( mgr, &(PINS[0][0]), &a_bit_i);
                }

        if ( b.encode_length > a.encode_length )
                for ( i = MIN(a.encode_length, b.encode_length)+1; i <= b.encode_length; i++){
                        b_bit_i = mdd_ret_bvar( &b, (b.encode_length - i), bvar_list);
                        single_var_block_build( &PINS, &b_bit_i, M);
                }

        less_than = build_lt_c(mgr, a_mvar_id, M);

        result = mdd_and(PINS[0][0], less_than, 1, 1);
                
        return result;  


}

static void mod_block_build	(	mdd_t ****	PINS_ptr,
		int	M,
		bvar_type *	a_bit_i_ptr,
		bvar_type *	b_bit_i_ptr
	)			[static]

Definition at line 50 of file mdd_mod.c.

{
        int i, j;
        mdd_t *THEN, *ELSE;

        for(i=0; i<M; i++)
                for (j=0; j<M; j++){
                        THEN = mdd_ite(b_bit_i_ptr->node, (*PINS_ptr)[(2*i+1)%M][(2*j+1)%M], 
                                                           (*PINS_ptr)[(2*i+1)%M][(2*j)%M],   1, 1, 1);
                        
                        ELSE = mdd_ite(b_bit_i_ptr->node, (*PINS_ptr)[(2*i)%M][(2*j+1)%M], 
                                                           (*PINS_ptr)[(2*i)%M][(2*j)%M],     1, 1, 1);
                
                        (*PINS_ptr)[i][j] = mdd_ite(a_bit_i_ptr->node, THEN, ELSE, 1, 1, 1);
                }                       
}

static void single_var_block_build	(	mdd_t ****	PINS_ptr,
		bvar_type *	b_bit_i_ptr,
		int	M
	)			[static]

Definition at line 36 of file mdd_mod.c.

{
        int i;

        for (i=0; i < M; i++)
                (*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);

}