cuddInteract.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

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

#if SIZEOF_LONG == 8
#define BPL 64
#define LOGBPL 6
#else
#define BPL 32
#define LOGBPL 5
#endif

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


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


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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddInteract.c,v 1.14 2012/02/05 01:07:19 fabio Exp $";
#endif

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


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

static void ddSuppInteract (DdNode *f, char *support);
static void ddClearLocal (DdNode *f);
static void ddUpdateInteract (DdManager *table, char *support);
static void ddClearGlobal (DdManager *table);

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


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


void
cuddSetInteract(
  DdManager * table,
  int  x,
  int  y)
{
    int posn, word, bit;

#ifdef DD_DEBUG
    assert(x < y);
    assert(y < table->size);
    assert(x >= 0);
#endif

    posn = ((((table->size << 1) - x - 3) * x) >> 1) + y - 1;
    word = posn >> LOGBPL;
    bit = posn & (BPL-1);
    table->interact[word] |= 1L << bit;

} /* end of cuddSetInteract */


int
cuddTestInteract(
  DdManager * table,
  int  x,
  int  y)
{
    int posn, word, bit, result;

    if (x > y) {
    int tmp = x;
    x = y;
    y = tmp;
    }
#ifdef DD_DEBUG
    assert(x < y);
    assert(y < table->size);
    assert(x >= 0);
#endif

    posn = ((((table->size << 1) - x - 3) * x) >> 1) + y - 1;
    word = posn >> LOGBPL;
    bit = posn & (BPL-1);
    result = (table->interact[word] >> bit) & 1L;
    return(result);

} /* end of cuddTestInteract */


int
cuddInitInteract(
  DdManager * table)
{
    int i,j;
    unsigned long words;
    long *interact;
    char *support;
    DdNode *f;
    DdNode *sentinel = &(table->sentinel);
    DdNodePtr *nodelist;
    int slots;
    unsigned long n = (unsigned long) table->size;

    words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
    table->interact = interact = ALLOC(long,words);
    if (interact == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    for (i = 0; i < words; i++) {
    interact[i] = 0;
    }

    support = ALLOC(char,n);
    if (support == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    FREE(interact);
    return(0);
    }
    for (i = 0; i < n; i++) {
        support[i] = 0;
    }

    for (i = 0; i < n; i++) {
    nodelist = table->subtables[i].nodelist;
    slots = table->subtables[i].slots;
    for (j = 0; j < slots; j++) {
        f = nodelist[j];
        while (f != sentinel) {
        /* A node is a root of the DAG if it cannot be
        ** reached by nodes above it. If a node was never
        ** reached during the previous depth-first searches,
        ** then it is a root, and we start a new depth-first
        ** search from it.
        */
        if (!Cudd_IsComplement(f->next)) {
            ddSuppInteract(f,support);
            ddClearLocal(f);
            ddUpdateInteract(table,support);
        }
        f = Cudd_Regular(f->next);
        }
    }
    }
    ddClearGlobal(table);

    FREE(support);
    return(1);

} /* end of cuddInitInteract */


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


static void
ddSuppInteract(
  DdNode * f,
  char * support)
{
    if (cuddIsConstant(f) || Cudd_IsComplement(cuddT(f))) {
    return;
    }

    support[f->index] = 1;
    ddSuppInteract(cuddT(f),support);
    ddSuppInteract(Cudd_Regular(cuddE(f)),support);
    /* mark as visited */
    cuddT(f) = Cudd_Complement(cuddT(f));
    f->next = Cudd_Complement(f->next);
    return;

} /* end of ddSuppInteract */


static void
ddClearLocal(
  DdNode * f)
{
    if (cuddIsConstant(f) || !Cudd_IsComplement(cuddT(f))) {
    return;
    }
    /* clear visited flag */
    cuddT(f) = Cudd_Regular(cuddT(f));
    ddClearLocal(cuddT(f));
    ddClearLocal(Cudd_Regular(cuddE(f)));
    return;

} /* end of ddClearLocal */


static void
ddUpdateInteract(
  DdManager * table,
  char * support)
{
    int i,j;
    int n = table->size;

    for (i = 0; i < n-1; i++) {
    if (support[i] == 1) {
            support[i] = 0;
        for (j = i+1; j < n; j++) {
        if (support[j] == 1) {
            cuddSetInteract(table,i,j);
        }
        }
    }
    }
    support[n-1] = 0;

} /* end of ddUpdateInteract */


static void
ddClearGlobal(
  DdManager * table)
{
    int i,j;
    DdNode *f;
    DdNode *sentinel = &(table->sentinel);
    DdNodePtr *nodelist;
    int slots;

    for (i = 0; i < table->size; i++) {
    nodelist = table->subtables[i].nodelist;
    slots = table->subtables[i].slots;
    for (j = 0; j < slots; j++) {
        f = nodelist[j];
        while (f != sentinel) {
        f->next = Cudd_Regular(f->next);
        f = f->next;
        }
    }
    }

} /* end of ddClearGlobal */