source: vis_dev/vis-2.3/src/grab/grabGrab.c @ 36

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

vis2.3
File size: 21.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [grabGrab.c]
4
5  PackageName [grab]
6
7  Synopsis    [The GRAB algorithm of computing a set of refinement variables.]
8
9  Description [The computation is based on all the shortest abstract
10  counter-examples.]
11 
12  Author      [Chao Wang]
13
14  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
15  All rights reserved.
16
17  Permission is hereby granted, without written agreement and without
18  license or royalty fees, to use, copy, modify, and distribute this
19  software and its documentation for any purpose, provided that the
20  above copyright notice and the following two paragraphs appear in
21  all copies of this software.]
22
23******************************************************************************/
24
25#include "grabInt.h"
26
27
28/*---------------------------------------------------------------------------*/
29/* Constant declarations                                                     */
30/*---------------------------------------------------------------------------*/
31
32/*---------------------------------------------------------------------------*/
33/* Structure declarations                                                    */
34/*---------------------------------------------------------------------------*/
35
36/*---------------------------------------------------------------------------*/
37/* Type declarations                                                         */
38/*---------------------------------------------------------------------------*/
39
40/*---------------------------------------------------------------------------*/
41/* Variable declarations                                                     */
42/*---------------------------------------------------------------------------*/
43static st_table *Sel0ScoreTable;
44static st_table *SelScoreTable;
45static st_table *Sel2ScoreTable;
46static st_table *Sel3ScoreTable;
47
48/*---------------------------------------------------------------------------*/
49/* Macro declarations                                                        */
50/*---------------------------------------------------------------------------*/
51
52/**AutomaticStart*************************************************************/
53
54/*---------------------------------------------------------------------------*/
55/* Static function prototypes                                                */
56/*---------------------------------------------------------------------------*/
57
58static array_t * GrabFsmComputeExRings(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, int cexType, int verbose);
59static int GrabCompareScores(const void *ptr1, const void *ptr2);
60static void GrabMddAppendSupports(mdd_manager *mddManager, mdd_t *mdd1, st_table *supportsTable);
61static array_t * ComputeDependence(Ntk_Network_t *network, st_table *vertexTable, array_t *leftVars);
62
63/**AutomaticEnd***************************************************************/
64
65/*---------------------------------------------------------------------------*/
66/* Definition of internal functions                                          */
67/*---------------------------------------------------------------------------*/
68
69/**Function********************************************************************
70
71  Synopsis    [Pick a set of refinement variables using Grab.]
72
73  Description [Pick a set of refinement variables using Grab. When
74  refine_direction is 1, refine in both directions (by adding latches
75  and bnvs); when refine_direction is 0, refine only in the boolean
76  direction (by adding bnvs).
77
78  The present state variables of absFsm must include all the invisible
79  variables; its next state variables must include only the visible
80  ones. On such a FSM, the preimage may contain some invisible
81  variables in its support. The set of preimages, ExRings, is the set
82  of augmented preimages (with invisible variables in the support).
83
84  The refinement variable will be put into either addedVars or
85  addedBnvs, depending on which class it bolongs to; at the same time,
86  it will be put into either absVarTable or
87  BnvTable.
88
89  nodeToFaninNumber is a global variable, whose values are used as
90  tie-breakers.]
91
92  SideEffects []
93
94******************************************************************************/
95void
96GrabRefineAbstractionByGrab(
97  Fsm_Fsm_t *absFsm,
98  array_t   *SORs,
99  st_table  *absVarTable,
100  st_table  *BnvTable,
101  array_t   *addedVars,
102  array_t   *addedBnvs,
103  int       refine_direction,   
104  st_table  *nodeToFaninNumberTable, 
105  int verbose)
106{
107  Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm);
108  mdd_manager   *mddManager = Ntk_NetworkReadMddManager(network);
109  array_t       *ExRings;
110  array_t       *visibleVarMddIds, *invisibleVarMddIds, *allPSVars;
111  array_t       *tempArray;
112  mdd_t         *mdd1, *mdd2;
113  char          *nodeName;
114  Ntk_Node_t    *node;
115  double        *Scores, *SelScores, *Sel0Scores, *Sel2Scores, *Sel3Scores;
116  double        epd, baseNum;
117  int           i, j, nRow, nCol;
118  long          mddId, value, value0;
119  boolean       isSupport, isLatch;
120  int           max_num_of_added_vars;
121
122  /* compute the preimages (with invisible vars in their support)
123   */
124  ExRings = GrabFsmComputeExRings(absFsm, absVarTable, BnvTable, SORs,
125                                  GRAB_CEX_SOR, verbose);
126  assert(ExRings != NIL(array_t));
127
128  visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm,absVarTable);
129  invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm,absVarTable,BnvTable);
130  allPSVars = array_dup(visibleVarMddIds);
131  array_append(allPSVars, invisibleVarMddIds);
132  assert(array_n(invisibleVarMddIds) > 0 );
133 
134  /* Compute the normalized number of "winning positions" for each individual
135   * invisibleVar, and store them in 'Scores'!
136   */
137  nRow = array_n(ExRings);
138  nCol = array_n(invisibleVarMddIds);
139  Scores = ALLOC(double, nRow*nCol);
140  memset(Scores, 0, sizeof(double)*nRow*nCol);
141
142
143  /*********************************************************
144   * for each set of abstract states in (mdd1, Ring[j+1] )
145   *********************************************************/
146  arrayForEachItem(mdd_t *, ExRings, j, mdd1) {
147    st_table *localSupportsTable = st_init_table(st_numcmp, st_numhash);
148    GrabMddAppendSupports(mddManager, mdd1, localSupportsTable);
149
150    if (mdd_get_number_of_bdd_vars(mddManager, allPSVars) <= 1023 )
151      baseNum = mdd_count_onset(mddManager, mdd1, allPSVars);
152    else {
153      mdd_t *stateMdd = mdd_smooth(mddManager, mdd1, invisibleVarMddIds);
154      baseNum = mdd_count_onset(mddManager, stateMdd, visibleVarMddIds);
155      mdd_free(stateMdd);
156    }
157   
158    /***********************************************************
159     * compute the impact of refining with each invisible var
160     ***********************************************************/
161    arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
162      /* for debugging purpose. won't affect the algorithm */
163      Scores[j*nCol+i] = -9E-99;
164
165      /* give credit simply for the appearance */
166      isSupport = st_is_member(localSupportsTable, (char *)mddId);
167      if (!isSupport || baseNum==0.0)   continue;
168      Scores[j*nCol+i] += 0.001;
169
170      node = Ntk_NetworkFindNodeByMddId(network, mddId);
171      isLatch = (Ntk_NodeTestIsLatch(node));
172      if (refine_direction==0 && isLatch)  continue;
173
174      {
175        array_t *universalQVars = array_alloc(int, 0);
176        /* MX */
177        array_insert_last(int, universalQVars, mddId);
178        mdd2 = mdd_consensus(mddManager, mdd1, universalQVars);
179        array_free(universalQVars);
180
181        if (mdd_get_number_of_bdd_vars(mddManager, allPSVars) <= 1023)
182          epd = mdd_count_onset(mddManager, mdd2, allPSVars);
183        else {
184          mdd_t *stateMdd = mdd_smooth(mddManager, mdd2, invisibleVarMddIds);
185          epd = mdd_count_onset(mddManager, stateMdd, visibleVarMddIds);
186          mdd_free(stateMdd);
187        }
188        mdd_free(mdd2);
189
190        Scores[j*nCol+i] = (baseNum - epd)/baseNum;
191      }
192     
193      if (j == 0)
194        Scores[j*nCol+i] /= 10.0;
195
196    }
197    st_free_table(localSupportsTable);
198  }
199
200  /* For each column, sum up the score over all the rows. The
201   * selection of refinement variables will be based mainly on these
202   * scores.
203   */
204  SelScores = ALLOC(double, nCol);
205  memset(SelScores, 0, sizeof(double)*nCol);
206  for (i=0; i<nRow; i++) {
207    for (j=0; j<nCol; j++) { 
208      SelScores[j] += Scores[i*nCol+j]; 
209    }
210  }
211
212  /* Other selection criteria:
213   * (0) when in the BOOLEAN refinement direction, only add bnvs
214   * (2) how many absLatches depending on the invisible var?
215   * (3) how much will the invisible var cost?
216   */ 
217  Sel0Scores  = ALLOC(double, nCol);
218  Sel2Scores  = ALLOC(double, nCol);
219  Sel3Scores  = ALLOC(double, nCol);
220  tempArray = ComputeDependence(network, absVarTable, invisibleVarMddIds);
221  value0 = lsLength(Ntk_NetworkReadNodes(network));
222  for (j=0; j<nCol; j++) {
223    mddId = array_fetch(int, invisibleVarMddIds, j);
224    node = Ntk_NetworkFindNodeByMddId(network, mddId);
225    isLatch = (Ntk_NodeTestIsLatch(node));
226    /* when refinement is in the BOOLEAN direction, only add bnvs
227     * otherwise, add either latches or bnvs
228     */
229    if (refine_direction==0 && !isLatch)
230      Sel0Scores[j] = 1.0;
231    else
232      Sel0Scores[j] = 0.0;     
233    /* dependence */
234    value = array_fetch(int, tempArray, j);
235    Sel2Scores[j] = ((double)value)/st_count(absVarTable);
236    /* cost */
237    value = GrabNodeComputeFaninNumberTableItem(network, 
238                                                nodeToFaninNumberTable,
239                                                node);
240    Sel3Scores[j] = 1.0 - ((double)value)/value0; 
241  }
242  array_free(tempArray);
243
244  /* Print out the 'Scores' matrix when requested
245   */
246  if (verbose >= 5) {
247    /* the entire score table */
248    fprintf(vis_stdout, "\n Scores[%d][%d] = \n", nRow, nCol);
249    arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
250      node = Ntk_NetworkFindNodeByMddId(network, mddId);
251      fprintf(vis_stdout, "%s ", (Ntk_NodeTestIsLatch(node)?"   L ":"     "));
252    }
253    fprintf(vis_stdout, "\n"); 
254    arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
255      node = Ntk_NetworkFindNodeByMddId(network, mddId);
256      fprintf(vis_stdout, "%5d ", i);
257    }
258    fprintf(vis_stdout, "\n"); 
259    for (i=0; i<nRow; i++) {
260      for (j=0; j<nCol; j++) { 
261        fprintf(vis_stdout, "%+1.2f ", Scores[i*nCol+j]); 
262      } 
263      fprintf(vis_stdout, "\n"); 
264    }
265    /* best score in each row */
266    for (i=0; i<nRow; i++) {
267      int best_local = 0;
268      for (j=0; j<nCol; j++) { 
269        if (Scores[i*nCol+best_local] < Scores[i*nCol+j])
270          best_local = j;
271      }
272      fprintf(vis_stdout, "best_local: Scores[%d][%d] = %5g\n",
273              i, best_local, Scores[i*nCol+best_local]);
274    }
275  }
276
277  /* Sorting the invisibleVarMddIds according to the Selection Scores
278   */
279  Sel0ScoreTable = st_init_table(st_numcmp, st_numhash);
280  SelScoreTable  = st_init_table(st_numcmp, st_numhash);
281  Sel2ScoreTable = st_init_table(st_numcmp, st_numhash);
282  Sel3ScoreTable = st_init_table(st_numcmp, st_numhash);
283  arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
284    st_insert(Sel0ScoreTable, (char *)mddId, (char *)(Sel0Scores+j));
285    st_insert(SelScoreTable,  (char *)mddId, (char *)(SelScores+j));
286    st_insert(Sel2ScoreTable, (char *)mddId, (char *)(Sel2Scores+j));
287    st_insert(Sel3ScoreTable, (char *)mddId, (char *)(Sel3Scores+j));
288  } 
289
290  array_sort(invisibleVarMddIds, GrabCompareScores);
291
292  if (verbose >= 4) {
293    fprintf(vis_stdout, "       \t  Sel0    Sel     Sel2    Sel3\n");
294    arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
295      double *addr;
296      st_lookup(Sel0ScoreTable, (char *)mddId, &addr);
297      i = (int)(addr-Sel0Scores);
298      node = Ntk_NetworkFindNodeByMddId(network, mddId);
299      isLatch = (Ntk_NodeTestIsLatch(node));
300      fprintf(vis_stdout, 
301              "%s[%d]\t %+1.3f  %+1.3f  %+1.3f  %+1.3f   %s\n",
302              (isLatch? "L":" "), 
303              i,
304              Sel0Scores[i], SelScores[i], Sel2Scores[i], Sel3Scores[i],
305              Ntk_NodeReadName(node)
306              );
307      /* only output the top 20 variables */
308      if (j >= 19) break;
309    }
310  }
311
312  st_free_table(Sel0ScoreTable);
313  st_free_table(SelScoreTable);
314  st_free_table(Sel2ScoreTable);
315  st_free_table(Sel3ScoreTable);
316
317  /* Now find the best (largest score) invisible Var   */
318  {
319    int num_absBnvs = BnvTable? st_count(BnvTable):0;
320
321    if ((st_count(absVarTable) + num_absBnvs) < 10)
322      max_num_of_added_vars = 1;
323    else
324      max_num_of_added_vars = 2 + (st_count(absVarTable)+num_absBnvs)/30;
325  }
326
327  arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
328
329    if (j >= max_num_of_added_vars)    break;
330
331    node = Ntk_NetworkFindNodeByMddId(network, mddId);
332    nodeName = Ntk_NodeReadName(node);
333    if (Ntk_NodeTestIsLatch(node)) {
334      assert(!st_is_member(absVarTable, node));
335      st_insert(absVarTable, node, (char *)(long)st_count(absVarTable));
336      array_insert_last(int, addedVars, mddId);
337      CHKPRINT2( (verbose>=3), "         add Latch %s\n", nodeName );
338    }else if (!Ntk_NodeTestIsLatch(node)) {
339      assert(!st_is_member(BnvTable, node));
340      st_insert(BnvTable, node, (char *)0);
341      array_insert_last(int, addedBnvs, mddId);
342      CHKPRINT2( (verbose>=3), "         add BNV %s\n", nodeName );
343    }
344  }
345
346  /* Clean-ups */
347  array_free(invisibleVarMddIds);
348  array_free(visibleVarMddIds);
349  array_free(allPSVars);
350  mdd_array_free(ExRings);
351  FREE(Scores);
352  FREE(Sel0Scores);
353  FREE(SelScores);
354  FREE(Sel2Scores);
355  FREE(Sel3Scores);
356}
357
358/**Function********************************************************************
359
360  Synopsis [Compute the number of fanin nodes]
361
362  Description [Compute the number of fanin nodes. The result is
363  inserted in the hash table.]
364
365  SideEffects []
366
367******************************************************************************/
368int
369GrabNodeComputeFaninNumberTableItem(
370  Ntk_Network_t   *network,
371  st_table        *nodeToFaninNumberTable,
372  Ntk_Node_t      *node)
373{
374  int          count;
375  array_t      *roots, *supports;
376
377  roots = array_alloc(Ntk_Node_t *, 0);
378  if (!st_lookup_int(nodeToFaninNumberTable, node, &count)) {
379    if (Ntk_NodeTestIsLatch(node)) 
380      array_insert(Ntk_Node_t *, roots, 0, Ntk_LatchReadDataInput(node));
381    else
382      array_insert(Ntk_Node_t *, roots, 0, node);
383
384    supports = Ntk_NodeComputeTransitiveFaninNodes(network, roots, TRUE,FALSE);
385
386    count = array_n(supports);
387    array_free(supports);
388    st_insert(nodeToFaninNumberTable, node, (char *)(long)count);
389  }
390  array_free(roots);
391
392  return count;
393}
394
395/*---------------------------------------------------------------------------*/
396/* Definition of static functions                                            */
397/*---------------------------------------------------------------------------*/
398
399/**Function********************************************************************
400
401  Synopsis [Compute the extended Synchronous Onion Rings (SORs).]
402
403  Description [Compute the extended Synchronous Onion Rings (SORs) on
404  the absFSm whose present state variables includes the invisible
405  variables. The preimages, therefore, may have invisible variables in
406  their support. The result is used only inside
407  GrabRefineAbstractionByGrab.]
408
409  SideEffects []
410
411******************************************************************************/
412static array_t *
413GrabFsmComputeExRings(
414  Fsm_Fsm_t *absFsm,
415  st_table  *absVarTable,
416  st_table  *absBnvTable,
417  array_t   *oldRings,
418  int       cexType,
419  int       verbose)
420{
421  Img_ImageInfo_t *imageInfo;
422  Ntk_Network_t   *network = Fsm_FsmReadNetwork(absFsm);
423  array_t         *careStatesArray = array_alloc(mdd_t *, 0);
424  array_t         *allPsVars, *invisibleVarMddIds;
425  array_t         *onionRings, *synOnionRings;
426  mdd_t           *mdd1, *mdd2, *mdd3, *mdd4, *initStates;
427  int             i, j, mddId;
428  Ntk_Node_t      *node;
429
430  imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 1, 0);
431
432  /* Compute the initial states based on all the related latches
433   * (i.e. visible latches and invisible ones that are in the
434   * immediate support)
435   */
436  allPsVars = GrabGetVisibleVarMddIds(absFsm, absVarTable);
437  invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absVarTable, 
438                                                 absBnvTable);
439  arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
440    node = Ntk_NetworkFindNodeByMddId(network, mddId);
441    if (Ntk_NodeTestIsLatch(node))
442      array_insert_last(int, allPsVars, mddId);
443  }
444  initStates = GrabComputeInitialStates(network, allPsVars);
445  array_free(allPsVars);
446  array_free(invisibleVarMddIds);
447
448  onionRings = oldRings;
449  if (onionRings == NIL(array_t))
450    onionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
451  assert(onionRings);
452
453  synOnionRings = array_alloc(mdd_t *, array_n(onionRings));
454
455  for (j=array_n(onionRings)-2; j>=0; j--) {
456    mdd1 = array_fetch(mdd_t *, onionRings, j+1);
457    mdd2 = array_fetch(mdd_t *, onionRings, j);
458
459    array_insert(mdd_t *, careStatesArray, 0, mdd2);
460    mdd3 = Img_ImageInfoComputeEXWithDomainVars(imageInfo,
461                                                mdd1,
462                                                mdd1,
463                                                careStatesArray);
464    mdd4 = mdd_and(mdd2, mdd3, 1, 1);
465    mdd_free(mdd3);
466
467    array_insert(mdd_t *, synOnionRings, j+1, mdd4);
468
469    /* when the more accurate initial states is available, use it */
470    if (j == 0) {
471      mdd1 = mdd_and(mdd4, initStates, 1, 1);
472      if (mdd_is_tautology(mdd1, 0)) {
473        mdd_free(mdd1);
474        mdd1 = mdd_dup(mdd4);
475      }
476      array_insert(mdd_t *, synOnionRings, j, mdd1);
477    }
478  }
479 
480  /* clean-up's */
481  mdd_free(initStates);
482  array_free(careStatesArray);
483
484  return synOnionRings;
485}
486
487/**Function********************************************************************
488
489  Synopsis    [Compare the scores of the two invisible variables.]
490
491  Description [Compare the scores of the two invisible variables. It
492  is used inside GrabRefineAbstractionByGrab() for sorting the array
493  of invisible variables.
494
495  Note that the hash tables like Sel0ScoreTable are declareled as
496  static global variables -- they are visible inside this source
497  file.]
498
499  SideEffects []
500
501******************************************************************************/
502static int
503GrabCompareScores(
504  const void *ptr1,
505  const void *ptr2)
506{
507  int  item1 = *((int *)ptr1);
508  int  item2 = *((int *)ptr2);
509  double *first0, *first, *first2, *first3;
510  double *second0, *second, *second2, *second3;
511  double value0, value, value2, value3;
512
513  st_lookup(Sel0ScoreTable, (char *)(long)item1,  &first0);
514  st_lookup(SelScoreTable,  (char *)(long)item1,  &first);
515  st_lookup(Sel2ScoreTable, (char *)(long)item1,  &first2);
516  st_lookup(Sel3ScoreTable, (char *)(long)item1,  &first3);
517
518  st_lookup(Sel0ScoreTable, (char *)(long)item2,  &second0);
519  st_lookup(SelScoreTable,  (char *)(long)item2,  &second);
520  st_lookup(Sel2ScoreTable, (char *)(long)item2,  &second2);
521  st_lookup(Sel3ScoreTable, (char *)(long)item2,  &second3);
522 
523  value0 = *second0 - *first0;
524  value  = *second  - *first;
525  value2 = *second2 - *first2;
526  value3 = *second3 - *first3;
527 
528  if (value0 > 0)         return 1;
529  if (value0 < 0)         return -1;
530
531  if (value > 0)          return 1;
532  if (value < 0)          return -1;
533
534  return 0;
535
536  /* Chao: The tie-breakers are not used for this release. We achieved
537   * the best performance on the suite of testing cases at hand
538   * without the tie-breakers. But the code is retained for the
539   * purpose of future experiments.
540   */
541 
542  if (value2 > 0)         return 1;
543  if (value2 < 0)         return -1;
544
545  if (value3 > 0)         return 1;
546  if (value3 < 0)         return -1;
547
548  return 0;
549}
550 
551 
552/**Function********************************************************************
553
554  Synopsis    [Add the supporting mddIds into the table.]
555
556  Description [Add the supporting mddIds into the table.]
557
558  SideEffects []
559
560******************************************************************************/
561static void 
562GrabMddAppendSupports( 
563  mdd_manager *mddManager, 
564  mdd_t *mdd1, 
565  st_table *supportsTable) 
566{
567  int mddId, k;
568  array_t *supports = mdd_get_support(mddManager, mdd1);
569
570  arrayForEachItem(int, supports, k, mddId) {
571    if (!st_is_member(supportsTable, (char *)(long)mddId)) 
572        st_insert(supportsTable, (char *)(long)mddId, (char *)0);
573  }
574  array_free(supports);
575}
576
577
578/**Function********************************************************************
579
580  Synopsis    [Compute the degree of dependence that the abstract model
581  has on the invisible variables.]
582
583  Description [Compute the degree of dependence that the abstract model
584  has on the invisible variables.]
585
586  SideEffects []
587
588******************************************************************************/
589static array_t * 
590ComputeDependence(
591  Ntk_Network_t *network, 
592  st_table *vertexTable, 
593  array_t *leftVars)
594{
595  array_t *roots, *supports;
596  st_table *supportTable;
597  st_generator *stgen;
598  array_t *dependenceArray = array_alloc(int, array_n(leftVars));
599  int i,mddId;
600  Ntk_Node_t *node, *node1;
601  int count;
602
603  /* initialize the scores to 0   */
604  supportTable = st_init_table(st_ptrcmp, st_ptrhash);
605  arrayForEachItem(int, leftVars, i, mddId) {
606    node = Ntk_NetworkFindNodeByMddId(network, mddId);
607    assert(node);
608    st_insert(supportTable, node, (char *)0);
609  }
610
611  /* compute the supports of the absFsm  */
612  roots = array_alloc(Ntk_Node_t *, 0);
613  st_foreach_item(vertexTable, stgen,  &node,  0) {
614    node = Ntk_LatchReadDataInput(node);
615    array_insert(Ntk_Node_t *, roots, 0, node);
616
617    supports = Ntk_NodeComputeTransitiveFaninNodes(network, roots, TRUE, 
618                                                   FALSE);
619
620    arrayForEachItem(Ntk_Node_t *, supports, i, node1) {
621      if (st_lookup_int(supportTable, node1, &count)) {
622        count++;
623        st_insert(supportTable, node1, (char *)(long)count);
624      }
625    }
626    array_free(supports);
627  }
628  array_free(roots);
629
630  /* put into an array  */
631  arrayForEachItem(int, leftVars, i, mddId) {
632    node = Ntk_NetworkFindNodeByMddId(network, mddId);
633    assert(node);
634    st_lookup_int(supportTable, node, &count);
635    array_insert(int, dependenceArray, i, count);
636  }
637
638  st_free_table(supportTable);
639
640  return dependenceArray;
641}
642
643
644
Note: See TracBrowser for help on using the repository browser.