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

Last change on this file since 14 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 42.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [baigNode.c]
4
5  PackageName [baig]
6
7  Synopsis    [Routines to access node data structure of the And/Inverter
8               graph.]
9
10  Author      [Mohammad Awedh, HoonSang Jin]
11
12  Copyright [ This file was created at the University of Colorado at
13  Boulder.  The University of Colorado at Boulder makes no warranty
14  about the suitability of this software for any purpose.  It is
15  presented on an AS IS basis.]
16
17
18******************************************************************************/
19
20#include "vm.h"
21#include "baig.h"
22#include "baigInt.h"
23
24static char rcsid[] UNUSED = "$Id: baigNode.c,v 1.33 2009/04/12 00:14:03 fabio Exp $";
25
26/*---------------------------------------------------------------------------*/
27/* Constant declarations                                                     */
28/*---------------------------------------------------------------------------*/
29
30/**AutomaticStart*************************************************************/
31
32/*---------------------------------------------------------------------------*/
33/* Static function prototypes                                                */
34/*---------------------------------------------------------------------------*/
35
36static void connectOutput(bAig_Manager_t *manager, bAigEdge_t from, bAigEdge_t to, int inputIndex);
37static bAigEdge_t HashTableLookup(bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2);
38static int HashTableAdd(bAig_Manager_t *manager, bAigEdge_t nodeIndexParent, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
39static int HashTableDelete(bAig_Manager_t *manager, bAigEdge_t node);
40
41/**AutomaticEnd***************************************************************/
42
43
44/*---------------------------------------------------------------------------*/
45/* Definition of exported functions                                          */
46/*---------------------------------------------------------------------------*/
47
48
49/**Function********************************************************************
50
51  Synopsis    [Read Node's name.]
52
53  Description [Read the name of a node given its index.]
54
55  SideEffects []
56
57  SeeAlso     []
58
59******************************************************************************/
60nameType_t *
61bAig_NodeReadName(
62   bAig_Manager_t *manager,
63   bAigEdge_t     node)
64{
65  return manager->nameList[bAigNodeID(node)];
66}
67
68/**Function********************************************************************
69
70  Synopsis    [Set Node's name.]
71
72  Description [Set the name of node in Symbol table and name List]
73
74  SideEffects []
75
76  SeeAlso     []
77
78******************************************************************************/
79void 
80bAig_NodeSetName(
81   bAig_Manager_t *manager,
82   bAigEdge_t     node,
83   nameType_t     *name)
84{
85  nameType_t *tmpName = manager->nameList[bAigNodeID(node)];
86  FREE(tmpName);
87  st_insert(manager->SymbolTable, name, (char*) (long) node);
88  manager->nameList[bAigNodeID(node)] = name;
89}
90
91/**Function********************************************************************
92
93  Synopsis    [Returns the index of the right node.]
94
95  Description []
96
97  SideEffects []
98
99  SeeAlso     []
100
101******************************************************************************/
102int
103bAig_NodeReadIndexOfRightChild(
104   bAig_Manager_t *manager,
105   bAigEdge_t nodeIndex)
106{
107  return rightChild(nodeIndex);
108}
109
110/**Function********************************************************************
111
112  Synopsis    [Returns the index of the left node.]
113
114  Description []
115
116  SideEffects []
117
118  SeeAlso     []
119
120******************************************************************************/
121bAigEdge_t
122bAig_NodeReadIndexOfLeftChild(
123   bAig_Manager_t *manager,
124   bAigEdge_t nodeIndex)
125{
126  return leftChild(nodeIndex);
127}
128
129/**Function********************************************************************
130
131  Synopsis    [Get canonical node of given node.]
132
133  Description [This function find node index that is functionally equivalent with given node index.] 
134
135  SideEffects []
136
137  SeeAlso     []
138
139******************************************************************************/
140bAigEdge_t
141bAig_GetCanonical(
142    bAig_Manager_t *manager, 
143    bAigEdge_t nodeIndex)
144{
145bAigEdge_t next;
146
147/*if(nodeIndex == bAig_NULL)    return(nodeIndex);*/
148
149//Bing:
150 if(nodeIndex == bAig_NULL||
151    nodeIndex == bAig_One ||
152    nodeIndex == bAig_Zero)
153   return(nodeIndex); 
154
155  while(bAigGetPassFlag(manager, nodeIndex)) {
156    next = canonical(nodeIndex);
157    if(bAig_IsInverted(nodeIndex))  next = bAig_Not(next);
158    nodeIndex = next;
159  }
160  return(nodeIndex);
161}
162
163/**Function********************************************************************
164
165  Synopsis    [Merge two functionally equivalent node.]
166
167  Description [This function merges the equivalent two nodes. ]
168
169  SideEffects []
170
171  SeeAlso     []
172
173******************************************************************************/
174int
175bAig_Merge(
176    bAig_Manager_t *manager,
177    bAigEdge_t nodeIndex1,
178    bAigEdge_t nodeIndex2)
179{
180bAigEdge_t newNodeIndex, nodeIndex, tnodeIndex;
181bAigEdge_t leftIndex, rightIndex;
182bAigEdge_t outIndex, *pfan;
183int id1, id2;
184bAigEdge_t cur;
185bdd_t **bddArray;
186array_t *nodeArray;
187int i, ii, iii;
188long *ManagerNodesArray;
189
190  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
191  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);
192
193  if(nodeIndex1 == nodeIndex2)  return(nodeIndex1);
194
195
196  ManagerNodesArray = manager->NodesArray;
197
198
199  newNodeIndex = nodeIndex1;     
200  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
201    nodeIndex1 = nodeIndex2;
202    nodeIndex2 = newNodeIndex;
203  }
204
205  if(bAig_IsInverted(nodeIndex2)) {
206    nodeIndex1 = bAig_Not(nodeIndex1);
207    nodeIndex2 = bAig_Not(nodeIndex2);
208  }
209
210  nodeArray = array_alloc(bAigEdge_t, 0);
211  nodeIndex = nodeIndex2;
212  array_insert_last(bAigEdge_t, nodeArray, nodeIndex);
213  while(bAig_NonInvertedEdge(canonical(nodeIndex)) != bAig_NonInvertedEdge(nodeIndex2)){
214    if(bAig_IsInverted(nodeIndex))
215      nodeIndex = bAig_Not(canonical(nodeIndex));
216    else
217      nodeIndex = canonical(nodeIndex);
218    array_insert_last(bAigEdge_t, nodeArray, nodeIndex);
219  }
220
221  bAigSetPassFlag(manager, nodeIndex2);
222  nodeIndex = nodeIndex1;
223  while(bAig_NonInvertedEdge(canonical(nodeIndex)) != bAig_NonInvertedEdge(nodeIndex1)) {
224    if(bAig_IsInverted(nodeIndex))
225      nodeIndex = bAig_Not(canonical(nodeIndex));
226    else
227      nodeIndex = canonical(nodeIndex);
228  }
229
230  for(i=0; i<array_n(nodeArray); i++) {
231    tnodeIndex = array_fetch(bAigEdge_t, nodeArray, i);
232    if(bAig_IsInverted(nodeIndex))
233      canonical(nodeIndex) = bAig_Not(tnodeIndex);
234    else 
235      canonical(nodeIndex) = tnodeIndex;
236
237    if(bAig_IsInverted(nodeIndex))
238      nodeIndex = bAig_Not(canonical(nodeIndex));
239    else
240      nodeIndex = canonical(nodeIndex);
241  }
242
243  if(bAig_IsInverted(nodeIndex))        {
244    canonical(nodeIndex) = bAig_Not(nodeIndex1);
245  }
246  else {
247    canonical(nodeIndex) = nodeIndex1;
248  }
249  array_free(nodeArray);
250
251  nodeArray = array_alloc(bAigEdge_t, 0);
252  bAigEdgeForEachFanout(manager, nodeIndex2, cur, ii, iii, pfan) {
253    cur = cur >> 1;
254    cur = bAig_NonInvertedEdge(cur);
255    array_insert_last(bAigEdge_t, nodeArray, cur);
256  }
257
258  for(i=0; i<array_n(nodeArray); i++) {
259    outIndex = array_fetch(bAigEdge_t, nodeArray, i);
260    leftIndex = leftChild(outIndex);
261    rightIndex = rightChild(outIndex);
262
263    HashTableDelete(manager, outIndex);
264
265    newNodeIndex = bAig_And(manager, leftIndex, rightIndex);
266
267    bAig_Merge(manager, newNodeIndex, outIndex);
268
269  }
270  array_free(nodeArray);
271
272  bddArray = manager->bddArray;
273  id1 = bAigNodeID(nodeIndex1);
274  id2 = bAigNodeID(nodeIndex2);
275  if(bddArray[id1] == 0 && bddArray[id2]){ 
276    if(bAig_IsInverted(nodeIndex2)) {
277      if(bAig_IsInverted(nodeIndex1)) {
278        bddArray[id1] = bdd_dup(bddArray[id2]);
279      }
280      else {
281        bddArray[id1] = bdd_not(bddArray[id2]);
282      }
283    }
284    else {
285      if(bAig_IsInverted(nodeIndex1)) {
286        bddArray[id1] = bdd_not(bddArray[id2]);
287      }
288      else {
289        bddArray[id1] = bdd_dup(bddArray[id2]);
290      }
291    }
292  }
293  return(nodeIndex1);
294}
295
296
297
298/**Function********************************************************************
299
300  Synopsis    [Print node information.]
301
302  Description [Print node information.]
303
304  SideEffects []
305
306  SeeAlso     []
307
308******************************************************************************/
309
310void
311bAig_PrintNode(
312  bAig_Manager_t *manager,
313  bAigEdge_t i)
314{
315  int j, size;
316  long cur, *pfan;
317
318  fprintf(vis_stdout, "nodeIndex : %ld (%ld)\n", i, bAigNodeID(i)); 
319  fprintf(vis_stdout, "child     : %ld%c, %ld%c\n", 
320          bAig_NonInvertedEdge(leftChild(i)), bAig_IsInverted(leftChild(i)) ? '\'' : ' ', 
321          bAig_NonInvertedEdge(rightChild(i)), bAig_IsInverted(rightChild(i)) ? '\'' : ' ');
322  fprintf(vis_stdout, "canonical : %s (%ld)\n", 
323          bAigGetPassFlag(manager, i) ? "pass" : "true", bAig_GetCanonical(manager, i));
324  fprintf(vis_stdout, "refCount  : %ld\n", nFanout(i));
325  fprintf(vis_stdout, "          : ");
326  size = nFanout(i);
327  for(j=0, pfan = (bAigEdge_t *)fanout(i); j<size; j++) {
328    cur = pfan[j];
329    cur = cur >> 1;
330    fprintf(vis_stdout, " %ld", cur);
331  }
332  fprintf(vis_stdout, "\n");
333
334  fprintf(vis_stdout, "next      : %ld\n", next(i));
335  fflush(vis_stdout);
336}
337   
338
339/**Function********************************************************************
340
341  Synopsis    [Performs the Logical AND of two nodes.]
342
343  Description [This function performs the Logical AND of two nodes.  The inputs
344               are the indices of the two nodes.  This function returns the index
345               of the result node.]
346
347  SideEffects []
348
349  SeeAlso     []
350
351******************************************************************************/
352bAigEdge_t
353bAig_And(
354   bAig_Manager_t *manager,
355   bAigEdge_t nodeIndex1,
356   bAigEdge_t nodeIndex2)
357{
358
359  bAigEdge_t newNodeIndex;
360
361  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
362  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);
363
364  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
365  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
366    nodeIndex1 = nodeIndex2;
367    nodeIndex2 = newNodeIndex;
368  }
369
370  if ( nodeIndex2 == bAig_Zero ) {
371    return bAig_Zero;
372  }
373  if ( nodeIndex1 == bAig_Zero ) {
374    return bAig_Zero;
375  }
376  if ( nodeIndex2 == bAig_One ) {
377    return nodeIndex1;
378  }
379  if ( nodeIndex1 == bAig_One ) {
380    return nodeIndex2;
381  }
382  if ( nodeIndex1 == nodeIndex2 ) {
383    return nodeIndex1;
384  }
385  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
386    return bAig_Zero;
387  }
388
389  /* Look for the new node in the Hash table */
390  newNodeIndex = HashTableLookup(manager, nodeIndex1, nodeIndex2);
391
392  if (newNodeIndex == bAig_NULL){ 
393    if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
394      newNodeIndex = bAig_And2(manager, nodeIndex1, nodeIndex2);
395    else if(bAigIsVar(manager, nodeIndex1)) 
396      newNodeIndex = bAig_And3(manager, nodeIndex1, nodeIndex2);
397    else if(bAigIsVar(manager, nodeIndex2)) 
398      newNodeIndex = bAig_And3(manager, nodeIndex2, nodeIndex1);
399    else {
400      newNodeIndex = bAig_And4(manager, nodeIndex1, nodeIndex2);
401    }
402  }
403   
404  return newNodeIndex;
405
406}
407
408/**Function********************************************************************
409
410  Synopsis    [Structural hashing for and2]
411
412  Description [Structural hashing for and2]
413
414  SideEffects []
415
416  SeeAlso     []
417
418******************************************************************************/
419bAigEdge_t
420bAig_And2(
421   bAig_Manager_t *manager,
422   bAigEdge_t nodeIndex1,
423   bAigEdge_t nodeIndex2)
424{
425  bAigEdge_t newNodeIndex;
426
427  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
428  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);
429
430  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
431  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
432    nodeIndex1 = nodeIndex2;
433    nodeIndex2 = newNodeIndex;
434  }
435  if ( nodeIndex2 == bAig_Zero ) {
436    return bAig_Zero;
437  }
438  if ( nodeIndex1 == bAig_Zero ) {
439    return bAig_Zero;
440  }
441  if ( nodeIndex2 == bAig_One ) {
442    return nodeIndex1;
443  }
444  if ( nodeIndex1 == bAig_One ) {
445    return nodeIndex2;
446  }
447  if ( nodeIndex1 == nodeIndex2 ) {
448    return nodeIndex1;
449  }
450  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
451    return bAig_Zero;
452  }
453  newNodeIndex = HashTableLookup(manager, nodeIndex1, nodeIndex2);
454
455  if (newNodeIndex == bAig_NULL){ 
456    newNodeIndex = bAigCreateAndNode(manager, nodeIndex1, nodeIndex2) ;
457
458    HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
459    connectOutput(manager, nodeIndex1, newNodeIndex, 0);
460    connectOutput(manager, nodeIndex2, newNodeIndex, 1);
461
462#if 0
463#ifdef LEARNING_
464    tNodeIndex = HashTableLookup(manager, bAig_Not(nodeIndex1), nodeIndex2);
465    if(tNodeIndex) bAig_Learn(manager, nodeIndex1, nodeIndex2);
466
467    tNodeIndex = HashTableLookup(manager, nodeIndex1, bAig_Not(nodeIndex2));
468    if(tNodeIndex) bAig_Learn(manager, nodeIndex2, nodeIndex1);
469#endif
470#endif
471  }
472  return newNodeIndex;
473
474}
475
476
477/**Function********************************************************************
478
479  Synopsis    [Performs the Logical OR of two nodes.]
480
481  Description [This function performs the Logical OR of two nodes.  The inputs
482               are the indices of the two nodes.  This function returns the index
483               of the result node.]
484
485  SideEffects []
486
487  SeeAlso     []
488
489******************************************************************************/
490bAigEdge_t
491bAig_Or(
492   bAig_Manager_t *manager,
493   bAigEdge_t nodeIndex1,
494   bAigEdge_t nodeIndex2)
495{
496  return ( bAig_Not(bAig_And(manager,  bAig_Not(nodeIndex1),  bAig_Not(nodeIndex2))));
497}
498
499/**Function********************************************************************
500
501  Synopsis    [Performs the Logical XOR of two nodes.]
502
503  Description [This function performs the Logical XOR of two nodes.  The inputs
504               are the indices of the two nodes.  This function returns the index
505               of the result node.]
506
507  SideEffects []
508
509  SeeAlso     []
510
511******************************************************************************/
512bAigEdge_t
513bAig_Xor(
514   bAig_Manager_t *manager,
515   bAigEdge_t nodeIndex1,
516   bAigEdge_t nodeIndex2)
517{
518 return bAig_Or(manager,
519            bAig_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
520            bAig_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
521        );
522}
523
524/**Function********************************************************************
525
526  Synopsis    [Performs the Logical Equal ( <--> XNOR) of two nodes.]
527
528  Description [This function performs the Logical XNOR of two nodes.  The inputs
529               are the indices of the two nodes.  This function returns the index
530               of the result node.]
531
532  SideEffects []
533
534  SeeAlso     []
535
536******************************************************************************/
537bAigEdge_t
538bAig_Eq(
539   bAig_Manager_t *manager,
540   bAigEdge_t nodeIndex1,
541   bAigEdge_t nodeIndex2)
542{
543 return bAig_Not(
544            bAig_Xor(manager, nodeIndex1, nodeIndex2)
545            );
546}
547
548/**Function********************************************************************
549
550  Synopsis    [Performs the Logical Then (--> Implies) of two nodes.]
551
552  Description [This function performs the Logical Implies of two nodes.  The inputs
553               are the indices of the two nodes.  This function returns the index
554               of the result node.]
555
556  SideEffects []
557
558  SeeAlso     []
559
560******************************************************************************/
561bAigEdge_t
562bAig_Then(
563   bAig_Manager_t *manager,
564   bAigEdge_t nodeIndex1,
565   bAigEdge_t nodeIndex2)
566{
567 return bAig_Or(manager,
568                bAig_Not(nodeIndex1),
569                nodeIndex2);
570}
571
572/**Function********************************************************************
573
574  Synopsis    [create new node]
575
576  Description []
577
578  SideEffects []
579
580  SeeAlso     []
581
582******************************************************************************/
583bAigEdge_t
584bAig_CreateNode(
585   bAig_Manager_t  *manager,
586   bAigEdge_t nodeIndex1,
587   bAigEdge_t nodeIndex2)
588{
589 
590  bAigEdge_t newNode = manager->nodesArraySize;
591
592  if (manager->nodesArraySize >= manager->maxNodesArraySize ){
593    manager->maxNodesArraySize = 2* manager->maxNodesArraySize;
594    manager->NodesArray = REALLOC(bAigEdge_t, manager->NodesArray, manager->maxNodesArraySize);
595    manager->nameList   = REALLOC(char *,     manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
596    manager->bddIdArray = REALLOC(int ,     manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
597    manager->bddArray   = REALLOC(bdd_t *,     manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
598  }
599  manager->NodesArray[bAig_NonInvertedEdge(newNode)+bAigRight] = nodeIndex2;
600  manager->NodesArray[bAig_NonInvertedEdge(newNode)+bAigLeft]  = nodeIndex1;
601 
602  next(newNode)     = bAig_NULL;
603  fanout(newNode) = 0;
604  canonical(newNode) = newNode;
605  flags(newNode) = 0;
606  nFanout(newNode) = 0;
607  manager->bddIdArray[bAigNodeID(newNode)] = -1; 
608  manager->bddArray[bAigNodeID(newNode)] = 0; 
609
610  manager->nodesArraySize +=bAigNodeSize;
611 
612  //Bing: for interpolation
613  aig_value(newNode) = 2;
614  manager->nameList[bAigNodeID(newNode)] = 0;
615  manager->NodesArray[newNode+bAigClass] = manager->class_;
616 
617  return(newNode);
618}
619
620
621/**Function********************************************************************
622
623  Synopsis [Return the bAig node given its name.]
624
625  SideEffects []
626
627******************************************************************************/
628bAigEdge_t
629bAig_FindNodeByName(
630  bAig_Manager_t *manager,
631  nameType_t     *name)
632{
633   
634  bAigEdge_t node;
635
636  if (!st_lookup(manager->SymbolTable, name, &node)){
637    node = bAig_NULL;
638  }
639
640  return bAig_GetCanonical(manager, node);
641}
642
643
644/**Function********************************************************************
645
646  Synopsis    [create var node ]
647
648  Description []
649
650  SideEffects []
651
652  SeeAlso     []
653
654******************************************************************************/
655bAigEdge_t
656bAig_CreateVarNode(
657   bAig_Manager_t  *manager,
658   nameType_t      *name)
659{
660   
661  bAigEdge_t varIndex;
662
663
664  if (!st_lookup(manager->SymbolTable, name, &varIndex)){
665    varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
666    if (varIndex == bAig_NULL){
667      return (varIndex);
668    } 
669    /* Insert the varaible in the Symbol Table */
670    st_insert(manager->SymbolTable, name, (char*) (long) varIndex);
671    manager->nameList[bAigNodeID(varIndex)] = name; 
672    return(varIndex);
673  }
674  else {
675    return (varIndex);
676  }
677}
678
679/**Function********************************************************************
680
681  Synopsis [Return True if this node is Variable node]
682
683  SideEffects []
684
685******************************************************************************/
686int 
687bAig_isVarNode(
688   bAig_Manager_t *manager,
689   bAigEdge_t      node)
690{
691  if((rightChild(node) == bAig_NULL) && (leftChild(node) == bAig_NULL)) {
692    return 1;
693  }
694  return 0;
695}
696
697
698
699/**Function********************************************************************
700
701  Synopsis [Build the binary AND/INVERTER graph for a given bdd function]
702
703  SideEffects [Build the binary AND/INVERTER graph for a given bdd function.
704               We assume that the return bdd nodes from the foreach_bdd_node are
705               in the order from childeren to parent. i.e all the childeren
706               nodes are returned before the parent node.]
707
708  SideEffects []
709
710  SeeAlso     []
711 
712******************************************************************************/
713bAigEdge_t
714bAig_bddTobAig(
715   bAig_Manager_t *bAigManager,
716   bdd_t          *fn)
717{
718  bdd_gen     *gen;
719  bdd_node    *node, *thenNode, *elseNode, *funcNode;
720  bdd_manager *bddManager = bdd_get_manager(fn);
721  /*
722    Used to read the variable name of a bdd node.
723  */
724  array_t     *mvar_list  = mdd_ret_mvar_list(bddManager);
725  array_t     *bvar_list  = mdd_ret_bvar_list(bddManager);
726  bvar_type   bv;
727  mvar_type   mv;
728 
729  bdd_node    *one        = bdd_read_one(bddManager); 
730  int         is_complemented;
731  int         flag; 
732  bAigEdge_t  var, left, right, result;
733 
734  char      name[100];
735  st_table  *bddTObaigTable;
736 
737  if (fn == NULL){
738    return bAig_NULL;
739  }
740  funcNode = bdd_get_node(fn, &is_complemented);
741  if (bdd_is_constant(funcNode)){
742    return (is_complemented?bAig_Zero:bAig_One);
743  }
744  bddTObaigTable = st_init_table(st_numcmp, st_numhash);
745  st_insert(bddTObaigTable, (char *) (long) bdd_regular(one),  (char *) bAig_One);
746
747  foreach_bdd_node(fn, gen, node){
748    int nodeIndex = bdd_node_read_index(node);
749    int index, rtnNodeIndex;
750
751    if (bdd_is_constant(node)){
752      continue;
753    }
754
755    bv = array_fetch(bvar_type, bvar_list, nodeIndex);
756    /*
757      get the multi-valued varaible.
758     */
759    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
760    arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
761      if (nodeIndex == rtnNodeIndex){
762        break;
763      }
764    }
765    assert(index < mv.encode_length);
766    /*
767    printf("Name of bdd node %s %d\n", mv.name, index);
768    */
769    sprintf(name, "%s_%d", mv.name, index);
770    /*
771      Create or Retrieve the bAigEdge_t  w.r.t. 'name'
772    */
773    var  = bAig_CreateVarNode(bAigManager, util_strsav(name));
774
775    thenNode  = bdd_bdd_T(node);
776    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(thenNode),
777                     &left);
778    assert(flag);
779     
780    elseNode  = bdd_bdd_E(node);
781    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(elseNode),
782                     &right);
783    assert(flag);
784    /*
785     test if the elseNode is complemented arc?
786    */
787    if (bdd_is_complement(elseNode)){
788      right = bAig_Not(right);
789    }
790    if (right ==  bAig_Zero){        /* result = var*then */
791      result =  bAig_And(bAigManager, var, left);
792    } else if (right ==  bAig_One){        /* result = then + not(var) */
793      result =  bAig_Or(bAigManager, left, bAig_Not(var));
794    } else if (left ==  bAig_One) { /* result = var + else */
795      result =  bAig_Or(bAigManager, var, right);     
796    } else {                        /* result = var * then + not(var)*else */
797      result =  bAig_Or(bAigManager, bAig_And(bAigManager, var, left),
798                        bAig_And(bAigManager, bAig_Not(var), right));
799    }
800    st_insert(bddTObaigTable, (char *) (long) bdd_regular(node),
801              (char *) (long) result);
802  }
803  flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(funcNode),
804                   &result); 
805  assert(flag);
806  st_free_table(bddTObaigTable);
807
808  if (is_complemented){
809    return bAig_Not(result);
810  } else {
811    return result;
812  }
813} /* end of bAig_bddtobAig() */
814
815
816/**Function********************************************************************
817
818  Synopsis [Print dot file for AIG nodes]
819
820  SideEffects []
821
822******************************************************************************/
823int
824bAig_PrintDot(
825  FILE *fp,
826  bAig_Manager_t *manager)
827{
828  long i;
829
830  /*
831   * Write out the header for the output file.
832   */
833  (void) fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
834  (void) fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
835  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");
836 
837 
838  for (i=bAigFirstNodeIndex ; i< manager->nodesArraySize ; i+=bAigNodeSize){
839    (void) fprintf(fp,"Node%ld  [label=\"%s \"];\n",i,bAig_NodeReadName(manager, i));
840  }
841  for (i=bAigFirstNodeIndex ; i< manager->nodesArraySize ; i+=bAigNodeSize){
842    if (rightChild(i) != bAig_NULL){
843      if (bAig_IsInverted(rightChild(i))){
844        (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",bAig_NonInvertedEdge(rightChild(i)), i);
845      }
846      else{
847        (void) fprintf(fp,"Node%ld -> Node%ld;\n",bAig_NonInvertedEdge(rightChild(i)), i);
848      }
849      if (bAig_IsInverted(leftChild(i))){
850        (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",bAig_NonInvertedEdge(leftChild(i)), i);
851      }
852      else{
853        (void) fprintf(fp,"Node%ld -> Node%ld;\n",bAig_NonInvertedEdge(leftChild(i)), i);
854      }
855    }/* if */ 
856  }/*for */
857
858  (void) fprintf(fp, "}\n");
859
860  return 1;
861}
862
863
864
865/**Function********************************************************************
866
867  Synopsis    [Set pass flag for node]
868
869  Description []
870
871  SideEffects []
872
873  SeeAlso     []
874
875******************************************************************************/
876void 
877bAigSetPassFlag(
878    bAig_Manager_t  *manager,
879    bAigEdge_t node)
880{
881
882   flags(node) |= CanonicalBitMask;
883}
884
885/**Function********************************************************************
886
887  Synopsis    [Reset pass flag for node]
888
889  Description []
890
891  SideEffects []
892
893  SeeAlso     []
894
895******************************************************************************/
896void 
897bAigResetPassFlag(
898    bAig_Manager_t  *manager,
899    bAigEdge_t node)
900{
901
902   flags(node) &= ResetCanonicalBitMask;
903}
904
905/**Function********************************************************************
906
907  Synopsis    [Get pass flag for node]
908
909  Description []
910
911  SideEffects []
912
913  SeeAlso     []
914
915******************************************************************************/
916int
917bAigGetPassFlag(
918    bAig_Manager_t  *manager,
919    bAigEdge_t node)
920   
921{
922
923  return((flags(node) & CanonicalBitMask) != 0);
924}
925
926
927
928/**Function********************************************************************
929
930  Synopsis    [Create AND node and assign name to it ]
931
932  Description []
933
934  SideEffects []
935
936  SeeAlso     []
937
938******************************************************************************/
939bAigEdge_t
940bAigCreateAndNode(
941   bAig_Manager_t  *manager,
942   bAigEdge_t node1,
943   bAigEdge_t node2)
944{
945   
946  bAigEdge_t varIndex;
947  char       *name = NIL(char);
948  char       *node1Str = util_inttostr(node1);
949  char       *node2Str = util_inttostr(node2);
950
951  name = util_strcat4("Nd", node1Str,"_", node2Str);
952  while (st_lookup(manager->SymbolTable, name, &varIndex)){
953    printf("Find redundant node at %ld %ld\n", node1, node2);
954    name = util_strcat3(name, node1Str, node2Str);
955  }
956  FREE(node1Str);
957  FREE(node2Str);
958  varIndex = bAig_CreateNode(manager, node1, node2);
959  if (varIndex == bAig_NULL){
960    FREE(name);
961    return (varIndex);
962  } 
963  /* Insert the varaible in the Symbol Table */
964  st_insert(manager->SymbolTable, name, (char*) (long) varIndex);
965  manager->nameList[bAigNodeID(varIndex)] = name; 
966
967  return(varIndex);
968
969}
970
971/*---------------------------------------------------------------------------*/
972/* Definition of static functions                                            */
973/*---------------------------------------------------------------------------*/
974
975/**Function********************************************************************
976
977  Synopsis    [Connect fanin fanout of two AIG nodes]
978
979  Description []
980
981  SideEffects []
982
983  SeeAlso     []
984
985******************************************************************************/
986static void
987connectOutput(
988   bAig_Manager_t *manager,
989   bAigEdge_t from,
990   bAigEdge_t to,
991   int inputIndex)
992{
993  bAigEdge_t *pfan;
994  int nfan;
995
996  to = bAig_NonInvertedEdge(to);
997  pfan = (bAigEdge_t *)fanout(from);
998  nfan = nFanout(from);
999  if(nfan == 0) pfan = ALLOC(bAigEdge_t, 2);
1000  else          pfan = REALLOC(bAigEdge_t, pfan, nfan+2);
1001  to += bAig_IsInverted(from);
1002  to = to << 1;
1003  to += inputIndex;
1004  pfan[nfan++] = to;
1005  pfan[nfan] = 0;
1006  fanout(from) = (long)pfan;
1007  nFanout(from) = nfan;
1008}
1009
1010
1011/**Function********************************************************************
1012
1013  Synopsis    [disconnect fanin fanout of two AIG nodes]
1014
1015  Description []
1016
1017  SideEffects []
1018
1019  SeeAlso     []
1020
1021static void
1022unconnectOutput(
1023   bAig_Manager_t *manager,
1024   bAigEdge_t from,
1025   bAigEdge_t to)
1026{
1027   bAigEdge_t cur, *pfan, *newfan;
1028   int i, nfan;
1029
1030  from = bAig_NonInvertedEdge(from);
1031  to = bAig_NonInvertedEdge(to);
1032
1033  pfan = (bAigEdge_t *)fanout(from);
1034  nfan = nFanout(from);
1035  newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
1036  for(i=0; i<nfan; i++) {
1037    cur = pfan[i];
1038    cur = cur >> 1;
1039    cur = bAig_NonInvertedEdge(cur);
1040    if(cur == to) {
1041      memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
1042      memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
1043      newfan[nfan-1] = 0;
1044      fanout(from) = (int)newfan;
1045      free(pfan);
1046      nFanout(from) = nfan-1;
1047      break;
1048    }
1049  }
1050}
1051******************************************************************************/
1052
1053
1054/**Function********************************************************************
1055
1056  Synopsis    [Look for the node in the Hash Table.]
1057
1058  Description [.]
1059
1060  SideEffects []
1061
1062  SeeAlso     []
1063
1064******************************************************************************/
1065static bAigEdge_t
1066HashTableLookup(
1067  bAig_Manager_t *manager, 
1068  bAigEdge_t  node1,
1069  bAigEdge_t  node2)
1070{
1071  bAigEdge_t key = HashTableFunction(node1, node2);
1072  bAigEdge_t node;
1073 
1074  node = manager->HashTable[key];
1075  if  (node == bAig_NULL) {
1076    return bAig_NULL;
1077  }
1078  else{
1079    while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
1080            (leftChild(bAig_NonInvertedEdge(node))  != node1)) {
1081 
1082      if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
1083        return(bAig_NULL); 
1084      }
1085      node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
1086    } /* While loop */ 
1087    return(node);
1088
1089  } /* If Then Else */
1090   
1091} /* End of HashTableLookup() */
1092
1093/**Function********************************************************************
1094
1095  Synopsis    [Add a node in the Hash Table.]
1096
1097  Description []
1098
1099  SideEffects []
1100
1101  SeeAlso     []
1102
1103******************************************************************************/
1104static int
1105HashTableAdd(
1106  bAig_Manager_t   *manager, 
1107  bAigEdge_t  nodeIndexParent,
1108  bAigEdge_t  nodeIndex1,
1109  bAigEdge_t  nodeIndex2)
1110{
1111  bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
1112  bAigEdge_t nodeIndex;
1113  bAigEdge_t node;
1114                                               
1115  nodeIndex = manager->HashTable[key];
1116  if  (nodeIndex == bAig_NULL) {
1117    manager->HashTable[key] = nodeIndexParent;
1118    return TRUE;
1119  }
1120  else{
1121    node = nodeIndex;
1122    nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));  /* Get the Node */
1123    while (nodeIndex != bAig_NULL) {
1124      node = nodeIndex;
1125      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
1126    }
1127    next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
1128    return TRUE;
1129  }
1130   
1131} /* End of HashTableAdd() */
1132
1133
1134/**Function********************************************************************
1135
1136  Synopsis    [Hash table delete]
1137
1138  Description [Hash table delete]
1139
1140  SideEffects []
1141
1142  SeeAlso     []
1143
1144******************************************************************************/
1145static int
1146HashTableDelete(
1147  bAig_Manager_t   *manager, 
1148  bAigEdge_t  node)
1149{
1150  bAigEdge_t key = HashTableFunction(leftChild(node), rightChild(node));
1151  bAigEdge_t nodeIndex;
1152                                               
1153  nodeIndex = manager->HashTable[key];
1154  if (nodeIndex == node) {
1155    manager->HashTable[key] = next(node);
1156    return TRUE;
1157  }
1158  else{
1159    while(nodeIndex && next(bAig_NonInvertedEdge(nodeIndex)) != node)
1160      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
1161
1162    next(bAig_NonInvertedEdge(nodeIndex)) = 
1163        next(bAig_NonInvertedEdge(next(bAig_NonInvertedEdge(nodeIndex))));
1164    return TRUE;
1165  }
1166   
1167} /* End of HashTableAdd() */
1168
1169
1170/**Function********************************************************************
1171
1172  Synopsis    [Structural hasing for and4]
1173
1174  Description [Structural hasing for and4]
1175
1176  SideEffects []
1177
1178  SeeAlso     []
1179
1180******************************************************************************/
1181
1182bAigEdge_t
1183bAig_And4(
1184           bAig_Manager_t *manager,
1185           bAigEdge_t l,
1186           bAigEdge_t r)
1187{
1188  int caseIndex, caseSig;
1189  bAigEdge_t ll, lr, rl, rr;
1190  bAigEdge_t t1, t2;
1191
1192  ll = leftChild(l);
1193  lr = rightChild(l);
1194  rl = leftChild(r);
1195  rr = rightChild(r);
1196
1197  if(bAigCompareNode(l, rl) ||
1198     bAigCompareNode(l, rr)) {
1199    return(bAig_And3(manager, l, r));
1200  }
1201  else if(bAigCompareNode(r, ll) ||
1202     bAigCompareNode(r, lr)) {
1203    return(bAig_And3(manager, r, l));
1204  }
1205
1206  if(ll > lr+1) bAigSwap(ll, lr);
1207  if(rl > rr+1) bAigSwap(rl, rr);
1208
1209  caseIndex = 0; /* (a b)(c d) */
1210  if(bAigCompareNode(ll, rl)) {
1211    if(bAigCompareNode(lr, rr)) {
1212      caseIndex = 4; /* (a b) (a b) */
1213    }
1214    else {
1215      caseIndex = 1; /* (a b) (a c) */
1216      if(lr > rr+1) {
1217        bAigSwap(ll, rl);
1218        bAigSwap(lr, rr); 
1219        bAigSwap(l, r); 
1220      }
1221    }
1222  }
1223  else if(bAigCompareNode(lr, rl)) {
1224    caseIndex = 2; /* (b a)(a c) */
1225  }
1226  else if(bAigCompareNode(lr, rr)) {
1227    caseIndex = 3; /* (b a)(c a) */
1228    if(ll > rl+1) {
1229      bAigSwap(ll, rl);
1230      bAigSwap(lr, rr); 
1231      bAigSwap(l, r); 
1232    }
1233  }
1234  else if(bAigCompareNode(ll, rr)) {
1235    /* (a b)(c a)  */
1236    bAigSwap(ll, rl);
1237    bAigSwap(lr, rr); 
1238    bAigSwap(l, r); 
1239    caseIndex = 2; /* (c a )(a b) because of c < b */
1240  }
1241
1242  caseSig = 0;
1243  if(bAig_IsInverted(ll)) caseSig += 32;
1244  if(bAig_IsInverted(lr)) caseSig += 16;
1245  if(bAig_IsInverted(l))  caseSig += 8;
1246  if(bAig_IsInverted(rl)) caseSig += 4;
1247  if(bAig_IsInverted(rr)) caseSig += 2;
1248  if(bAig_IsInverted(r))  caseSig += 1;
1249  /**
1250  fprintf(vis_stdout, "Index: %d Sig: %2d  (%5d%c %5d%c)%c (%5d%c %5d%c)%c (%5d, %5d)\n",
1251          caseIndex, caseSig,
1252          bAig_NonInvertedEdge(ll), bAig_IsInverted(ll) ? '\'' : ' ',
1253          bAig_NonInvertedEdge(lr), bAig_IsInverted(lr) ? '\'' : ' ',
1254          bAig_IsInverted(l) ? '\'' : ' ',
1255          bAig_NonInvertedEdge(rl), bAig_IsInverted(rl) ? '\'' : ' ',
1256          bAig_NonInvertedEdge(rr), bAig_IsInverted(rr) ? '\'' : ' ',
1257          bAig_IsInverted(r) ? '\'' : ' ',
1258          bAig_NonInvertedEdge(l), bAig_NonInvertedEdge(r)
1259           );
1260           **/
1261  if(caseIndex == 0) {
1262    return(bAig_And2(manager, l, r));
1263  }
1264  else if(caseIndex == 1) {
1265    switch(caseSig) {
1266        case 19 :
1267        case 17 :
1268        case 3 :
1269        case 1 :
1270        case 55 :
1271        case 53 :
1272        case 39 :
1273        case 37 :
1274      t1 = bAig_And(manager, lr, bAig_Not(rr));
1275      t2 = bAig_And(manager, ll, t1);
1276      return(t2);
1277        case 18 :
1278        case 16 :
1279        case 2 :
1280        case 0 :
1281        case 54 :
1282        case 52 :
1283        case 38 :
1284        case 36 :
1285      t1 = bAig_And(manager, lr, rr);
1286      t2 = bAig_And(manager, ll, t1);
1287      return(t2);
1288        case 26 :
1289        case 24 :
1290        case 10 :
1291        case 8 :
1292        case 62 :
1293        case 60 :
1294        case 46 :
1295        case 44 :
1296      t1 = bAig_And(manager, bAig_Not(lr), rr);
1297      t2 = bAig_And(manager, ll, t1);
1298      return(t2);
1299        case 61 :
1300        case 27 :
1301        case 25 :
1302        case 11 :
1303        case 63 :
1304        case 47 :
1305        case 9 :
1306        case 45 :
1307      t1 = bAig_And(manager, bAig_Not(lr), bAig_Not(rr));
1308      t2 = bAig_Or(manager, bAig_Not(ll), t1);
1309      return(t2);
1310        case 23 :
1311        case 21 :
1312        case 7 :
1313        case 5 :
1314        case 51 :
1315        case 49 :
1316        case 35 :
1317        case 33 :
1318      return(l);
1319        case 30 :
1320        case 28 :
1321        case 14 :
1322        case 12 :
1323        case 58 :
1324        case 56 :
1325        case 42 :
1326        case 40 :
1327      return(r);
1328        case 22 :
1329        case 20 :
1330        case 6 :
1331        case 4 :
1332        case 50 :
1333        case 48 :
1334        case 34 :
1335        case 32 :
1336      return(bAig_Zero);
1337        case 31 :
1338        case 29 :
1339        case 15 :
1340        case 13 :
1341        case 59 :
1342        case 57 :
1343        case 43 :
1344        case 41 :
1345      t1 = bAig_And2(manager, l, r);
1346      return(t1);
1347    }
1348  }
1349  else if(caseIndex == 2) {
1350    switch(caseSig) {
1351        case 35 :
1352        case 33 :
1353        case 3 :
1354        case 1 :
1355        case 55 :
1356        case 53 :
1357        case 23 :
1358        case 21 :
1359      t1 = bAig_And(manager, lr, bAig_Not(rr));
1360      t2 = bAig_And(manager, ll, t1);
1361      return(t2);
1362        case 34 :
1363        case 32 :
1364        case 2 :
1365        case 0 :
1366        case 54 :
1367        case 52 :
1368        case 22 :
1369        case 20 :
1370      t1 = bAig_And(manager, lr, rr);
1371      t2 = bAig_And(manager, ll, t1);
1372      return(t2);
1373        case 42 :
1374        case 40 :
1375        case 10 :
1376        case 8 :
1377        case 62 :
1378        case 60 :
1379        case 30 :
1380        case 28 :
1381      t1 = bAig_And(manager, lr, rr);
1382      t2 = bAig_And(manager, bAig_Not(ll), t1);
1383      return(t2);
1384        case 43 :
1385        case 41 :
1386        case 11 :
1387        case 9 :
1388        case 63 :
1389        case 61 :
1390        case 31 :
1391        case 29 :
1392      t1 = bAig_And(manager, bAig_Not(ll), bAig_Not(rr));
1393      t2 = bAig_Or(manager, bAig_Not(lr), t1);
1394      return(t2);
1395        case 39 :
1396        case 37 :
1397        case 7 :
1398        case 5 :
1399        case 51 :
1400        case 49 :
1401        case 19 :
1402        case 17 :
1403      return(l);
1404        case 46 :
1405        case 44 :
1406        case 14 :
1407        case 12 :
1408        case 58 :
1409        case 56 :
1410        case 26 :
1411        case 24 :
1412      return(r);
1413        case 38 :
1414        case 36 :
1415        case 6 :
1416        case 4 :
1417        case 50 :
1418        case 48 :
1419        case 18 :
1420        case 16 :
1421      return(bAig_Zero);
1422        case 45 :
1423        case 15 :
1424        case 13 :
1425        case 59 :
1426        case 57 :
1427        case 47 :
1428        case 27 :
1429        case 25 :
1430      t1 = bAig_And2(manager, l, r);
1431      return(t1);
1432    }
1433  }
1434  else if(caseIndex == 3) {
1435    switch(caseSig) {
1436        case 37 :
1437        case 33 :
1438        case 5 :
1439        case 1 :
1440        case 55 :
1441        case 51 :
1442        case 23 :
1443        case 19 :
1444      t1 = bAig_And(manager, bAig_Not(rl), lr);
1445      t2 = bAig_And(manager, ll, t1);
1446      return(t2);
1447        case 36 :
1448        case 32 :
1449        case 4 :
1450        case 0 :
1451        case 54 :
1452        case 50 :
1453        case 22 :
1454        case 18 :
1455      t1 = bAig_And(manager, rl, lr);
1456      t2 = bAig_And(manager, ll, t1);
1457      return(t2);
1458        case 44 :
1459        case 40 :
1460        case 12 :
1461        case 8 :
1462        case 62 :
1463        case 58 :
1464        case 30 :
1465        case 26 :
1466      t1 = bAig_And(manager, rl, lr);
1467      t2 = bAig_And(manager, bAig_Not(ll), t1);
1468      return(t2);
1469        case 45 :
1470        case 41 :
1471        case 13 :
1472        case 9 :
1473        case 63 :
1474        case 59 :
1475        case 31 :
1476        case 27 :
1477      t1 = bAig_And(manager, bAig_Not(ll), bAig_Not(rl));
1478      t2 = bAig_Or(manager, bAig_Not(lr), t1);
1479      return(t2);
1480        case 39 :
1481        case 35 :
1482        case 7 :
1483        case 3 :
1484        case 53 :
1485        case 49 :
1486        case 21 :
1487        case 17 :
1488      return(l);
1489        case 46 :
1490        case 42 :
1491        case 14 :
1492        case 10 :
1493        case 60 :
1494        case 56 :
1495        case 28 :
1496        case 24 :
1497      return(r);
1498        case 38 :
1499        case 34 :
1500        case 6 :
1501        case 2 :
1502        case 52 :
1503        case 48 :
1504        case 20 :
1505        case 16 :
1506      return(bAig_Zero);
1507        case 47 :
1508        case 43 :
1509        case 15 :
1510        case 11 :
1511        case 61 :
1512        case 57 :
1513        case 29 :
1514        case 25 :
1515      t1 = bAig_And2(manager, l, r);
1516      return(t1);
1517    }
1518  }
1519  else if(caseIndex == 4) {
1520    switch(caseSig) {
1521        case 22 :
1522        case 20 :
1523        case 6 :
1524        case 4 :
1525        case 50 :
1526        case 48 :
1527        case 34 :
1528        case 32 :
1529        case 2 :
1530        case 16 :
1531        case 52 :
1532        case 1 :
1533        case 8 :
1534        case 19 :
1535        case 26 :
1536        case 37 :
1537        case 44 :
1538        case 38 :
1539        case 55 :
1540        case 62 :
1541      return(bAig_Zero);
1542        case 0 :
1543        case 18 :
1544        case 36 :
1545        case 54 :
1546        case 9 :
1547        case 27 :
1548        case 45 :
1549        case 63 :
1550        case 5 :
1551        case 23 :
1552        case 33 :
1553        case 51 :
1554        case 3 :
1555        case 17 :
1556        case 49 :
1557        case 7 :
1558        case 35 :
1559        case 21 :
1560        case 39 :
1561        case 53 :
1562      return(l);
1563        case 40 :
1564        case 58 :
1565        case 12 :
1566        case 30 :
1567        case 24 :
1568        case 10 :
1569        case 14 :
1570        case 56 :
1571        case 28 :
1572        case 42 :
1573        case 60 :
1574        case 46 :
1575      return(r);
1576        case 11 :
1577        case 47 :
1578        case 25 :
1579        case 61 :
1580      return(bAig_Not(ll));
1581        case 41 :
1582        case 59 :
1583        case 13 :
1584        case 31 :
1585      return(bAig_Not(lr));
1586        case 15 :
1587      t1 = bAig_And(manager, ll, bAig_Not(lr));
1588      t2 = bAig_And(manager, bAig_Not(ll), lr);
1589      return(bAig_Not(bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
1590        case 57 :
1591      t1 = bAig_And(manager, rl, bAig_Not(rr));
1592      t2 = bAig_And(manager, bAig_Not(rl), rr);
1593      return(bAig_Not(bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
1594        case 29 :
1595      t1 = bAig_And(manager, ll, lr);
1596      t2 = bAig_And(manager, bAig_Not(ll), bAig_Not(lr));
1597      return((bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
1598        case 43 :
1599      t1 = bAig_And(manager, rl, rr);
1600      t2 = bAig_And(manager, bAig_Not(rl), bAig_Not(rr));
1601      return((bAig_And2(manager, bAig_Not(t1), bAig_Not(t2))));
1602    }
1603  }
1604  return(0);
1605}
1606
1607
1608/**Function********************************************************************
1609
1610  Synopsis    [Structural hasing for and3]
1611
1612  Description [Structural hasing for and3]
1613
1614  SideEffects []
1615
1616  SeeAlso     []
1617
1618******************************************************************************/
1619bAigEdge_t
1620bAig_And3(
1621           bAig_Manager_t *manager,
1622           bAigEdge_t l,
1623           bAigEdge_t r)
1624{
1625  int caseIndex, caseSig;
1626  bAigEdge_t rl, rr;
1627
1628  rl = leftChild(r);
1629  rr = rightChild(r);
1630
1631  caseIndex = 0; /* (a)(b c) */
1632  if(bAigCompareNode(l, rl)) {
1633    caseIndex = 1; /* (a)(a b) */
1634  }
1635  else if(bAigCompareNode(l, rr)) {
1636    caseIndex = 2; /* (a)(b a) */
1637  }
1638
1639  caseSig = 0;
1640  if(bAig_IsInverted(l))  caseSig += 8;
1641  if(bAig_IsInverted(rl)) caseSig += 4;
1642  if(bAig_IsInverted(rr)) caseSig += 2;
1643  if(bAig_IsInverted(r))  caseSig += 1;
1644  if(caseIndex == 0) {
1645    return(bAig_And2(manager, l, r));
1646  }
1647  else if(caseIndex == 1) {
1648    switch(caseSig) {
1649        case 2 :
1650        case 0 :
1651        case 14 :
1652        case 12 :
1653      return(r);
1654        case 10 :
1655        case 8 :
1656        case 6 :
1657        case 4 :
1658      return(bAig_Zero);
1659        case 3 :
1660        case 1 :
1661        case 15 :
1662        case 13 :
1663      return(bAig_And(manager, rl, bAig_Not(rr)));
1664        case 11 :
1665        case 9 :
1666        case 7 :
1667        case 5 :
1668      return(l);
1669    }
1670  }
1671  else if(caseIndex == 2) {
1672    switch(caseSig) {
1673        case 4 :
1674        case 0 :
1675        case 14 :
1676        case 10 :
1677      return(r);
1678        case 12 :
1679        case 8 :
1680        case 6 :
1681        case 2 :
1682      return(bAig_Zero);
1683        case 5 :
1684        case 1 :
1685        case 15 :
1686        case 11 :
1687      return(bAig_And(manager, bAig_Not(rl), rr));
1688        case 13 :
1689        case 9 :
1690        case 7 :
1691        case 3 :
1692      return(l);
1693    }
1694  }
1695  return(0);
1696}
1697
1698/**Function********************************************************************
1699
1700  Synopsis    [Set mask for transitive fanin nodes]
1701
1702  Description [Set mask for transitive fanin nodes]
1703
1704  SideEffects []
1705
1706  SeeAlso     []
1707
1708******************************************************************************/
1709void
1710bAig_SetMaskTransitiveFanin(
1711        bAig_Manager_t *manager,
1712        int v,
1713        unsigned int mask)
1714{
1715  if(v == 2)    return;
1716
1717
1718  if(flags(v) & mask)   return;
1719
1720  flags(v) |= mask;
1721
1722  bAig_SetMaskTransitiveFanin(manager, leftChild(v), mask);
1723  bAig_SetMaskTransitiveFanin(manager, rightChild(v), mask);
1724}
1725
1726/**Function********************************************************************
1727
1728  Synopsis    [Reset mask for transitive fanin nodes]
1729
1730  Description [Reset mask for transitive fanin nodes]
1731
1732  SideEffects []
1733
1734  SeeAlso     []
1735
1736******************************************************************************/
1737void
1738bAig_ResetMaskTransitiveFanin(
1739        bAig_Manager_t *manager,
1740        int v,
1741        unsigned int mask,
1742        unsigned int resetMask)
1743{
1744  if(v == 2)    return;
1745
1746
1747  if(!(flags(v) & mask))        return;
1748
1749  flags(v) &= resetMask;
1750  bAig_ResetMaskTransitiveFanin(manager, leftChild(v), mask, resetMask);
1751  bAig_ResetMaskTransitiveFanin(manager, rightChild(v), mask, resetMask);
1752}
1753
1754
1755/**Function********************************************************************
1756
1757   Synopsis [Get value of aig node.]
1758
1759   Description [The default falue is 2, which is same as UNKNOWN. This value can be assigned from SAT solver.]
1760
1761   SideEffects []
1762   
1763   SeeAlso     []
1764   
1765******************************************************************************/
1766
1767int
1768bAig_GetValueOfNode(bAig_Manager_t *manager, bAigEdge_t v)
1769{
1770  unsigned int value, lvalue, rvalue;
1771  bAigEdge_t left, right;
1772
1773
1774  /*
1775  if(!(flags(v) & CoiMask))     return(2);
1776  **/
1777  if(v == 2)    return(2);
1778
1779  value = aig_value(v);
1780  if(value == 3)        return(2);
1781  if(value == 2) {
1782    left = bAig_GetCanonical(manager, leftChild(v));
1783    lvalue = bAig_GetValueOfNode(manager, left);
1784    if(lvalue == 0)     {
1785      value = 0;
1786    }
1787    else {
1788      right = bAig_GetCanonical(manager, rightChild(v));
1789      rvalue = bAig_GetValueOfNode(manager, right);
1790      if(rvalue == 0) {
1791        value = 0;
1792      }
1793      else if(rvalue == 1 && lvalue == 1) {
1794        value = 1;
1795      }
1796      else {
1797        value = 2;
1798      }
1799    }
1800  }
1801
1802  if(value == 2) {
1803    aig_value(v) = 3;
1804    return(value);
1805  }
1806  else  {       
1807    aig_value(v) = value;
1808    return(value ^ bAig_IsInverted(v));
1809  }
1810}
1811
Note: See TracBrowser for help on using the repository browser.