src/mark/markGetScc.c

Go to the documentation of this file.

#include "markInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


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

static bdd_node * pickOneCube(bdd_manager *manager, bdd_node *node, bdd_node **xVars, int nVars);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

bdd_node *
MarkGetSCC(
  bdd_manager *manager,
  bdd_node *tr,
  bdd_node *tc,
  bdd_node *reached,
  bdd_node **xVars,
  bdd_node **yVars,
  int nVars,
  st_table **scc_table)

{
    bdd_node *zero = bdd_read_logic_zero(manager);
    bdd_node *cr,               /* Cycle relation */
        *ee,            /* Exterior edges relation, edges between SCCs */
        *nofanout,      /* Nodes without fanout outside the SCC */
        *nocycle,       /* Nodes that are not in any cycle */
        *tnofanout,     /* Temporary nodes without fanout when
                         * decomposing into SCCs.
                         */
        *cub,           /* Arbitrary cube picked inside the SCC */
        *scc,           /* States in the current SCC */
        *tmp1,*tmp2;   
    bdd_node *yCube;
    bdd_node **permutArray;
    int i, size;
  

    /* Build the cycle relation CR(x,y) = TC(x,y)*TC(y,x) */
    /* tmp1 = tc(y,x) -- retain it to use later in edge relation */
    bdd_ref(tmp1 = bdd_bdd_swap_variables(manager,tc,xVars,yVars,nVars));
    bdd_ref(cr = bdd_bdd_and(manager,tc,tmp1));
  
    /* Break into SCCs */
    *scc_table = st_init_table(st_ptrcmp,st_ptrhash);
  
    /* Build the exterior edge relation EE(x,y) = tTC(x,y)*tTC'(y,x) */
    bdd_ref(ee = bdd_bdd_and(manager,tc,bdd_not_bdd_node(tmp1)));
    bdd_recursive_deref(manager,tmp1);
  
    /* Calculate nodes without outgoing edges out the SCCS */
    bdd_ref(yCube = bdd_bdd_compute_cube(manager,yVars,NULL,nVars));
    bdd_ref(tmp2 = bdd_bdd_exist_abstract(manager,ee,yCube));
    bdd_ref(tmp1 = bdd_bdd_and(manager,bdd_not_bdd_node(tmp2),reached));
    bdd_recursive_deref(manager,tmp2);
    bdd_recursive_deref(manager,ee);
    nofanout = tmp1;

    /* Detect the Single SCCs ( SSCCs ) */
    bdd_ref(tmp2 = bdd_bdd_and(manager,nofanout,cr));
    bdd_ref(tmp1 = bdd_bdd_exist_abstract(manager,tmp2,yCube));
    bdd_recursive_deref(manager,tmp2);
    bdd_ref(nocycle = bdd_bdd_and(manager,nofanout,bdd_not_bdd_node(tmp1)));
    bdd_recursive_deref(manager,tmp1);

    bdd_recursive_deref(manager,yCube);
  
    /* Given the nofanout nodes, expand the SCCs that are inside */
    bdd_ref(tnofanout = bdd_bdd_and(manager,nofanout,bdd_not_bdd_node(nocycle)));
    bdd_recursive_deref(manager,nocycle);

    size = bdd_num_vars(manager);
    permutArray = ALLOC(bdd_node *, size);
    for(i = 0; i < size; i++) {
        permutArray[i] = bdd_bdd_ith_var(manager,i);
        bdd_ref(permutArray[i]);
    }
    for(i = 0; i < nVars; i++) {
        int yindex;
    
        yindex = bdd_node_read_index(yVars[i]);
        bdd_recursive_deref(manager,permutArray[yindex]);
        bdd_ref(permutArray[yindex] = xVars[i]);
    }

    /* While there are still nodes in the set tnofanout */
    while(tnofanout != zero) {
      
        /* Pick a point inside the nofanout set */
        bdd_ref(cub = pickOneCube(manager,tnofanout,xVars,nVars));

        /* Obtain the points connected to "cube" by a cycle and 
         * rename variables.
         */

        bdd_ref(tmp1 = bdd_bdd_constrain(manager,cr,cub));

        bdd_ref(tmp2 = bdd_bdd_vector_compose(manager,tmp1,permutArray));
        bdd_recursive_deref(manager,tmp1);

        /* Add the cube to the set, because may be it is not in it */
        bdd_ref(scc = bdd_bdd_or(manager,tmp2,cub));
        bdd_recursive_deref(manager,tmp2);
        st_insert(*scc_table,(char *)cub,(char *)scc);

        /* Delete the SCC from the points without fanout */
        bdd_ref(tmp2 = bdd_bdd_and(manager,tnofanout,bdd_not_bdd_node(scc)));
        bdd_recursive_deref(manager,tnofanout);
        tnofanout = tmp2; 
    }
  
    for(i = 0; i < size; i++) {
        bdd_recursive_deref(manager,permutArray[i]);
    }
    FREE(permutArray);
    bdd_recursive_deref(manager,tnofanout);
    bdd_recursive_deref(manager,cr);
  
    return(nofanout);
}

/*---------------------------------------------------------------------------*/
/* Definition of static   functions                                          */
/*---------------------------------------------------------------------------*/

static bdd_node *
pickOneCube(
  bdd_manager *manager,
  bdd_node *node,
  bdd_node **xVars,
  int nVars)
{
    char *string;
    int i, size;
    int *indices;
    bdd_node *old, *new_;
  
    size = bdd_num_vars(manager);
    indices = ALLOC(int,nVars);
    string = ALLOC(char,size);
    if(! bdd_bdd_pick_one_cube(manager,node,string)) {
        fprintf(stdout,"mark<->MarkPickOneCube: could not pick a cube\n");
        exit(-1);
    }
    for (i = 0; i < nVars; i++) {
        indices[i] = bdd_node_read_index(xVars[i]);
    }

    bdd_ref(old = bdd_read_one(manager));

    for (i = 0; i < nVars; i++) {
        switch(string[indices[i]]) {
        case 0:
            bdd_ref(new_ = bdd_bdd_and(manager,old,bdd_not_bdd_node(xVars[i])));
            bdd_recursive_deref(manager,old);
            old = new_;
            break;
        case 1:
            bdd_ref(new_ = bdd_bdd_and(manager,old,xVars[i]));
            bdd_recursive_deref(manager,old);
            old = new_;
            break;
        }
    }
    FREE(string);
    FREE(indices);
    bdd_deref(old);
    return old;
}