source: vis_dev/vis-2.3/src/baig/baigNode.c @ 64

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

  FileName    [baigNode.c]

  PackageName [baig]

  Synopsis    [Routines to access node data structure of the And/Inverter
               graph.]

  Author      [Mohammad Awedh, 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 "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                                                     */
/*---------------------------------------------------------------------------*/

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

/*---------------------------------------------------------------------------*/
/* 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);

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


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


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

  Synopsis    [Read Node's name.]

  Description [Read the name of a node given its index.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Set Node's name.]

  Description [Set the name of node in Symbol table and name List]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Returns the index of the right node.]

  Description []

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Returns the index of the left node.]

  Description []

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Get canonical node of given node.]

  Description [This function find node index that is functionally equivalent with given node index.]  

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Merge two functionally equivalent node.]

  Description [This function merges the equivalent two nodes. ]

  SideEffects []

  SeeAlso     []

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



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

  Synopsis    [Print node information.]

  Description [Print node information.]

  SideEffects []

  SeeAlso     []

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

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);
}
   

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

  Synopsis    [Performs the Logical AND of two nodes.]

  Description [This function performs the Logical AND of two nodes.  The inputs
               are the indices of the two nodes.  This function returns the index 
               of the result node.]

  SideEffects []

  SeeAlso     []

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

}

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

  Synopsis    [Structural hashing for and2]

  Description [Structural hashing for and2]

  SideEffects []

  SeeAlso     []

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

}


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

  Synopsis    [Performs the Logical OR of two nodes.]

  Description [This function performs the Logical OR of two nodes.  The inputs
               are the indices of the two nodes.  This function returns the index 
               of the result node.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Performs the Logical XOR of two nodes.]

  Description [This function performs the Logical XOR of two nodes.  The inputs
               are the indices of the two nodes.  This function returns the index 
               of the result node.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Performs the Logical Equal ( <--> XNOR) of two nodes.]

  Description [This function performs the Logical XNOR of two nodes.  The inputs
               are the indices of the two nodes.  This function returns the index 
               of the result node.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Performs the Logical Then (--> Implies) of two nodes.]

  Description [This function performs the Logical Implies of two nodes.  The inputs
               are the indices of the two nodes.  This function returns the index 
               of the result node.]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [create new node] 

  Description []

  SideEffects []

  SeeAlso     []

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


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

  Synopsis [Return the bAig node given its name.]

  SideEffects []

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


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

  Synopsis    [create var node ] 

  Description []

  SideEffects []

  SeeAlso     []

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

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

  Synopsis [Return True if this node is Variable node]

  SideEffects []

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



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

  Synopsis [Build the binary AND/INVERTER graph for a given bdd function]

  SideEffects [Build the binary AND/INVERTER graph for a given bdd function.
               We assume that the return bdd nodes from the foreach_bdd_node are
               in the order from childeren to parent. i.e all the childeren
               nodes are returned before the parent node.]

  SideEffects []

  SeeAlso     []
  
******************************************************************************/
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() */


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

  Synopsis [Print dot file for AIG nodes]

  SideEffects []

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



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

  Synopsis    [Set pass flag for node] 

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void 
bAigSetPassFlag(
    bAig_Manager_t  *manager,
    bAigEdge_t node)
{

   flags(node) |= CanonicalBitMask;
}

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

  Synopsis    [Reset pass flag for node] 

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void 
bAigResetPassFlag(
    bAig_Manager_t  *manager,
    bAigEdge_t node)
{

   flags(node) &= ResetCanonicalBitMask;
}

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

  Synopsis    [Get pass flag for node] 

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
bAigGetPassFlag(
    bAig_Manager_t  *manager,
    bAigEdge_t node)
   
{

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



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

  Synopsis    [Create AND node and assign name to it ] 

  Description []

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Connect fanin fanout of two AIG nodes]

  Description []

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [disconnect fanin fanout of two AIG nodes]

  Description []

  SideEffects []

  SeeAlso     []

static void
unconnectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to)
{
   bAigEdge_t cur, *pfan, *newfan;
   int i, nfan;

  from = bAig_NonInvertedEdge(from);
  to = bAig_NonInvertedEdge(to);

  pfan = (bAigEdge_t *)fanout(from);
  nfan = nFanout(from);
  newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
  for(i=0; i<nfan; i++) {
    cur = pfan[i];
    cur = cur >> 1;
    cur = bAig_NonInvertedEdge(cur);
    if(cur == to) {
      memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
      memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
      newfan[nfan-1] = 0;
      fanout(from) = (int)newfan;
      free(pfan);
      nFanout(from) = nfan-1;
      break;
    }
  }
}
******************************************************************************/


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

  Synopsis    [Look for the node in the Hash Table.]

  Description [.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
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() */

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

  Synopsis    [Add a node in the Hash Table.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
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() */


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

  Synopsis    [Hash table delete]

  Description [Hash table delete]

  SideEffects []

  SeeAlso     []

******************************************************************************/
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() */


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

  Synopsis    [Structural hasing for and4]

  Description [Structural hasing for and4]

  SideEffects []

  SeeAlso     []

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

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;
  /**
  fprintf(vis_stdout, "Index: %d Sig: %2d  (%5d%c %5d%c)%c (%5d%c %5d%c)%c (%5d, %5d)\n", 
          caseIndex, caseSig, 
          bAig_NonInvertedEdge(ll), bAig_IsInverted(ll) ? '\'' : ' ',
          bAig_NonInvertedEdge(lr), bAig_IsInverted(lr) ? '\'' : ' ',
          bAig_IsInverted(l) ? '\'' : ' ',
          bAig_NonInvertedEdge(rl), bAig_IsInverted(rl) ? '\'' : ' ',
          bAig_NonInvertedEdge(rr), bAig_IsInverted(rr) ? '\'' : ' ',
          bAig_IsInverted(r) ? '\'' : ' ',
          bAig_NonInvertedEdge(l), bAig_NonInvertedEdge(r)
           );
           **/
  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);
}


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

  Synopsis    [Structural hasing for and3]

  Description [Structural hasing for and3]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Set mask for transitive fanin nodes]

  Description [Set mask for transitive fanin nodes]

  SideEffects []

  SeeAlso     []

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

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

  Synopsis    [Reset mask for transitive fanin nodes]

  Description [Reset mask for transitive fanin nodes]

  SideEffects []

  SeeAlso     []

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


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

   Synopsis [Get value of aig node.]

   Description [The default falue is 2, which is same as UNKNOWN. This value can be assigned from SAT solver.]

   SideEffects []
   
   SeeAlso     []
   
******************************************************************************/

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));
  }
}