src/cuPort/cuPortIter.c

Go to the documentation of this file.

#include "cuPortInt.h"

#ifndef lint
static char rcsid[] UNUSED = "$Id: cuPortIter.c,v 1.13 2004/08/13 18:39:31 fabio Exp $";
#endif

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


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

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/
typedef struct {
    DdManager   *manager;
    DdGen       *ddGen;
    array_t     *cube;
} cu_bdd_gen;

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


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


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


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

bdd_gen_status
bdd_gen_read_status(bdd_gen *gen)
{
  if (Cudd_IsGenEmpty(((cu_bdd_gen *)gen)->ddGen)) {
    return bdd_EMPTY;
  }
  else {
    return bdd_NONEMPTY;
  }

} /* end of bdd_gen_read_status */


bdd_gen *
bdd_first_disjoint_cube(bdd_t *fn, array_t **cube /* of bdd_literal */)
{
    DdManager *manager;
    cu_bdd_gen *gen;
    int i;
    int *icube;
    CUDD_VALUE_TYPE value;

    /* Make sure we receive a valid bdd_t. (So to speak.) */
    assert(fn != 0);

    manager = (DdManager *)fn->mgr;

    /* Initialize the generator. */
    gen = ALLOC(cu_bdd_gen,1);
    if (gen == NULL) {
      return(NIL(bdd_gen));
    }
    gen->manager = manager;

    gen->cube = array_alloc(bdd_literal, manager->size);
    if (gen->cube == NULL) {
        fail("Bdd Package: Out of memory in bdd_first_cube");
    }

    gen->ddGen = Cudd_FirstCube(manager,(DdNode *)fn->node,&icube,&value);
    if (gen->ddGen == NULL) {
        fail("Cudd Package: Out of memory in bdd_first_cube");
    }

    if (!Cudd_IsGenEmpty(gen->ddGen)) {
        /* Copy icube to the array_t cube. */
        for (i = 0; i < manager->size; i++) {
            int myconst = icube[i];
            array_insert(bdd_literal, gen->cube, i, myconst);
        }
        *cube = gen->cube;
    }

    return(gen);

} /* end of bdd_first_disjoint_cube */


boolean
bdd_next_disjoint_cube(bdd_gen *gen_, array_t **cube /* of bdd_literal */)
{
    cu_bdd_gen *gen;
    int retval;
    int *icube;
    CUDD_VALUE_TYPE value;
    int i;

    gen = (cu_bdd_gen *)gen_;

    retval = Cudd_NextCube(gen->ddGen,&icube,&value);
    if (!Cudd_IsGenEmpty(gen->ddGen)) {
        /* Copy icube to the array_t cube. */
        for (i = 0; i < gen->manager->size; i++) {
            int myconst = icube[i];
            array_insert(bdd_literal, gen->cube, i, myconst);
        }
        *cube = gen->cube;
    }

    return(retval);

} /* end of bdd_next_disjoint_cube */


bdd_gen *
bdd_first_cube(bdd_t *fn, array_t **cube /* of bdd_literal */)
{
    DdManager *manager;
    cu_bdd_gen *gen;
    int i;
    int *icube;

    /* Make sure we receive a valid bdd_t. (So to speak.) */
    assert(fn != 0);

    manager = (DdManager *)fn->mgr;

    /* Initialize the generator. */
    gen = ALLOC(cu_bdd_gen,1);
    if (gen == NULL) {
      return(NIL(bdd_gen));
    }
    gen->manager = manager;

    gen->cube = array_alloc(bdd_literal, manager->size);
    if (gen->cube == NULL) {
        fail("Bdd Package: Out of memory in bdd_first_cube");
    }

    gen->ddGen = Cudd_FirstPrime(manager,(DdNode *)fn->node,
                                 (DdNode *)fn->node,&icube);
    if (gen->ddGen == NULL) {
        fail("Cudd Package: Out of memory in bdd_first_cube");
    }

    if (!Cudd_IsGenEmpty(gen->ddGen)) {
        /* Copy icube to the array_t cube. */
        for (i = 0; i < manager->size; i++) {
            int myconst = icube[i];
            array_insert(bdd_literal, gen->cube, i, myconst);
        }
        *cube = gen->cube;
    }

    return(gen);

} /* end of bdd_first_cube */


boolean
bdd_next_cube(bdd_gen *gen_, array_t **cube /* of bdd_literal */)
{
    cu_bdd_gen *gen;
    int retval;
    int *icube;
    int i;

    gen = (cu_bdd_gen *)gen_;

    retval = Cudd_NextPrime(gen->ddGen,&icube);
    if (!Cudd_IsGenEmpty(gen->ddGen)) {
        /* Copy icube to the array_t cube. */
        for (i = 0; i < gen->manager->size; i++) {
            int myconst = icube[i];
            array_insert(bdd_literal, gen->cube, i, myconst);
        }
        *cube = gen->cube;
    }

    return(retval);

} /* end of bdd_next_cube */


bdd_gen *
bdd_first_node(bdd_t *fn, bdd_node **node /* return */)
{
    bdd_manager *manager;
    cu_bdd_gen *gen;

    /* Make sure we receive a valid bdd_t. (So to speak.) */
    assert(fn != 0);

    manager = fn->mgr;

    /* Initialize the generator. */
    gen = ALLOC(cu_bdd_gen,1);
    if (gen == NULL) return(NULL);
    gen->manager = (DdManager *) manager;
    gen->cube = NULL;

    gen->ddGen = Cudd_FirstNode((DdManager *)manager,(DdNode *)fn->node,
                                (DdNode **)node);
    if (gen->ddGen == NULL) {
        fail("Cudd Package: Out of memory in bdd_first_node");
    }

    return(gen);

} /* end of bdd_first_node */


boolean
bdd_next_node(bdd_gen *gen, bdd_node **node /* return */)
{
    return(Cudd_NextNode(((cu_bdd_gen *)gen)->ddGen,(DdNode **)node));

} /* end of bdd_next_node */


int
bdd_gen_free(bdd_gen *gen_)
{
    cu_bdd_gen *gen;

    gen = (cu_bdd_gen *)gen_;
    if (gen->cube != NULL) array_free(gen->cube);
    Cudd_GenFree(gen->ddGen);
    FREE(gen);
    return(0);

} /* end of bdd_gen_free */

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

---