src/cuBdd/cuddInteract.c

Go to the documentation of this file.

#include "util.h"
#include "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.12 2004/08/13 18:04:49 fabio Exp $";
#endif

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


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

static void ddSuppInteract (DdNode *f, int *support);
static void ddClearLocal (DdNode *f);
static void ddUpdateInteract (DdManager *table, int *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,k;
    int words;
    long *interact;
    int *support;
    DdNode *f;
    DdNode *sentinel = &(table->sentinel);
    DdNodePtr *nodelist;
    int slots;
    int n = 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(int,n);
    if (support == NULL) {
        table->errorCode = CUDD_MEMORY_OUT;
        FREE(interact);
        return(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)) {
                    for (k = 0; k < n; k++) {
                        support[k] = 0;
                    }
                    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,
  int * 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,
  int * support)
{
    int i,j;
    int n = table->size;

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

} /* 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 */

---