src/baig/baigNode.c

Go to the documentation of this file.

#include "vm.h"
#include "baig.h"
#include "baigInt.h"

static char rcsid[] UNUSED = "$Id: baigNode.c,v 1.33 2009/04/12 00:14:03 fabio Exp $";

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

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

static void connectOutput(bAig_Manager_t *manager, bAigEdge_t from, bAigEdge_t to, int inputIndex);
static bAigEdge_t HashTableLookup(bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2);
static int HashTableAdd(bAig_Manager_t *manager, bAigEdge_t nodeIndexParent, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
static int HashTableDelete(bAig_Manager_t *manager, bAigEdge_t node);

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


nameType_t *
bAig_NodeReadName(
   bAig_Manager_t *manager,
   bAigEdge_t     node)
{
  return manager->nameList[bAigNodeID(node)];
}

void 
bAig_NodeSetName(
   bAig_Manager_t *manager,
   bAigEdge_t     node,
   nameType_t     *name)
{
  nameType_t *tmpName = manager->nameList[bAigNodeID(node)];
  FREE(tmpName);
  st_insert(manager->SymbolTable, name, (char*) (long) node);
  manager->nameList[bAigNodeID(node)] = name;
}

int
bAig_NodeReadIndexOfRightChild(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex)
{
  return rightChild(nodeIndex);
}

bAigEdge_t
bAig_NodeReadIndexOfLeftChild(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex)
{
  return leftChild(nodeIndex);
}

bAigEdge_t
bAig_GetCanonical(
    bAig_Manager_t *manager, 
    bAigEdge_t nodeIndex)
{
bAigEdge_t next;

/*if(nodeIndex == bAig_NULL)    return(nodeIndex);*/

//Bing: 
 if(nodeIndex == bAig_NULL||
    nodeIndex == bAig_One ||
    nodeIndex == bAig_Zero)
   return(nodeIndex); 

  while(bAigGetPassFlag(manager, nodeIndex)) {
    next = canonical(nodeIndex);
    if(bAig_IsInverted(nodeIndex))  next = bAig_Not(next);
    nodeIndex = next;
  }
  return(nodeIndex);
}

int
bAig_Merge(
    bAig_Manager_t *manager,
    bAigEdge_t nodeIndex1,
    bAigEdge_t nodeIndex2)
{
bAigEdge_t newNodeIndex, nodeIndex, tnodeIndex;
bAigEdge_t leftIndex, rightIndex;
bAigEdge_t outIndex, *pfan;
int id1, id2;
bAigEdge_t cur;
bdd_t **bddArray;
array_t *nodeArray;
int i, ii, iii;
long *ManagerNodesArray;

  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);

  if(nodeIndex1 == nodeIndex2)  return(nodeIndex1);


  ManagerNodesArray = manager->NodesArray;


  newNodeIndex = nodeIndex1;     
  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
    nodeIndex1 = nodeIndex2;
    nodeIndex2 = newNodeIndex;
  }

  if(bAig_IsInverted(nodeIndex2)) {
    nodeIndex1 = bAig_Not(nodeIndex1);
    nodeIndex2 = bAig_Not(nodeIndex2);
  }

  nodeArray = array_alloc(bAigEdge_t, 0);
  nodeIndex = nodeIndex2;
  array_insert_last(bAigEdge_t, nodeArray, nodeIndex);
  while(bAig_NonInvertedEdge(canonical(nodeIndex)) != bAig_NonInvertedEdge(nodeIndex2)){
    if(bAig_IsInverted(nodeIndex))
      nodeIndex = bAig_Not(canonical(nodeIndex));
    else
      nodeIndex = canonical(nodeIndex);
    array_insert_last(bAigEdge_t, nodeArray, nodeIndex);
  }

  bAigSetPassFlag(manager, nodeIndex2);
  nodeIndex = nodeIndex1;
  while(bAig_NonInvertedEdge(canonical(nodeIndex)) != bAig_NonInvertedEdge(nodeIndex1)) {
    if(bAig_IsInverted(nodeIndex))
      nodeIndex = bAig_Not(canonical(nodeIndex));
    else
      nodeIndex = canonical(nodeIndex);
  }

  for(i=0; i<array_n(nodeArray); i++) {
    tnodeIndex = array_fetch(bAigEdge_t, nodeArray, i);
    if(bAig_IsInverted(nodeIndex))
      canonical(nodeIndex) = bAig_Not(tnodeIndex);
    else 
      canonical(nodeIndex) = tnodeIndex;

    if(bAig_IsInverted(nodeIndex))
      nodeIndex = bAig_Not(canonical(nodeIndex));
    else
      nodeIndex = canonical(nodeIndex);
  }

  if(bAig_IsInverted(nodeIndex))        {
    canonical(nodeIndex) = bAig_Not(nodeIndex1);
  }
  else {
    canonical(nodeIndex) = nodeIndex1;
  }
  array_free(nodeArray);

  nodeArray = array_alloc(bAigEdge_t, 0);
  bAigEdgeForEachFanout(manager, nodeIndex2, cur, ii, iii, pfan) {
    cur = cur >> 1;
    cur = bAig_NonInvertedEdge(cur);
    array_insert_last(bAigEdge_t, nodeArray, cur);
  }

  for(i=0; i<array_n(nodeArray); i++) {
    outIndex = array_fetch(bAigEdge_t, nodeArray, i);
    leftIndex = leftChild(outIndex);
    rightIndex = rightChild(outIndex);

    HashTableDelete(manager, outIndex);

    newNodeIndex = bAig_And(manager, leftIndex, rightIndex);

    bAig_Merge(manager, newNodeIndex, outIndex);

  }
  array_free(nodeArray);

  bddArray = manager->bddArray;
  id1 = bAigNodeID(nodeIndex1);
  id2 = bAigNodeID(nodeIndex2);
  if(bddArray[id1] == 0 && bddArray[id2]){ 
    if(bAig_IsInverted(nodeIndex2)) {
      if(bAig_IsInverted(nodeIndex1)) {
        bddArray[id1] = bdd_dup(bddArray[id2]);
      }
      else {
        bddArray[id1] = bdd_not(bddArray[id2]);
      }
    }
    else {
      if(bAig_IsInverted(nodeIndex1)) {
        bddArray[id1] = bdd_not(bddArray[id2]);
      }
      else {
        bddArray[id1] = bdd_dup(bddArray[id2]);
      }
    }
  }
  return(nodeIndex1);
}



void
bAig_PrintNode(
  bAig_Manager_t *manager,
  bAigEdge_t i)
{
  int j, size;
  long cur, *pfan;

  fprintf(vis_stdout, "nodeIndex : %ld (%ld)\n", i, bAigNodeID(i)); 
  fprintf(vis_stdout, "child     : %ld%c, %ld%c\n", 
          bAig_NonInvertedEdge(leftChild(i)), bAig_IsInverted(leftChild(i)) ? '\'' : ' ', 
          bAig_NonInvertedEdge(rightChild(i)), bAig_IsInverted(rightChild(i)) ? '\'' : ' ');
  fprintf(vis_stdout, "canonical : %s (%ld)\n", 
          bAigGetPassFlag(manager, i) ? "pass" : "true", bAig_GetCanonical(manager, i));
  fprintf(vis_stdout, "refCount  : %ld\n", nFanout(i));
  fprintf(vis_stdout, "          : ");
  size = nFanout(i);
  for(j=0, pfan = (bAigEdge_t *)fanout(i); j<size; j++) {
    cur = pfan[j];
    cur = cur >> 1;
    fprintf(vis_stdout, " %ld", cur);
  }
  fprintf(vis_stdout, "\n");

  fprintf(vis_stdout, "next      : %ld\n", next(i));
  fflush(vis_stdout);
}
   

bAigEdge_t
bAig_And(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{

  bAigEdge_t newNodeIndex;

  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);

  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
    nodeIndex1 = nodeIndex2;
    nodeIndex2 = newNodeIndex;
  }

  if ( nodeIndex2 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex1 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex2 == bAig_One ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_One ) {
    return nodeIndex2;
  }
  if ( nodeIndex1 == nodeIndex2 ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
    return bAig_Zero;
  }

  /* Look for the new node in the Hash table */
  newNodeIndex = HashTableLookup(manager, nodeIndex1, nodeIndex2);

  if (newNodeIndex == bAig_NULL){ 
    if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
      newNodeIndex = bAig_And2(manager, nodeIndex1, nodeIndex2);
    else if(bAigIsVar(manager, nodeIndex1)) 
      newNodeIndex = bAig_And3(manager, nodeIndex1, nodeIndex2);
    else if(bAigIsVar(manager, nodeIndex2)) 
      newNodeIndex = bAig_And3(manager, nodeIndex2, nodeIndex1);
    else {
      newNodeIndex = bAig_And4(manager, nodeIndex1, nodeIndex2);
    }
  }
    
  return newNodeIndex;

}

bAigEdge_t
bAig_And2(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  bAigEdge_t newNodeIndex;

  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);

  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
    nodeIndex1 = nodeIndex2;
    nodeIndex2 = newNodeIndex;
  }
  if ( nodeIndex2 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex1 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex2 == bAig_One ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_One ) {
    return nodeIndex2;
  }
  if ( nodeIndex1 == nodeIndex2 ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
    return bAig_Zero;
  }
  newNodeIndex = HashTableLookup(manager, nodeIndex1, nodeIndex2);

  if (newNodeIndex == bAig_NULL){ 
    newNodeIndex = bAigCreateAndNode(manager, nodeIndex1, nodeIndex2) ;

    HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
    connectOutput(manager, nodeIndex1, newNodeIndex, 0);
    connectOutput(manager, nodeIndex2, newNodeIndex, 1);

#if 0
#ifdef LEARNING_
    tNodeIndex = HashTableLookup(manager, bAig_Not(nodeIndex1), nodeIndex2);
    if(tNodeIndex) bAig_Learn(manager, nodeIndex1, nodeIndex2);

    tNodeIndex = HashTableLookup(manager, nodeIndex1, bAig_Not(nodeIndex2));
    if(tNodeIndex) bAig_Learn(manager, nodeIndex2, nodeIndex1);
#endif
#endif
  }
  return newNodeIndex;

}


bAigEdge_t
bAig_Or(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  return ( bAig_Not(bAig_And(manager,  bAig_Not(nodeIndex1),  bAig_Not(nodeIndex2))));
}

bAigEdge_t
bAig_Xor(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return bAig_Or(manager,
            bAig_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
            bAig_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
        );
}

bAigEdge_t
bAig_Eq(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return bAig_Not(
            bAig_Xor(manager, nodeIndex1, nodeIndex2)
            );
}

bAigEdge_t
bAig_Then(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return bAig_Or(manager,
                bAig_Not(nodeIndex1),
                nodeIndex2);
}

bAigEdge_t
bAig_CreateNode(
   bAig_Manager_t  *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  
  bAigEdge_t newNode = manager->nodesArraySize;

  if (manager->nodesArraySize >= manager->maxNodesArraySize ){
    manager->maxNodesArraySize = 2* manager->maxNodesArraySize;
    manager->NodesArray = REALLOC(bAigEdge_t, manager->NodesArray, manager->maxNodesArraySize);
    manager->nameList   = REALLOC(char *,     manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddIdArray = REALLOC(int ,     manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddArray   = REALLOC(bdd_t *,     manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
  }
  manager->NodesArray[bAig_NonInvertedEdge(newNode)+bAigRight] = nodeIndex2;
  manager->NodesArray[bAig_NonInvertedEdge(newNode)+bAigLeft]  = nodeIndex1;
 
  next(newNode)     = bAig_NULL;
  fanout(newNode) = 0;
  canonical(newNode) = newNode;
  flags(newNode) = 0;
  nFanout(newNode) = 0;
  manager->bddIdArray[bAigNodeID(newNode)] = -1; 
  manager->bddArray[bAigNodeID(newNode)] = 0; 

  manager->nodesArraySize +=bAigNodeSize;
  
  //Bing: for interpolation
  aig_value(newNode) = 2;
  manager->nameList[bAigNodeID(newNode)] = 0;
  manager->NodesArray[newNode+bAigClass] = manager->class_;
  
  return(newNode);
}


bAigEdge_t
bAig_FindNodeByName(
  bAig_Manager_t *manager,
  nameType_t     *name)
{
   
  bAigEdge_t node;

  if (!st_lookup(manager->SymbolTable, name, &node)){
    node = bAig_NULL;
  }

  return bAig_GetCanonical(manager, node);
}


bAigEdge_t
bAig_CreateVarNode(
   bAig_Manager_t  *manager,
   nameType_t      *name)
{
   
  bAigEdge_t varIndex;


  if (!st_lookup(manager->SymbolTable, name, &varIndex)){
    varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
    if (varIndex == bAig_NULL){
      return (varIndex);
    } 
    /* Insert the varaible in the Symbol Table */
    st_insert(manager->SymbolTable, name, (char*) (long) varIndex);
    manager->nameList[bAigNodeID(varIndex)] = name; 
    return(varIndex);
  }
  else {
    return (varIndex);
  }
}

int 
bAig_isVarNode(
   bAig_Manager_t *manager,
   bAigEdge_t      node)
{
  if((rightChild(node) == bAig_NULL) && (leftChild(node) == bAig_NULL)) {
    return 1;
  }
  return 0;
}



bAigEdge_t
bAig_bddTobAig(
   bAig_Manager_t *bAigManager,
   bdd_t          *fn)
{
  bdd_gen     *gen;
  bdd_node    *node, *thenNode, *elseNode, *funcNode;
  bdd_manager *bddManager = bdd_get_manager(fn);
  /*
    Used to read the variable name of a bdd node.
  */
  array_t     *mvar_list  = mdd_ret_mvar_list(bddManager);
  array_t     *bvar_list  = mdd_ret_bvar_list(bddManager);
  bvar_type   bv;
  mvar_type   mv;
  
  bdd_node    *one        = bdd_read_one(bddManager);  
  int         is_complemented;
  int         flag;  
  bAigEdge_t  var, left, right, result;
  
  char      name[100];
  st_table  *bddTObaigTable;
  
  if (fn == NULL){
    return bAig_NULL;
  }
  funcNode = bdd_get_node(fn, &is_complemented);
  if (bdd_is_constant(funcNode)){
    return (is_complemented?bAig_Zero:bAig_One);
  }
  bddTObaigTable = st_init_table(st_numcmp, st_numhash);
  st_insert(bddTObaigTable, (char *) (long) bdd_regular(one),  (char *) bAig_One);

  foreach_bdd_node(fn, gen, node){
    int nodeIndex = bdd_node_read_index(node);
    int index, rtnNodeIndex;

    if (bdd_is_constant(node)){
      continue;
    }

    bv = array_fetch(bvar_type, bvar_list, nodeIndex);
    /*
      get the multi-valued varaible.
     */
    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
    arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
      if (nodeIndex == rtnNodeIndex){
        break;
      }
    }
    assert(index < mv.encode_length);
    /*
    printf("Name of bdd node %s %d\n", mv.name, index);
    */
    sprintf(name, "%s_%d", mv.name, index);
    /*
      Create or Retrieve the bAigEdge_t  w.r.t. 'name'
    */
    var  = bAig_CreateVarNode(bAigManager, util_strsav(name));

    thenNode  = bdd_bdd_T(node);
    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(thenNode),
                     &left);
    assert(flag);
      
    elseNode  = bdd_bdd_E(node);
    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(elseNode),
                     &right);
    assert(flag);
    /*
     test if the elseNode is complemented arc?
    */
    if (bdd_is_complement(elseNode)){
      right = bAig_Not(right);
    }
    if (right ==  bAig_Zero){        /* result = var*then */
      result =  bAig_And(bAigManager, var, left);
    } else if (right ==  bAig_One){        /* result = then + not(var) */
      result =  bAig_Or(bAigManager, left, bAig_Not(var));
    } else if (left ==  bAig_One) { /* result = var + else */
      result =  bAig_Or(bAigManager, var, right);      
    } else {                        /* result = var * then + not(var)*else */
      result =  bAig_Or(bAigManager, bAig_And(bAigManager, var, left),
                        bAig_And(bAigManager, bAig_Not(var), right));
    }
    st_insert(bddTObaigTable, (char *) (long) bdd_regular(node),
              (char *) (long) result);
  }
  flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(funcNode),
                   &result);  
  assert(flag);
  st_free_table(bddTObaigTable);

  if (is_complemented){
    return bAig_Not(result);
  } else {
    return result;
  }
} /* end of bAig_bddtobAig() */


int
bAig_PrintDot(
  FILE *fp,
  bAig_Manager_t *manager)
{
  long i;

  /*
   * Write out the header for the output file.
   */
  (void) fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
  (void) fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");
 
  
  for (i=bAigFirstNodeIndex ; i< manager->nodesArraySize ; i+=bAigNodeSize){
    (void) fprintf(fp,"Node%ld  [label=\"%s \"];\n",i,bAig_NodeReadName(manager, i));
  }
  for (i=bAigFirstNodeIndex ; i< manager->nodesArraySize ; i+=bAigNodeSize){
    if (rightChild(i) != bAig_NULL){
      if (bAig_IsInverted(rightChild(i))){
        (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",bAig_NonInvertedEdge(rightChild(i)), i);
      }
      else{
        (void) fprintf(fp,"Node%ld -> Node%ld;\n",bAig_NonInvertedEdge(rightChild(i)), i);
      }
      if (bAig_IsInverted(leftChild(i))){
        (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",bAig_NonInvertedEdge(leftChild(i)), i);
      }
      else{
        (void) fprintf(fp,"Node%ld -> Node%ld;\n",bAig_NonInvertedEdge(leftChild(i)), i);
      }
    }/* if */ 
  }/*for */

  (void) fprintf(fp, "}\n");

  return 1;
}



void 
bAigSetPassFlag(
    bAig_Manager_t  *manager,
    bAigEdge_t node)
{

   flags(node) |= CanonicalBitMask;
}

void 
bAigResetPassFlag(
    bAig_Manager_t  *manager,
    bAigEdge_t node)
{

   flags(node) &= ResetCanonicalBitMask;
}

int
bAigGetPassFlag(
    bAig_Manager_t  *manager,
    bAigEdge_t node)
   
{

  return((flags(node) & CanonicalBitMask) != 0);
}



bAigEdge_t
bAigCreateAndNode(
   bAig_Manager_t  *manager,
   bAigEdge_t node1,
   bAigEdge_t node2)
{
   
  bAigEdge_t varIndex;
  char       *name = NIL(char);
  char       *node1Str = util_inttostr(node1);
  char       *node2Str = util_inttostr(node2);

  name = util_strcat4("Nd", node1Str,"_", node2Str);
  while (st_lookup(manager->SymbolTable, name, &varIndex)){
    printf("Find redundant node at %ld %ld\n", node1, node2);
    name = util_strcat3(name, node1Str, node2Str);
  }
  FREE(node1Str);
  FREE(node2Str);
  varIndex = bAig_CreateNode(manager, node1, node2);
  if (varIndex == bAig_NULL){
    FREE(name);
    return (varIndex);
  } 
  /* Insert the varaible in the Symbol Table */
  st_insert(manager->SymbolTable, name, (char*) (long) varIndex);
  manager->nameList[bAigNodeID(varIndex)] = name; 

  return(varIndex);

}

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

static void
connectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to,
   int inputIndex)
{
  bAigEdge_t *pfan;
  int nfan;

  to = bAig_NonInvertedEdge(to);
  pfan = (bAigEdge_t *)fanout(from);
  nfan = nFanout(from);
  if(nfan == 0) pfan = ALLOC(bAigEdge_t, 2);
  else          pfan = REALLOC(bAigEdge_t, pfan, nfan+2);
  to += bAig_IsInverted(from);
  to = to << 1;
  to += inputIndex;
  pfan[nfan++] = to;
  pfan[nfan] = 0;
  fanout(from) = (long)pfan;
  nFanout(from) = nfan;
}


static bAigEdge_t
HashTableLookup(
  bAig_Manager_t *manager,  
  bAigEdge_t  node1,
  bAigEdge_t  node2)
{
  bAigEdge_t key = HashTableFunction(node1, node2);
  bAigEdge_t node;
  
  node = manager->HashTable[key];
  if  (node == bAig_NULL) {
    return bAig_NULL;
  }
  else{
    while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
            (leftChild(bAig_NonInvertedEdge(node))  != node1)) {
  
      if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
        return(bAig_NULL); 
      }
      node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
    } /* While loop */ 
    return(node);

  } /* If Then Else */
    
} /* End of HashTableLookup() */

static int
HashTableAdd(
  bAig_Manager_t   *manager,  
  bAigEdge_t  nodeIndexParent,
  bAigEdge_t  nodeIndex1,
  bAigEdge_t  nodeIndex2)
{
  bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
  bAigEdge_t nodeIndex;
  bAigEdge_t node;
                                                
  nodeIndex = manager->HashTable[key];
  if  (nodeIndex == bAig_NULL) {
    manager->HashTable[key] = nodeIndexParent;
    return TRUE;
  }
  else{
    node = nodeIndex;
    nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));  /* Get the Node */
    while (nodeIndex != bAig_NULL) {
      node = nodeIndex;
      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
    }
    next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
    return TRUE;
  }
    
} /* End of HashTableAdd() */


static int
HashTableDelete(
  bAig_Manager_t   *manager,  
  bAigEdge_t  node)
{
  bAigEdge_t key = HashTableFunction(leftChild(node), rightChild(node));
  bAigEdge_t nodeIndex;
                                                
  nodeIndex = manager->HashTable[key];
  if (nodeIndex == node) {
    manager->HashTable[key] = next(node);
    return TRUE;
  }
  else{
    while(nodeIndex && next(bAig_NonInvertedEdge(nodeIndex)) != node)
      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));

    next(bAig_NonInvertedEdge(nodeIndex)) = 
        next(bAig_NonInvertedEdge(next(bAig_NonInvertedEdge(nodeIndex))));
    return TRUE;
  }
    
} /* End of HashTableAdd() */


bAigEdge_t
bAig_And4(
           bAig_Manager_t *manager,
           bAigEdge_t l,
           bAigEdge_t r)
{
  int caseIndex, caseSig;
  bAigEdge_t ll, lr, rl, rr;
  bAigEdge_t t1, t2;

  ll = leftChild(l);
  lr = rightChild(l);
  rl = leftChild(r);
  rr = rightChild(r);

  if(bAigCompareNode(l, rl) ||
     bAigCompareNode(l, rr)) {
    return(bAig_And3(manager, l, r));
  }
  else if(bAigCompareNode(r, ll) ||
     bAigCompareNode(r, lr)) {
    return(bAig_And3(manager, r, l));
  }

  if(ll > lr+1) bAigSwap(ll, lr);
  if(rl > rr+1) bAigSwap(rl, rr);

  caseIndex = 0; /* (a b)(c d) */
  if(bAigCompareNode(ll, rl)) {
    if(bAigCompareNode(lr, rr)) {
      caseIndex = 4; /* (a b) (a b) */
    }
    else {
      caseIndex = 1; /* (a b) (a c) */
      if(lr > rr+1) {
        bAigSwap(ll, rl);
        bAigSwap(lr, rr); 
        bAigSwap(l, r); 
      }
    }
  }
  else if(bAigCompareNode(lr, rl)) {
    caseIndex = 2; /* (b a)(a c) */
  }
  else if(bAigCompareNode(lr, rr)) {
    caseIndex = 3; /* (b a)(c a) */
    if(ll > rl+1) {
      bAigSwap(ll, rl);
      bAigSwap(lr, rr); 
      bAigSwap(l, r); 
    }
  }
  else if(bAigCompareNode(ll, rr)) {
    /* (a b)(c a)  */
    bAigSwap(ll, rl);
    bAigSwap(lr, rr); 
    bAigSwap(l, r); 
    caseIndex = 2; /* (c a )(a b) because of c < b */
  }

  caseSig = 0;
  if(bAig_IsInverted(ll)) caseSig += 32;
  if(bAig_IsInverted(lr)) caseSig += 16;
  if(bAig_IsInverted(l))  caseSig += 8;
  if(bAig_IsInverted(rl)) caseSig += 4;
  if(bAig_IsInverted(rr)) caseSig += 2;
  if(bAig_IsInverted(r))  caseSig += 1;
  if(caseIndex == 0) {
    return(bAig_And2(manager, l, r));
  }
  else if(caseIndex == 1) {
    switch(caseSig) {
        case 19 :
        case 17 :
        case 3 :
        case 1 :
        case 55 :
        case 53 :
        case 39 :
        case 37 :
      t1 = bAig_And(manager, lr, bAig_Not(rr));
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 18 :
        case 16 :
        case 2 :
        case 0 :
        case 54 :
        case 52 :
        case 38 :
        case 36 :
      t1 = bAig_And(manager, lr, rr);
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 26 :
        case 24 :
        case 10 :
        case 8 :
        case 62 :
        case 60 :
        case 46 :
        case 44 :
      t1 = bAig_And(manager, bAig_Not(lr), rr);
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 61 :
        case 27 :
        case 25 :
        case 11 :
        case 63 :
        case 47 :
        case 9 :
        case 45 :
      t1 = bAig_And(manager, bAig_Not(lr), bAig_Not(rr));
      t2 = bAig_Or(manager, bAig_Not(ll), t1);
      return(t2);
        case 23 :
        case 21 :
        case 7 :
        case 5 :
        case 51 :
        case 49 :
        case 35 :
        case 33 :
      return(l);
        case 30 :
        case 28 :
        case 14 :
        case 12 :
        case 58 :
        case 56 :
        case 42 :
        case 40 :
      return(r);
        case 22 :
        case 20 :
        case 6 :
        case 4 :
        case 50 :
        case 48 :
        case 34 :
        case 32 :
      return(bAig_Zero);
        case 31 :
        case 29 :
        case 15 :
        case 13 :
        case 59 :
        case 57 :
        case 43 :
        case 41 :
      t1 = bAig_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 2) {
    switch(caseSig) {
        case 35 :
        case 33 :
        case 3 :
        case 1 :
        case 55 :
        case 53 :
        case 23 :
        case 21 :
      t1 = bAig_And(manager, lr, bAig_Not(rr));
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 34 :
        case 32 :
        case 2 :
        case 0 :
        case 54 :
        case 52 :
        case 22 :
        case 20 :
      t1 = bAig_And(manager, lr, rr);
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 42 :
        case 40 :
        case 10 :
        case 8 :
        case 62 :
        case 60 :
        case 30 :
        case 28 :
      t1 = bAig_And(manager, lr, rr);
      t2 = bAig_And(manager, bAig_Not(ll), t1);
      return(t2);
        case 43 :
        case 41 :
        case 11 :
        case 9 :
        case 63 :
        case 61 :
        case 31 :
        case 29 :
      t1 = bAig_And(manager, bAig_Not(ll), bAig_Not(rr));
      t2 = bAig_Or(manager, bAig_Not(lr), t1);
      return(t2);
        case 39 :
        case 37 :
        case 7 :
        case 5 :
        case 51 :
        case 49 :
        case 19 :
        case 17 :
      return(l);
        case 46 :
        case 44 :
        case 14 :
        case 12 :
        case 58 :
        case 56 :
        case 26 :
        case 24 :
      return(r);
        case 38 :
        case 36 :
        case 6 :
        case 4 :
        case 50 :
        case 48 :
        case 18 :
        case 16 :
      return(bAig_Zero);
        case 45 :
        case 15 :
        case 13 :
        case 59 :
        case 57 :
        case 47 :
        case 27 :
        case 25 :
      t1 = bAig_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 3) {
    switch(caseSig) {
        case 37 :
        case 33 :
        case 5 :
        case 1 :
        case 55 :
        case 51 :
        case 23 :
        case 19 :
      t1 = bAig_And(manager, bAig_Not(rl), lr);
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 36 :
        case 32 :
        case 4 :
        case 0 :
        case 54 :
        case 50 :
        case 22 :
        case 18 :
      t1 = bAig_And(manager, rl, lr);
      t2 = bAig_And(manager, ll, t1);
      return(t2);
        case 44 :
        case 40 :
        case 12 :
        case 8 :
        case 62 :
        case 58 :
        case 30 :
        case 26 :
      t1 = bAig_And(manager, rl, lr);
      t2 = bAig_And(manager, bAig_Not(ll), t1);
      return(t2);
        case 45 :
        case 41 :
        case 13 :
        case 9 :
        case 63 :
        case 59 :
        case 31 :
        case 27 :
      t1 = bAig_And(manager, bAig_Not(ll), bAig_Not(rl));
      t2 = bAig_Or(manager, bAig_Not(lr), t1);
      return(t2);
        case 39 :
        case 35 :
        case 7 :
        case 3 :
        case 53 :
        case 49 :
        case 21 :
        case 17 :
      return(l);
        case 46 :
        case 42 :
        case 14 :
        case 10 :
        case 60 :
        case 56 :
        case 28 :
        case 24 :
      return(r);
        case 38 :
        case 34 :
        case 6 :
        case 2 :
        case 52 :
        case 48 :
        case 20 :
        case 16 :
      return(bAig_Zero);
        case 47 :
        case 43 :
        case 15 :
        case 11 :
        case 61 :
        case 57 :
        case 29 :
        case 25 :
      t1 = bAig_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 4) {
    switch(caseSig) {
        case 22 :
        case 20 :
        case 6 :
        case 4 :
        case 50 :
        case 48 :
        case 34 :
        case 32 :
        case 2 :
        case 16 :
        case 52 :
        case 1 :
        case 8 :
        case 19 :
        case 26 :
        case 37 :
        case 44 :
        case 38 :
        case 55 :
        case 62 :
      return(bAig_Zero);
        case 0 :
        case 18 :
        case 36 :
        case 54 :
        case 9 :
        case 27 :
        case 45 :
        case 63 :
        case 5 :
        case 23 :
        case 33 :
        case 51 :
        case 3 :
        case 17 :
        case 49 :
        case 7 :
        case 35 :
        case 21 :
        case 39 :
        case 53 :
      return(l);
        case 40 :
        case 58 :
        case 12 :
        case 30 :
        case 24 :
        case 10 :
        case 14 :
        case 56 :
        case 28 :
        case 42 :
        case 60 :
        case 46 :
      return(r);
        case 11 :
        case 47 :
        case 25 :
        case 61 :
      return(bAig_Not(ll));
        case 41 :
        case 59 :
        case 13 :
        case 31 :
      return(bAig_Not(lr));
        case 15 :
      t1 = bAig_And(manager, ll, bAig_Not(lr));
      t2 = bAig_And(manager, bAig_Not(ll), lr);
      return(bAig_Not(bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
        case 57 :
      t1 = bAig_And(manager, rl, bAig_Not(rr));
      t2 = bAig_And(manager, bAig_Not(rl), rr);
      return(bAig_Not(bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
        case 29 :
      t1 = bAig_And(manager, ll, lr);
      t2 = bAig_And(manager, bAig_Not(ll), bAig_Not(lr));
      return((bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
        case 43 :
      t1 = bAig_And(manager, rl, rr);
      t2 = bAig_And(manager, bAig_Not(rl), bAig_Not(rr));
      return((bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
    }
  }
  return(0);
}


bAigEdge_t
bAig_And3(
           bAig_Manager_t *manager,
           bAigEdge_t l,
           bAigEdge_t r)
{
  int caseIndex, caseSig;
  bAigEdge_t rl, rr;

  rl = leftChild(r);
  rr = rightChild(r);

  caseIndex = 0; /* (a)(b c) */
  if(bAigCompareNode(l, rl)) {
    caseIndex = 1; /* (a)(a b) */
  }
  else if(bAigCompareNode(l, rr)) {
    caseIndex = 2; /* (a)(b a) */
  }

  caseSig = 0;
  if(bAig_IsInverted(l))  caseSig += 8;
  if(bAig_IsInverted(rl)) caseSig += 4;
  if(bAig_IsInverted(rr)) caseSig += 2;
  if(bAig_IsInverted(r))  caseSig += 1;
  if(caseIndex == 0) {
    return(bAig_And2(manager, l, r));
  }
  else if(caseIndex == 1) {
    switch(caseSig) {
        case 2 :
        case 0 :
        case 14 :
        case 12 :
      return(r);
        case 10 :
        case 8 :
        case 6 :
        case 4 :
      return(bAig_Zero);
        case 3 :
        case 1 :
        case 15 :
        case 13 :
      return(bAig_And(manager, rl, bAig_Not(rr)));
        case 11 :
        case 9 :
        case 7 :
        case 5 :
      return(l);
    }
  }
  else if(caseIndex == 2) {
    switch(caseSig) {
        case 4 :
        case 0 :
        case 14 :
        case 10 :
      return(r);
        case 12 :
        case 8 :
        case 6 :
        case 2 :
      return(bAig_Zero);
        case 5 :
        case 1 :
        case 15 :
        case 11 :
      return(bAig_And(manager, bAig_Not(rl), rr));
        case 13 :
        case 9 :
        case 7 :
        case 3 :
      return(l);
    }
  }
  return(0);
}

void
bAig_SetMaskTransitiveFanin(
        bAig_Manager_t *manager,
        int v,
        unsigned int mask)
{
  if(v == 2)    return;


  if(flags(v) & mask)   return;

  flags(v) |= mask;

  bAig_SetMaskTransitiveFanin(manager, leftChild(v), mask);
  bAig_SetMaskTransitiveFanin(manager, rightChild(v), mask);
}

void
bAig_ResetMaskTransitiveFanin(
        bAig_Manager_t *manager,
        int v,
        unsigned int mask,
        unsigned int resetMask)
{
  if(v == 2)    return;


  if(!(flags(v) & mask))        return;

  flags(v) &= resetMask;
  bAig_ResetMaskTransitiveFanin(manager, leftChild(v), mask, resetMask);
  bAig_ResetMaskTransitiveFanin(manager, rightChild(v), mask, resetMask);
}


int
bAig_GetValueOfNode(bAig_Manager_t *manager, bAigEdge_t v)
{
  unsigned int value, lvalue, rvalue;
  bAigEdge_t left, right;


  /*
  if(!(flags(v) & CoiMask))     return(2);
  **/
  if(v == 2)    return(2);

  value = aig_value(v);
  if(value == 3)        return(2);
  if(value == 2) {
    left = bAig_GetCanonical(manager, leftChild(v));
    lvalue = bAig_GetValueOfNode(manager, left);
    if(lvalue == 0)     {
      value = 0;
    }
    else {
      right = bAig_GetCanonical(manager, rightChild(v));
      rvalue = bAig_GetValueOfNode(manager, right);
      if(rvalue == 0) {
        value = 0;
      }
      else if(rvalue == 1 && lvalue == 1) {
        value = 1;
      }
      else {
        value = 2;
      }
    }
  }

  if(value == 2) {
    aig_value(v) = 3;
    return(value);
  }
  else  {       
    aig_value(v) = value;
    return(value ^ bAig_IsInverted(v));
  }
}