VIS
|
#include "vm.h"
#include "baig.h"
#include "baigInt.h"
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 $" |
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; }
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; }
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); }
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); }
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() */
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); }
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); } }
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) ); }
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); }
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); }
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)); } }
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; }
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); }
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)];
}
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)))); }
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; }
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); }
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); }
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); }
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); }
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) ); }
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); }
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);
}
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; }
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; }
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() */
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() */
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() */
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.