/**CFile***********************************************************************

  FileName    [baigBddSweep.c]

  PackageName [baig]

  Synopsis    [Functions to find functional equivalent node index using bdd sweeping.]

  Author      [HoonSang Jin]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "maig.h"
#include "ntk.h"
#include "cmd.h"
#include "baig.h"
#include "baigInt.h"
#include "heap.h"
#include "ntmaig.h"
#include "ord.h"

static char rcsid[] UNUSED = "$Id: baigBddSweep.c,v 1.13 2005/05/18 18:11:42 jinh Exp $";

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


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


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


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

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


/**AutomaticStart*************************************************************/

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

static int SweepBddCompare(const char *x, const char *y);
static int SweepBddHash(char *x, int size);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
void bAig_BuildAigBFSManner( Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep);
void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray);
void bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray);

/**Function********************************************************************

  Synopsis    [Compare function for BDD sweeping]

  Description [Compare function for BDD sweeping]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
SweepBddCompare(const char *x, const char *y)
{
  return(bdd_ptrcmp((bdd_t *)x, (bdd_t *)y));
}

/**Function********************************************************************

  Synopsis    [Hashing function for BDD sweeping]

  Description [Hashing function for BDD sweeping]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
SweepBddHash(char *x, int size)
{

  return(bdd_ptrhash((bdd_t *)x, size));
}

/**Function********************************************************************

  Synopsis    [BDD sweeping for aig nodes]

  Description [BDD sweeping for aig nodes rooted at latch data inputs and 
               primary outputs]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray)
{
  array_t *mVarList, *bVarList;
  bdd_t *bdd, *func;
  int bddIdIndex;
  int i, count, sizeLimit, mvfSize;
  int maxSize, curSize;
  array_t *tnodeArray;
  lsGen gen;
  st_generator *gen1;
  Ntk_Node_t *node;
  bAigEdge_t v;
  MvfAig_Function_t  *mvfAig;
  mAig_Manager_t *manager;
  mdd_manager *mgr;
  st_table *node2MvfAigTable;
  st_table * bdd2vertex;
  mAigMvar_t mVar;
  mAigBvar_t bVar;
  int index1, mAigId;


  manager = Ntk_NetworkReadMAigManager(network);

  mgr = Ntk_NetworkReadMddManager(network);
  if(mgr == 0) {
    Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 
	    Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 
	    Ord_Unassigned_c, 0, 0);
    mgr = Ntk_NetworkReadMddManager(network);
  }
  node2MvfAigTable = 
      (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);

  bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);

  sizeLimit = 500;
  maxSize = manager->nodesArraySize;

  tnodeArray = 0;
  if(nodeArray == 0) {
    bVarList = mAigReadBinVarList(manager);
    mVarList = mAigReadMulVarList(manager);
    tnodeArray = array_alloc(bAigEdge_t, 0);
    Ntk_NetworkForEachLatch(network, gen, node) { 
      node = Ntk_LatchReadDataInput(node);
      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i<mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
	array_insert_last(bAigEdge_t, tnodeArray, v);
      }

      mAigId = Ntk_NodeReadMAigId(node);
      mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
      for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
        bVar = array_fetch(mAigBvar_t, bVarList, index1++);
        v = bVar.node;
        v = bAig_GetCanonical(manager, v);
	array_insert_last(bAigEdge_t, tnodeArray, v);
      }
    }
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 
      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i<mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
	array_insert_last(bAigEdge_t, tnodeArray, v);
      }
    }
  }

  count = bAigNodeID(manager->nodesArraySize);
  for(i=0; i<count; i++) {
    manager->bddIdArray[i] = -1;
    manager->bddArray[i] = 0;
  }
  manager->bddArray[0] = bdd_zero(mgr);

  bddIdIndex = 0;
  for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
    if(leftChild(i) != 2)	continue;
    bdd = bdd_get_variable(mgr, bddIdIndex);
    manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
    manager->bddArray[bAigNodeID(i)] = bdd;
    bddIdIndex++;
  }

  if(nodeArray) {
    for(i=0; i<array_n(nodeArray); i++) {
      v = array_fetch(bAigEdge_t, nodeArray, i);
      v = bAig_GetCanonical(manager, v);
      bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
    }
  }
  else {
    for(i=0; i<array_n(tnodeArray); i++) {
      v = array_fetch(bAigEdge_t, tnodeArray, i);
      v = bAig_GetCanonical(manager, v);
      bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
    }
    array_free(tnodeArray);
  }
  
  count = bAigNodeID(manager->nodesArraySize);
  for(i=0; i<count; i++) {
    if(manager->bddArray[i])	{
      bdd_free(manager->bddArray[i]);
      manager->bddArray[i] = 0;
    }
  }

  st_foreach_item(bdd2vertex, gen1, &func, &v) {
    bdd_free(func);
  }
  st_free_table(bdd2vertex);

  count = bAigNodeID(manager->nodesArraySize);
  curSize = 0;
  for(i=0; i<count; i++) {
    if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
      curSize++;
    }
  }
  /*
  fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 
	  maxSize/bAigNodeSize, count, (maxSize-curSize)/bAigNodeSize);
  fflush(vis_stdout);
  */
  return;

}

/**Function********************************************************************

  Synopsis    [Auxiliary function for BDD sweeping]

  Description [Auxiliary function for BDD sweeping]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_BddSweepSub(
	bAig_Manager_t *manager, 
	mdd_manager *mgr, 
	bAigEdge_t v, 
	st_table *bdd2vertex,
	int sizeLimit,
	int *newBddIdIndex)
{
  bAigEdge_t left, right, oldV, nv;
  bdd_t *leftBdd, *rightBdd;
  bdd_t *func, *nfunc, *funcBar, *newBdd;
  int newId, size;

  if(v == 0 || v == 1)	return;
  if(manager->bddArray[bAigNodeID(v)]) {
    return;
  }

  left = leftChild(v);
  right = rightChild(v);
  left = bAig_GetCanonical(manager, left);
  right = bAig_GetCanonical(manager, right);

  if(left == 2 && right == 2) {
    return;
  }

  bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
  bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);

  v = bAig_GetCanonical(manager, v);
  if(manager->bddArray[bAigNodeID(v)]) {
    return;
  }

  left = leftChild(v);
  right = rightChild(v);
  left = bAig_GetCanonical(manager, left);
  right = bAig_GetCanonical(manager, right);

  leftBdd = manager->bddArray[bAigNodeID(left)];
  rightBdd = manager->bddArray[bAigNodeID(right)];

  if(leftBdd == 0) {
    bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
    left = bAig_GetCanonical(manager, left);
    leftBdd = manager->bddArray[bAigNodeID(left)];
  }

  if(rightBdd == 0) {
    bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
    right = bAig_GetCanonical(manager, right);
    rightBdd = manager->bddArray[bAigNodeID(right)];
  }

  /**
  bAig_VerifyBddArray(manager, leftBdd, left);
  bAig_VerifyBddArray(manager, rightBdd, right);
  **/

  if(leftBdd == 0 || rightBdd == 0) {
    fprintf(vis_stdout, 
	    "ERROR : all the nodes should have bdd node at this moment\n");
  }

  func = bdd_and(leftBdd, rightBdd, 
	     !bAig_IsInverted(left), !bAig_IsInverted(right));

  if(bAig_IsInverted(v))	{
    funcBar = bdd_not(func);
    nfunc = funcBar;
  }
  else {
    nfunc = bdd_dup(func);
  }

  if(st_lookup(bdd2vertex, nfunc, &oldV)) {
    bAig_Merge(manager, oldV, v);
  }
  else {
    funcBar = bdd_not(nfunc);
    if(st_lookup(bdd2vertex, funcBar, &oldV)) {
      bAig_Merge(manager, bAig_Not(oldV), v);
    }
    bdd_free(funcBar);
  }
  bdd_free(nfunc);

  v = bAig_NonInvertedEdge(v);
  nv = bAig_GetCanonical(manager, v);
  v = nv;

  if(manager->bddArray[bAigNodeID(v)] == 0) {
    size = bdd_size(func);
    if(size > sizeLimit) {
      newId = *newBddIdIndex;
      (*newBddIdIndex) ++;
      newBdd = bdd_get_variable(mgr, newId);
      manager->bddIdArray[bAigNodeID(v)] = newId;
      bdd_free(func);
      func = newBdd;
      manager->bddArray[bAigNodeID(v)] = func;
      st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v));
    }
    else {
      if(bAig_IsInverted(v)) {
        funcBar = bdd_not(func);
        manager->bddArray[bAigNodeID(v)] = funcBar;
        st_insert(bdd2vertex, (char *)func, (char *)v);
      }
      else {
        manager->bddArray[bAigNodeID(v)] = func;
        st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v);
      }
    }
  }
  else 	bdd_free(func);

}

/**Function********************************************************************

  Synopsis    [Build aig nodes in breath first manner]

  Description [Build aig nodes in breath first manner]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_BuildAigBFSManner(
	Ntk_Network_t *network, 
	mAig_Manager_t *manager, 
	st_table *leaves,
	int sweep)
{
array_t *nodeArray, *result;
lsGen gen1;
int iter, maxLevel, level;
int i, j, k;
bAigEdge_t v;
Ntk_Node_t *node, *fanin, *fanout;
st_table *node2mvfAigTable;
array_t *curArray, *nextArray, *tmpArray;
array_t *levelArray, *clevelArray;
MvfAig_Function_t  *mvfAig;
int mvfSize;
st_generator *gen;

  Ntk_NetworkForEachNode(network, gen1, node) {
    Ntk_NodeSetUndef(node, (void *)0);
  }

  curArray = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(leaves, gen, &node, &fanout) {
    array_insert_last(Ntk_Node_t *, curArray, node);
    Ntk_NodeSetUndef(node, (void *)1);
  }

  levelArray = array_alloc(array_t *, 10);
  nextArray = array_alloc(Ntk_Node_t *, 0);
  iter = 0;
  while(1) {
    clevelArray = array_alloc(array_t *, 10);
    array_insert_last(array_t *, levelArray, clevelArray);
    for(i=0; i<array_n(curArray); i++) {
      node = array_fetch(Ntk_Node_t *, curArray, i);
      Ntk_NodeForEachFanout(node, j, fanout) {  

	level = (int)(long)Ntk_NodeReadUndef(fanout);
	if(level > 0)	continue;

	maxLevel = 0;
	Ntk_NodeForEachFanin(fanout, k, fanin) {
	  level = (int)(long)Ntk_NodeReadUndef(fanin);
	  if(level == 0) {
	    maxLevel = 0;
	    break;
	  }
	  else if(level > maxLevel) {
	    maxLevel = level;
	  }
	}

	if(maxLevel > 0) {
          Ntk_NodeSetUndef(fanout, (void *)(long)(maxLevel+1));
	  array_insert_last(Ntk_Node_t *, nextArray, fanout);
	  array_insert_last(Ntk_Node_t *, clevelArray, fanout);
	}
      }
    }
    
    curArray->num = 0;
    tmpArray = curArray;
    curArray = nextArray;
    nextArray = tmpArray;
    if(curArray->num == 0)	break;

    iter++;
  }

  Ntk_NetworkForEachNode(network, gen1, node) {
    Ntk_NodeSetUndef(node, (void *)0);
  }

  for(i=0; i<array_n(levelArray); i++) {
    clevelArray = array_fetch(array_t *, levelArray, i);
    result = ntmaig_NetworkBuildMvfAigs(network, clevelArray, leaves);
    MvfAig_FunctionArrayFree(result);
    node2mvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(
	    network, MVFAIG_NETWORK_APPL_KEY);

    if(i < 50 && sweep) {
      nodeArray = array_alloc(bAigEdge_t, 0);
      for(j=0; j<array_n(clevelArray); j++) {
        node = array_fetch(Ntk_Node_t *, clevelArray, j);
        st_lookup(node2mvfAigTable, node, &mvfAig);
        mvfSize = array_n(mvfAig);
        for(k=0; k<mvfSize; k++){
          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
          array_insert_last(bAigEdge_t, nodeArray, v);
        }
      }

      bAig_BddSweepForceMain(network, nodeArray);
  
      for(j=0; j<array_n(clevelArray); j++) {
        node = array_fetch(Ntk_Node_t *, clevelArray, j);
        st_lookup(node2mvfAigTable, node, &mvfAig);
        mvfSize = array_n(mvfAig);
        for(k=0; k<mvfSize; k++){
          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
          array_insert(bAigEdge_t, nodeArray, v, k);
        }
      }
      array_free(nodeArray);
    }

    array_free(clevelArray);
  }
  array_free(levelArray);
}


/**Function********************************************************************

  Synopsis    [BDD sweeping ]

  Description [BDD sweeping ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray)
{
  array_t *mVarList, *bVarList;
  bdd_t *bdd, *func;
  int bddIdIndex;
  int i, count, sizeLimit, mvfSize;
  int maxSize, curSize;
  array_t *tnodeArray;
  lsGen gen;
  st_generator *gen1;
  Ntk_Node_t *node;
  bAigEdge_t v;
  MvfAig_Function_t  *mvfAig;
  mAig_Manager_t *manager;
  mdd_manager *mgr;
  st_table *node2MvfAigTable;
  st_table * bdd2vertex;
  mAigMvar_t mVar;
  mAigBvar_t bVar;
  int index1, mAigId;
  int newmask, resetNewmask;
  int usedAig;


  manager = Ntk_NetworkReadMAigManager(network);

  mgr = Ntk_NetworkReadMddManager(network);
  if(mgr == 0) {
    Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 
	    Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 
	    Ord_Unassigned_c, 0, 0);
    mgr = Ntk_NetworkReadMddManager(network);
  }
  node2MvfAigTable = 
      (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);

  bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);

  sizeLimit = 500;
  maxSize = manager->nodesArraySize;

  tnodeArray = 0;
  if(nodeArray == 0) {
    bVarList = mAigReadBinVarList(manager);
    mVarList = mAigReadMulVarList(manager);
    tnodeArray = array_alloc(bAigEdge_t, 0);
    Ntk_NetworkForEachLatch(network, gen, node) { 
      node = Ntk_LatchReadDataInput(node);
      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i<mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
	array_insert_last(bAigEdge_t, tnodeArray, v);
      }

      mAigId = Ntk_NodeReadMAigId(node);
      mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
      for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
        bVar = array_fetch(mAigBvar_t, bVarList, index1++);
        v = bVar.node;
        v = bAig_GetCanonical(manager, v);
	array_insert_last(bAigEdge_t, tnodeArray, v);
      }
    }
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 
      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i<mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
	array_insert_last(bAigEdge_t, tnodeArray, v);
      }
    }
  }

  count = bAigNodeID(manager->nodesArraySize);
  for(i=0; i<count; i++) {
    manager->bddIdArray[i] = -1;
    manager->bddArray[i] = 0;
  }
  manager->bddArray[0] = bdd_zero(mgr);

  bddIdIndex = 0;
  for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
    if(leftChild(i) != 2)	continue;
    bdd = bdd_get_variable(mgr, bddIdIndex);
    manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
    manager->bddArray[bAigNodeID(i)] = bdd;
    bddIdIndex++;
  }

  if(nodeArray) {
    for(i=0; i<array_n(nodeArray); i++) {
      v = array_fetch(bAigEdge_t, nodeArray, i);
      v = bAig_GetCanonical(manager, v);
      bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
    }
  }
  else {
    for(i=0; i<array_n(tnodeArray); i++) {
      v = array_fetch(bAigEdge_t, tnodeArray, i);
      v = bAig_GetCanonical(manager, v);
      bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
    }
  }
  
  count = bAigNodeID(manager->nodesArraySize);
  for(i=0; i<count; i++) {
    if(manager->bddArray[i])	{
      bdd_free(manager->bddArray[i]);
      manager->bddArray[i] = 0;
    }
  }

  st_foreach_item(bdd2vertex, gen1, &func, &v) {
    bdd_free(func);
  }
  st_free_table(bdd2vertex);

  count = bAigNodeID(manager->nodesArraySize);
  curSize = 0;
  for(i=0; i<count; i++) {
    if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
      curSize++;
    }
  }


  newmask = 0x00000100;
  resetNewmask = 0xfffffeff;
  if(tnodeArray) {
  for(i=0; i<array_n(tnodeArray); i++) {
    v = array_fetch(int, tnodeArray, i);
    bAig_SetMaskTransitiveFanin(manager, v, newmask);
  }

  usedAig = 0;
  for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
    if(flags(i) & newmask)	usedAig++;
  }

  for(i=0; i<array_n(tnodeArray); i++) {
    v = array_fetch(int, tnodeArray, i);
    bAig_ResetMaskTransitiveFanin(manager, v, newmask, resetNewmask);
  }
  array_free(tnodeArray);
  fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 
	  maxSize/bAigNodeSize, count, usedAig);
  fflush(vis_stdout);
  }

}

/**Function********************************************************************

  Synopsis    [Auxilary function BDD sweeping ]

  Description [Auxilary function BDD sweeping ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_BddSweepForceSub(
	bAig_Manager_t *manager, 
	mdd_manager *mgr, 
	bAigEdge_t v, 
	st_table *bdd2vertex,
	int sizeLimit,
	int *newBddIdIndex)
{
  bAigEdge_t left, right, oldV, nv;
  bdd_t *leftBdd, *rightBdd;
  bdd_t *func, *nfunc, *funcBar, *newBdd;
  int newId, size;

  if(v == 0 || v == 1)	return;
  if(manager->bddArray[bAigNodeID(v)]) {
    return;
  }


  left = leftChild(v);
  right = rightChild(v);
  left = bAig_GetCanonical(manager, left);
  right = bAig_GetCanonical(manager, right);

  if(left == 2 && right == 2) {
    return;
  }

  bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
  bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);

  v = bAig_GetCanonical(manager, v);
  if(manager->bddArray[bAigNodeID(v)]) {
    return;
  }

  left = leftChild(v);
  right = rightChild(v);
  left = bAig_GetCanonical(manager, left);
  right = bAig_GetCanonical(manager, right);

  leftBdd = manager->bddArray[bAigNodeID(left)];
  rightBdd = manager->bddArray[bAigNodeID(right)];

  if(leftBdd == 0) {
    bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
    left = bAig_GetCanonical(manager, left);
    leftBdd = manager->bddArray[bAigNodeID(left)];
  }

  if(rightBdd == 0) {
    bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
    right = bAig_GetCanonical(manager, right);
    rightBdd = manager->bddArray[bAigNodeID(right)];
  }

  /**
  bAig_VerifyBddArray(manager, leftBdd, left);
  bAig_VerifyBddArray(manager, rightBdd, right);
  **/

  if(leftBdd == 0 || rightBdd == 0) {
    fprintf(vis_stdout, 
	    "ERROR : all the nodes should have bdd node at this moment\n");
  }

  func = bdd_and(leftBdd, rightBdd, 
	     !bAig_IsInverted(left), !bAig_IsInverted(right));

  if(bAig_IsInverted(v))	{
    funcBar = bdd_not(func);
    nfunc = funcBar;
  }
  else {
    nfunc = bdd_dup(func);
  }

  if(st_lookup(bdd2vertex, nfunc, &oldV)) {
    bAig_Merge(manager, oldV, v);
  }
  else {
    funcBar = bdd_not(nfunc);
    if(st_lookup(bdd2vertex, funcBar, &oldV)) {
      bAig_Merge(manager, bAig_Not(oldV), v);
    }
    bdd_free(funcBar);
  }
  bdd_free(nfunc);

  v = bAig_NonInvertedEdge(v);
  nv = bAig_GetCanonical(manager, v);
  v = nv;

  if(manager->bddArray[bAigNodeID(v)] == 0) {
    size = bdd_size(func);
    if(size > sizeLimit) {
      newId = *newBddIdIndex;
      (*newBddIdIndex) ++;
      newBdd = bdd_get_variable(mgr, newId);
      manager->bddIdArray[bAigNodeID(v)] = newId;
      bdd_free(func);
      func = newBdd;
      manager->bddArray[bAigNodeID(v)] = func;
      st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v));
    }
    else {
      if(bAig_IsInverted(v)) {
        funcBar = bdd_not(func);
        manager->bddArray[bAigNodeID(v)] = funcBar;
        st_insert(bdd2vertex, (char *)func, (char *)v);
      }
      else {
        manager->bddArray[bAigNodeID(v)] = func;
        st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v);
      }
    }
  }
  else 	bdd_free(func);

  return;
}