src/mdd/mdd_cofactor.c File Reference

#include "mdd.h"

Include dependency graph for mdd_cofactor.c:

Go to the source code of this file.

Functions
static void	mdd_traverse (mdd_manager *mgr, bdd_t *top, boolean *mvar_present)
static array_t *	mvars_extract (mdd_manager *mgr, mdd_t *fn)
mdd_t *	mdd_cofactor (mdd_manager *mgr, mdd_t *fn, mdd_t *cube)

---

Function Documentation

mdd_t* mdd_cofactor	(	mdd_manager *	mgr,
		mdd_t *	fn,
		mdd_t *	cube
	)

Definition at line 32 of file mdd_cofactor.c.

{
    array_t *mvars;
    mdd_t *top;

    mvars = mvars_extract(mgr, cube);
    top = mdd_and_smooth(mgr, fn, cube, mvars);
    array_free(mvars);
    return top;
}

static void mdd_traverse	(	mdd_manager *	mgr,
		bdd_t *	top,
		boolean *	mvar_present
	)			[static]

Definition at line 51 of file mdd_cofactor.c.

{
    bvar_type bv;
    array_t *bvar_list = mdd_ret_bvar_list(mgr);
    int is_complemented;
    bdd_t *uncomp_top, *child, *temp_child;

    if (bdd_is_tautology(top,1)) {
        return;
    }
    if (bdd_is_tautology(top,0)) {
        return;
    }

    (void)bdd_get_node(top,&is_complemented);

    bv = array_fetch(bvar_type, bvar_list, bdd_top_var_id(top));
    mvar_present[bv.mvar_id] = 1;

    if (is_complemented) uncomp_top = bdd_not(top);
    else uncomp_top = mdd_dup(top);

    child = bdd_then(uncomp_top);
    (void) bdd_get_node(child,&is_complemented);
    if (is_complemented) {
        temp_child = child;
        child = bdd_not(temp_child);
        mdd_free(temp_child);
    }
    
    mdd_traverse(mgr, child , mvar_present);
    mdd_free(child);

    child = bdd_else(uncomp_top);
    (void) bdd_get_node(child,&is_complemented);
    if (is_complemented) {
        temp_child = child;
        child = bdd_not(temp_child);
        mdd_free(temp_child);
    }

    mdd_traverse(mgr, child, mvar_present);
    
 
    mdd_free(child);
    mdd_free(uncomp_top);
    return;    
}

static array_t * mvars_extract	(	mdd_manager *	mgr,
		mdd_t *	fn
	)			[static]

Definition at line 105 of file mdd_cofactor.c.

{
    int i, no_mvar;
    boolean *mvar_present;
    array_t *mvar_list = mdd_ret_mvar_list(mgr);
    array_t *mvars;
                                                                          

    mvars = array_alloc(int, 0);
    no_mvar = array_n(mvar_list);
    mvar_present = ALLOC(boolean, no_mvar);
    for (i=0; i<no_mvar; i++) mvar_present[i] = 0;
    mdd_traverse(mgr, fn, mvar_present);
    for (i=0; i<no_mvar; i++) 
        if (mvar_present[i] == 1) array_insert_last(int, mvars, i);
    FREE(mvar_present);
    return mvars;
}