source: vis_dev/glu-2.1/src/calBdd/calCacheTableTwo.c @ 6

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

Ajout de glus pour dev VIS mod
File size: 23.8 KB
RevLine 
[6]1/**CFile***********************************************************************
2
3  FileName    [calCacheTableTwo.c]
4
5  PackageName [cal]
6
7  Synopsis    [Functions to manage the Cache tables.]
8  Description [ ]
9
10  SeeAlso     [optional]
11
12  Author      [ Rajeev K. Ranjan   (rajeev@eecs.berkeley.edu)
13                Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
14              ]
15  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without license
19  or royalty fees, to use, copy, modify, and distribute this software and its
20  documentation for any purpose, provided that the above copyright notice and
21  the following two paragraphs appear in all copies of this software.
22
23  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
24  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
32  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34  Revision    [$Id: calCacheTableTwo.c,v 1.4 1998/09/15 19:02:52 ravi Exp $]
35
36******************************************************************************/
37
38#include "calInt.h"
39
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44/* cache table management related constants */
45#define CACHE_TABLE_DEFAULT_SIZE_INDEX 16
46#define CACHE_TABLE_DEFAULT_CACHE_RATIO 4
47
48/*---------------------------------------------------------------------------*/
49/* Type declarations                                                         */
50/*---------------------------------------------------------------------------*/
51typedef struct CacheEntryStruct CacheEntry_t;
52
53/*---------------------------------------------------------------------------*/
54/* Stucture declarations                                                     */
55/*---------------------------------------------------------------------------*/
56struct CalCacheTableStruct {
57  long numBins;
58  int sizeIndex;
59  CacheEntry_t *bins;
60  int cacheRatio;
61  long numInsertions;
62  long numEntries;
63  long numHits;
64  long numLookups;
65  long numCollisions;
66};
67
68struct CacheEntryStruct {
69  CalBddNode_t *operand1;
70  CalBddNode_t *operand2;
71  CalBddNode_t *resultBddNode;
72  Cal_BddId_t resultBddId;
73  unsigned short opCode;
74};
75
76
77/*---------------------------------------------------------------------------*/
78/* Variable declarations                                                     */
79/*---------------------------------------------------------------------------*/
80
81/*---------------------------------------------------------------------------*/
82/* Macro declarations                                                        */
83/*---------------------------------------------------------------------------*/
84#ifdef USE_POWER_OF_2
85#  define CacheTableTwoDoHash(table, operand1, operand2, opCode) \
86   (((((((CalAddress_t)(operand1)) +    ((CalAddress_t)(operand2))) / NODE_SIZE) << 2) + opCode + ((CalAddress_t)operand1 & 0x1)+ (((CalAddress_t)operand2 & 0x1)<<1)) &((table)->numBins - 1))
87#else
88#  define CacheTableTwoDoHash(table, operand1, operand2, opCode) \
89   ((((((CalAddress_t)(operand1)) +     ((CalAddress_t)(operand2))) / NODE_SIZE) + opCode + ((CalAddress_t)operand1 & 0x1)+ ((CalAddress_t)operand2 & 0x1)) %((table)->numBins))
90/*(((((CalAddress_t)(operand1)) +       ((CalAddress_t)(operand2))) + opCode) &((table)->numBins - 1))
91((opCode + (((CalAddress_t)(operand1)) << 1) + (((CalAddress_t)(operand2)) <<2)) &((table)->numBins - 1))
92((opCode + ((((CalAddress_t)(operand1)) + ((CalAddress_t)(operand2))) )+(((CalAddress_t)operand1 & 0x1) << (table->sizeIndex-1)) + (((CalAddress_t)operand2 & 0x1) << (table->sizeIndex-2))) &((table)->numBins - 1))
93((opCode + (((CalAddress_t)(operand1)) << 1) + (((CalAddress_t)(operand2)) << 2)) &((table)->numBins - 1))
94*/
95#endif
96
97#define CacheTableTwoCompareCacheEntry(entry, _operand1, _operand2, _opCode)  \
98((((CalBddNode_t *)(((CalAddress_t)((entry)->operand1)) & ~0x2)) == (_operand1))\
99 &&                                                             \
100 ((entry)->operand2 == (_operand2))\
101 &&                                                             \
102 ((entry)->opCode == _opCode))
103
104#define CacheResultNodeIsForwardedTo(resultBddNode, resultBddId) \
105{ \
106  CalBddNode_t *__resultBddNode;\
107  __resultBddNode = CAL_BDD_POINTER(resultBddNode); \
108  if(CalRequestNodeGetElseRequestNode(__resultBddNode) == FORWARD_FLAG){ \
109    resultBddId = __resultBddNode->thenBddId; \
110    resultBddNode = (CalBddNode_t*) \
111                    (((CalAddress_t)(__resultBddNode->thenBddNode) & ~0xe)        \
112                         ^(CAL_TAG0(resultBddNode))); \
113  } \
114}
115
116/**AutomaticStart*************************************************************/
117
118/*---------------------------------------------------------------------------*/
119/* Static function prototypes                                                */
120/*---------------------------------------------------------------------------*/
121
122static void CacheTableTwoRehash(CalCacheTable_t *cacheTable, int grow);
123static void CacheTablePrint(CalCacheTable_t *cacheTable);
124
125/**AutomaticEnd***************************************************************/
126
127
128/*---------------------------------------------------------------------------*/
129/* Definition of exported functions                                          */
130/*---------------------------------------------------------------------------*/
131
132
133/*---------------------------------------------------------------------------*/
134/* Definition of internal functions                                          */
135/*---------------------------------------------------------------------------*/
136/**Function********************************************************************
137
138  Synopsis    [Initialize a Cache table using default parameters.]
139
140  Description [optional]
141
142  SideEffects [required]
143
144  SeeAlso     [optional]
145
146******************************************************************************/
147CalCacheTable_t *
148CalCacheTableTwoInit(Cal_BddManager_t *bddManager)
149{
150  CalCacheTable_t  *cacheTable;
151  cacheTable = Cal_MemAlloc(CalCacheTable_t, 1);
152  if (cacheTable == Cal_Nil(CalCacheTable_t)){
153    CalBddFatalMessage("out of memory");
154  }
155  cacheTable->sizeIndex = CACHE_TABLE_DEFAULT_SIZE_INDEX;
156  cacheTable->numBins = TABLE_SIZE(cacheTable->sizeIndex);
157  cacheTable->cacheRatio = CACHE_TABLE_DEFAULT_CACHE_RATIO;
158  cacheTable->bins = Cal_MemAlloc(CacheEntry_t, cacheTable->numBins);
159  if(cacheTable->bins == Cal_Nil(CacheEntry_t)){
160    CalBddFatalMessage("out of memory");
161  }             
162  memset((char *)cacheTable->bins, 0,
163         cacheTable->numBins*sizeof(CacheEntry_t));
164  cacheTable->numInsertions = 0;
165  cacheTable->numEntries = 0;
166  cacheTable->numHits = 0;
167  cacheTable->numLookups = 0;
168  cacheTable->numCollisions = 0;
169  return cacheTable;
170}
171
172
173/**Function********************************************************************
174
175  Synopsis    [Free a Cache table along with the associated storage.]
176
177  Description [optional]
178
179  SideEffects [required]
180
181  SeeAlso     [optional]
182
183******************************************************************************/
184int
185CalCacheTableTwoQuit(CalCacheTable_t *cacheTable)
186{
187  if(cacheTable == Cal_Nil(CalCacheTable_t))return 1;
188  Cal_MemFree(cacheTable->bins);
189  Cal_MemFree(cacheTable);
190  return 0;
191}
192
193
194/**Function********************************************************************
195
196  Synopsis    [Directly insert a BDD node in the Cache table.]
197
198  Description [optional]
199
200  SideEffects [required]
201
202  SeeAlso     [optional]
203
204******************************************************************************/
205void
206CalCacheTableTwoInsert(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
207                       Cal_Bdd_t g, Cal_Bdd_t result, unsigned long
208                       opCode, int cacheLevel)
209{
210  int hashValue;
211  CalCacheTable_t *cacheTable;
212  CacheEntry_t *bin;
213  CalBddNode_t *operand1Node, *operand2Node;
214
215  cacheTable = bddManager->cacheTable;
216  cacheTable->numInsertions++;
217  hashValue = CacheTableTwoDoHash(cacheTable, CalBddGetBddNode(f),
218                                  CalBddGetBddNode(g), opCode); 
219
220  bin = cacheTable->bins + hashValue;
221  if (bin->opCode != CAL_OP_INVALID){
222    cacheTable->numCollisions++;
223  }
224  else{
225    cacheTable->numEntries++;
226  }
227 
228  bin->opCode = opCode;
229  if ((CalAddress_t)CalBddGetBddNode(f) >
230      (CalAddress_t)CalBddGetBddNode(g)){ 
231    operand1Node = CalBddGetBddNode(g);
232    operand2Node = CalBddGetBddNode(f);
233  }
234  else{
235    operand1Node = CalBddGetBddNode(f);
236    operand2Node = CalBddGetBddNode(g);
237  }
238 
239  if (cacheLevel){
240  /*
241   * Mark this result as temporary node to be forwarded at the end of
242   * operation. The reason we can use this tagging is because the
243   * size of the structure is 16 bytes and we are requiring 8 or 16 byte
244   * alignment (at least last 3 bits should be zero).
245   */
246    bin->operand1 = (CalBddNode_t *) (((CalAddress_t)operand1Node) | 0x2);
247  }
248  else {
249    bin->operand1 = operand1Node;
250  }
251  bin->operand2 = operand2Node;
252  bin->resultBddNode = CalBddGetBddNode(result);
253  bin->resultBddId = CalBddGetBddId(result);
254  return;
255}
256
257 
258/**Function********************************************************************
259
260  Synopsis    [required]
261
262  Description [optional]
263
264  SideEffects [required]
265
266  SeeAlso     [optional]
267
268******************************************************************************/
269int
270CalCacheTableTwoLookup(Cal_BddManager_t *bddManager, Cal_Bdd_t f,
271                       Cal_Bdd_t g, unsigned long opCode, Cal_Bdd_t
272                       *resultBddPtr) 
273{
274  int hashValue;
275  CalCacheTable_t *cacheTable;
276  CacheEntry_t *bin;
277  CalBddNode_t *operand1Node, *operand2Node;
278 
279  cacheTable = bddManager->cacheTable;
280  cacheTable->numLookups++;
281  hashValue = CacheTableTwoDoHash(cacheTable, CalBddGetBddNode(f),
282                                  CalBddGetBddNode(g), opCode); 
283
284  bin = cacheTable->bins+hashValue;
285 
286  if ((CalAddress_t)CalBddGetBddNode(f) > (CalAddress_t)CalBddGetBddNode(g)){
287    operand1Node = CalBddGetBddNode(g);
288    operand2Node = CalBddGetBddNode(f);
289  }
290  else{
291    operand1Node = CalBddGetBddNode(f);
292    operand2Node = CalBddGetBddNode(g);
293  }
294  if (CacheTableTwoCompareCacheEntry(bin, operand1Node, operand2Node,
295                                     opCode)){
296    CalBddPutBddId((*resultBddPtr), bin->resultBddId);
297    CalBddPutBddNode((*resultBddPtr), bin->resultBddNode);
298    cacheTable->numHits++;
299    return 1;
300  }
301  *resultBddPtr = bddManager->bddNull;
302  return 0;
303}
304
305/**Function********************************************************************
306
307  Synopsis    [Free a Cache table along with the associated storage.]
308
309  Description [optional]
310
311  SideEffects [required]
312
313  SeeAlso     [optional]
314
315******************************************************************************/
316void
317CalCacheTableTwoFlush(CalCacheTable_t *cacheTable)
318{
319  memset((char *)cacheTable->bins, 0,
320         cacheTable->numBins*sizeof(CacheEntry_t));
321  cacheTable->numEntries = 0;
322}
323
324/**Function********************************************************************
325
326  Synopsis    [Free a Cache table along with the associated storage.]
327
328  Description [optional]
329
330  SideEffects [required]
331
332  SeeAlso     [optional]
333
334******************************************************************************/
335int
336CalCacheTableTwoFlushAll(CalCacheTable_t *cacheTable)
337{
338  CalCacheTableTwoFlush(cacheTable);
339  cacheTable->numInsertions = 0;
340  cacheTable->numCollisions = 0;
341  cacheTable->numLookups = 0;
342  cacheTable->numHits = 0;
343  return 0;
344}
345/**Function********************************************************************
346
347  Synopsis           [required]
348
349  Description        [optional]
350
351  SideEffects        [required]
352
353  SeeAlso            [optional]
354
355******************************************************************************/
356void
357CalCacheTableTwoGCFlush(CalCacheTable_t *cacheTable)
358{
359  int i;
360  CacheEntry_t *bin = cacheTable->bins;
361  int numBins = cacheTable->numBins;
362  if (cacheTable->numEntries == 0) return;
363  for (i=0; i<numBins; bin++,i++){
364    if (bin->opCode != CAL_OP_INVALID){
365      if (CalBddNodeIsMarked((CAL_BDD_POINTER(bin->operand1))) ||
366          CalBddNodeIsMarked((CAL_BDD_POINTER(bin->operand2))) ||
367          CalBddNodeIsMarked((CAL_BDD_POINTER(bin->resultBddNode)))){
368        /* This entry needs to be freed */
369        cacheTable->numEntries--;
370        memset((char *)bin, 0, sizeof(CacheEntry_t));
371      }
372    }
373  }
374}
375
376/**Function********************************************************************
377
378  Synopsis           [required]
379
380  Description        [optional]
381
382  SideEffects        [required]
383
384  SeeAlso            [optional]
385
386******************************************************************************/
387void
388CalCacheTableTwoRepackUpdate(CalCacheTable_t *cacheTable)
389{
390  int i;
391  CacheEntry_t *bin = cacheTable->bins;
392  int numBins = cacheTable->numBins;
393 
394  for (i=0; i<numBins; bin++,i++){
395    if (bin->opCode != CAL_OP_INVALID){
396      if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand1))){
397        CalBddNodeForward(bin->operand1);
398      }
399      if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand2))){
400        CalBddNodeForward(bin->operand2);
401      }
402      if (CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->resultBddNode))){
403        CalBddNodeForward(bin->resultBddNode);
404      }
405    }
406  }
407}
408
409/**Function********************************************************************
410
411  Synopsis           [required]
412
413  Description        [optional]
414
415  SideEffects        [required]
416
417  SeeAlso            [optional]
418
419******************************************************************************/
420void
421CalCheckCacheTableValidity(Cal_BddManager bddManager)
422{
423  CalCacheTable_t *cacheTable = bddManager->cacheTable;
424  int i;
425  CacheEntry_t *bin = cacheTable->bins;
426  int numBins = cacheTable->numBins;
427 
428  for (i=0; i<numBins; bin++,i++){
429    if (bin->opCode != CAL_OP_INVALID){
430      Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand1))
431                 == 0);
432      Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->operand2))
433                 == 0);
434      Cal_Assert(CalBddNodeIsForwarded(CAL_BDD_POINTER(bin->resultBddNode))
435                 == 0);
436    }
437  }
438}
439
440/**Function********************************************************************
441
442  Synopsis    [required]
443
444  Description [optional]
445
446  SideEffects [required]
447
448  SeeAlso     [optional]
449
450******************************************************************************/
451void
452CalCacheTableTwoFixResultPointers(Cal_BddManager_t *bddManager)
453{
454  CalCacheTable_t *cacheTable = bddManager->cacheTable;
455  int i;
456  CacheEntry_t *bin = cacheTable->bins;
457  int numBins = cacheTable->numBins;
458 
459  for (i=0; i<numBins; bin++,i++){
460    if ((CalAddress_t)bin->operand1 & 0x2){ /* If the result node is temporary
461                                   node */
462      CacheResultNodeIsForwardedTo(bin->resultBddNode, bin->resultBddId);
463      bin->operand1 = (CalBddNode_t *)((CalAddress_t)bin->operand1 &
464                                       ~0x2); /* It is no longer temporary */
465    }
466  }
467}
468
469
470
471/**Function********************************************************************
472
473  Synopsis    [required]
474
475  Description [optional]
476
477  SideEffects [required]
478
479  SeeAlso     [optional]
480
481******************************************************************************/
482void
483CalCacheTablePrint(Cal_BddManager_t *bddManager)
484{
485  CacheTablePrint(bddManager->cacheTable);
486}
487
488/**Function********************************************************************
489
490  Synopsis    [required]
491
492  Description [optional]
493
494  SideEffects [required]
495
496  SeeAlso     [optional]
497
498******************************************************************************/
499void
500CalBddManagerGetCacheTableData(Cal_BddManager_t *bddManager,
501                               unsigned long *cacheSize,
502                               unsigned long *cacheEntries,
503                               unsigned long *cacheInsertions,
504                               unsigned long *cacheLookups,
505                               unsigned long *cacheHits,
506                               unsigned long *cacheCollisions)
507{
508  CalCacheTable_t *cacheTable = bddManager->cacheTable;
509  *cacheSize += cacheTable->numBins;
510  *cacheEntries += cacheTable->numEntries;
511  *cacheInsertions += cacheTable->numInsertions;
512  *cacheLookups += cacheTable->numLookups;
513  *cacheHits += cacheTable->numHits;
514  *cacheCollisions += cacheTable->numCollisions;
515}
516
517/**Function********************************************************************
518
519  Synopsis    [required]
520
521  Description [optional]
522
523  SideEffects [required]
524
525  SeeAlso     [optional]
526
527******************************************************************************/
528void
529CalCacheTableRehash(Cal_BddManager_t *bddManager)
530{
531  CalCacheTable_t *cacheTable = bddManager->cacheTable;
532  if((3*cacheTable->numBins < cacheTable->cacheRatio*cacheTable->numEntries) &&
533     (32*cacheTable->numBins <
534      8*(bddManager->numNodes))){
535    CacheTableTwoRehash(cacheTable, 1);
536  }
537}
538/**Function********************************************************************
539
540  Synopsis           [Flushes the entries from the cache which
541                      correspond to the given associationId.]
542
543  Description        []
544
545  SideEffects        [Cache entries are affected.]
546
547  SeeAlso            []
548
549******************************************************************************/
550void
551CalCacheTableTwoFlushAssociationId(Cal_BddManager_t *bddManager, int
552                                   associationId)
553{
554  CalCacheTable_t *cacheTable =   bddManager->cacheTable;
555  int i;
556  CacheEntry_t *bin;
557 
558  for (i=0; i < cacheTable->numBins; i++){
559    bin = cacheTable->bins+i;
560    if ((bin->opCode == (CAL_OP_QUANT+associationId)) ||
561        (bin->opCode == (CAL_OP_REL_PROD+associationId)) ||
562        (bin->opCode == (CAL_OP_VAR_SUBSTITUTE+associationId))){
563      /* This entry needs to be freed */
564      cacheTable->numEntries--;
565      memset((char *)bin, 0, sizeof(CacheEntry_t));
566    }
567  }
568}
569
570/**Function********************************************************************
571
572  Synopsis           [required]
573
574  Description        [optional]
575
576  SideEffects        [required]
577
578  SeeAlso            [optional]
579
580******************************************************************************/
581unsigned long
582CalCacheTableMemoryConsumption(CalCacheTable_t *cacheTable)
583{
584  return (unsigned long) (sizeof(cacheTable)+cacheTable->numBins*sizeof(CacheEntry_t));
585}
586
587/*---------------------------------------------------------------------------*/
588/* Definition of static functions                                            */
589/*---------------------------------------------------------------------------*/
590
591
592/**Function********************************************************************
593
594  Synopsis    [required]
595
596  Description [optional]
597
598  SideEffects [required]
599
600  SeeAlso     [optional]
601
602******************************************************************************/
603static void
604CacheTableTwoRehash(CalCacheTable_t *cacheTable,int grow)
605{
606  CacheEntry_t *oldBins = cacheTable->bins;
607  int i, hashValue;
608  int oldNumBins = cacheTable->numBins;
609  CacheEntry_t *bin, *newBin;
610 
611 
612  if(grow){
613    cacheTable->sizeIndex++;
614  }
615  else{
616    if (cacheTable->sizeIndex <= CACHE_TABLE_DEFAULT_SIZE_INDEX){/* No need to Rehash */
617      return;
618    }
619    cacheTable->sizeIndex--;
620  }
621
622  cacheTable->numBins = TABLE_SIZE(cacheTable->sizeIndex);
623  cacheTable->bins = Cal_MemAlloc(CacheEntry_t, cacheTable->numBins);
624  if(cacheTable->bins == Cal_Nil(CacheEntry_t)){
625    CalBddFatalMessage("out of memory");
626  }
627 
628  memset((char *)cacheTable->bins, 0, 
629         cacheTable->numBins*sizeof(CacheEntry_t));
630
631  for(i = 0; i < oldNumBins; i++){
632      bin  = oldBins+i;
633      if (bin->opCode == CAL_OP_INVALID) continue;
634      hashValue = CacheTableTwoDoHash(cacheTable,
635                                      bin->operand1,
636                                      bin->operand2,
637                                      bin->opCode);
638      newBin = cacheTable->bins+hashValue;
639      if (newBin->opCode != CAL_OP_INVALID){
640        cacheTable->numEntries--;
641      }
642      newBin->opCode = bin->opCode;
643      newBin->operand1 = bin->operand1;
644      newBin->operand2 = bin->operand2;
645      newBin->resultBddId = bin->resultBddId;
646      newBin->resultBddNode = bin->resultBddNode;
647  }
648  Cal_MemFree(oldBins);
649}
650
651/**Function********************************************************************
652
653  Synopsis    [required]
654
655  Description [optional]
656
657  SideEffects [required]
658
659  SeeAlso     [optional]
660
661******************************************************************************/
662static void
663CacheTablePrint(CalCacheTable_t *cacheTable)
664{
665  int i;
666  unsigned long opCode;
667  CacheEntry_t *bin;
668 
669  printf("cacheTable entries(%ld) bins(%ld)\n",
670         cacheTable->numEntries, cacheTable->numBins);
671  for(i = 0; i < cacheTable->numBins; i++){
672    bin = cacheTable->bins+i;
673    opCode = bin->opCode;
674    if (opCode != CAL_OP_INVALID){
675      fprintf(stdout,"Op = %s O1 = %lx, O2 = %lx RId = %d, RNode = %lx\n",
676              ((opCode == CAL_OP_OR) ? "OR" : ((opCode == CAL_OP_AND) ? "AND" :
677                                               ((opCode ==
678                                                            CAL_OP_QUANT) ?
679                                                           "QUANT" :
680                                                           ((opCode ==
681                                                             CAL_OP_REL_PROD)   
682                                                            ?
683                                                            "RELPROD"
684                                                            :
685                                                            "Nothing")))), 
686              (CalAddress_t)bin->operand1,
687              (CalAddress_t)bin->operand2, bin->resultBddId, 
688              (CalAddress_t)bin->resultBddNode);
689    }
690  }
691}
692
693
694#ifdef CACHE_TABLE_TWO_TEST
695main(int argc, char **argv)
696{
697  Cal_Bdd_t f1, f2, f3, f4, f5, result;
698  Cal_BddManager_t *bddManager = Cal_BddManagerInit();
699  int i;
700  CalCacheTable_t *cacheTable;
701 
702  for (i=0; i<5; i++){
703    Cal_BddManagerCreateNewVarLast(bddManager);
704  }
705
706  CalCacheTablePrint(bddManager);
707 
708  f1 = bddManager->varBdds[1];
709  f2 = bddManager->varBdds[2];
710  f3 = bddManager->varBdds[3];
711  f4 = bddManager->varBdds[4];
712  f5 = bddManager->varBdds[5];
713 
714  CalCacheTableTwoInsert(bddManager, f1, f2, f3, CAL_OP_OR, 0);
715  CalCacheTableTwoInsert(bddManager, f3, f2, f4, CAL_OP_AND,0);
716  CalCacheTableTwoInsert(bddManager, f3, f4, f5, CAL_OP_REL_PROD,0);
717  /*CacheTableTwoRehash(bddManager->cacheTableArray[2], 1);*/
718  CalCacheTablePrint(bddManager);
719 
720  /* Look up */
721  CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_AND, &result);
722  assert(CalBddIsEqual(result, f4));
723
724  CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_OR, &result);
725  assert(CalBddIsEqual(result, bddManager->bddNull));
726 
727  CalCacheTableTwoLookup(bddManager, f3, f1, CAL_OP_OR, &result);
728  assert(CalBddIsEqual(result, bddManager->bddNull));
729
730  /* Another look up */
731  CalCacheTableTwoLookup(bddManager, f4, f3, CAL_OP_REL_PROD, &result);
732  assert(CalBddIsEqual(result, f5));
733
734  /* It will bump off the entry (f2, f2, AND, f4)*/
735  CalCacheTableTwoInsert(bddManager, f3, f2, f1, CAL_OP_AND,0);
736  /* Do lookup and see if that's what happened */
737  CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_AND, &result);
738  assert(CalBddIsEqual(result, f1));
739
740  /*
741   * Rehashing will visit (f2, f3, AND, f4) first and then (f2, f3,
742   * AND, f1)
743   * Hence the we should have (f2, f3, AND, f1) in the first slot
744   */
745  CacheTableTwoRehash(bddManager->cacheTable, 1);
746  CalCacheTableTwoLookup(bddManager, f3, f2, CAL_OP_AND, &result);
747  assert(CalBddIsEqual(result, f1));
748  Cal_BddManagerQuit(bddManager);
749 
750}
751#endif
Note: See TracBrowser for help on using the repository browser.