VIS

src/baig/baigNode.c File Reference

#include "vm.h"
#include "baig.h"
#include "baigInt.h"
Include dependency graph for baigNode.c:

Go to the source code of this file.

Functions

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)
nameType_t * bAig_NodeReadName (bAig_Manager_t *manager, bAigEdge_t node)
void bAig_NodeSetName (bAig_Manager_t *manager, bAigEdge_t node, nameType_t *name)
int bAig_NodeReadIndexOfRightChild (bAig_Manager_t *manager, bAigEdge_t nodeIndex)
bAigEdge_t bAig_NodeReadIndexOfLeftChild (bAig_Manager_t *manager, bAigEdge_t nodeIndex)
bAigEdge_t bAig_GetCanonical (bAig_Manager_t *manager, bAigEdge_t nodeIndex)
int bAig_Merge (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
void bAig_PrintNode (bAig_Manager_t *manager, bAigEdge_t i)
bAigEdge_t bAig_And (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_And2 (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_Or (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_Xor (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_Eq (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_Then (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_CreateNode (bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2)
bAigEdge_t bAig_FindNodeByName (bAig_Manager_t *manager, nameType_t *name)
bAigEdge_t bAig_CreateVarNode (bAig_Manager_t *manager, nameType_t *name)
int bAig_isVarNode (bAig_Manager_t *manager, bAigEdge_t node)
bAigEdge_t bAig_bddTobAig (bAig_Manager_t *bAigManager, bdd_t *fn)
int bAig_PrintDot (FILE *fp, bAig_Manager_t *manager)
void bAigSetPassFlag (bAig_Manager_t *manager, bAigEdge_t node)
void bAigResetPassFlag (bAig_Manager_t *manager, bAigEdge_t node)
int bAigGetPassFlag (bAig_Manager_t *manager, bAigEdge_t node)
bAigEdge_t bAigCreateAndNode (bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2)
bAigEdge_t bAig_And4 (bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r)
bAigEdge_t bAig_And3 (bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r)
void bAig_SetMaskTransitiveFanin (bAig_Manager_t *manager, int v, unsigned int mask)
void bAig_ResetMaskTransitiveFanin (bAig_Manager_t *manager, int v, unsigned int mask, unsigned int resetMask)
int bAig_GetValueOfNode (bAig_Manager_t *manager, bAigEdge_t v)

Variables

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

Function Documentation

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

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 []

Definition at line 353 of file baigNode.c.

{

  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;

}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_And2 ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex1,
bAigEdge_t  nodeIndex2 
)

Function********************************************************************

Synopsis [Structural hashing for and2]

Description [Structural hashing for and2]

SideEffects []

SeeAlso []

Definition at line 420 of file baigNode.c.

{
  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;

}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_And3 ( bAig_Manager_t *  manager,
bAigEdge_t  l,
bAigEdge_t  r 
)

Function********************************************************************

Synopsis [Structural hasing for and3]

Description [Structural hasing for and3]

SideEffects []

SeeAlso []

Definition at line 1620 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_And4 ( bAig_Manager_t *  manager,
bAigEdge_t  l,
bAigEdge_t  r 
)

Function********************************************************************

Synopsis [Structural hasing for and4]

Description [Structural hasing for and4]

SideEffects []

SeeAlso []

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

Definition at line 1183 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_bddTobAig ( bAig_Manager_t *  bAigManager,
bdd_t *  fn 
)

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 []

Definition at line 714 of file baigNode.c.

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

Here is the call graph for this function:

bAigEdge_t bAig_CreateNode ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex1,
bAigEdge_t  nodeIndex2 
)

Function********************************************************************

Synopsis [create new node]

Description []

SideEffects []

SeeAlso []

Definition at line 584 of file baigNode.c.

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

Here is the caller graph for this function:

bAigEdge_t bAig_CreateVarNode ( bAig_Manager_t *  manager,
nameType_t *  name 
)

Function********************************************************************

Synopsis [create var node ]

Description []

SideEffects []

SeeAlso []

Definition at line 656 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_Eq ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex1,
bAigEdge_t  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 []

Definition at line 538 of file baigNode.c.

{
 return bAig_Not(
            bAig_Xor(manager, nodeIndex1, nodeIndex2)
            );
}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_FindNodeByName ( bAig_Manager_t *  manager,
nameType_t *  name 
)

Function********************************************************************

Synopsis [Return the bAig node given its name.]

SideEffects []

Definition at line 629 of file baigNode.c.

{
   
  bAigEdge_t node;

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

  return bAig_GetCanonical(manager, node);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_GetCanonical ( bAig_Manager_t *  manager,
bAigEdge_t  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 []

Definition at line 141 of file baigNode.c.

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

Here is the call graph for this function:

int bAig_GetValueOfNode ( bAig_Manager_t *  manager,
bAigEdge_t  v 
)

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 []

Definition at line 1768 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int bAig_isVarNode ( bAig_Manager_t *  manager,
bAigEdge_t  node 
)

Function********************************************************************

Synopsis [Return True if this node is Variable node]

SideEffects []

Definition at line 687 of file baigNode.c.

{
  if((rightChild(node) == bAig_NULL) && (leftChild(node) == bAig_NULL)) {
    return 1;
  }
  return 0;
}

Here is the caller graph for this function:

int bAig_Merge ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex1,
bAigEdge_t  nodeIndex2 
)

Function********************************************************************

Synopsis [Merge two functionally equivalent node.]

Description [This function merges the equivalent two nodes. ]

SideEffects []

SeeAlso []

Definition at line 175 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_NodeReadIndexOfLeftChild ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex 
)

Function********************************************************************

Synopsis [Returns the index of the left node.]

Description []

SideEffects []

SeeAlso []

Definition at line 122 of file baigNode.c.

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

Function********************************************************************

Synopsis [Returns the index of the right node.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file baigNode.c.

{
  return rightChild(nodeIndex);
}
nameType_t* bAig_NodeReadName ( bAig_Manager_t *  manager,
bAigEdge_t  node 
)

AutomaticEnd Function********************************************************************

Synopsis [Read Node's name.]

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

SideEffects []

SeeAlso []

Definition at line 61 of file baigNode.c.

{
  return manager->nameList[bAigNodeID(node)];
}

Here is the caller graph for this function:

void bAig_NodeSetName ( bAig_Manager_t *  manager,
bAigEdge_t  node,
nameType_t *  name 
)

Function********************************************************************

Synopsis [Set Node's name.]

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

SideEffects []

SeeAlso []

Definition at line 80 of file baigNode.c.

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

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 []

Definition at line 491 of file baigNode.c.

{
  return ( bAig_Not(bAig_And(manager,  bAig_Not(nodeIndex1),  bAig_Not(nodeIndex2))));
}

Here is the call graph for this function:

Here is the caller graph for this function:

int bAig_PrintDot ( FILE *  fp,
bAig_Manager_t *  manager 
)

Function********************************************************************

Synopsis [Print dot file for AIG nodes]

SideEffects []

Definition at line 824 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void bAig_PrintNode ( bAig_Manager_t *  manager,
bAigEdge_t  i 
)

Function********************************************************************

Synopsis [Print node information.]

Description [Print node information.]

SideEffects []

SeeAlso []

Definition at line 311 of file baigNode.c.

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

Here is the call graph for this function:

void bAig_ResetMaskTransitiveFanin ( bAig_Manager_t *  manager,
int  v,
unsigned int  mask,
unsigned int  resetMask 
)

Function********************************************************************

Synopsis [Reset mask for transitive fanin nodes]

Description [Reset mask for transitive fanin nodes]

SideEffects []

SeeAlso []

Definition at line 1738 of file baigNode.c.

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

Here is the caller graph for this function:

void bAig_SetMaskTransitiveFanin ( bAig_Manager_t *  manager,
int  v,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Set mask for transitive fanin nodes]

Description [Set mask for transitive fanin nodes]

SideEffects []

SeeAlso []

Definition at line 1710 of file baigNode.c.

{
  if(v == 2)    return;


  if(flags(v) & mask)   return;

  flags(v) |= mask;

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

Here is the caller graph for this function:

bAigEdge_t bAig_Then ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex1,
bAigEdge_t  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 []

Definition at line 562 of file baigNode.c.

{
 return bAig_Or(manager,
                bAig_Not(nodeIndex1),
                nodeIndex2);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAig_Xor ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndex1,
bAigEdge_t  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 []

Definition at line 513 of file baigNode.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t bAigCreateAndNode ( bAig_Manager_t *  manager,
bAigEdge_t  node1,
bAigEdge_t  node2 
)

Function********************************************************************

Synopsis [Create AND node and assign name to it ]

Description []

SideEffects []

SeeAlso []

Definition at line 940 of file baigNode.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

int bAigGetPassFlag ( bAig_Manager_t *  manager,
bAigEdge_t  node 
)

Function********************************************************************

Synopsis [Get pass flag for node]

Description []

SideEffects []

SeeAlso []

Definition at line 917 of file baigNode.c.

{

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

Here is the caller graph for this function:

void bAigResetPassFlag ( bAig_Manager_t *  manager,
bAigEdge_t  node 
)

Function********************************************************************

Synopsis [Reset pass flag for node]

Description []

SideEffects []

SeeAlso []

Definition at line 897 of file baigNode.c.

{

   flags(node) &= ResetCanonicalBitMask;
}
void bAigSetPassFlag ( bAig_Manager_t *  manager,
bAigEdge_t  node 
)

Function********************************************************************

Synopsis [Set pass flag for node]

Description []

SideEffects []

SeeAlso []

Definition at line 877 of file baigNode.c.

{

   flags(node) |= CanonicalBitMask;
}

Here is the caller graph for this function:

static void connectOutput ( bAig_Manager_t *  manager,
bAigEdge_t  from,
bAigEdge_t  to,
int  inputIndex 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [Connect fanin fanout of two AIG nodes]

Description []

SideEffects []

SeeAlso []

Definition at line 987 of file baigNode.c.

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

Here is the caller graph for this function:

static int HashTableAdd ( bAig_Manager_t *  manager,
bAigEdge_t  nodeIndexParent,
bAigEdge_t  nodeIndex1,
bAigEdge_t  nodeIndex2 
) [static]

Function********************************************************************

Synopsis [Add a node in the Hash Table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1105 of file baigNode.c.

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

Here is the caller graph for this function:

static int HashTableDelete ( bAig_Manager_t *  manager,
bAigEdge_t  node 
) [static]

Function********************************************************************

Synopsis [Hash table delete]

Description [Hash table delete]

SideEffects []

SeeAlso []

Definition at line 1146 of file baigNode.c.

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

Here is the caller graph for this function:

static bAigEdge_t HashTableLookup ( bAig_Manager_t *  manager,
bAigEdge_t  node1,
bAigEdge_t  node2 
) [static]

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 []

Definition at line 1066 of file baigNode.c.

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

Here is the caller graph for this function:


Variable Documentation

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

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.]

Definition at line 24 of file baigNode.c.