src/calPort/calPortIter.c

Go to the documentation of this file.

#include "calPortInt.h"

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


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct CalBddGenStruct CalBddGen_t;
/*
 * Traversal of BDD Formulas
 */

typedef enum {
    bdd_gen_cubes,
    bdd_gen_nodes
} bdd_gen_type;


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/
struct CalBddGenStruct {
  Cal_BddManager manager;
  bdd_gen_status status;
  bdd_gen_type type;
  union {
        struct {
      array_t *cube;    /* of bdd_literal */
        } cubes;
        struct {
      st_table *visited;        /* of bdd_node* */
        } nodes;
  } gen;        
  struct {
        int sp;
        CalBddNode_t **nodeStack;
    int *idStack;
  } stack;
  CalBddNode_t *node;
};




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


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


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static void pop_node_stack(CalBddGen_t *gen);
static void push_node_stack(Cal_Bdd_t f, CalBddGen_t *gen);
static void pop_cube_stack(CalBddGen_t *gen);
static void push_cube_stack(Cal_Bdd_t f, CalBddGen_t *gen);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
/*
 *    Defines an iterator on the onset of a BDD.  Two routines are
 *    provided: bdd_first_cube, which extracts one cube from a BDD and
 *    returns a bdd_gen structure containing the information necessary to
 *    continue the enumeration; and bdd_next_cube, which returns 1 if
 *     another cube was 
 *    found, and 0 otherwise. A cube is represented
 *    as an array of bdd_literal (which are integers in {0, 1, 2}),
 *    where 0 represents 
 *    negated literal, 1 for literal, and 2 for don't care.  Returns a
 *    disjoint 
 *    cover.  A third routine is there to clean up. 
 */

bdd_gen_status
bdd_gen_read_status(bdd_gen *gen)
{
  return ((CalBddGen_t *)gen)->status;
}

bdd_gen *
bdd_first_cube(bdd_t *fn,array_t **cube)
{
  Cal_BddManager_t *manager;
  CalBddGen_t *gen;
  int i;
  long numVars;
  Cal_Bdd function;
  Cal_Bdd_t calBdd;
  
  if (fn == NIL(bdd_t)) {
        CalBddFatalMessage("bdd_first_cube: invalid BDD");
  }

  manager = fn->bddManager;
  function = fn->calBdd;
  
  /*
   *    Allocate a new generator structure and fill it in; the stack and the 
   *    cube will be used, but the visited table and the node will not be used.
   */
  gen = ALLOC(CalBddGen_t, 1);
  
    /*
     *    first - init all the members to a rational value for cube iteration
     */
  gen->manager = manager;
  gen->status = bdd_EMPTY;
  gen->type = bdd_gen_cubes;
  gen->gen.cubes.cube = NIL(array_t);
  gen->stack.sp = 0;
  gen->stack.nodeStack = NIL(CalBddNode_t *);
  gen->stack.idStack = NIL(int);
  gen->node = NIL(CalBddNode_t);
  
  numVars = Cal_BddVars(manager);
  gen->gen.cubes.cube = array_alloc(bdd_literal, numVars);
    
  /*
   * Initialize each literal to 2 (don't care).
   */
  for (i = 0; i < numVars; i++) {
    array_insert(bdd_literal, gen->gen.cubes.cube, i, 2);
  }
  
  /*
   * The stack size will never exceed the number of variables in the BDD, since
   * the longest possible path from root to constant 1 is the number
   * of variables in the BDD.
   */
  gen->stack.sp = 0;
  gen->stack.nodeStack = ALLOC(CalBddNode_t *, numVars);
  gen->stack.idStack = ALLOC(int, numVars);

  /*
   * Clear out the stack so that in bdd_gen_free, we can decrement the
   * ref count of those nodes still on the stack.
   */
  for (i = 0; i < numVars; i++) {
        gen->stack.nodeStack[i] = NIL(CalBddNode_t);
        gen->stack.idStack[i] = -1;
  }
  
  if (Cal_BddIsBddZero(manager, function)){
        /*
         *    All done, for this was but the zero constant ...
         *    We are enumerating the onset, (which is vacuous).
     *    gen->status initialized to bdd_EMPTY above, so this
     *    appears to be redundant.
         */
        gen->status = bdd_EMPTY;
  } else {
        /*
         *    Get to work enumerating the onset.  Get the first cube.  Note that
     *    if fn is just the constant 1, push_cube_stack will properly
     *    handle this. 
         *    Get a new pointer to fn->node beforehand: this increments 
         *    the reference count of fn->node; this is necessary, because
     *    when fn->node 
         *    is popped from the stack at the very end, it's ref count is
     *    decremented. 
         */
        gen->status = bdd_NONEMPTY;
    calBdd = CalBddGetInternalBdd(manager, function);
    push_cube_stack(calBdd, gen);
  }
  *cube = gen->gen.cubes.cube;
  return (bdd_gen *)(gen);
}

boolean
bdd_next_cube(bdd_gen *gen_, array_t **cube)
{
  CalBddGen_t *gen = (CalBddGen_t *) gen_;
  pop_cube_stack(gen);
  if (gen->status == bdd_EMPTY) {
    return (FALSE);
  }
  *cube = gen->gen.cubes.cube;
  return (TRUE);
}

bdd_gen *
bdd_first_disjoint_cube(bdd_t *fn,array_t **cube)
{
  return(bdd_first_cube(fn,cube));
}

boolean
bdd_next_disjoint_cube(bdd_gen *gen_, array_t **cube)
{
  return(bdd_next_cube(gen_,cube));
}

bdd_gen *
bdd_first_node(bdd_t *fn, bdd_node **node)
{
  Cal_BddManager_t *manager;
  CalBddGen_t *gen;
  long numVars;
  int i;
  Cal_Bdd_t calBdd;
  Cal_Bdd function;
  
  if (fn == NIL(bdd_t)) {
        CalBddFatalMessage("bdd_first_node: invalid BDD");
  }
  
  manager = fn->bddManager;
  function = fn->calBdd;
  
  /*
   *    Allocate a new generator structure and fill it in; the
   *    visited table will be used, as will the stack, but the
   *    cube array will not be used.
   */
  gen = ALLOC(CalBddGen_t, 1);
  
  /*
   *    first - init all the members to a rational value for node iteration.
   */
  gen->manager = manager;
  gen->status = bdd_NONEMPTY;
  gen->type = bdd_gen_nodes;
  gen->gen.nodes.visited = NIL(st_table);
  gen->stack.sp = 0;
  gen->stack.nodeStack = NIL(CalBddNode_t *);
  gen->stack.idStack = NIL(int);
  gen->node = NIL(CalBddNode_t);
  
  /* 
   * Set up the hash table for visited nodes.  Every time we visit a node,
   * we insert it into the table.
   */
  gen->gen.nodes.visited = st_init_table(st_ptrcmp, st_ptrhash);
  
  /*
   * The stack size will never exceed the number of variables in the BDD, since
   * the longest possible path from root to constant 1 is the number
   * of variables in the BDD.
   */
  gen->stack.sp = 0;
  numVars = Cal_BddVars(manager);
  gen->stack.nodeStack = ALLOC(CalBddNode_t *, numVars);
  gen->stack.idStack = ALLOC(int, numVars);
  /*
   * Clear out the stack so that in bdd_gen_free, we can decrement the
   * ref count of those nodes still on the stack.
   */
  for (i = 0; i < numVars; i++) {
        gen->stack.nodeStack[i] = NIL(CalBddNode_t);
        gen->stack.idStack[i] = -1;
  }
  
  /*
   * Get the first node.  Get a new pointer to fn->node beforehand:
   * this increments 
   * the reference count of fn->node; this is necessary, because when fn->node
   * is popped from the stack at the very end, it's ref count is decremented.
   */
  calBdd = CalBddGetInternalBdd(manager, function);
  push_node_stack(calBdd, gen);
  gen->status = bdd_NONEMPTY;
  
  *node = (bdd_node *)gen->node;        /* return the node */
  return (bdd_gen *)(gen);      /* and the new generator */
}

boolean
bdd_next_node(bdd_gen *gen_,bdd_node **node)
{
  CalBddGen_t *gen = (CalBddGen_t *) gen_;
  pop_node_stack(gen);
  if (gen->status == bdd_EMPTY) {
        return (FALSE);
  }
  *node = (bdd_node *) gen->node;
  return (TRUE);
}

int
bdd_gen_free(bdd_gen *gen_)
{
  CalBddGen_t *gen = (CalBddGen_t *) gen_;
  st_table *visited_table;

  switch (gen->type) {
    case bdd_gen_cubes:
      array_free(gen->gen.cubes.cube);
      gen->gen.cubes.cube = NIL(array_t);
      break;
    case bdd_gen_nodes:
      visited_table = gen->gen.nodes.visited;
      st_free_table(visited_table);
      visited_table = NIL(st_table);
      break;
  }
  FREE(gen->stack.nodeStack);
  FREE(gen->stack.idStack);
  FREE(gen);
  return (0);   /* make it return some sort of an int */
}

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
/*
 *    Invariants:
 *
 *    gen->stack.stack contains nodes that remain to be explored.
 *
 *    For a cube generator,
 *        gen->gen.cubes.cube reflects the choices made to reach node
 *        at top of the stack. 
 *    For a node generator,
 *        gen->gen.nodes.visited reflects the nodes already visited in
 *         the BDD dag. 
 */

static void
push_cube_stack(Cal_Bdd_t f, CalBddGen_t *gen)
{
  bdd_variableId topId;
  Cal_Bdd_t f0, f1;
  Cal_BddManager_t *manager;

  manager = gen->manager;
  
  if (CalBddIsBddOne(manager, f)){
    return;
  }

  topId = f.bddId-1;
  CalBddGetElseBdd(f, f0);
  CalBddGetThenBdd(f, f1);

  if (CalBddIsBddZero(manager, f1)){ 
/*
 *    No choice: take the 0 branch.  Since there is only one branch to 
 *    explore from f, there is no need to push f onto the stack, because
 *    after exploring this branch we are done with f.  A consequence of 
 *    this is that there will be no f to pop either.  Same goes for the
 *    next case.  Decrement the ref count of f and of the branch leading
 *    to zero, since we will no longer need to access these nodes.
 */
    array_insert(bdd_literal, gen->gen.cubes.cube, topId, 0);
        push_cube_stack(f0, gen);
  }
  else if (CalBddIsBddZero(manager, f0)){
        /*
         *    No choice: take the 1 branch
         */
        array_insert(bdd_literal, gen->gen.cubes.cube, topId, 1);
        push_cube_stack(f1, gen);
  } else {
    /*
     * In this case, we must explore both branches of f.  We always choose
     * to explore the 0 branch first.  We must push f on the stack, so that
     * we can later pop it and explore its 1 branch. Decrement the ref count 
     * of f1 since we will no longer need to access this node.  Note that 
     * the parent of f1 was bdd_freed above or in pop_cube_stack.
     */
    gen->stack.nodeStack[gen->stack.sp] = f.bddNode;
    gen->stack.idStack[gen->stack.sp++] = f.bddId;
    array_insert(bdd_literal, gen->gen.cubes.cube, topId, 0);
    push_cube_stack(f0, gen);
  }
}

static void
pop_cube_stack(CalBddGen_t *gen)
{
  CalBddNode_t *fNode;
  int fId, fIndex, i;
  Cal_Bdd_t f1, f;
  Cal_BddManager_t *manager;
  
  manager = gen->manager;
  if (gen->stack.sp == 0) {
    /*
     * Stack is empty.  Have already explored both the 0 and 1 branches of 
     * the root of the BDD.
     */
        gen->status = bdd_EMPTY;
  } else {
    /*
     * Explore the 1 branch of the node at the top of the stack (since it is
     * on the stack, this means we have already explored the 0 branch).  We 
     * permanently pop the top node, and bdd_free it, since there are
     * no more edges left to explore. 
     */
        fNode = gen->stack.nodeStack[--gen->stack.sp];
        fId = gen->stack.idStack[gen->stack.sp];
        gen->stack.nodeStack[gen->stack.sp] = NIL(CalBddNode_t); /* overwrite */
                                                         /* with NIL */
        gen->stack.idStack[gen->stack.sp] = -1;
        array_insert(bdd_literal, gen->gen.cubes.cube, fId-1, 1);
    fIndex = manager->idToIndex[fId];
        for (i = fIndex + 1; i < array_n(gen->gen.cubes.cube); i++) {
      array_insert(bdd_literal, gen->gen.cubes.cube,
                   manager->indexToId[i]-1, 2); 
        }
    f.bddNode = fNode;
    f.bddId = fId;
    CalBddGetThenBdd(f, f1);
        push_cube_stack(f1, gen);
  }
}

static void
push_node_stack(Cal_Bdd_t f, CalBddGen_t *gen)
{
  Cal_Bdd_t f0, f1;
  bdd_node *reg_f, *reg_f0, *reg_f1;

  reg_f = (CalBddNode_t *) CAL_BDD_POINTER(f.bddNode);  /* use of calInt.h */
  if (st_is_member(gen->gen.nodes.visited, (char *) reg_f)){
    /* 
     * Already been visited.
     */
        return;
  }
  
  if (CalBddIsBddConst(f)){
    /*
     * If f is the constant node and it has not been visited yet, then
     * put it in the visited table and set the gen->node pointer.
     * There is no need to put it in the stack because 
     * the constant node does not have any branches, and there is no
     * need to free f because constant nodes have a saturated
     * reference count. 
     */
        st_insert(gen->gen.nodes.visited, (char *) reg_f, NIL(char));
        gen->node = (CalBddNode_t *) reg_f;
  } else {
    /*
     * f has not been marked as visited.  We don't know yet if any of
     * its branches remain to be explored.  First get its branches.
     */
    CalBddGetElseBdd(f, f0);
    CalBddGetThenBdd(f, f1);

        reg_f0 = (CalBddNode_t *) CAL_BDD_POINTER(f0.bddNode);
        reg_f1 = (CalBddNode_t *) CAL_BDD_POINTER(f1.bddNode);

        if (st_is_member(gen->gen.nodes.visited, (char *) reg_f0) == 0){
      /* 
       * The 0 child has not been visited, so explore the 0 branch.
       * First push f on the stack.  Bdd_free f1 since we will not
       * need to access this exact pointer any more.
       */
      gen->stack.nodeStack[gen->stack.sp] = f.bddNode;
      gen->stack.idStack[gen->stack.sp++] = f.bddId;
      push_node_stack(f0, gen);
        } else{
      if (st_is_member(gen->gen.nodes.visited, (char *) reg_f1) == 0){
        /* 
         * The 0 child has been visited, but the 1 child has not been
         * visited, so explore the 1 branch.  First push f on the
         * stack. 
         */
        gen->stack.nodeStack[gen->stack.sp] = f.bddNode;
        gen->stack.idStack[gen->stack.sp++] = f.bddId;
        push_node_stack(f1, gen);
      } else {
        /*
         * Both the 0 and 1 children have been visited. Thus we are done
         * exploring from f.   
         * Mark f as visited (put it in the visited table), and set the
         * gen->node pointer. 
         */
        st_insert(gen->gen.nodes.visited, (char *) reg_f, NIL(char));
        gen->node = (CalBddNode_t *) reg_f;
      }
    }
  }
}

static void
pop_node_stack(CalBddGen_t *gen)
{
  CalBddNode_t *fNode;
  int fId;
  Cal_Bdd_t calBdd;
  
  if (gen->stack.sp == 0) {
    gen->status = bdd_EMPTY;
    return;
  }
  fNode = gen->stack.nodeStack[--gen->stack.sp]; 
  fId = gen->stack.idStack[gen->stack.sp];
  gen->stack.nodeStack[gen->stack.sp] = NIL(CalBddNode_t);
  gen->stack.idStack[gen->stack.sp] = -1;
  calBdd.bddNode = fNode;
  calBdd.bddId = fId;
  push_node_stack(calBdd, gen);
}

---