source: vis_dev/cusp-1.1/src/aig/aigNode.c @ 23

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

cusp added
File size: 71.3 KB
RevLine 
[12]1/**CFile***********************************************************************
2
3  FileName    [AigNode.c]
4
5  PackageName [Aig]
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 "aig.h"
21#include "aigInt.h"
22
23static char rcsid[] UNUSED = "$Id: aigNode.c,v 1.2 2009-04-10 16:33:36 hhkim Exp $";
24
25/*---------------------------------------------------------------------------*/
26/* Constant declarations                                                     */
27/*---------------------------------------------------------------------------*/
28
29/**AutomaticStart*************************************************************/
30
31/*---------------------------------------------------------------------------*/
32/* Static function prototypes                                                */
33/*---------------------------------------------------------------------------*/
34
35static void connectOutput(Aig_Manager_t *bm, AigEdge_t from, AigEdge_t to, int inputIndex);
36static AigEdge_t HashTableLookup(Aig_Manager_t *bm, AigEdge_t node1, AigEdge_t node2);
37static int HashTableAdd(Aig_Manager_t *bm, AigEdge_t nodeIndexParent, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
38/* static int HashTableDelete(Aig_Manager_t *bm, AigEdge_t node); */
39
40/**AutomaticEnd***************************************************************/
41
42
43/*---------------------------------------------------------------------------*/
44/* Definition of exported functions                                          */
45/*---------------------------------------------------------------------------*/
46
47
48/**Function********************************************************************
49
50  Synopsis    [Read Node's name.]
51
52  Description [Read the name of a node given its index.]
53
54  SideEffects []
55
56  SeeAlso     []
57
58******************************************************************************/
59nameType_t *
60Aig_NodeReadName(
61   Aig_Manager_t *bm,
62   AigEdge_t     node)
63{
64  return bm->nameList[AigNodeID(node)];
65}
66
67/**Function********************************************************************
68
69  Synopsis    [Set Node's name.]
70
71  Description [Set the name of node in Symbol table and name List]
72
73  SideEffects []
74
75  SeeAlso     []
76
77******************************************************************************/
78void 
79Aig_NodeSetName(
80   Aig_Manager_t *bm,
81   AigEdge_t     node,
82   nameType_t     *name)
83{
84  nameType_t *tmpName = bm->nameList[AigNodeID(node)];
85  FREE(tmpName);
86  st_insert(bm->SymbolTable, name, (char*) (long) node);
87  bm->nameList[AigNodeID(node)] = name;
88}
89
90/**Function********************************************************************
91
92  Synopsis    [Returns the index of the right node.]
93
94  Description []
95
96  SideEffects []
97
98  SeeAlso     []
99
100******************************************************************************/
101int
102Aig_NodeReadIndexOfRightChild(
103   Aig_Manager_t *bm,
104   AigEdge_t nodeIndex)
105{
106  return rightChild(nodeIndex);
107}
108
109/**Function********************************************************************
110
111  Synopsis    [Returns the index of the left node.]
112
113  Description []
114
115  SideEffects []
116
117  SeeAlso     []
118
119******************************************************************************/
120AigEdge_t
121Aig_NodeReadIndexOfLeftChild(
122   Aig_Manager_t *bm,
123   AigEdge_t nodeIndex)
124{
125  return leftChild(nodeIndex);
126}
127
128/**Function********************************************************************
129
130  Synopsis    [Get canonical node of given node.]
131
132  Description [This function find node index that is functionally equivalent with given node index.] 
133
134  SideEffects []
135
136  SeeAlso     []
137
138******************************************************************************/
139#if 1
140AigEdge_t
141Aig_GetCanonical(
142    Aig_Manager_t *bm, 
143    AigEdge_t nodeIndex)
144{
145  AigEdge_t next;
146 
147  /* Bing */
148 
149  if(nodeIndex == Aig_NULL||
150     nodeIndex == Aig_One ||
151     nodeIndex == Aig_Zero)
152    return(nodeIndex); 
153 
154 
155  while(AigGetPassFlag(bm, nodeIndex)) {
156    next = canonical(nodeIndex);
157    if(Aig_IsInverted(nodeIndex))  next = Aig_Not(next);
158    nodeIndex = next;
159  }
160  return(nodeIndex);
161}
162#endif
163
164/**Function********************************************************************
165
166  Synopsis    [Merge two functionally equivalent node.]
167
168  Description [This function merges the equivalent two nodes. ]
169
170  SideEffects []
171
172  SeeAlso     []
173
174******************************************************************************/
175/**
176int
177Aig_Merge(
178    Aig_Manager_t *bm,
179    AigEdge_t nodeIndex1,
180    AigEdge_t nodeIndex2)
181{
182AigEdge_t newNodeIndex, nodeIndex, tnodeIndex;
183AigEdge_t leftIndex, rightIndex;
184AigEdge_t outIndex, *pfan;
185int id1, id2;
186AigEdge_t cur;
187bdd_t **bddArray;
188array_t *nodeArray;
189int i, ii, iii;
190long *ManagerNodesArray;
191
192  nodeIndex1 = Aig_GetCanonical(bm, nodeIndex1);
193  nodeIndex2 = Aig_GetCanonical(bm, nodeIndex2);
194
195  if(nodeIndex1 == nodeIndex2)  return(nodeIndex1);
196
197
198  ManagerNodesArray = bm->NodesArray;
199
200
201  newNodeIndex = nodeIndex1;     
202  if (Aig_NonInvertedEdge(nodeIndex1) > Aig_NonInvertedEdge(nodeIndex2)){
203    nodeIndex1 = nodeIndex2;
204    nodeIndex2 = newNodeIndex;
205  }
206
207  if(Aig_IsInverted(nodeIndex2)) {
208    nodeIndex1 = Aig_Not(nodeIndex1);
209    nodeIndex2 = Aig_Not(nodeIndex2);
210  }
211
212  nodeArray = array_alloc(AigEdge_t, 0);
213  nodeIndex = nodeIndex2;
214  array_insert_last(AigEdge_t, nodeArray, nodeIndex);
215  while(Aig_NonInvertedEdge(canonical(nodeIndex)) != Aig_NonInvertedEdge(nodeIndex2)){
216    if(Aig_IsInverted(nodeIndex))
217      nodeIndex = Aig_Not(canonical(nodeIndex));
218    else
219      nodeIndex = canonical(nodeIndex);
220    array_insert_last(AigEdge_t, nodeArray, nodeIndex);
221  }
222
223  AigSetPassFlag(bm, nodeIndex2);
224  nodeIndex = nodeIndex1;
225  while(Aig_NonInvertedEdge(canonical(nodeIndex)) != Aig_NonInvertedEdge(nodeIndex1)) {
226    if(Aig_IsInverted(nodeIndex))
227      nodeIndex = Aig_Not(canonical(nodeIndex));
228    else
229      nodeIndex = canonical(nodeIndex);
230  }
231
232  for(i=0; i<array_n(nodeArray); i++) {
233    tnodeIndex = array_fetch(AigEdge_t, nodeArray, i);
234    if(Aig_IsInverted(nodeIndex))
235      canonical(nodeIndex) = Aig_Not(tnodeIndex);
236    else
237      canonical(nodeIndex) = tnodeIndex;
238
239    if(Aig_IsInverted(nodeIndex))
240      nodeIndex = Aig_Not(canonical(nodeIndex));
241    else
242      nodeIndex = canonical(nodeIndex);
243  }
244
245  if(Aig_IsInverted(nodeIndex)) {
246    canonical(nodeIndex) = Aig_Not(nodeIndex1);
247  }
248  else {
249    canonical(nodeIndex) = nodeIndex1;
250  }
251  array_free(nodeArray);
252
253  nodeArray = array_alloc(AigEdge_t, 0);
254  AigEdgeForEachFanout(bm, nodeIndex2, cur, ii, iii, pfan) {
255    cur = cur >> 1;
256    cur = Aig_NonInvertedEdge(cur);
257    array_insert_last(AigEdge_t, nodeArray, cur);
258  }
259
260  for(i=0; i<array_n(nodeArray); i++) {
261    outIndex = array_fetch(AigEdge_t, nodeArray, i);
262    leftIndex = leftChild(outIndex);
263    rightIndex = rightChild(outIndex);
264
265    HashTableDelete(bm, outIndex);
266
267    newNodeIndex = Aig_And(bm, leftIndex, rightIndex);
268
269    Aig_Merge(bm, newNodeIndex, outIndex);
270
271  }
272  array_free(nodeArray);
273
274  bddArray = bm->bddArray;
275  id1 = AigNodeID(nodeIndex1);
276  id2 = AigNodeID(nodeIndex2);
277  if(bddArray[id1] == 0 && bddArray[id2]){
278    if(Aig_IsInverted(nodeIndex2)) {
279      if(Aig_IsInverted(nodeIndex1)) {
280        bddArray[id1] = bdd_dup(bddArray[id2]);
281      }
282      else {
283        bddArray[id1] = bdd_not(bddArray[id2]);
284      }
285    }
286    else {
287      if(Aig_IsInverted(nodeIndex1)) {
288        bddArray[id1] = bdd_not(bddArray[id2]);
289      }
290      else {
291        bddArray[id1] = bdd_dup(bddArray[id2]);
292      }
293    }
294  }
295  return(nodeIndex1);
296}
297**/
298
299
300/**Function********************************************************************
301
302  Synopsis    [Print node information.]
303
304  Description [Print node information.]
305
306  SideEffects []
307
308  SeeAlso     []
309
310******************************************************************************/
311
312void
313Aig_PrintNode(
314  Aig_Manager_t *bm,
315  AigEdge_t i)
316{
317  int j, size;
318  long cur, *pfan;
319
320  fprintf(stdout, "nodeIndex : %ld (%ld)\n", i, AigNodeID(i)); 
321  fprintf(stdout, "child     : %ld%c, %ld%c\n", 
322          Aig_NonInvertedEdge(leftChild(i)), Aig_IsInverted(leftChild(i)) ? '\'' : ' ', 
323          Aig_NonInvertedEdge(rightChild(i)), Aig_IsInverted(rightChild(i)) ? '\'' : ' ');
324
325  fprintf(stdout, "refCount  : %ld\n", nFanout(i));
326  fprintf(stdout, "          : ");
327  size = nFanout(i);
328  for(j=0, pfan = (AigEdge_t *)fanout(i); j<size; j++) {
329    cur = pfan[j];
330    cur = cur >> 1;
331    fprintf(stdout, " %ld", cur);
332  }
333  fprintf(stdout, "\n");
334
335  fprintf(stdout, "next      : %ld\n", aig_next(i));
336  fflush(stdout);
337}
338   
339
340/**Function********************************************************************
341
342  Synopsis    [Performs the Logical AND of two nodes.]
343
344  Description [This function performs the Logical AND of two nodes.  The inputs
345               are the indices of the two nodes.  This function returns the index
346               of the result node.]
347
348  SideEffects []
349
350  SeeAlso     []
351
352******************************************************************************/
353AigEdge_t
354Aig_And(
355   Aig_Manager_t *bm,
356   AigEdge_t nodeIndex1,
357   AigEdge_t nodeIndex2)
358{
359
360  AigEdge_t newNodeIndex;
361
362  nodeIndex1 = Aig_GetCanonical(bm, nodeIndex1);
363  nodeIndex2 = Aig_GetCanonical(bm, nodeIndex2);
364
365  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
366  if (Aig_NonInvertedEdge(nodeIndex1) > Aig_NonInvertedEdge(nodeIndex2)){
367    nodeIndex1 = nodeIndex2;
368    nodeIndex2 = newNodeIndex;
369  }
370
371  if ( nodeIndex2 == Aig_Zero ) {
372    return Aig_Zero;
373  }
374  if ( nodeIndex1 == Aig_Zero ) {
375    return Aig_Zero;
376  }
377  if ( nodeIndex2 == Aig_One ) {
378    return nodeIndex1;
379  }
380  if ( nodeIndex1 == Aig_One ) {
381    return nodeIndex2;
382  }
383  if ( nodeIndex1 == nodeIndex2 ) {
384    return nodeIndex1;
385  }
386  if ( nodeIndex1 == Aig_Not(nodeIndex2) ) {
387    return Aig_Zero;
388  }
389
390  /* Look for the new node in the Hash table */
391  newNodeIndex = HashTableLookup(bm, nodeIndex1, nodeIndex2);
392
393  if (newNodeIndex == Aig_NULL){ 
394    if(AigIsVar(bm, nodeIndex1) && AigIsVar(bm, nodeIndex2))
395      newNodeIndex = Aig_And2(bm, nodeIndex1, nodeIndex2);
396    else if(AigIsVar(bm, nodeIndex1)) 
397      newNodeIndex = Aig_And3(bm, nodeIndex1, nodeIndex2);
398    else if(AigIsVar(bm, nodeIndex2)) 
399      newNodeIndex = Aig_And3(bm, nodeIndex2, nodeIndex1);
400    else {
401      newNodeIndex = Aig_And4(bm, nodeIndex1, nodeIndex2);
402    }
403  }
404   
405  return newNodeIndex;
406
407}
408
409/**Function********************************************************************
410
411  Synopsis    [Structural hashing for and2]
412
413  Description [Structural hashing for and2]
414
415  SideEffects []
416
417  SeeAlso     []
418
419******************************************************************************/
420AigEdge_t
421Aig_And2(
422   Aig_Manager_t *bm,
423   AigEdge_t nodeIndex1,
424   AigEdge_t nodeIndex2)
425{
426  AigEdge_t newNodeIndex;
427
428  nodeIndex1 = Aig_GetCanonical(bm, nodeIndex1);
429  nodeIndex2 = Aig_GetCanonical(bm, nodeIndex2);
430
431  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
432  if (Aig_NonInvertedEdge(nodeIndex1) > Aig_NonInvertedEdge(nodeIndex2)){
433    nodeIndex1 = nodeIndex2;
434    nodeIndex2 = newNodeIndex;
435  }
436  if ( nodeIndex2 == Aig_Zero ) {
437    return Aig_Zero;
438  }
439  if ( nodeIndex1 == Aig_Zero ) {
440    return Aig_Zero;
441  }
442  if ( nodeIndex2 == Aig_One ) {
443    return nodeIndex1;
444  }
445  if ( nodeIndex1 == Aig_One ) {
446    return nodeIndex2;
447  }
448  if ( nodeIndex1 == nodeIndex2 ) {
449    return nodeIndex1;
450  }
451  if ( nodeIndex1 == Aig_Not(nodeIndex2) ) {
452    return Aig_Zero;
453  }
454  newNodeIndex = HashTableLookup(bm, nodeIndex1, nodeIndex2);
455
456  if (newNodeIndex == Aig_NULL){ 
457    newNodeIndex = AigCreateAndNode(bm, nodeIndex1, nodeIndex2) ;
458
459    HashTableAdd(bm, newNodeIndex, nodeIndex1, nodeIndex2);
460    connectOutput(bm, nodeIndex1, newNodeIndex, 0);
461    connectOutput(bm, nodeIndex2, newNodeIndex, 1);
462
463#if 0
464#ifdef LEARNING_
465    tNodeIndex = HashTableLookup(bm, Aig_Not(nodeIndex1), nodeIndex2);
466    if(tNodeIndex) Aig_Learn(bm, nodeIndex1, nodeIndex2);
467
468    tNodeIndex = HashTableLookup(bm, nodeIndex1, Aig_Not(nodeIndex2));
469    if(tNodeIndex) Aig_Learn(bm, nodeIndex2, nodeIndex1);
470#endif
471#endif
472  }
473  return newNodeIndex;
474
475}
476
477/**Function********************************************************************
478
479  Synopsis    [Performs the Logical AND of multiple nodes.]
480
481  Description [This function performs the Logical AND of multiple nodes.  The input
482               is the array of the node indices.  This function returns the index
483               of the result node.]
484
485  SideEffects []
486
487  SeeAlso     []
488
489******************************************************************************/
490AigEdge_t
491Aig_AndsInBFSManner(
492   Aig_Manager_t *bm,
493   array_t * nodeIndexArray)
494{
495  AigEdge_t nodeIndex1, nodeIndex2, nodeIndex3, newNodeIndex;
496  array_t * tmpNodeIndexArray;
497  int i;
498
499  nodeIndex1 = 0;
500  nodeIndex2 = 0;
501  nodeIndex3 = 0;
502  newNodeIndex = 0; 
503 
504  tmpNodeIndexArray = array_alloc(AigEdge_t, nodeIndexArray->num/2 + 1);
505
506  if (nodeIndexArray->num == 1) {
507    newNodeIndex = array_fetch(AigEdge_t, nodeIndexArray, 0);
508    array_free(tmpNodeIndexArray);   
509    return newNodeIndex;
510  }
511  else if (nodeIndexArray->num == 0) {
512    array_free(tmpNodeIndexArray);
513    return Aig_NULL;
514  }
515 
516  for(i = 0; i < nodeIndexArray->num; i=i+2) {
517    nodeIndex1 = array_fetch(AigEdge_t, nodeIndexArray, i);
518    if (i < nodeIndexArray->num-1) {
519      nodeIndex2 = array_fetch(AigEdge_t, nodeIndexArray, i+1);
520      nodeIndex3 = Aig_And(bm, nodeIndex1, nodeIndex2);
521    } else
522      nodeIndex3 = nodeIndex1;
523   
524    array_insert_last(AigEdge_t, tmpNodeIndexArray, nodeIndex3);
525  }
526
527  if (tmpNodeIndexArray->num > 1)
528    newNodeIndex = Aig_AndsInBFSManner(bm, tmpNodeIndexArray);
529  else
530    newNodeIndex = nodeIndex3;
531 
532  array_free(tmpNodeIndexArray);
533
534  return newNodeIndex;
535
536}
537
538/**Function********************************************************************
539
540  Synopsis    [Performs the Logical OR of two nodes.]
541
542  Description [This function performs the Logical OR of two nodes.  The inputs
543               are the indices of the two nodes.  This function returns the index
544               of the result node.]
545
546  SideEffects []
547
548  SeeAlso     []
549
550******************************************************************************/
551AigEdge_t
552Aig_Or(
553   Aig_Manager_t *bm,
554   AigEdge_t nodeIndex1,
555   AigEdge_t nodeIndex2)
556{
557  AigEdge_t NotNodeIndex1;
558  AigEdge_t NotNodeIndex2;
559  AigEdge_t AndNodeIndex;
560  AigEdge_t NotNodeIndex;
561 
562  NotNodeIndex1 = Aig_Not(nodeIndex1);
563  NotNodeIndex2 = Aig_Not(nodeIndex2);
564  AndNodeIndex = Aig_And(bm,  NotNodeIndex1, NotNodeIndex2);
565  NotNodeIndex = Aig_Not(AndNodeIndex);
566
567  return NotNodeIndex;
568
569}
570
571/**Function********************************************************************
572
573  Synopsis    [Performs the Logical OR of multiple nodes.]
574
575  Description [This function performs the Logical OR of multiple nodes.  The input
576               is the array of the node indices.  This function returns the index
577               of the result node.]
578
579  SideEffects []
580
581  SeeAlso     []
582
583******************************************************************************/
584AigEdge_t
585Aig_OrsInBFSManner(
586   Aig_Manager_t *bm,
587   array_t * nodeIndexArray)
588{
589  int i;
590  AigEdge_t nodeIndex1, nodeIndex2, nodeIndex3, newNodeIndex;
591  array_t * tmpNodeIndexArray;
592
593  nodeIndex1 = 0;
594  nodeIndex2 = 0;
595  nodeIndex3 = 0;
596  newNodeIndex = 0; 
597 
598  tmpNodeIndexArray = array_alloc(AigEdge_t, nodeIndexArray->num/2 + 1); 
599
600  if (nodeIndexArray->num == 1) {
601    newNodeIndex = array_fetch(AigEdge_t, nodeIndexArray, 0);
602    array_free(tmpNodeIndexArray);
603    return newNodeIndex;
604  }
605  else if (nodeIndexArray->num == 0) {
606    array_free(tmpNodeIndexArray);
607    return Aig_NULL;
608  }
609 
610  for(i = 0; i < nodeIndexArray->num; i=i+2) {
611    nodeIndex1 = array_fetch(AigEdge_t, nodeIndexArray, i);
612    if (i < nodeIndexArray->num-1) {
613      nodeIndex2 = array_fetch(AigEdge_t, nodeIndexArray, i+1);
614      nodeIndex3 = Aig_Or(bm, nodeIndex1, nodeIndex2);
615    } else
616      nodeIndex3 = nodeIndex1;
617   
618    array_insert_last(AigEdge_t, tmpNodeIndexArray, nodeIndex3);
619  }
620
621  if (tmpNodeIndexArray->num > 1)
622    newNodeIndex = Aig_OrsInBFSManner(bm, tmpNodeIndexArray);
623  else
624    newNodeIndex = nodeIndex3;
625 
626  array_free(tmpNodeIndexArray);
627
628  return newNodeIndex;
629
630}
631
632/**Function********************************************************************
633
634  Synopsis    [Performs the Logical XOR of two nodes.]
635
636  Description [This function performs the Logical XOR of two nodes.  The inputs
637               are the indices of the two nodes.  This function returns the index
638               of the result node.]
639
640  SideEffects []
641
642  SeeAlso     []
643
644******************************************************************************/
645AigEdge_t
646Aig_Xor(
647   Aig_Manager_t *bm,
648   AigEdge_t nodeIndex1,
649   AigEdge_t nodeIndex2)
650{
651  AigEdge_t NotNodeIndex1;
652  AigEdge_t NotNodeIndex2;
653  AigEdge_t AndNodeIndex1;
654  AigEdge_t AndNodeIndex2;
655  AigEdge_t OrNodeIndex;
656
657  NotNodeIndex1 = Aig_Not(nodeIndex1);
658  NotNodeIndex2 = Aig_Not(nodeIndex2);
659  AndNodeIndex1 = Aig_And(bm, nodeIndex1, NotNodeIndex2);
660  AndNodeIndex2 = Aig_And(bm, NotNodeIndex1, nodeIndex2);
661
662  OrNodeIndex = Aig_Or(bm, AndNodeIndex1, AndNodeIndex2);
663
664  return OrNodeIndex;
665}
666
667/**Function********************************************************************
668
669  Synopsis    [Performs the Logical Equal ( <--> XNOR) of two nodes.]
670
671  Description [This function performs the Logical XNOR of two nodes.  The inputs
672               are the indices of the two nodes.  This function returns the index
673               of the result node.]
674
675  SideEffects []
676
677  SeeAlso     []
678
679******************************************************************************/
680AigEdge_t
681Aig_Eq(
682   Aig_Manager_t *bm,
683   AigEdge_t nodeIndex1,
684   AigEdge_t nodeIndex2)
685{
686  return Aig_Not(
687                  Aig_Xor(bm, nodeIndex1, nodeIndex2)
688                  );
689}
690
691/**Function********************************************************************
692
693  Synopsis    [Performs the Logical Then (--> Implies) of two nodes.]
694
695  Description [This function performs the Logical Implies of two nodes.  The inputs
696               are the indices of the two nodes.  This function returns the index
697               of the result node.]
698
699  SideEffects []
700
701  SeeAlso     []
702
703******************************************************************************/
704AigEdge_t
705Aig_Then(
706   Aig_Manager_t *bm,
707   AigEdge_t nodeIndex1,
708   AigEdge_t nodeIndex2)
709{
710 return Aig_Or(bm,
711                Aig_Not(nodeIndex1),
712                nodeIndex2);
713}
714
715/**Function********************************************************************
716
717  Synopsis    [Performs the Logical nand of two nodes.]
718
719  Description [This function performs the Logical NAND of two nodes.  The inputs
720               are the indices of the two nodes.  This function returns the index
721               of the result node.]
722
723  SideEffects []
724
725  SeeAlso     []
726
727******************************************************************************/
728AigEdge_t
729Aig_Nand(
730   Aig_Manager_t *bm,
731   AigEdge_t nodeIndex1,
732   AigEdge_t nodeIndex2)
733{
734 return Aig_Not(
735            Aig_And(bm, nodeIndex1, nodeIndex2)
736            );
737}
738
739/**Function********************************************************************
740
741  Synopsis    [Performs the Logical ITE of three nodes.]
742
743  Description [This function performs the Logical ITE of three nodes.  The inputs
744               are the indices of the three nodes.  This function returns the index
745               of the result node.]
746
747  SideEffects []
748
749  SeeAlso     []
750
751******************************************************************************/
752AigEdge_t
753Aig_Ite(
754   Aig_Manager_t *bm,
755   AigEdge_t nodeIndex1,
756   AigEdge_t nodeIndex2,
757   AigEdge_t nodeIndex3)
758{
759  AigEdge_t rIndex, nodeIndex4, nodeIndex5;
760
761  nodeIndex4 = Aig_Then(bm, nodeIndex1, nodeIndex2);
762  nodeIndex5 = Aig_Or(bm, nodeIndex1, nodeIndex3);
763 
764  rIndex = Aig_And(bm, nodeIndex4, nodeIndex5);
765  return rIndex;
766}
767
768
769/**Function********************************************************************
770
771  Synopsis    [Generates a Aig for the function x - y &ge; c.]
772
773  Description [This function generates a Aig for the function x -y &ge; c.
774  Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
775  y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
776  The BDD is built bottom-up.
777  It has a linear number of nodes if the variables are ordered as follows:
778  x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
779
780  SideEffects [None]
781
782  SeeAlso     []
783
784******************************************************************************/
785#if 0
786AigEdge_t
787Aig_Inequality(
788   Aig_Manager_t *bm,
789   int  N /* number of x and y variables */,
790   int c /* right-hand side constant */,
791   AigEdge_t *x /* array of x variables */,
792   AigEdge_t *y /* array of y variables */)
793{
794    /* The nodes at level i represent values of the difference that are
795    ** multiples of 2^i.  We use variables with names starting with k
796    ** to denote the multipliers of 2^i in such multiples. */
797    int kTrue = c;
798    int kFalse = c - 1;
799    /* Mask used to compute the ceiling function.  Since we divide by 2^i,
800    ** we want to know whether the dividend is a multiple of 2^i.  If it is,
801    ** then ceiling and floor coincide; otherwise, they differ by one. */
802    int mask = 1;
803    int i;
804
805    AigEdge_t f = Aig_NULL;             /* the eventual result */
806
807    /* Two x-labeled nodes are created at most at each iteration.  They are
808    ** stored, along with their k values, in these variables.  At each level,
809    ** the old nodes are freed and the new nodes are copied into the old map.
810    */
811    AigEdge_t map[2];
812    int invalidIndex = (1 << N)-1;
813    int index[2] = {invalidIndex, invalidIndex};
814
815    /* This should never happen. */
816    if (N < 0) return(Aig_NULL);
817
818    /* If there are no bits, both operands are 0.  The result depends on c. */
819    if (N == 0) {
820        if (c >= 0) return(Aig_One);
821        else return(Aig_Zero);
822    }
823
824    /* The maximum or the minimum difference comparing to c can generate the terminal case */
825    if ((1 << N) - 1 < c) return(Aig_Zero);
826    else if ((-(1 << N) + 1) >= c) return(Aig_One);
827
828    /* Build the result bottom up. */
829    for (i = 1; i <= N; i++) {
830        int kTrueLower, kFalseLower;
831        int leftChild, middleChild, rightChild;
832        AigEdge_t g0, g1, fplus, fequal, fminus;
833        int j;
834        AigEdge_t newMap[2];
835        int newIndex[2];
836
837        kTrueLower = kTrue; /** 2, **/
838        kFalseLower = kFalse; /** 1, **/
839        /* kTrue = ceiling((c-1)/2^i) + 1 */
840        kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1; /** 2,  **/
841        mask = (mask << 1) | 1; /** 0x11,  **/
842        /* kFalse = floor(c/2^i) - 1 */
843        kFalse = (c >> i) - 1; /** 0, **/
844        newIndex[0] = invalidIndex;
845        newIndex[1] = invalidIndex;
846       
847        for (j = kFalse + 1; j < kTrue; j++) {
848            /* Skip if node is not reachable from top of AIG. */
849            if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
850
851            /* Find f- */
852            leftChild = (j << 1) - 1;
853            if (leftChild >= kTrueLower) {
854                fminus = Aig_One;
855            } else if (leftChild <= kFalseLower) {
856                fminus = Aig_Zero;
857            } else {
858                assert(leftChild == index[0] || leftChild == index[1]);
859                if (leftChild == index[0]) {
860                    fminus = map[0];
861                } else {
862                    fminus = map[1];
863                }
864            }
865
866            /* Find f= */
867            middleChild = j << 1;
868            if (middleChild >= kTrueLower) {
869                fequal = Aig_One;
870            } else if (middleChild <= kFalseLower) {
871                fequal = Aig_Zero;
872            } else {
873                assert(middleChild == index[0] || middleChild == index[1]);
874                if (middleChild == index[0]) {
875                    fequal = map[0];
876                } else {
877                    fequal = map[1];
878                }
879            }
880
881            /* Find f+ */
882            rightChild = (j << 1) + 1;
883            if (rightChild >= kTrueLower) {
884                fplus = Aig_One;
885            } else if (rightChild <= kFalseLower) {
886                fplus = Aig_Zero;
887            } else {
888                assert(rightChild == index[0] || rightChild == index[1]);
889                if (rightChild == index[0]) {
890                    fplus = map[0];
891                } else {
892                    fplus = map[1];
893                }
894            }
895
896            /* Build new nodes. */
897            g1 = Aig_Ite(bm, y[N - i], fequal, fplus);
898            if (g1 == Aig_NULL) return(Aig_NULL);
899            g0 = Aig_Ite(bm, y[N - i], fminus, fequal);
900            if (g0 == Aig_NULL) return(Aig_NULL);
901            f = Aig_Ite(bm, x[N - i], g1, g0);
902            if (f == Aig_NULL) return(Aig_NULL);
903
904            /* Save newly computed node in map. */
905            assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
906            if (newIndex[0] == invalidIndex) {
907                newIndex[0] = j;
908                newMap[0] = f;
909            } else {
910                newIndex[1] = j;
911                newMap[1] = f;
912            }
913        }
914
915        /* Copy new map to map. */
916        map[0] = newMap[0];
917        map[1] = newMap[1];
918        index[0] = newIndex[0];
919        index[1] = newIndex[1];
920    }
921
922    return(f);
923
924} /* end of Aig_Inequality */
925#endif
926
927AigEdge_t
928Aig_Inequality(
929   Aig_Manager_t *bm,
930   int  N /* number of x and y variables */,
931   int  nx /* number of x variables */, 
932   int  ny /* number of y variables */,
933   int c /* right-hand side constant */,
934   AigEdge_t *x /* array of x variables */,
935   AigEdge_t *y /* array of y variables */)
936{
937    /* The nodes at level i represent values of the difference that are
938    ** multiples of 2^i.  We use variables with names starting with k
939    ** to denote the multipliers of 2^i in such multiples. */
940    int kTrue = c;
941    int kFalse = c - 1;
942    /* Mask used to compute the ceiling function.  Since we divide by 2^i,
943    ** we want to know whether the dividend is a multiple of 2^i.  If it is,
944    ** then ceiling and floor coincide; otherwise, they differ by one. */
945    int mask = 1;
946    int i;
947
948    AigEdge_t f = Aig_NULL;             /* the eventual result */
949
950    /* Two x-labeled nodes are created at most at each iteration.  They are
951    ** stored, along with their k values, in these variables.  At each level,
952    ** the old nodes are freed and the new nodes are copied into the old map.
953    */
954    AigEdge_t map[2];
955    int invalidIndex = (1 << N)-1;
956    int index[2] = {invalidIndex, invalidIndex};
957    int kTrueLower, kFalseLower;
958    int leftChild, middleChild, rightChild;
959    AigEdge_t g0, g1, fplus, fequal, fminus;
960    int j;
961    AigEdge_t newMap[2];
962    int newIndex[2];
963
964    map[0] = 0;
965    map[1] = 0;
966    newMap[0] = 0;
967    newMap[1] = 0;
968
969    /* This should never happen. */
970    if (N < 0) return(Aig_NULL);
971
972    /* If there are no bits, both operands are 0.  The result depends on c. */
973    if (N == 0) {
974        if (c >= 0) return(Aig_One);
975        else return(Aig_Zero);
976    }
977
978    /* The maximum or the minimum difference comparing to c can generate the terminal case */
979    if ((1 << N) - 1 < c) return(Aig_Zero);
980    else if ((-(1 << N) + 1) >= c) return(Aig_One); 
981
982    /* Build the result bottom up. */
983    for (i = 1; i <= N; i++) {
984        kTrueLower = kTrue; /** 2, **/
985        kFalseLower = kFalse; /** 1, **/
986        /* kTrue = ceiling((c-1)/2^i) + 1 */
987        kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1; /** 2,  **/
988        mask = (mask << 1) | 1; /** 0x11,  **/
989        /* kFalse = floor(c/2^i) - 1 */
990        kFalse = (c >> i) - 1; /** 0, **/
991        newIndex[0] = invalidIndex;
992        newIndex[1] = invalidIndex;
993       
994        for (j = kFalse + 1; j < kTrue; j++) {
995            /* Skip if node is not reachable from top of AIG. */
996            if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
997
998            /* Find f- */
999            leftChild = (j << 1) - 1;
1000            if (leftChild >= kTrueLower) {
1001                fminus = Aig_One;
1002            } else if (leftChild <= kFalseLower) {
1003                fminus = Aig_Zero;
1004            } else {
1005                assert(leftChild == index[0] || leftChild == index[1]);
1006                if (leftChild == index[0]) {
1007                    fminus = map[0];
1008                } else {
1009                    fminus = map[1];
1010                }
1011            }
1012
1013            /* Find f= */
1014            middleChild = j << 1;
1015            if (middleChild >= kTrueLower) {
1016                fequal = Aig_One;
1017            } else if (middleChild <= kFalseLower) {
1018                fequal = Aig_Zero;
1019            } else {
1020                assert(middleChild == index[0] || middleChild == index[1]);
1021                if (middleChild == index[0]) {
1022                    fequal = map[0];
1023                } else {
1024                    fequal = map[1];
1025                }
1026            }
1027
1028            /* Find f+ */
1029            rightChild = (j << 1) + 1;
1030            if (rightChild >= kTrueLower) {
1031                fplus = Aig_One;
1032            } else if (rightChild <= kFalseLower) {
1033                fplus = Aig_Zero;
1034            } else {
1035                assert(rightChild == index[0] || rightChild == index[1]);
1036                if (rightChild == index[0]) {
1037                    fplus = map[0];
1038                } else {
1039                    fplus = map[1];
1040                }
1041            }
1042
1043            /* Build new nodes. */
1044            if (i > ny) 
1045              g1 = fplus;
1046            else
1047              g1 = Aig_Ite(bm, y[i-1], fequal, fplus);
1048           
1049            if (g1 == Aig_NULL) return(Aig_NULL);
1050           
1051            if (i > ny) 
1052              g0 = fequal;
1053            else
1054              g0 = Aig_Ite(bm, y[i-1], fminus, fequal);
1055           
1056            if (g0 == Aig_NULL) return(Aig_NULL);
1057           
1058            if (i > nx) 
1059              f = g0;
1060            else 
1061              f = Aig_Ite(bm, x[i-1], g1, g0);
1062
1063            if (f == Aig_NULL) return(Aig_NULL);
1064
1065            /* Save newly computed node in map. */
1066            assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1067            if (newIndex[0] == invalidIndex) {
1068                newIndex[0] = j;
1069                newMap[0] = f;
1070            } else {
1071                newIndex[1] = j;
1072                newMap[1] = f;
1073            }
1074        }
1075
1076        /* Copy new map to map. */
1077        map[0] = newMap[0];
1078        map[1] = newMap[1];
1079        index[0] = newIndex[0];
1080        index[1] = newIndex[1];
1081    }
1082
1083    return(f);
1084
1085} /* end of Aig_Inequality */
1086
1087
1088/**Function********************************************************************
1089
1090  Synopsis    [Generates a AIG for the function x - y = c.]
1091
1092  Description [This function generates a AIG for the function x -y = c.
1093  Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
1094  y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
1095  The AIG is built bottom-up.
1096  It has a linear number of nodes if the variables are ordered as follows:
1097  x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
1098
1099  SideEffects [None]
1100
1101  SeeAlso     []
1102
1103******************************************************************************/
1104AigEdge_t
1105Aig_Equality(
1106  Aig_Manager_t *bm,
1107  int  N /* number of max variables */,
1108  int  nx /* number of x variables */, 
1109  int  ny /* number of y variables */,
1110  int c /* right-hand side constant */,
1111  AigEdge_t *x /* array of x variables */,
1112  AigEdge_t *y /* array of y variables */)
1113{
1114  /* The nodes at level i represent values of the difference that are
1115  ** multiples of 2^i.  We use variables with names starting with k
1116  ** to denote the multipliers of 2^i in such multiples. */
1117  int kTrueLb = c + 1;
1118  int kTrueUb = c - 1;
1119  int kTrue = c;
1120  /* Mask used to compute the ceiling function.  Since we divide by 2^i,
1121  ** we want to know whether the dividend is a multiple of 2^i.  If it is,
1122  ** then ceiling and floor coincide; otherwise, they differ by one. */
1123  int mask = 1;
1124  int i;
1125 
1126  AigEdge_t f = Aig_NULL;               /* the eventual result */
1127 
1128  /* Two x-labeled nodes are created at most at each iteration.  They are
1129  ** stored, along with their k values, in these variables.  At each level,
1130  ** the old nodes are freed and the new nodes are copied into the old map.
1131  */
1132  AigEdge_t map[2];
1133  int invalidIndex = (1 << N)-1;
1134  int index[2] = {invalidIndex, invalidIndex};
1135
1136  int kTrueLbLower, kTrueUbLower;
1137  int leftChild, middleChild, rightChild;
1138  AigEdge_t g0, g1, fplus, fequal, fminus;
1139  int j;
1140  AigEdge_t newMap[2];
1141  int newIndex[2];
1142
1143  map[0] = 0;
1144  map[1] = 0;
1145  newMap[0] = 0;
1146  newMap[1] = 0;
1147 
1148  /* This should never happen. */
1149  if (N < 0) return(Aig_NULL);
1150 
1151  /* If there are no bits, both operands are 0.  The result depends on c. */
1152  if (N == 0) {
1153    if (c != 0) return(Aig_Zero);
1154    else return(Aig_One);
1155  }
1156 
1157  /* The maximum or the minimum difference comparing to c can generate the terminal case */
1158  if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(Aig_Zero);
1159 
1160  /* Build the result bottom up. */
1161  for (i = 1; i <= N; i++) {
1162   
1163    kTrueLbLower = kTrueLb;
1164    kTrueUbLower = kTrueUb;
1165    /* kTrueLb = floor((c-1)/2^i) + 2 */
1166    kTrueLb = ((c-1) >> i) + 2;
1167    /* kTrueUb = ceiling((c+1)/2^i) - 2 */
1168    kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2;
1169    mask = (mask << 1) | 1;
1170    newIndex[0] = invalidIndex;
1171    newIndex[1] = invalidIndex;
1172   
1173    for (j = kTrueUb + 1; j < kTrueLb; j++) {
1174      /* Skip if node is not reachable from top of AIG. */
1175      if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
1176     
1177      /* Find f- */
1178      leftChild = (j << 1) - 1;
1179      if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) {
1180        fminus = Aig_Zero;
1181      } else if (i == 1 && leftChild == kTrue) {
1182        fminus = Aig_One;
1183      } else {
1184        assert(leftChild == index[0] || leftChild == index[1]);
1185        if (leftChild == index[0]) {
1186          fminus = map[0];
1187        } else {
1188          fminus = map[1];
1189        }
1190      }
1191     
1192      /* Find f= */
1193      middleChild = j << 1;
1194      if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) {
1195        fequal = Aig_Zero;
1196      } else if (i == 1 && middleChild == kTrue) {
1197        fequal = Aig_One;
1198      } else {
1199        assert(middleChild == index[0] || middleChild == index[1]);
1200        if (middleChild == index[0]) {
1201          fequal = map[0];
1202        } else {
1203          fequal = map[1];
1204        }
1205      }
1206     
1207      /* Find f+ */
1208      rightChild = (j << 1) + 1;
1209      if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) {
1210        fplus = Aig_Zero;
1211      } else if (i == 1 && rightChild == kTrue) {
1212        fplus = Aig_One;
1213      } else {
1214        assert(rightChild == index[0] || rightChild == index[1]);
1215        if (rightChild == index[0]) {
1216          fplus = map[0];
1217        } else {
1218          fplus = map[1];
1219        }
1220      }
1221     
1222      /* Build new nodes. */
1223      if (i > ny) 
1224        g1 = fplus;
1225      else {
1226        g1 = Aig_Ite(bm, y[i-1], fequal, fplus);
1227      }
1228     
1229      if (g1 == Aig_NULL) return(Aig_NULL);
1230     
1231      if (i > ny) 
1232        g0 = fequal;
1233      else {
1234        g0 = Aig_Ite(bm, y[i-1], fminus, fequal);
1235      }
1236     
1237      if (g0 == Aig_NULL) return(Aig_NULL);
1238     
1239      if (i > nx) /* number of bits in x is less than N */
1240        f = g0; /* x[N - i] is false */
1241      else {
1242        f = Aig_Ite(bm, x[i-1], g1, g0);
1243      }
1244     
1245      if (f == Aig_NULL) return(Aig_NULL);
1246     
1247      /* Save newly computed node in map. */
1248      assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1249      if (newIndex[0] == invalidIndex) {
1250        newIndex[0] = j;
1251        newMap[0] = f;
1252      } else {
1253        newIndex[1] = j;
1254        newMap[1] = f;
1255      }
1256    }
1257   
1258    /* Copy new map to map. */
1259    map[0] = newMap[0];
1260    map[1] = newMap[1];
1261    index[0] = newIndex[0];
1262    index[1] = newIndex[1];
1263  }
1264 
1265  return(f);
1266 
1267} /* end of Aig_Equality */
1268
1269/**Function********************************************************************
1270
1271  Synopsis    [Generates a AIG for the function x - y != c.]
1272
1273  Description [This function generates a AIG for the function x -y != c.
1274  Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
1275  y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
1276  The BDD is built bottom-up.
1277  It has a linear number of nodes if the variables are ordered as follows:
1278  x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].]
1279
1280  SideEffects [None]
1281
1282  SeeAlso     []
1283
1284******************************************************************************/
1285AigEdge_t
1286Aig_Disequality(
1287  Aig_Manager_t *bm,
1288  int  N /* number of x and y variables */,
1289  int c /* right-hand side constant */,
1290  AigEdge_t *x /* array of x variables */,
1291  AigEdge_t *y /* array of y variables */)
1292{
1293  /* The nodes at level i represent values of the difference that are
1294  ** multiples of 2^i.  We use variables with names starting with k
1295  ** to denote the multipliers of 2^i in such multiples. */
1296  int kTrueLb = c + 1;
1297  int kTrueUb = c - 1;
1298  int kFalse = c;
1299  /* Mask used to compute the ceiling function.  Since we divide by 2^i,
1300  ** we want to know whether the dividend is a multiple of 2^i.  If it is,
1301  ** then ceiling and floor coincide; otherwise, they differ by one. */
1302  int mask = 1;
1303  int i;
1304 
1305  AigEdge_t f = Aig_NULL;               /* the eventual result */
1306 
1307  /* Two x-labeled nodes are created at most at each iteration.  They are
1308  ** stored, along with their k values, in these variables.  At each level,
1309  ** the old nodes are freed and the new nodes are copied into the old map.
1310  */
1311  AigEdge_t map[2];
1312  int invalidIndex = (1 << N)-1;
1313  int index[2] = {invalidIndex, invalidIndex};
1314
1315  int kTrueLbLower, kTrueUbLower;
1316  int leftChild, middleChild, rightChild;
1317  AigEdge_t g0, g1, fplus, fequal, fminus;
1318  int j;
1319  AigEdge_t newMap[2];
1320  int newIndex[2];
1321 
1322  map[0] = 0;
1323  map[1] = 0;
1324  newMap[0] = 0;
1325  newMap[1] = 0;
1326
1327  /* This should never happen. */
1328  if (N < 0) return(Aig_NULL);
1329 
1330  /* If there are no bits, both operands are 0.  The result depends on c. */
1331  if (N == 0) {
1332    if (c != 0) return(Aig_One);
1333    else return(Aig_Zero);
1334  }
1335 
1336  /* The maximum or the minimum difference comparing to c can generate the terminal case */
1337  if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(Aig_One);
1338 
1339  /* Build the result bottom up. */
1340  for (i = 1; i <= N; i++) {
1341    kTrueLbLower = kTrueLb;
1342    kTrueUbLower = kTrueUb;
1343    /* kTrueLb = floor((c-1)/2^i) + 2 */
1344    kTrueLb = ((c-1) >> i) + 2;
1345    /* kTrueUb = ceiling((c+1)/2^i) - 2 */
1346    kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2;
1347    mask = (mask << 1) | 1;
1348    newIndex[0] = invalidIndex;
1349    newIndex[1] = invalidIndex;
1350   
1351    for (j = kTrueUb + 1; j < kTrueLb; j++) {
1352      /* Skip if node is not reachable from top of AIG. */
1353      if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
1354     
1355      /* Find f- */
1356      leftChild = (j << 1) - 1;
1357      if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) {
1358        fminus = Aig_One;
1359      } else if (i == 1 && leftChild == kFalse) {
1360        fminus = Aig_Zero;
1361      } else {
1362        assert(leftChild == index[0] || leftChild == index[1]);
1363        if (leftChild == index[0]) {
1364          fminus = map[0];
1365        } else {
1366          fminus = map[1];
1367        }
1368      }
1369     
1370      /* Find f= */
1371      middleChild = j << 1;
1372      if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) {
1373        fequal = Aig_One;
1374      } else if (i == 1 && middleChild == kFalse) {
1375        fequal = Aig_Zero;
1376      } else {
1377        assert(middleChild == index[0] || middleChild == index[1]);
1378        if (middleChild == index[0]) {
1379          fequal = map[0];
1380        } else {
1381          fequal = map[1];
1382        }
1383      }
1384     
1385      /* Find f+ */
1386      rightChild = (j << 1) + 1;
1387      if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) {
1388        fplus = Aig_One;
1389      } else if (i == 1 && rightChild == kFalse) {
1390        fplus = Aig_Zero;
1391      } else {
1392        assert(rightChild == index[0] || rightChild == index[1]);
1393        if (rightChild == index[0]) {
1394          fplus = map[0];
1395        } else {
1396          fplus = map[1];
1397        }
1398      }
1399     
1400      /* Build new nodes. */
1401      g1 = Aig_Ite(bm, y[N - i], fequal, fplus);
1402      if (g1 == Aig_NULL) return(Aig_NULL);
1403      g0 = Aig_Ite(bm, y[N - i], fminus, fequal);
1404      if (g0 == Aig_NULL) return(Aig_NULL);
1405      f = Aig_Ite(bm, x[N - i], g1, g0);
1406      if (f == Aig_NULL) return(Aig_NULL);
1407     
1408      /* Save newly computed node in map. */
1409      assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1410      if (newIndex[0] == invalidIndex) {
1411        newIndex[0] = j;
1412        newMap[0] = f;
1413      } else {
1414        newIndex[1] = j;
1415        newMap[1] = f;
1416      }
1417    }
1418   
1419    /* Copy new map to map. */
1420    map[0] = newMap[0];
1421    map[1] = newMap[1];
1422    index[0] = newIndex[0];
1423    index[1] = newIndex[1];
1424  }
1425 
1426  return(f);
1427 
1428} /* end of Aig_Disequality */
1429
1430
1431/**Function********************************************************************
1432
1433  Synopsis    [Generates a Aig for the function lb &le; x &ge; ub.]
1434
1435  Description [This function generates a Aig for the function lb &le; x &ge; ub.
1436  x is N-bit number, x\[0\] x\[1\] ... x\[N-1\] and with 0 the most significant
1437  bit.  The BDD is built bottom-up.
1438  It has a linear number of nodes if the variables are ordered as follows:
1439  x\[0\] x\[1\] ... x\[N-1\].]
1440
1441  SideEffects [None]
1442
1443  SeeAlso     []
1444
1445******************************************************************************/
1446AigEdge_t
1447Aig_Bound(
1448   Aig_Manager_t *bm,
1449   int  N /* number of x variables */,
1450   int lb /* lower bound */,
1451   int ub /* upper bound */,
1452   AigEdge_t *x /* array of x variables */)
1453{
1454  /* The nodes at level i represent values of the difference that are
1455  ** multiples of 2^i.  We use variables with names starting with k
1456  ** to denote the multipliers of 2^i in such multiples. */
1457  int kTrueLb = lb;
1458  int kTrueUb = ub;
1459  int kFalseLb = ub + 1;
1460  int kFalseUb = lb - 1;
1461  /* Mask used to compute the ceiling function.  Since we divide by 2^i,
1462  ** we want to know whether the dividend is a multiple of 2^i.  If it is,
1463  ** then ceiling and floor coincide; otherwise, they differ by one. */
1464  int mask = 1;
1465  int i;
1466 
1467  AigEdge_t f = Aig_NULL;               /* the eventual result */
1468 
1469  /* Two x-labeled nodes are created at most at each iteration.  They are
1470  ** stored, along with their k values, in these variables.  At each level,
1471  ** the old nodes are freed and the new nodes are copied into the old map.
1472  */
1473  AigEdge_t map[2];
1474  int invalidIndex = (1 << N)-1;
1475  /** int invalidValue = (1 << N)-1; **/
1476  int index[2] = {invalidIndex, invalidIndex};
1477 
1478  int max, min;
1479  int kTrueLbLower, kTrueUbLower, kFalseLbLower, kFalseUbLower;
1480  int leftChild, rightChild;
1481  AigEdge_t f1, f0;
1482  int j;
1483  AigEdge_t newMap[2];
1484  int newIndex[2];
1485
1486  map[0] = 0;
1487  map[1] = 0;
1488  newMap[0] = 0;
1489  newMap[1] = 0;
1490
1491  /* This should never happen. */
1492  if (N < 0) return(Aig_NULL);
1493 
1494  /* If there are no bits, both operands are 0.  The result depends on c. */
1495  if (N == 0) {
1496    if (lb <= 0 && ub >= 0) return(Aig_One);
1497    else return(Aig_Zero);
1498  }
1499 
1500  /* The maximum or the minimum difference comparing to c generates the terminal case */
1501  {
1502    max = (1 << N) - 1;
1503    min = 0;
1504   
1505    if (max < lb || min > ub) return(Aig_Zero);
1506    else if (max <= ub && min >= lb) return(Aig_One); 
1507   
1508    /* Build the result bottom up. */
1509    for (i = 1; i <= N; i++) {
1510     
1511      kTrueLbLower = kTrueLb;
1512      kTrueUbLower = kTrueUb;
1513      kFalseLbLower = kFalseLb;
1514      kFalseUbLower = kFalseUb;
1515      /* kTrueLb = ceiling(lb/2^i) */
1516      kTrueLb = (lb >> i) + (((lb+1) & mask) != 1);
1517      /* kTrueUb = floor((ub+1)/2^i) - 1 */
1518      kTrueUb = ((ub+1) >> i) - 1;
1519      /* kFalseLb = ceiling((ub+1)/2^i) */
1520      kFalseLb = ((ub+1) >> i) + (((ub+2) & mask) != 1);
1521      /* kFalseUb = floor(lb/2^i) - 1 */
1522      kFalseUb = (lb >> i) - 1;
1523      mask = (mask << 1) | 1;
1524      newIndex[0] = invalidIndex;
1525      newIndex[1] = invalidIndex;
1526     
1527      j = kTrueUb + 1;
1528      if (j >= 0 && j < (1 << (N - i)) && j < kFalseLb) {
1529        /* Find f1 */
1530        leftChild = (j << 1) + 1;
1531        if (leftChild >= kTrueLbLower && leftChild <= kTrueUbLower) {
1532          f1 = Aig_One;
1533        } else if (leftChild <= kFalseUbLower || leftChild >= kFalseLbLower) {
1534          f1 = Aig_Zero;
1535        } else {
1536          assert(leftChild == index[0] || leftChild == index[1]);
1537          if (leftChild == index[0]) {
1538            f1 = map[0];
1539          } else {
1540            f1 = map[1];
1541          }
1542        }
1543       
1544        /* Find f0 */
1545        rightChild = j << 1;
1546        if (rightChild >= kTrueLbLower && rightChild <= kTrueUbLower) {
1547          f0 = Aig_One;
1548        } else if (rightChild <= kFalseUbLower || rightChild >= kFalseLbLower) {
1549          f0 = Aig_Zero;
1550        } else {
1551          assert(rightChild == index[0] || rightChild == index[1]);
1552          if (rightChild == index[0]) {
1553            f0 = map[0];
1554          } else {
1555            f0 = map[1];
1556          }
1557        }
1558       
1559        /* Build new nodes. */
1560        f = Aig_Ite(bm, x[i-1], f1, f0);
1561       
1562        if (f == Aig_NULL) return(Aig_NULL);
1563       
1564        /* Save newly computed node in map. */
1565        assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1566        if (newIndex[0] == invalidIndex) {
1567          newIndex[0] = j;
1568          newMap[0] = f;
1569        } else {
1570          newIndex[1] = j;
1571          newMap[1] = f;
1572        }
1573      }
1574     
1575      j = kFalseUb + 1;
1576      if (kTrueUb != kFalseUb && j >= 0 && j < (1 << (N - i)) && j < kTrueLb) { 
1577        /* Find f1 */
1578        leftChild = (j << 1) + 1;
1579        if (leftChild >= kTrueLbLower && leftChild <= kTrueUbLower) {
1580          f1 = Aig_One;
1581        } else if (leftChild <= kFalseUbLower || leftChild >= kFalseLbLower) {
1582          f1 = Aig_Zero;
1583        } else {
1584          assert(leftChild == index[0] || leftChild == index[1]);
1585          if (leftChild == index[0]) {
1586            f1 = map[0];
1587          } else {
1588            f1 = map[1];
1589          }
1590        }
1591       
1592        /* Find f0 */
1593        rightChild = j << 1;
1594        if (rightChild >= kTrueLbLower && rightChild <= kTrueUbLower) {
1595          f0 = Aig_One;
1596        } else if (rightChild <= kFalseUbLower || rightChild >= kFalseLbLower) {
1597          f0 = Aig_Zero;
1598        } else {
1599          assert(rightChild == index[0] || rightChild == index[1]);
1600          if (rightChild == index[0]) {
1601            f0 = map[0];
1602          } else {
1603            f0 = map[1];
1604          }
1605        }
1606       
1607        /* Build new nodes. */
1608        f = Aig_Ite(bm, x[i-1], f1, f0);
1609        if (f == Aig_NULL) return(Aig_NULL);
1610       
1611        /* Save newly computed node in map. */
1612        assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1613        if (newIndex[0] == invalidIndex) {
1614          newIndex[0] = j;
1615          newMap[0] = f;
1616        } else {
1617          newIndex[1] = j;
1618          newMap[1] = f;
1619        }
1620      }
1621     
1622      /* Copy new map to map. */
1623      map[0] = newMap[0];
1624      map[1] = newMap[1];
1625      index[0] = newIndex[0];
1626      index[1] = newIndex[1];
1627    }
1628  }
1629 
1630  return(f);
1631 
1632} /* end of Aig_Inequality */
1633
1634/**Function********************************************************************
1635
1636  Synopsis    [create new node]
1637
1638  Description []
1639
1640  SideEffects []
1641
1642  SeeAlso     []
1643
1644******************************************************************************/
1645AigEdge_t
1646Aig_CreateNode(
1647   Aig_Manager_t  *bm,
1648   AigEdge_t nodeIndex1,
1649   AigEdge_t nodeIndex2)
1650{
1651 
1652  AigEdge_t newNode = bm->nodesArraySize;
1653
1654  if (bm->nodesArraySize >= bm->maxNodesArraySize ){
1655    bm->maxNodesArraySize = 2* bm->maxNodesArraySize;
1656    bm->NodesArray = REALLOC(AigEdge_t, bm->NodesArray, bm->maxNodesArraySize);
1657    bm->nameList   = REALLOC(char *,     bm->nameList  , bm->maxNodesArraySize/AigNodeSize);
1658  }
1659  bm->NodesArray[Aig_NonInvertedEdge(newNode)+AigRight] = nodeIndex2;
1660  bm->NodesArray[Aig_NonInvertedEdge(newNode)+AigLeft]  = nodeIndex1;
1661 
1662  aig_next(newNode)     = Aig_NULL;
1663  fanout(newNode) = 0;
1664  canonical(newNode) = newNode;
1665  flags(newNode) = 0;
1666  nFanout(newNode) = 0;
1667
1668  bm->nodesArraySize +=AigNodeSize;
1669 
1670  return(newNode);
1671}
1672
1673
1674/**Function********************************************************************
1675
1676  Synopsis [Return the Aig node given its name.]
1677
1678  SideEffects []
1679
1680******************************************************************************/
1681AigEdge_t
1682Aig_FindNodeByName(
1683  Aig_Manager_t *bm,
1684  nameType_t     *name)
1685{
1686   
1687  AigEdge_t node;
1688
1689  if (!st_lookup(bm->SymbolTable, name, &node)){
1690    node = Aig_NULL;
1691  }
1692
1693  return Aig_GetCanonical(bm, node);
1694}
1695
1696
1697/**Function********************************************************************
1698
1699  Synopsis    [create var node ]
1700
1701  Description []
1702
1703  SideEffects []
1704
1705  SeeAlso     []
1706
1707******************************************************************************/
1708AigEdge_t
1709Aig_CreateVarNode(
1710   Aig_Manager_t  *bm,
1711   nameType_t      *name)
1712{
1713   
1714  AigEdge_t varIndex;
1715
1716
1717  if (!st_lookup(bm->SymbolTable, name, &varIndex)){
1718    varIndex = Aig_CreateNode(bm, Aig_NULL, Aig_NULL);
1719    if (varIndex == Aig_NULL){
1720      return (varIndex);
1721    } 
1722    /* Insert the varaible in the Symbol Table */
1723    st_insert(bm->SymbolTable, name, (char*) (long) varIndex);
1724    bm->nameList[AigNodeID(varIndex)] = name; 
1725    return(varIndex);
1726  }
1727  else {
1728    return (varIndex);
1729  }
1730}
1731
1732/**Function********************************************************************
1733
1734  Synopsis [Return True if this node is Variable node]
1735
1736  SideEffects []
1737
1738******************************************************************************/
1739int 
1740Aig_isVarNode(
1741   Aig_Manager_t *bm,
1742   AigEdge_t      node)
1743{
1744  if((rightChild(node) == Aig_NULL) && (leftChild(node) == Aig_NULL)) {
1745    return 1;
1746  }
1747  return 0;
1748}
1749
1750
1751
1752/**Function********************************************************************
1753
1754  Synopsis [Build the binary AND/INVERTER graph for a given bdd function]
1755
1756  SideEffects [Build the binary AND/INVERTER graph for a given bdd function.
1757               We assume that the return bdd nodes from the foreach_bdd_node are
1758               in the order from childeren to parent. i.e all the childeren
1759               nodes are returned before the parent node.]
1760
1761  SideEffects []
1762
1763  SeeAlso     []
1764 
1765******************************************************************************/
1766#if 0
1767AigEdge_t
1768Aig_bddToAig(
1769   Aig_Manager_t *AigManager,
1770   bdd_t          *fn)
1771{
1772  bdd_gen     *gen;
1773  bdd_node    *node, *thenNode, *elseNode, *funcNode;
1774  bdd_manager *bddManager = bdd_get_manager(fn);
1775  /*
1776    Used to read the variable name of a bdd node.
1777  */
1778  array_t     *mvar_list  = mdd_ret_mvar_list(bddManager);
1779  array_t     *bvar_list  = mdd_ret_bvar_list(bddManager);
1780  bvar_type   bv;
1781  mvar_type   mv;
1782 
1783  bdd_node    *one        = bdd_read_one(bddManager); 
1784  int         is_complemented;
1785  int         flag; 
1786  AigEdge_t  var, left, right, result;
1787 
1788  char      name[100];
1789  st_table  *bddTOAigTable;
1790 
1791  if (fn == NULL){
1792    return Aig_NULL;
1793  }
1794  funcNode = bdd_get_node(fn, &is_complemented);
1795  if (bdd_is_constant(funcNode)){
1796    return (is_complemented?Aig_Zero:Aig_One);
1797  }
1798  bddTOAigTable = st_init_table(st_numcmp, st_numhash);
1799  st_insert(bddTOAigTable, (char *) (long) bdd_regular(one),  (char *) Aig_One);
1800
1801  foreach_bdd_node(fn, gen, node){
1802    int nodeIndex = bdd_node_read_index(node);
1803    int index, rtnNodeIndex;
1804
1805    if (bdd_is_constant(node)){
1806      continue;
1807    }
1808
1809    bv = array_fetch(bvar_type, bvar_list, nodeIndex);
1810    /*
1811      get the multi-valued varaible.
1812     */
1813    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
1814    arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
1815      if (nodeIndex == rtnNodeIndex){
1816        break;
1817      }
1818    }
1819    assert(index < mv.encode_length);
1820    /*
1821    printf("Name of bdd node %s %d\n", mv.name, index);
1822    */
1823    sprintf(name, "%s_%d", mv.name, index);
1824    /*
1825      Create or Retrieve the AigEdge_t  w.r.t. 'name'
1826    */
1827    var  = Aig_CreateVarNode(AigManager, util_strsav(name));
1828
1829    thenNode  = bdd_bdd_T(node);
1830    flag = st_lookup(bddTOAigTable, (char *) (long) bdd_regular(thenNode),
1831                     &left);
1832    assert(flag);
1833     
1834    elseNode  = bdd_bdd_E(node);
1835    flag = st_lookup(bddTOAigTable, (char *) (long) bdd_regular(elseNode),
1836                     &right);
1837    assert(flag);
1838    /*
1839     test if the elseNode is complemented arc?
1840    */
1841    if (bdd_is_complement(elseNode)){
1842      right = Aig_Not(right);
1843    }
1844    if (right ==  Aig_Zero){        /* result = var*then */
1845      result =  Aig_And(AigManager, var, left);
1846    } else if (right ==  Aig_One){        /* result = then + not(var) */
1847      result =  Aig_Or(AigManager, left, Aig_Not(var));
1848    } else if (left ==  Aig_One) { /* result = var + else */
1849      result =  Aig_Or(AigManager, var, right);     
1850    } else {                        /* result = var * then + not(var)*else */
1851      result =  Aig_Or(AigManager, Aig_And(AigManager, var, left),
1852                        Aig_And(AigManager, Aig_Not(var), right));
1853    }
1854    st_insert(bddTOAigTable, (char *) (long) bdd_regular(node),
1855              (char *) (long) result);
1856  }
1857  flag = st_lookup(bddTOAigTable, (char *) (long) bdd_regular(funcNode),
1858                   &result); 
1859  assert(flag);
1860  st_free_table(bddTOAigTable);
1861
1862  if (is_complemented){
1863    return Aig_Not(result);
1864  } else {
1865    return result;
1866  }
1867} /* end of Aig_bddtoAig() */
1868#endif
1869
1870/**Function********************************************************************
1871
1872  Synopsis [Print dot file for AIG nodes]
1873
1874  SideEffects []
1875
1876******************************************************************************/
1877int
1878Aig_PrintDot(
1879  FILE *fp,
1880  Aig_Manager_t *bm)
1881{
1882  long i;
1883
1884  /*
1885   * Write out the header for the output file.
1886   */
1887  (void) fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
1888  (void) fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
1889  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");
1890 
1891 
1892  for (i=AigFirstNodeIndex ; i<bm->nodesArraySize ; i+=AigNodeSize){
1893    (void) fprintf(fp,"Node%ld  [label=\"%s \"];\n",i,Aig_NodeReadName(bm, i));
1894  }
1895  for (i=AigFirstNodeIndex ; i< bm->nodesArraySize ; i+=AigNodeSize){
1896    if (rightChild(i) != Aig_NULL){
1897      if (Aig_IsInverted(rightChild(i))){
1898        (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",Aig_NonInvertedEdge(rightChild(i)), i);
1899      }
1900      else{
1901        (void) fprintf(fp,"Node%ld -> Node%ld;\n",Aig_NonInvertedEdge(rightChild(i)), i);
1902      }
1903      if (Aig_IsInverted(leftChild(i))){
1904        (void) fprintf(fp,"Node%ld -> Node%ld [color = red];\n",Aig_NonInvertedEdge(leftChild(i)), i);
1905      }
1906      else{
1907        (void) fprintf(fp,"Node%ld -> Node%ld;\n",Aig_NonInvertedEdge(leftChild(i)), i);
1908      }
1909    }/* if */ 
1910  }/*for */
1911
1912  (void) fprintf(fp, "}\n");
1913
1914  return 1;
1915}
1916
1917
1918
1919/**Function********************************************************************
1920
1921  Synopsis [Print dot file for AIG nodes]
1922
1923  SideEffects []
1924
1925******************************************************************************/
1926int
1927Aig_PrintAIG(Aig_Manager_t *bm, AigEdge_t object, char *fileName)
1928{
1929  FILE *fp;
1930  long nInput, nAnd;
1931  long i;
1932  char *str;
1933
1934  str = util_strcat3(fileName, ".aag", "");
1935
1936  fp = fopen(str, "w");
1937
1938  free(str);
1939
1940  /* count # of inputs & # of and gates */
1941  for (i=AigFirstNodeIndex, nInput=0, nAnd=0; i<bm->nodesArraySize ; i+=AigNodeSize){
1942    if (leftChild(i)==Aig_NULL && rightChild(i)==Aig_NULL)
1943      nInput++;
1944    else
1945      nAnd++;
1946  }
1947
1948  /*
1949   * Write out the header for the output file:
1950   * # of nodes, # of inputs, # of latches, # of outputs, # of AND gates
1951   */
1952  (void) fprintf(fp, "aag %ld %ld 0 1 %ld\n", nInput+nAnd, nInput, nAnd);
1953 
1954  /* Input */
1955  for (i=AigFirstNodeIndex ; i<bm->nodesArraySize ; i+=AigNodeSize){
1956    if (leftChild(i)==Aig_NULL && rightChild(i)==Aig_NULL)
1957      fprintf(fp,"%ld\n",i/4);
1958  }
1959  /* Output */
1960  if (Aig_IsInverted(object))
1961    fprintf(fp, "%ld\n", (Aig_NonInvertedEdge(object)/4)+1);
1962  else
1963    fprintf(fp, "%ld\n", (Aig_NonInvertedEdge(object)/4));
1964
1965  /* AND gates */
1966  for (i=AigFirstNodeIndex ; i< bm->nodesArraySize ; i+=AigNodeSize){
1967    if (leftChild(i)!=Aig_NULL || rightChild(i)!=Aig_NULL) {
1968      fprintf(fp, "%ld ", i/4);
1969      if (rightChild(i) != Aig_NULL) {
1970        if (Aig_IsInverted(rightChild(i)))
1971          fprintf(fp,"%ld ", (Aig_NonInvertedEdge(rightChild(i))/4)+1);
1972        else
1973          fprintf(fp,"%ld ", Aig_NonInvertedEdge(rightChild(i))/4);
1974      }
1975      if (leftChild(i) != Aig_NULL) {
1976        if (Aig_IsInverted(leftChild(i)))
1977          fprintf(fp,"%ld", (Aig_NonInvertedEdge(leftChild(i))/4)+1);
1978        else
1979          fprintf(fp,"%ld", Aig_NonInvertedEdge(leftChild(i))/4);
1980      }     
1981      fprintf(fp, "\n");
1982    }
1983  }
1984
1985  fclose(fp);
1986
1987  return 1;
1988}
1989
1990
1991
1992/**Function********************************************************************
1993
1994  Synopsis    [Set pass flag for node]
1995
1996  Description []
1997
1998  SideEffects []
1999
2000  SeeAlso     []
2001
2002******************************************************************************/
2003
2004void 
2005AigSetPassFlag(
2006    Aig_Manager_t  *bm,
2007    AigEdge_t node)
2008{
2009
2010   flags(node) |= CanonicalBitMask;
2011}
2012
2013/**Function********************************************************************
2014
2015  Synopsis    [Reset pass flag for node]
2016
2017  Description []
2018
2019  SideEffects []
2020
2021  SeeAlso     []
2022
2023******************************************************************************/
2024
2025void 
2026AigResetPassFlag(
2027    Aig_Manager_t  *bm,
2028    AigEdge_t node)
2029{
2030
2031   flags(node) &= ResetCanonicalBitMask;
2032}
2033
2034/**Function********************************************************************
2035
2036  Synopsis    [Get pass flag for node]
2037
2038  Description []
2039
2040  SideEffects []
2041
2042  SeeAlso     []
2043
2044******************************************************************************/
2045
2046int
2047AigGetPassFlag(
2048    Aig_Manager_t  *bm,
2049    AigEdge_t node)
2050   
2051{
2052  return((flags(node) & CanonicalBitMask) != 0);
2053}
2054
2055/**Function********************************************************************
2056
2057  Synopsis    [Create AND node and assign name to it ]
2058
2059  Description []
2060
2061  SideEffects []
2062
2063  SeeAlso     []
2064
2065******************************************************************************/
2066AigEdge_t
2067AigCreateAndNode(
2068   Aig_Manager_t  *bm,
2069   AigEdge_t node1,
2070   AigEdge_t node2)
2071{
2072   
2073  AigEdge_t varIndex;
2074  char       *name = NIL(char);
2075  char       *node1Str = util_inttostr(node1);
2076  char       *node2Str = util_inttostr(node2);
2077
2078  name = util_strcat4("Nd", node1Str,"_", node2Str);
2079  while (st_lookup(bm->SymbolTable, name, &varIndex)){
2080    printf("Find redundant node at %ld %ld\n", node1, node2);
2081    name = util_strcat3(name, node1Str, node2Str);
2082  }
2083  FREE(node1Str);
2084  FREE(node2Str);
2085  varIndex = Aig_CreateNode(bm, node1, node2);
2086  if (varIndex == Aig_NULL){
2087    FREE(name);
2088    return (varIndex);
2089  } 
2090  /* Insert the varaible in the Symbol Table */
2091  st_insert(bm->SymbolTable, name, (char*) (long) varIndex);
2092  bm->nameList[AigNodeID(varIndex)] = name; 
2093
2094  return(varIndex);
2095
2096}
2097
2098/*---------------------------------------------------------------------------*/
2099/* Definition of static functions                                            */
2100/*---------------------------------------------------------------------------*/
2101
2102/**Function********************************************************************
2103
2104  Synopsis    [Connect fanin fanout of two AIG nodes]
2105
2106  Description []
2107
2108  SideEffects []
2109
2110  SeeAlso     []
2111
2112******************************************************************************/
2113static void
2114connectOutput(
2115   Aig_Manager_t *bm,
2116   AigEdge_t from,
2117   AigEdge_t to,
2118   int inputIndex)
2119{
2120  AigEdge_t *pfan;
2121  int nfan;
2122
2123  to = Aig_NonInvertedEdge(to);
2124  pfan = (AigEdge_t *)fanout(from);
2125  nfan = nFanout(from);
2126  if(nfan == 0) pfan = ALLOC(AigEdge_t, 2);
2127  else          pfan = REALLOC(AigEdge_t, pfan, nfan+2);
2128  to += Aig_IsInverted(from);
2129  to = to << 1;
2130  to += inputIndex;
2131  pfan[nfan++] = to;
2132  pfan[nfan] = 0;
2133  fanout(from) = (long)pfan;
2134  nFanout(from) = nfan;
2135}
2136
2137
2138/**Function********************************************************************
2139
2140  Synopsis    [disconnect fanin fanout of two AIG nodes]
2141
2142  Description []
2143
2144  SideEffects []
2145
2146  SeeAlso     []
2147
2148static void
2149unconnectOutput(
2150   Aig_Manager_t *bm,
2151   AigEdge_t from,
2152   AigEdge_t to)
2153{
2154   AigEdge_t cur, *pfan, *newfan;
2155   int i, nfan;
2156
2157  from = Aig_NonInvertedEdge(from);
2158  to = Aig_NonInvertedEdge(to);
2159
2160  pfan = (AigEdge_t *)fanout(from);
2161  nfan = nFanout(from);
2162  newfan = (AigEdge_t *)malloc(sizeof(AigEdge_t)*(nfan));
2163  for(i=0; i<nfan; i++) {
2164    cur = pfan[i];
2165    cur = cur >> 1;
2166    cur = Aig_NonInvertedEdge(cur);
2167    if(cur == to) {
2168      memcpy(newfan, pfan, sizeof(AigEdge_t)*i);
2169      memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(AigEdge_t)*(nfan-i-1));
2170      newfan[nfan-1] = 0;
2171      fanout(from) = (int)newfan;
2172      free(pfan);
2173      nFanout(from) = nfan-1;
2174      break;
2175    }
2176  }
2177}
2178******************************************************************************/
2179
2180
2181/**Function********************************************************************
2182
2183  Synopsis    [Look for the node in the Hash Table.]
2184
2185  Description [.]
2186
2187  SideEffects []
2188
2189  SeeAlso     []
2190
2191******************************************************************************/
2192static AigEdge_t
2193HashTableLookup(
2194  Aig_Manager_t *bm, 
2195  AigEdge_t  node1,
2196  AigEdge_t  node2)
2197{
2198  AigEdge_t key = HashTableFunction(node1, node2);
2199  AigEdge_t node;
2200 
2201  node = bm->HashTable[key];
2202  if  (node == Aig_NULL) {
2203    return Aig_NULL;
2204  }
2205  else{
2206    while ( (rightChild(Aig_NonInvertedEdge(node)) != node2) ||
2207            (leftChild(Aig_NonInvertedEdge(node))  != node1)) {
2208 
2209      if (aig_next(Aig_NonInvertedEdge(node)) == Aig_NULL){
2210        return(Aig_NULL); 
2211      }
2212      node = aig_next(Aig_NonInvertedEdge(node)); /* Get the next Node */
2213    } /* While loop */ 
2214    return(node);
2215
2216  } /* If Then Else */
2217   
2218} /* End of HashTableLookup() */
2219
2220/**Function********************************************************************
2221
2222  Synopsis    [Add a node in the Hash Table.]
2223
2224  Description []
2225
2226  SideEffects []
2227
2228  SeeAlso     []
2229
2230******************************************************************************/
2231static int
2232HashTableAdd(
2233  Aig_Manager_t   *bm, 
2234  AigEdge_t  nodeIndexParent,
2235  AigEdge_t  nodeIndex1,
2236  AigEdge_t  nodeIndex2)
2237{
2238  AigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
2239  AigEdge_t nodeIndex;
2240  AigEdge_t node;
2241                                               
2242  nodeIndex = bm->HashTable[key];
2243  if  (nodeIndex == Aig_NULL) {
2244    bm->HashTable[key] = nodeIndexParent;
2245    return TRUE;
2246  }
2247  else{
2248    node = nodeIndex;
2249    nodeIndex = aig_next(Aig_NonInvertedEdge(nodeIndex));  /* Get the Node */
2250    while (nodeIndex != Aig_NULL) {
2251      node = nodeIndex;
2252      nodeIndex = aig_next(Aig_NonInvertedEdge(nodeIndex));
2253    }
2254    aig_next(Aig_NonInvertedEdge(node)) = nodeIndexParent;
2255    return TRUE;
2256  }
2257   
2258} /* End of HashTableAdd() */
2259
2260
2261/**Function********************************************************************
2262
2263  Synopsis    [Hash table delete]
2264
2265  Description [Hash table delete]
2266
2267  SideEffects []
2268
2269  SeeAlso     []
2270
2271******************************************************************************/
2272#if 0
2273static int
2274HashTableDelete(
2275  Aig_Manager_t   *bm, 
2276  AigEdge_t  node)
2277{
2278  AigEdge_t key = HashTableFunction(leftChild(node), rightChild(node));
2279  AigEdge_t nodeIndex;
2280                                               
2281  nodeIndex = bm->HashTable[key];
2282  if (nodeIndex == node) {
2283    bm->HashTable[key] = aig_next(node);
2284    return TRUE;
2285  }
2286  else{
2287    while(nodeIndex && aig_next(Aig_NonInvertedEdge(nodeIndex)) != node)
2288      nodeIndex = aig_next(Aig_NonInvertedEdge(nodeIndex));
2289
2290    aig_next(Aig_NonInvertedEdge(nodeIndex)) =
2291        aig_next(Aig_NonInvertedEdge(aig_next(Aig_NonInvertedEdge(nodeIndex))));
2292    return TRUE;
2293  }
2294   
2295} /* End of HashTableAdd() */
2296#endif
2297
2298/**Function********************************************************************
2299
2300  Synopsis    [Structural hasing for and4]
2301
2302  Description [Structural hasing for and4]
2303
2304  SideEffects []
2305
2306  SeeAlso     []
2307
2308******************************************************************************/
2309
2310AigEdge_t
2311Aig_And4(
2312           Aig_Manager_t *bm,
2313           AigEdge_t l,
2314           AigEdge_t r)
2315{
2316  int caseIndex, caseSig;
2317  AigEdge_t ll, lr, rl, rr;
2318  AigEdge_t t1, t2;
2319
2320  ll = leftChild(l);
2321  lr = rightChild(l);
2322  rl = leftChild(r);
2323  rr = rightChild(r);
2324
2325  if(AigCompareNode(l, rl) ||
2326     AigCompareNode(l, rr)) {
2327    return(Aig_And3(bm, l, r));
2328  }
2329  else if(AigCompareNode(r, ll) ||
2330     AigCompareNode(r, lr)) {
2331    return(Aig_And3(bm, r, l));
2332  }
2333
2334  if(ll > lr+1) AigSwap(ll, lr);
2335  if(rl > rr+1) AigSwap(rl, rr);
2336
2337  caseIndex = 0; /* (a b)(c d) */
2338  if(AigCompareNode(ll, rl)) {
2339    if(AigCompareNode(lr, rr)) {
2340      caseIndex = 4; /* (a b) (a b) */
2341    }
2342    else {
2343      caseIndex = 1; /* (a b) (a c) */
2344      if(lr > rr+1) {
2345        AigSwap(ll, rl);
2346        AigSwap(lr, rr); 
2347        AigSwap(l, r); 
2348      }
2349    }
2350  }
2351  else if(AigCompareNode(lr, rl)) {
2352    caseIndex = 2; /* (b a)(a c) */
2353  }
2354  else if(AigCompareNode(lr, rr)) {
2355    caseIndex = 3; /* (b a)(c a) */
2356    if(ll > rl+1) {
2357      AigSwap(ll, rl);
2358      AigSwap(lr, rr); 
2359      AigSwap(l, r); 
2360    }
2361  }
2362  else if(AigCompareNode(ll, rr)) {
2363    /* (a b)(c a)  */
2364    AigSwap(ll, rl);
2365    AigSwap(lr, rr); 
2366    AigSwap(l, r); 
2367    caseIndex = 2; /* (c a )(a b) because of c < b */
2368  }
2369
2370  caseSig = 0;
2371  if(Aig_IsInverted(ll)) caseSig += 32;
2372  if(Aig_IsInverted(lr)) caseSig += 16;
2373  if(Aig_IsInverted(l))  caseSig += 8;
2374  if(Aig_IsInverted(rl)) caseSig += 4;
2375  if(Aig_IsInverted(rr)) caseSig += 2;
2376  if(Aig_IsInverted(r))  caseSig += 1;
2377  /**
2378  fprintf(stdout, "Index: %d Sig: %2d  (%5d%c %5d%c)%c (%5d%c %5d%c)%c (%5d, %5d)\n",
2379          caseIndex, caseSig,
2380          Aig_NonInvertedEdge(ll), Aig_IsInverted(ll) ? '\'' : ' ',
2381          Aig_NonInvertedEdge(lr), Aig_IsInverted(lr) ? '\'' : ' ',
2382          Aig_IsInverted(l) ? '\'' : ' ',
2383          Aig_NonInvertedEdge(rl), Aig_IsInverted(rl) ? '\'' : ' ',
2384          Aig_NonInvertedEdge(rr), Aig_IsInverted(rr) ? '\'' : ' ',
2385          Aig_IsInverted(r) ? '\'' : ' ',
2386          Aig_NonInvertedEdge(l), Aig_NonInvertedEdge(r)
2387           );
2388           **/
2389  if(caseIndex == 0) {
2390    return(Aig_And2(bm, l, r));
2391  }
2392  else if(caseIndex == 1) {
2393    switch(caseSig) {
2394        case 19 :
2395        case 17 :
2396        case 3 :
2397        case 1 :
2398        case 55 :
2399        case 53 :
2400        case 39 :
2401        case 37 :
2402      t1 = Aig_And(bm, lr, Aig_Not(rr));
2403      t2 = Aig_And(bm, ll, t1);
2404      return(t2);
2405        case 18 :
2406        case 16 :
2407        case 2 :
2408        case 0 :
2409        case 54 :
2410        case 52 :
2411        case 38 :
2412        case 36 :
2413      t1 = Aig_And(bm, lr, rr);
2414      t2 = Aig_And(bm, ll, t1);
2415      return(t2);
2416        case 26 :
2417        case 24 :
2418        case 10 :
2419        case 8 :
2420        case 62 :
2421        case 60 :
2422        case 46 :
2423        case 44 :
2424      t1 = Aig_And(bm, Aig_Not(lr), rr);
2425      t2 = Aig_And(bm, ll, t1);
2426      return(t2);
2427        case 61 :
2428        case 27 :
2429        case 25 :
2430        case 11 :
2431        case 63 :
2432        case 47 :
2433        case 9 :
2434        case 45 :
2435      t1 = Aig_And(bm, Aig_Not(lr), Aig_Not(rr));
2436      t2 = Aig_Or(bm, Aig_Not(ll), t1);
2437      return(t2);
2438        case 23 :
2439        case 21 :
2440        case 7 :
2441        case 5 :
2442        case 51 :
2443        case 49 :
2444        case 35 :
2445        case 33 :
2446      return(l);
2447        case 30 :
2448        case 28 :
2449        case 14 :
2450        case 12 :
2451        case 58 :
2452        case 56 :
2453        case 42 :
2454        case 40 :
2455      return(r);
2456        case 22 :
2457        case 20 :
2458        case 6 :
2459        case 4 :
2460        case 50 :
2461        case 48 :
2462        case 34 :
2463        case 32 :
2464      return(Aig_Zero);
2465        case 31 :
2466        case 29 :
2467        case 15 :
2468        case 13 :
2469        case 59 :
2470        case 57 :
2471        case 43 :
2472        case 41 :
2473      t1 = Aig_And2(bm, l, r);
2474      return(t1);
2475    }
2476  }
2477  else if(caseIndex == 2) {
2478    switch(caseSig) {
2479        case 35 :
2480        case 33 :
2481        case 3 :
2482        case 1 :
2483        case 55 :
2484        case 53 :
2485        case 23 :
2486        case 21 :
2487      t1 = Aig_And(bm, lr, Aig_Not(rr));
2488      t2 = Aig_And(bm, ll, t1);
2489      return(t2);
2490        case 34 :
2491        case 32 :
2492        case 2 :
2493        case 0 :
2494        case 54 :
2495        case 52 :
2496        case 22 :
2497        case 20 :
2498      t1 = Aig_And(bm, lr, rr);
2499      t2 = Aig_And(bm, ll, t1);
2500      return(t2);
2501        case 42 :
2502        case 40 :
2503        case 10 :
2504        case 8 :
2505        case 62 :
2506        case 60 :
2507        case 30 :
2508        case 28 :
2509      t1 = Aig_And(bm, lr, rr);
2510      t2 = Aig_And(bm, Aig_Not(ll), t1);
2511      return(t2);
2512        case 43 :
2513        case 41 :
2514        case 11 :
2515        case 9 :
2516        case 63 :
2517        case 61 :
2518        case 31 :
2519        case 29 :
2520      t1 = Aig_And(bm, Aig_Not(ll), Aig_Not(rr));
2521      t2 = Aig_Or(bm, Aig_Not(lr), t1);
2522      return(t2);
2523        case 39 :
2524        case 37 :
2525        case 7 :
2526        case 5 :
2527        case 51 :
2528        case 49 :
2529        case 19 :
2530        case 17 :
2531      return(l);
2532        case 46 :
2533        case 44 :
2534        case 14 :
2535        case 12 :
2536        case 58 :
2537        case 56 :
2538        case 26 :
2539        case 24 :
2540      return(r);
2541        case 38 :
2542        case 36 :
2543        case 6 :
2544        case 4 :
2545        case 50 :
2546        case 48 :
2547        case 18 :
2548        case 16 :
2549      return(Aig_Zero);
2550        case 45 :
2551        case 15 :
2552        case 13 :
2553        case 59 :
2554        case 57 :
2555        case 47 :
2556        case 27 :
2557        case 25 :
2558      t1 = Aig_And2(bm, l, r);
2559      return(t1);
2560    }
2561  }
2562  else if(caseIndex == 3) {
2563    switch(caseSig) {
2564        case 37 :
2565        case 33 :
2566        case 5 :
2567        case 1 :
2568        case 55 :
2569        case 51 :
2570        case 23 :
2571        case 19 :
2572      t1 = Aig_And(bm, Aig_Not(rl), lr);
2573      t2 = Aig_And(bm, ll, t1);
2574      return(t2);
2575        case 36 :
2576        case 32 :
2577        case 4 :
2578        case 0 :
2579        case 54 :
2580        case 50 :
2581        case 22 :
2582        case 18 :
2583      t1 = Aig_And(bm, rl, lr);
2584      t2 = Aig_And(bm, ll, t1);
2585      return(t2);
2586        case 44 :
2587        case 40 :
2588        case 12 :
2589        case 8 :
2590        case 62 :
2591        case 58 :
2592        case 30 :
2593        case 26 :
2594      t1 = Aig_And(bm, rl, lr);
2595      t2 = Aig_And(bm, Aig_Not(ll), t1);
2596      return(t2);
2597        case 45 :
2598        case 41 :
2599        case 13 :
2600        case 9 :
2601        case 63 :
2602        case 59 :
2603        case 31 :
2604        case 27 :
2605      t1 = Aig_And(bm, Aig_Not(ll), Aig_Not(rl));
2606      t2 = Aig_Or(bm, Aig_Not(lr), t1);
2607      return(t2);
2608        case 39 :
2609        case 35 :
2610        case 7 :
2611        case 3 :
2612        case 53 :
2613        case 49 :
2614        case 21 :
2615        case 17 :
2616      return(l);
2617        case 46 :
2618        case 42 :
2619        case 14 :
2620        case 10 :
2621        case 60 :
2622        case 56 :
2623        case 28 :
2624        case 24 :
2625      return(r);
2626        case 38 :
2627        case 34 :
2628        case 6 :
2629        case 2 :
2630        case 52 :
2631        case 48 :
2632        case 20 :
2633        case 16 :
2634      return(Aig_Zero);
2635        case 47 :
2636        case 43 :
2637        case 15 :
2638        case 11 :
2639        case 61 :
2640        case 57 :
2641        case 29 :
2642        case 25 :
2643      t1 = Aig_And2(bm, l, r);
2644      return(t1);
2645    }
2646  }
2647  else if(caseIndex == 4) {
2648    switch(caseSig) {
2649        case 22 :
2650        case 20 :
2651        case 6 :
2652        case 4 :
2653        case 50 :
2654        case 48 :
2655        case 34 :
2656        case 32 :
2657        case 2 :
2658        case 16 :
2659        case 52 :
2660        case 1 :
2661        case 8 :
2662        case 19 :
2663        case 26 :
2664        case 37 :
2665        case 44 :
2666        case 38 :
2667        case 55 :
2668        case 62 :
2669      return(Aig_Zero);
2670        case 0 :
2671        case 18 :
2672        case 36 :
2673        case 54 :
2674        case 9 :
2675        case 27 :
2676        case 45 :
2677        case 63 :
2678        case 5 :
2679        case 23 :
2680        case 33 :
2681        case 51 :
2682        case 3 :
2683        case 17 :
2684        case 49 :
2685        case 7 :
2686        case 35 :
2687        case 21 :
2688        case 39 :
2689        case 53 :
2690      return(l);
2691        case 40 :
2692        case 58 :
2693        case 12 :
2694        case 30 :
2695        case 24 :
2696        case 10 :
2697        case 14 :
2698        case 56 :
2699        case 28 :
2700        case 42 :
2701        case 60 :
2702        case 46 :
2703      return(r);
2704        case 11 :
2705        case 47 :
2706        case 25 :
2707        case 61 :
2708      return(Aig_Not(ll));
2709        case 41 :
2710        case 59 :
2711        case 13 :
2712        case 31 :
2713      return(Aig_Not(lr));
2714        case 15 :
2715      t1 = Aig_And(bm, ll, Aig_Not(lr));
2716      t2 = Aig_And(bm, Aig_Not(ll), lr);
2717      return(Aig_Not(Aig_And2(bm, Aig_Not(t1), Aig_Not(t2))));
2718        case 57 :
2719      t1 = Aig_And(bm, rl, Aig_Not(rr));
2720      t2 = Aig_And(bm, Aig_Not(rl), rr);
2721      return(Aig_Not(Aig_And2(bm, Aig_Not(t1), Aig_Not(t2))));
2722        case 29 :
2723      t1 = Aig_And(bm, ll, lr);
2724      t2 = Aig_And(bm, Aig_Not(ll), Aig_Not(lr));
2725      return((Aig_And2(bm, Aig_Not(t1), Aig_Not(t2))));
2726        case 43 :
2727      t1 = Aig_And(bm, rl, rr);
2728      t2 = Aig_And(bm, Aig_Not(rl), Aig_Not(rr));
2729      return((Aig_And2(bm, Aig_Not(t1), Aig_Not(t2))));
2730    }
2731  }
2732  return(0);
2733}
2734
2735
2736/**Function********************************************************************
2737
2738  Synopsis    [Structural hasing for and3]
2739
2740  Description [Structural hasing for and3]
2741
2742  SideEffects []
2743
2744  SeeAlso     []
2745
2746******************************************************************************/
2747AigEdge_t
2748Aig_And3(
2749           Aig_Manager_t *bm,
2750           AigEdge_t l,
2751           AigEdge_t r)
2752{
2753  int caseIndex, caseSig;
2754  AigEdge_t rl, rr;
2755
2756  rl = leftChild(r);
2757  rr = rightChild(r);
2758
2759  caseIndex = 0; /* (a)(b c) */
2760  if(AigCompareNode(l, rl)) {
2761    caseIndex = 1; /* (a)(a b) */
2762  }
2763  else if(AigCompareNode(l, rr)) {
2764    caseIndex = 2; /* (a)(b a) */
2765  }
2766
2767  caseSig = 0;
2768  if(Aig_IsInverted(l))  caseSig += 8;
2769  if(Aig_IsInverted(rl)) caseSig += 4;
2770  if(Aig_IsInverted(rr)) caseSig += 2;
2771  if(Aig_IsInverted(r))  caseSig += 1;
2772  if(caseIndex == 0) {
2773    return(Aig_And2(bm, l, r));
2774  }
2775  else if(caseIndex == 1) {
2776    switch(caseSig) {
2777        case 2 :
2778        case 0 :
2779        case 14 :
2780        case 12 :
2781      return(r);
2782        case 10 :
2783        case 8 :
2784        case 6 :
2785        case 4 :
2786      return(Aig_Zero);
2787        case 3 :
2788        case 1 :
2789        case 15 :
2790        case 13 :
2791      return(Aig_And(bm, rl, Aig_Not(rr)));
2792        case 11 :
2793        case 9 :
2794        case 7 :
2795        case 5 :
2796      return(l);
2797    }
2798  }
2799  else if(caseIndex == 2) {
2800    switch(caseSig) {
2801        case 4 :
2802        case 0 :
2803        case 14 :
2804        case 10 :
2805      return(r);
2806        case 12 :
2807        case 8 :
2808        case 6 :
2809        case 2 :
2810      return(Aig_Zero);
2811        case 5 :
2812        case 1 :
2813        case 15 :
2814        case 11 :
2815      return(Aig_And(bm, Aig_Not(rl), rr));
2816        case 13 :
2817        case 9 :
2818        case 7 :
2819        case 3 :
2820      return(l);
2821    }
2822  }
2823  return(0);
2824}
2825
2826/**Function********************************************************************
2827
2828  Synopsis    [Set mask for transitive fanin nodes]
2829
2830  Description [Set mask for transitive fanin nodes]
2831
2832  SideEffects []
2833
2834  SeeAlso     []
2835
2836******************************************************************************/
2837void
2838Aig_SetMaskTransitiveFanin(
2839        Aig_Manager_t *bm,
2840        int v,
2841        unsigned int mask)
2842{
2843  if(v == 2)    return;
2844
2845
2846  if(flags(v) & mask)   return;
2847
2848  flags(v) |= mask;
2849
2850  Aig_SetMaskTransitiveFanin(bm, leftChild(v), mask);
2851  Aig_SetMaskTransitiveFanin(bm, rightChild(v), mask);
2852}
2853
2854/**Function********************************************************************
2855
2856  Synopsis    [Reset mask for transitive fanin nodes]
2857
2858  Description [Reset mask for transitive fanin nodes]
2859
2860  SideEffects []
2861
2862  SeeAlso     []
2863
2864******************************************************************************/
2865void
2866Aig_ResetMaskTransitiveFanin(
2867        Aig_Manager_t *bm,
2868        int v,
2869        unsigned int mask,
2870        unsigned int resetMask)
2871{
2872  if(v == 2)    return;
2873
2874
2875  if(!(flags(v) & mask))        return;
2876
2877  flags(v) &= resetMask;
2878  Aig_ResetMaskTransitiveFanin(bm, leftChild(v), mask, resetMask);
2879  Aig_ResetMaskTransitiveFanin(bm, rightChild(v), mask, resetMask);
2880}
2881
2882
2883/**Function********************************************************************
2884
2885   Synopsis [Get value of aig node.]
2886
2887   Description [The default falue is 2, which is same as UNKNOWN. This calue can be assigned from SAT solver.]
2888
2889   SideEffects []
2890   
2891   SeeAlso     []
2892   
2893******************************************************************************/
2894
2895int
2896Aig_GetValueOfNode(Aig_Manager_t *bm, AigEdge_t v)
2897{
2898  unsigned int value, lvalue, rvalue;
2899  AigEdge_t left, right;
2900
2901
2902  /*
2903  if(!(flags(v) & CoiMask))     return(2);
2904  **/
2905  if(v == 2)    return(2);
2906
2907  value = aig_value(v);
2908  if(value == 3)        return(2);
2909  if(value == 2) {
2910    left = Aig_GetCanonical(bm, leftChild(v));
2911    lvalue = Aig_GetValueOfNode(bm, left);
2912    if(lvalue == 0)     {
2913      value = 0;
2914    }
2915    else {
2916      right = Aig_GetCanonical(bm, rightChild(v));
2917      rvalue = Aig_GetValueOfNode(bm, right);
2918      if(rvalue == 0) {
2919        value = 0;
2920      }
2921      else if(rvalue == 1 && lvalue == 1) {
2922        value = 1;
2923      }
2924      else {
2925        value = 2;
2926      }
2927    }
2928  }
2929
2930  if(value == 2) {
2931    aig_value(v) = 3;
2932    return(value);
2933  }
2934  else  {       
2935    aig_value(v) = value;
2936    return(value ^ Aig_IsInverted(v));
2937  }
2938}
2939
Note: See TracBrowser for help on using the repository browser.