source: vis_dev/glu-2.3/src/calBdd/cal.c @ 67

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

library glu 2.3
File size: 31.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cal.c]
4
5  PackageName [cal]
6
7  Synopsis    [Miscellaneous collection of exported BDD functions]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [
14               Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and
15               Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu
16              ]
17
18  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
19  All rights reserved.
20
21  Permission is hereby granted, without written agreement and without license
22  or royalty fees, to use, copy, modify, and distribute this software and its
23  documentation for any purpose, provided that the above copyright notice and
24  the following two paragraphs appear in all copies of this software.
25
26  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
27  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
28  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
29  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30
31  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
32  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
33  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
34  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
35  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
36
37  Revision    [$Id: cal.c,v 1.2 2009/04/11 23:43:52 fabio Exp $]
38
39******************************************************************************/
40
41#include "calInt.h"
42
43
44/*---------------------------------------------------------------------------*/
45/* Constant declarations                                                     */
46/*---------------------------------------------------------------------------*/
47
48
49/*---------------------------------------------------------------------------*/
50/* Type declarations                                                         */
51/*---------------------------------------------------------------------------*/
52
53
54/*---------------------------------------------------------------------------*/
55/* Stucture declarations                                                     */
56/*---------------------------------------------------------------------------*/
57
58
59/*---------------------------------------------------------------------------*/
60/* Variable declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Macro declarations                                                        */
66/*---------------------------------------------------------------------------*/
67
68
69/**AutomaticStart*************************************************************/
70
71/*---------------------------------------------------------------------------*/
72/* Static function prototypes                                                */
73/*---------------------------------------------------------------------------*/
74
75static Cal_Bdd_t BddIntersectsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g);
76
77/**AutomaticEnd***************************************************************/
78
79
80/*---------------------------------------------------------------------------*/
81/* Definition of exported functions                                          */
82/*---------------------------------------------------------------------------*/
83/**Function********************************************************************
84
85  Synopsis    [Returns 1 if argument BDDs are equal, 0 otherwise.]
86
87  Description [Returns 1 if argument BDDs are equal, 0 otherwise.]
88
89  SideEffects [None.]
90
91  SeeAlso     []
92
93******************************************************************************/
94int
95Cal_BddIsEqual(Cal_BddManager bddManager, Cal_Bdd userBdd1, Cal_Bdd userBdd2)
96{
97  return (userBdd1 == userBdd2);
98}
99
100/**Function********************************************************************
101
102  Synopsis    [Returns 1 if the argument BDD is constant one, 0 otherwise.]
103
104  Description [Returns 1 if the argument BDD is constant one, 0 otherwise.]
105
106  SideEffects [None.]
107
108  SeeAlso     [Cal_BddIsBddZero]
109
110******************************************************************************/
111int
112Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd)
113{
114  return (userBdd == bddManager->userOneBdd);
115}
116
117/**Function********************************************************************
118
119  Synopsis    [Returns 1 if the argument BDD is constant zero, 0 otherwise.]
120
121  Description [Returns 1 if the argument BDD is constant zero, 0 otherwise.]
122
123  SideEffects [None.]
124
125  SeeAlso     [Cal_BddIsBddOne]
126
127******************************************************************************/
128int
129Cal_BddIsBddZero(
130  Cal_BddManager bddManager,
131  Cal_Bdd userBdd)
132{
133  return (userBdd == bddManager->userZeroBdd);
134}
135 
136/**Function********************************************************************
137
138  Synopsis    [Returns 1 if the argument BDD is NULL, 0 otherwise.]
139
140  Description [Returns 1 if the argument BDD is NULL, 0 otherwise.]
141
142  SideEffects [None.]
143
144******************************************************************************/
145int
146Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd)
147{
148  return (userBdd == 0);
149}
150
151
152/**Function********************************************************************
153
154  Synopsis    [Returns 1 if the argument BDD is a constant, 0 otherwise.]
155
156  Description [Returns 1 if the argument BDD is either constant one or
157  constant zero, otherwise returns 0.]
158
159  SideEffects [None.]
160
161  SeeAlso     [Cal_BddIsBddOne, Cal_BddIsBddZero]
162
163******************************************************************************/
164int
165Cal_BddIsBddConst(
166  Cal_BddManager bddManager,
167  Cal_Bdd userBdd)
168{
169  return ((userBdd == bddManager->userOneBdd) ||
170          (userBdd == bddManager->userZeroBdd));
171}
172
173/**Function********************************************************************
174
175  Synopsis    [Returns the duplicate BDD of the argument BDD.]
176
177  Description [Returns the duplicate BDD of the argument BDD.]
178
179  SideEffects [The reference count of the BDD is increased by 1.]
180
181  SeeAlso     [Cal_BddNot]
182
183******************************************************************************/
184Cal_Bdd
185Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd)
186{
187  /* Interface BDD reference count */
188  CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
189  CalBddNodeIcrRefCount(bddNode);
190  return userBdd;
191}
192
193/**Function********************************************************************
194
195  Synopsis    [Returns the BDD for the constant one]
196
197  Description [Returns the BDD for the constant one]
198
199  SideEffects [None]
200
201  SeeAlso     [Cal_BddZero]
202
203******************************************************************************/
204Cal_Bdd
205Cal_BddOne(Cal_BddManager bddManager)
206{
207  return bddManager->userOneBdd;
208}
209
210/**Function********************************************************************
211
212  Synopsis    [Returns the BDD for the constant zero]
213
214  Description [Returns the BDD for the constant zero]
215
216  SideEffects [None]
217
218  SeeAlso     [Cal_BddOne]
219
220******************************************************************************/
221Cal_Bdd
222Cal_BddZero(Cal_BddManager bddManager)
223{
224  return bddManager->userZeroBdd;
225}
226
227
228/**Function********************************************************************
229
230  Synopsis    [Returns the complement of the argument BDD.]
231
232  Description [Returns the complement of the argument BDD.]
233
234  SideEffects [The reference count of the argument BDD is increased by 1.]
235
236  SeeAlso     [Cal_BddIdentity]
237
238******************************************************************************/
239Cal_Bdd
240Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd)
241{
242  /* Interface BDD reference count */
243  CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
244  CalBddNodeIcrRefCount(bddNode);
245  return CalBddNodeNot(userBdd);
246}
247
248/**Function********************************************************************
249
250  Synopsis    [Returns the index of the top variable of the argument BDD.]
251
252  Description [Returns the index of the top variable of the argument BDD.]
253
254  SideEffects [None]
255
256  SeeAlso     [Cal_BddGetIfId]
257
258******************************************************************************/
259Cal_BddId_t
260Cal_BddGetIfIndex(Cal_BddManager bddManager, Cal_Bdd userBdd)
261{
262  Cal_Bdd_t F;
263  if (CalBddPreProcessing(bddManager, 1, userBdd) == 1){
264    F = CalBddGetInternalBdd(bddManager, userBdd);
265    if (CalBddIsBddConst(F)){
266      return -1;
267    }
268    return CalBddGetBddIndex(bddManager, F);
269  }
270  return -1;
271}
272
273
274/**Function********************************************************************
275
276  Synopsis    [Returns the id of the top variable of the argument BDD.]
277
278  Description [Returns the id of the top variable of the argument BDD.]
279
280  SideEffects [None]
281
282  SeeAlso     [Cal_BddGetIfIndex]
283
284******************************************************************************/
285Cal_BddId_t
286Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd)
287{
288  Cal_Bdd_t F;
289  if (CalBddPreProcessing(bddManager, 1, userBdd) == 1){
290    F = CalBddGetInternalBdd(bddManager, userBdd);
291    if (CalBddIsBddConst(F)){
292      return 0;
293    }
294    return CalBddGetBddId(F);
295  }
296  return -1;
297}
298
299/**Function********************************************************************
300
301  Synopsis    [Returns the BDD corresponding to the top variable of
302  the argument BDD.]
303
304  Description [Returns the BDD corresponding to the top variable of
305  the argument BDD.]
306
307  SideEffects [None.]
308
309******************************************************************************/
310Cal_Bdd
311Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd)
312{
313  Cal_Bdd_t F;
314  if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
315    return (Cal_Bdd)0;
316  }
317  F = CalBddGetInternalBdd(bddManager, userBdd);
318  if (CalBddIsBddConst(F)){
319    CalBddWarningMessage("Cal_BddIf: argument is constant");
320  }
321  return CalBddGetExternalBdd(bddManager, bddManager->varBdds[CalBddGetBddId(F)]);
322}
323
324
325/**Function********************************************************************
326
327  Synopsis    [Returns the positive cofactor of the argument BDD with
328  respect to the top variable of the BDD.]
329
330  Description [Returns the positive cofactor of the argument BDD with
331  respect to the top variable of the BDD.]
332
333  SideEffects [The reference count of the returned BDD is increased by 1.]
334
335  SeeAlso     [Cal_BddElse]
336
337******************************************************************************/
338Cal_Bdd
339Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd)
340{
341  Cal_Bdd_t thenBdd;
342  Cal_Bdd_t F;
343  if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
344    return (Cal_Bdd)0;
345  }
346  F = CalBddGetInternalBdd(bddManager, userBdd);
347  CalBddGetThenBdd(F, thenBdd);
348  return CalBddGetExternalBdd(bddManager, thenBdd);
349}
350
351/**Function********************************************************************
352
353  Synopsis    [Returns the negative cofactor of the argument BDD with
354  respect to the top variable of the BDD.]
355
356  Description [Returns the negative cofactor of the argument BDD with
357  respect to the top variable of the BDD.]
358
359  SideEffects [The reference count of the returned BDD is increased by 1.]
360
361  SeeAlso     [Cal_BddThen]
362
363******************************************************************************/
364Cal_Bdd
365Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd)
366{
367  Cal_Bdd_t elseBdd;
368  Cal_Bdd_t F;
369  if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
370    return (Cal_Bdd) 0;
371  }
372  F = CalBddGetInternalBdd(bddManager, userBdd);
373  CalBddGetElseBdd(F, elseBdd);
374  return CalBddGetExternalBdd(bddManager, elseBdd);
375}
376
377/**Function********************************************************************
378
379  Synopsis    [Frees the argument BDD.]
380
381  Description [Frees the argument BDD. It is an error to free a BDD
382  more than once.]
383
384  SideEffects [The reference count of the argument BDD is decreased by 1.]
385
386  SeeAlso     [Cal_BddUnFree]
387
388******************************************************************************/
389void
390Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
391{
392  /* Interface BDD reference count */
393  CalBddNodeDcrRefCount(CAL_BDD_POINTER(userBdd));
394}
395
396
397/**Function********************************************************************
398
399  Synopsis    [Unfrees the argument BDD.]
400
401  Description [Unfrees the argument BDD. It is an error to pass a BDD
402  with reference count of zero to be unfreed.]
403
404  SideEffects [The reference count of the argument BDD is increased by 1.]
405
406  SeeAlso     [Cal_BddFree]
407
408******************************************************************************/
409void
410Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
411{
412  /* Interface BDD reference count */
413  CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
414  CalBddNodeIcrRefCount(bddNode);
415}
416
417
418/**Function********************************************************************
419
420  Synopsis    [Returns a BDD with positive from a given BDD with arbitrary phase]
421
422  Description [Returns a BDD with positive from a given BDD with arbitrary phase]
423
424  SideEffects [None.]
425
426******************************************************************************/
427Cal_Bdd
428Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd)
429{
430  return CAL_BDD_POINTER(userBdd);
431}
432
433/**Function********************************************************************
434
435  Synopsis    [Computes a BDD that implies conjunction of f and g.]
436
437  Description [Computes a BDD that implies conjunction of f and g.]
438
439  SideEffects [None]
440
441  SeeAlso     [Cal_BddImplies]
442
443******************************************************************************/
444Cal_Bdd
445Cal_BddIntersects(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd
446                  gUserBdd) 
447{
448  Cal_Bdd_t result;
449  Cal_Bdd_t f, g;
450  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd) == 0){
451    return (Cal_Bdd) 0;
452  }
453  f = CalBddGetInternalBdd(bddManager, fUserBdd);
454  g = CalBddGetInternalBdd(bddManager, gUserBdd);
455  result = BddIntersectsStep(bddManager,f,g);
456  return CalBddGetExternalBdd(bddManager, result);
457}
458
459/**Function********************************************************************
460
461  Synopsis    [Computes a BDD that implies conjunction of f and Cal_BddNot(g)]
462
463  Description [Computes a BDD that implies conjunction of f and Cal_BddNot(g)]
464
465  SideEffects [none]
466
467  SeeAlso     [Cal_BddIntersects]
468
469******************************************************************************/
470Cal_Bdd
471Cal_BddImplies(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
472{
473  Cal_Bdd_t result;
474  Cal_Bdd_t f, g;
475  if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
476    Cal_Bdd_t gNot;
477    f = CalBddGetInternalBdd(bddManager, fUserBdd);
478    g = CalBddGetInternalBdd(bddManager, gUserBdd);
479    CalBddNot(g, gNot);
480    result = BddIntersectsStep(bddManager,f, gNot);
481  }
482  else{
483    return (Cal_Bdd) 0;
484  }
485  return CalBddGetExternalBdd(bddManager, result);
486}
487
488/**Function********************************************************************
489
490  Synopsis    [Returns the number of nodes in the Unique table]
491
492  Description [Returns the number of nodes in the Unique table]
493
494  SideEffects [None]
495
496  SeeAlso     [Cal_BddManagerGetNumNodes]
497
498******************************************************************************/
499unsigned long
500Cal_BddTotalSize(Cal_BddManager bddManager)
501{
502  return Cal_BddManagerGetNumNodes(bddManager);
503}
504
505
506/**Function********************************************************************
507
508  Synopsis    [Prints miscellaneous BDD statistics]
509
510  Description [Prints miscellaneous BDD statistics]
511
512  SideEffects [None]
513
514******************************************************************************/
515void
516Cal_BddStats(Cal_BddManager bddManager, FILE * fp)
517{
518  unsigned long cacheInsertions = 0;
519  unsigned long cacheEntries = 0;
520  unsigned long cacheSize = 0;
521  unsigned long cacheHits = 0;
522  unsigned long cacheLookups = 0;
523  unsigned long cacheCollisions = 0;
524  unsigned long numLockedNodes = 0;
525  int i, id, depth;
526  long numPages;
527  unsigned long totalBytes;
528 
529 
530  fprintf(fp, "**** CAL modifiable parameters ****\n");
531  fprintf(fp, "Node limit: %lu\n", bddManager->nodeLimit);
532  fprintf(fp, "Garbage collection enabled: %s\n",
533          ((bddManager->gcMode) ? "yes" : "no"));
534  fprintf(fp, "Maximum number of variables sifted per reordering: %ld\n", 
535          bddManager->maxNumVarsSiftedPerReordering);
536  fprintf(fp, "Maximum number of variable swaps per reordering: %ld\n",
537          bddManager->maxNumSwapsPerReordering);
538  fprintf(fp, "Maximum growth while sifting a variable: %2.2f\n",
539          bddManager->maxSiftingGrowth);
540  fprintf(fp, "Dynamic reordering of BDDs enabled: %s\n", 
541          ((bddManager->dynamicReorderingEnableFlag) ? "yes" : "no"));
542  fprintf(fp, "Repacking after GC Threshold: %f\n", 
543          bddManager->repackAfterGCThreshold);
544  fprintf(fp, "**** CAL statistics ****\n");
545  fprintf(fp, "Total BDD Node Usage : %lu nodes, %lu Bytes\n",
546          bddManager->numNodes, bddManager->numNodes*sizeof(CalBddNode_t));
547  fprintf(fp, "Peak BDD Node Usage : %lu nodes, %lu Bytes\n",
548          bddManager->numPeakNodes,
549          bddManager->numPeakNodes*sizeof(CalBddNode_t)); 
550  for (i=1; i<=bddManager->numVars; i++){
551    numLockedNodes += CalBddUniqueTableNumLockedNodes(bddManager,
552                                                      bddManager->uniqueTable[i]);
553  }
554  fprintf(fp, "Number of nodes locked: %lu\n", numLockedNodes);
555  fprintf(fp, "Total Number of variables: %d\n", bddManager->numVars);
556  numPages =
557      bddManager->pageManager1->totalNumPages+
558      bddManager->pageManager2->totalNumPages;
559  fprintf(fp, "Total memory allocated for BDD nodes: %ld pages (%ld Bytes)\n",
560          numPages, PAGE_SIZE*numPages);
561  /* Calculate the memory consumed */
562  totalBytes =
563      /* Over all bdd manager */
564      sizeof(Cal_BddManager_t)+
565      bddManager->maxNumVars*(sizeof(Cal_Bdd_t)+sizeof(CalNodeManager_t *)+
566                              sizeof(CalHashTable_t *) +
567                              sizeof(CalHashTable_t *) + sizeof(CalRequestNode_t*)*2)+
568      sizeof(CalPageManager_t)*2+
569      /* Page manager */
570      bddManager->pageManager1->maxNumSegments*(sizeof(CalAddress_t *)+sizeof(int))+
571      bddManager->pageManager2->maxNumSegments*
572      (sizeof(CalAddress_t *)+sizeof(int)); 
573
574  for (id=0; id <= bddManager->numVars; id++){
575    totalBytes += bddManager->nodeManagerArray[id]->maxNumPages*sizeof(int);;
576  }
577  /* IndexToId and IdToIndex */
578  totalBytes += 2*bddManager->maxNumVars*(sizeof(Cal_BddIndex_t));
579  for (id=0; id <= bddManager->numVars; id++){
580    totalBytes += bddManager->uniqueTable[id]->numBins*sizeof(int);;
581  }
582  /* Cache Table */
583  totalBytes += CalCacheTableMemoryConsumption(bddManager->cacheTable);
584 
585  /* Req que */
586  totalBytes += bddManager->maxDepth*sizeof(CalHashTable_t **);
587  for (depth = 0; depth < bddManager->depth; depth++){
588    for (id=0; id <= bddManager->numVars; id++){
589      if (bddManager->reqQue[depth][id]){
590        totalBytes +=
591            bddManager->reqQue[depth][id]->numBins*
592            sizeof(CalBddNode_t*);
593      }
594    }
595  }
596  /* Association */
597  totalBytes += sizeof(CalAssociation_t)*2;
598  /* Block */
599  totalBytes += CalBlockMemoryConsumption(bddManager->superBlock);
600
601  fprintf(fp, "Total memory consumed: %lu Pages (%lu Bytes)\n",
602          numPages+totalBytes/PAGE_SIZE,
603          PAGE_SIZE*numPages+totalBytes); 
604
605  CalBddManagerGetCacheTableData(bddManager, &cacheSize,
606                                 &cacheEntries, &cacheInsertions, 
607                                 &cacheLookups, &cacheHits, &cacheCollisions);
608  fprintf(fp, "Cache Size: %lu\n", cacheSize);
609  fprintf(fp, "Cache Entries: %lu\n", cacheEntries);
610  fprintf(fp, "Cache Insertions: %lu\n", cacheInsertions);
611  fprintf(fp, "Cache Collisions: %lu\n", cacheCollisions);
612  fprintf(fp, "Cache Hits: %lu\n", cacheHits);
613  if (cacheLookups){
614    fprintf(fp, "Cache Lookup: %lu\n", cacheLookups);
615    fprintf(fp, "Cache hit ratio: %-.2f\n", ((double)cacheHits)/cacheLookups);
616  }
617  fprintf(fp, "Number of nodes garbage collected: %lu\n",
618          bddManager->numNodesFreed);
619  fprintf(fp,"number of garbage collections: %d\n", bddManager->numGC);
620  fprintf(fp,"number of dynamic reorderings: %d\n",
621          bddManager->numReorderings); 
622  fprintf(fp,"number of trivial swaps: %ld\n", bddManager->numTrivialSwaps); 
623  fprintf(fp,"number of swaps in last reordering: %ld\n", bddManager->numSwaps); 
624  fprintf(fp,"garbage collection limit: %lu\n", bddManager->uniqueTableGCLimit);
625  fflush(fp);
626}
627
628/**Function********************************************************************
629
630  Synopsis    [Specify dynamic reordering technique.]
631
632  Description [Selects the method for dynamic reordering.]
633
634  SideEffects [None]
635
636  SeeAlso     [Cal_BddReorder]
637
638******************************************************************************/
639void
640Cal_BddDynamicReordering(Cal_BddManager bddManager, int technique)
641{
642  bddManager->reorderTechnique = technique;
643  bddManager->dynamicReorderingEnableFlag = 1;
644}
645
646/**Function********************************************************************
647
648  Synopsis    [Invoke the current dynamic reodering method.]
649
650  Description [Invoke the current dynamic reodering method.]
651
652  SideEffects [Index of a variable may change due to reodering]
653
654  SeeAlso     [Cal_BddDynamicReordering]
655
656******************************************************************************/
657void
658Cal_BddReorder(Cal_BddManager bddManager)
659{
660  if ((bddManager->dynamicReorderingEnableFlag == 0) ||
661      (bddManager->reorderTechnique == CAL_REORDER_NONE)){
662    return;
663  }
664  CalCacheTableTwoFlush(bddManager->cacheTable);
665  if (bddManager->reorderMethod == CAL_REORDER_METHOD_DF){
666    CalBddReorderAuxDF(bddManager);
667  }
668  else if (bddManager->reorderMethod == CAL_REORDER_METHOD_BF){ 
669    Cal_BddManagerGC(bddManager);
670    CalBddReorderAuxBF(bddManager);
671  }
672}
673
674
675/**Function********************************************************************
676
677  Synopsis    [Returns type of a BDD ( 0, 1, +var, -var, ovrflow, nonterminal)]
678
679  Description [Returns BDD_TYPE_ZERO if f is false, BDD_TYPE_ONE
680  if f is true, BDD_TYPE_POSVAR is f is an unnegated variable,
681  BDD_TYPE_NEGVAR if f is a negated variable, BDD_TYPE_OVERFLOW if f
682  is null, and BDD_TYPE_NONTERMINAL otherwise.]
683
684  SideEffects [None]
685
686******************************************************************************/
687int
688Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
689{
690  Cal_Bdd_t f;
691  if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
692    f = CalBddGetInternalBdd(bddManager, fUserBdd);
693    return (CalBddTypeAux(bddManager, f));
694  }
695  return (CAL_BDD_TYPE_OVERFLOW);
696}
697/**Function********************************************************************
698
699  Synopsis    [Returns the number of BDD variables]
700
701  Description [Returns the number of BDD variables]
702
703  SideEffects [None]
704
705******************************************************************************/
706long
707Cal_BddVars(Cal_BddManager bddManager)
708{
709  return (bddManager->numVars);
710}
711
712
713/**Function********************************************************************
714
715  Synopsis    [Sets the node limit to new_limit and returns the old limit.]
716
717  Description [Sets the node limit to new_limit and returns the old limit.]
718
719  SideEffects [Threshold for garbage collection may change]
720
721  SeeAlso     [Cal_BddManagerGC]
722
723******************************************************************************/
724long
725Cal_BddNodeLimit(
726  Cal_BddManager bddManager,
727  long  newLimit)
728{
729  long oldLimit;
730
731  oldLimit = bddManager->nodeLimit;
732  if (newLimit < 0){
733    newLimit=0;
734  }
735  bddManager->nodeLimit = newLimit;
736  if (newLimit && (bddManager->uniqueTableGCLimit > newLimit)){
737    bddManager->uniqueTableGCLimit = newLimit;
738  }
739  return (oldLimit);
740}
741
742/**Function********************************************************************
743
744  Synopsis    [Returns 1 if the node limit has been exceeded, 0 otherwise. The
745  overflow flag is cleared.]
746
747  Description [Returns 1 if the node limit has been exceeded, 0 otherwise. The
748  overflow flag is cleared.]
749
750  SideEffects [None]
751
752  SeeAlso     [Cal_BddNodeLimit]
753
754******************************************************************************/
755int
756Cal_BddOverflow(Cal_BddManager bddManager)
757{
758  int result;
759  result = bddManager->overflow;
760  bddManager->overflow = 0;
761  return (result);
762}
763
764/**Function********************************************************************
765
766  Synopsis           [Returns 1 if the argument BDD is a cube, 0 otherwise]
767
768  Description        [Returns 1 if the argument BDD is a cube, 0 otherwise]
769
770  SideEffects        [None]
771
772******************************************************************************/
773int
774Cal_BddIsCube(
775  Cal_BddManager bddManager,
776  Cal_Bdd fUserBdd)
777{
778  Cal_Bdd_t f0, f1;
779  Cal_Bdd_t f;
780  f = CalBddGetInternalBdd(bddManager, fUserBdd);
781  if (CalBddIsBddConst(f)){
782    if (CalBddIsBddZero(bddManager, f)){
783      CalBddFatalMessage("Cal_BddIsCube called with 0");
784    }
785    else return 1;
786  }
787
788  CalBddGetThenBdd(f, f1);
789  CalBddGetElseBdd(f, f0);
790  /*
791   * Exactly one branch of f must point to ZERO to be a cube.
792   */
793  if (CalBddIsBddZero(bddManager, f1)){
794        return (CalBddIsCubeStep(bddManager, f0));
795  } else if (CalBddIsBddZero(bddManager, f0)){
796        return (CalBddIsCubeStep(bddManager, f1));
797  } else { /* not a cube, because neither branch is zero */
798        return 0;
799  }
800}
801
802/**Function********************************************************************
803
804  Synopsis           [Returns the hooks field of the manager.]
805
806  Description        [Returns the hooks field of the manager.]
807
808  SideEffects        [None]
809
810  SeeAlso            []
811
812******************************************************************************/
813void *
814Cal_BddManagerGetHooks(Cal_BddManager bddManager)
815{
816  return bddManager->hooks;
817}
818
819/**Function********************************************************************
820
821  Synopsis           [Sets the hooks field of the manager.]
822
823  Description        [Sets the hooks field of the manager.]
824
825  SideEffects        [Hooks field changes. ]
826
827  SeeAlso            []
828
829******************************************************************************/
830void 
831Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks)
832{
833  bddManager->hooks = hooks;
834}
835
836
837/*---------------------------------------------------------------------------*/
838/* Definition of internal functions                                          */
839/*---------------------------------------------------------------------------*/
840/**Function********************************************************************
841
842  Synopsis    [Returns the BDD corresponding to the top variable of
843  the argument BDD.]
844
845  Description [Returns the BDD corresponding to the top variable of
846  the argument BDD.]
847
848  SideEffects [None.]
849
850******************************************************************************/
851Cal_Bdd_t
852CalBddIf(Cal_BddManager bddManager, Cal_Bdd_t F)
853{
854  if (CalBddIsBddConst(F)){
855    CalBddWarningMessage("CalBddIf: argument is constant");
856  }
857  return bddManager->varBdds[CalBddGetBddId(F)];
858}
859
860/**Function********************************************************************
861
862  Synopsis           [Returns 1 if the argument BDD is a cube, 0 otherwise]
863
864  Description        [Returns 1 if the argument BDD is a cube, 0 otherwise]
865
866  SideEffects        [None]
867
868******************************************************************************/
869int
870CalBddIsCubeStep(Cal_BddManager bddManager, Cal_Bdd_t f)
871{
872  Cal_Bdd_t f0, f1;
873  if (CalBddIsBddConst(f)){
874    if (CalBddIsBddZero(bddManager, f)){
875      CalBddFatalMessage("Cal_BddIsCube called with 0");
876    }
877    else return 1;
878  }
879
880  CalBddGetThenBdd(f, f1);
881  CalBddGetElseBdd(f, f0);
882  /*
883   * Exactly one branch of f must point to ZERO to be a cube.
884   */
885  if (CalBddIsBddZero(bddManager, f1)){
886        return (CalBddIsCubeStep(bddManager, f0));
887  } else if (CalBddIsBddZero(bddManager, f0)){
888        return (CalBddIsCubeStep(bddManager, f1));
889  } else { /* not a cube, because neither branch is zero */
890        return 0;
891  }
892}
893
894/**Function********************************************************************
895
896  Synopsis    [Returns the BDD type by recursively traversing the argument BDD]
897
898  Description [Returns the BDD type by recursively traversing the argument BDD]
899
900  SideEffects [None]
901
902******************************************************************************/
903int
904CalBddTypeAux(Cal_BddManager_t * bddManager, Cal_Bdd_t f)
905{
906  Cal_Bdd_t thenBdd, elseBdd;
907 
908  if (CalBddIsBddConst(f)){
909    if (CalBddIsBddZero(bddManager, f)) return (CAL_BDD_TYPE_ZERO);
910    if (CalBddIsBddOne(bddManager, f)) return (CAL_BDD_TYPE_ONE);
911  }
912  CalBddGetThenBdd(f, thenBdd);
913  CalBddGetElseBdd(f, elseBdd);
914  if (CalBddIsBddOne(bddManager, thenBdd) &&
915      CalBddIsBddZero(bddManager, elseBdd))
916    return CAL_BDD_TYPE_POSVAR;
917  if (CalBddIsBddZero(bddManager, thenBdd) &&
918      CalBddIsBddOne(bddManager, elseBdd))
919    return (CAL_BDD_TYPE_NEGVAR);
920  return (CAL_BDD_TYPE_NONTERMINAL);
921}
922
923/**Function********************************************************************
924
925  Synopsis    [Returns the duplicate BDD of the argument BDD.]
926
927  Description [Returns the duplicate BDD of the argument BDD.]
928
929  SideEffects [The reference count of the BDD is increased by 1.]
930
931  SeeAlso     [Cal_BddNot]
932
933******************************************************************************/
934Cal_Bdd_t
935CalBddIdentity(Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd)
936{
937  CalBddIcrRefCount(calBdd);
938  return calBdd;
939}
940
941
942/*---------------------------------------------------------------------------*/
943/* Definition of static functions                                            */
944/*---------------------------------------------------------------------------*/
945/**Function********************************************************************
946
947  Synopsis    [Recursive routine to returns a BDD that implies conjunction of
948  argument BDDs]
949
950  Description [Recursive routine to returns a BDD that implies conjunction of
951  argument BDDs]
952
953  SideEffects [None]
954
955******************************************************************************/
956static Cal_Bdd_t
957BddIntersectsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t  g)
958{
959  Cal_Bdd_t f1, f2, g1, g2, result, temp;
960  Cal_BddId_t topId;
961 
962 
963  if (CalBddIsBddConst(f)){
964    if (CalBddIsBddZero(bddManager, f)){
965      return f;
966    }
967    else {
968      return g;
969    }
970  }
971  if (CalBddIsBddConst(g)){
972    if (CalBddIsBddZero(bddManager, g)){
973      return g;
974    }
975    else {
976      return f;
977    }
978  }
979  if (CalBddSameOrNegation(f, g)){
980    if (CalBddIsEqual(f, g)){
981      return f;
982    }
983    else
984      return bddManager->bddZero;
985  }
986  if (CAL_BDD_OUT_OF_ORDER(f, g)) CAL_BDD_SWAP(f, g);
987  CalBddGetMinId2(bddManager, f, g, topId);
988  CalBddGetCofactors(f, topId, f1, f2);
989  CalBddGetCofactors(g, topId, g1, g2);
990  temp = BddIntersectsStep(bddManager, f1, g1);
991  if (CalBddIsBddZero(bddManager, temp)){
992    temp = BddIntersectsStep(bddManager, f2, g2);
993    if (CalBddIsBddZero(bddManager, temp)){
994      return bddManager->bddZero;
995    }
996    else{
997      if(CalUniqueTableForIdFindOrAdd(bddManager,
998                                      bddManager->uniqueTable[topId], 
999                                      bddManager->bddZero, temp,
1000                                      &result) == 0){
1001        CalBddIcrRefCount(temp);
1002      }
1003    }
1004  }
1005  else {
1006    if(CalUniqueTableForIdFindOrAdd(bddManager, bddManager->uniqueTable[topId],
1007                          temp, bddManager->bddZero,&result) == 0){
1008      CalBddIcrRefCount(temp);
1009    }
1010  }
1011  return result;
1012}
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
Note: See TracBrowser for help on using the repository browser.