00001
00041 #include "calInt.h"
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066
00067
00068
00071
00072
00073
00074
00075 static Cal_Bdd_t BddIntersectsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g);
00076
00080
00081
00082
00094 int
00095 Cal_BddIsEqual(Cal_BddManager bddManager, Cal_Bdd userBdd1, Cal_Bdd userBdd2)
00096 {
00097 return (userBdd1 == userBdd2);
00098 }
00099
00111 int
00112 Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd)
00113 {
00114 return (userBdd == bddManager->userOneBdd);
00115 }
00116
00128 int
00129 Cal_BddIsBddZero(
00130 Cal_BddManager bddManager,
00131 Cal_Bdd userBdd)
00132 {
00133 return (userBdd == bddManager->userZeroBdd);
00134 }
00135
00145 int
00146 Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd)
00147 {
00148 return (userBdd == 0);
00149 }
00150
00151
00164 int
00165 Cal_BddIsBddConst(
00166 Cal_BddManager bddManager,
00167 Cal_Bdd userBdd)
00168 {
00169 return ((userBdd == bddManager->userOneBdd) ||
00170 (userBdd == bddManager->userZeroBdd));
00171 }
00172
00184 Cal_Bdd
00185 Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd)
00186 {
00187
00188 CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
00189 CalBddNodeIcrRefCount(bddNode);
00190 return userBdd;
00191 }
00192
00204 Cal_Bdd
00205 Cal_BddOne(Cal_BddManager bddManager)
00206 {
00207 return bddManager->userOneBdd;
00208 }
00209
00221 Cal_Bdd
00222 Cal_BddZero(Cal_BddManager bddManager)
00223 {
00224 return bddManager->userZeroBdd;
00225 }
00226
00227
00239 Cal_Bdd
00240 Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd)
00241 {
00242
00243 CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
00244 CalBddNodeIcrRefCount(bddNode);
00245 return CalBddNodeNot(userBdd);
00246 }
00247
00259 Cal_BddId_t
00260 Cal_BddGetIfIndex(Cal_BddManager bddManager, Cal_Bdd userBdd)
00261 {
00262 Cal_Bdd_t F;
00263 if (CalBddPreProcessing(bddManager, 1, userBdd) == 1){
00264 F = CalBddGetInternalBdd(bddManager, userBdd);
00265 if (CalBddIsBddConst(F)){
00266 return -1;
00267 }
00268 return CalBddGetBddIndex(bddManager, F);
00269 }
00270 return -1;
00271 }
00272
00273
00285 Cal_BddId_t
00286 Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd)
00287 {
00288 Cal_Bdd_t F;
00289 if (CalBddPreProcessing(bddManager, 1, userBdd) == 1){
00290 F = CalBddGetInternalBdd(bddManager, userBdd);
00291 if (CalBddIsBddConst(F)){
00292 return 0;
00293 }
00294 return CalBddGetBddId(F);
00295 }
00296 return -1;
00297 }
00298
00310 Cal_Bdd
00311 Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd)
00312 {
00313 Cal_Bdd_t F;
00314 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00315 return (Cal_Bdd)0;
00316 }
00317 F = CalBddGetInternalBdd(bddManager, userBdd);
00318 if (CalBddIsBddConst(F)){
00319 CalBddWarningMessage("Cal_BddIf: argument is constant");
00320 }
00321 return CalBddGetExternalBdd(bddManager, bddManager->varBdds[CalBddGetBddId(F)]);
00322 }
00323
00324
00338 Cal_Bdd
00339 Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd)
00340 {
00341 Cal_Bdd_t thenBdd;
00342 Cal_Bdd_t F;
00343 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00344 return (Cal_Bdd)0;
00345 }
00346 F = CalBddGetInternalBdd(bddManager, userBdd);
00347 CalBddGetThenBdd(F, thenBdd);
00348 return CalBddGetExternalBdd(bddManager, thenBdd);
00349 }
00350
00364 Cal_Bdd
00365 Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd)
00366 {
00367 Cal_Bdd_t elseBdd;
00368 Cal_Bdd_t F;
00369 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00370 return (Cal_Bdd) 0;
00371 }
00372 F = CalBddGetInternalBdd(bddManager, userBdd);
00373 CalBddGetElseBdd(F, elseBdd);
00374 return CalBddGetExternalBdd(bddManager, elseBdd);
00375 }
00376
00389 void
00390 Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
00391 {
00392
00393 CalBddNodeDcrRefCount(CAL_BDD_POINTER(userBdd));
00394 }
00395
00396
00409 void
00410 Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd)
00411 {
00412
00413 CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
00414 CalBddNodeIcrRefCount(bddNode);
00415 }
00416
00417
00427 Cal_Bdd
00428 Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd)
00429 {
00430 return CAL_BDD_POINTER(userBdd);
00431 }
00432
00444 Cal_Bdd
00445 Cal_BddIntersects(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd
00446 gUserBdd)
00447 {
00448 Cal_Bdd_t result;
00449 Cal_Bdd_t f, g;
00450 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd) == 0){
00451 return (Cal_Bdd) 0;
00452 }
00453 f = CalBddGetInternalBdd(bddManager, fUserBdd);
00454 g = CalBddGetInternalBdd(bddManager, gUserBdd);
00455 result = BddIntersectsStep(bddManager,f,g);
00456 return CalBddGetExternalBdd(bddManager, result);
00457 }
00458
00470 Cal_Bdd
00471 Cal_BddImplies(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
00472 {
00473 Cal_Bdd_t result;
00474 Cal_Bdd_t f, g;
00475 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00476 Cal_Bdd_t gNot;
00477 f = CalBddGetInternalBdd(bddManager, fUserBdd);
00478 g = CalBddGetInternalBdd(bddManager, gUserBdd);
00479 CalBddNot(g, gNot);
00480 result = BddIntersectsStep(bddManager,f, gNot);
00481 }
00482 else{
00483 return (Cal_Bdd) 0;
00484 }
00485 return CalBddGetExternalBdd(bddManager, result);
00486 }
00487
00499 unsigned long
00500 Cal_BddTotalSize(Cal_BddManager bddManager)
00501 {
00502 return Cal_BddManagerGetNumNodes(bddManager);
00503 }
00504
00505
00515 void
00516 Cal_BddStats(Cal_BddManager bddManager, FILE * fp)
00517 {
00518 unsigned long cacheInsertions = 0;
00519 unsigned long cacheEntries = 0;
00520 unsigned long cacheSize = 0;
00521 unsigned long cacheHits = 0;
00522 unsigned long cacheLookups = 0;
00523 unsigned long cacheCollisions = 0;
00524 unsigned long numLockedNodes = 0;
00525 int i, id, depth;
00526 long numPages;
00527 unsigned long totalBytes;
00528
00529
00530 fprintf(fp, "**** CAL modifiable parameters ****\n");
00531 fprintf(fp, "Node limit: %lu\n", bddManager->nodeLimit);
00532 fprintf(fp, "Garbage collection enabled: %s\n",
00533 ((bddManager->gcMode) ? "yes" : "no"));
00534 fprintf(fp, "Maximum number of variables sifted per reordering: %ld\n",
00535 bddManager->maxNumVarsSiftedPerReordering);
00536 fprintf(fp, "Maximum number of variable swaps per reordering: %ld\n",
00537 bddManager->maxNumSwapsPerReordering);
00538 fprintf(fp, "Maximum growth while sifting a variable: %2.2f\n",
00539 bddManager->maxSiftingGrowth);
00540 fprintf(fp, "Dynamic reordering of BDDs enabled: %s\n",
00541 ((bddManager->dynamicReorderingEnableFlag) ? "yes" : "no"));
00542 fprintf(fp, "Repacking after GC Threshold: %f\n",
00543 bddManager->repackAfterGCThreshold);
00544 fprintf(fp, "**** CAL statistics ****\n");
00545 fprintf(fp, "Total BDD Node Usage : %lu nodes, %lu Bytes\n",
00546 bddManager->numNodes, bddManager->numNodes*sizeof(CalBddNode_t));
00547 fprintf(fp, "Peak BDD Node Usage : %lu nodes, %lu Bytes\n",
00548 bddManager->numPeakNodes,
00549 bddManager->numPeakNodes*sizeof(CalBddNode_t));
00550 for (i=1; i<=bddManager->numVars; i++){
00551 numLockedNodes += CalBddUniqueTableNumLockedNodes(bddManager,
00552 bddManager->uniqueTable[i]);
00553 }
00554 fprintf(fp, "Number of nodes locked: %lu\n", numLockedNodes);
00555 fprintf(fp, "Total Number of variables: %d\n", bddManager->numVars);
00556 numPages =
00557 bddManager->pageManager1->totalNumPages+
00558 bddManager->pageManager2->totalNumPages;
00559 fprintf(fp, "Total memory allocated for BDD nodes: %ld pages (%ld Bytes)\n",
00560 numPages, PAGE_SIZE*numPages);
00561
00562 totalBytes =
00563
00564 sizeof(Cal_BddManager_t)+
00565 bddManager->maxNumVars*(sizeof(Cal_Bdd_t)+sizeof(CalNodeManager_t *)+
00566 sizeof(CalHashTable_t *) +
00567 sizeof(CalHashTable_t *) + sizeof(CalRequestNode_t*)*2)+
00568 sizeof(CalPageManager_t)*2+
00569
00570 bddManager->pageManager1->maxNumSegments*(sizeof(CalAddress_t *)+sizeof(int))+
00571 bddManager->pageManager2->maxNumSegments*
00572 (sizeof(CalAddress_t *)+sizeof(int));
00573
00574 for (id=0; id <= bddManager->numVars; id++){
00575 totalBytes += bddManager->nodeManagerArray[id]->maxNumPages*sizeof(int);;
00576 }
00577
00578 totalBytes += 2*bddManager->maxNumVars*(sizeof(Cal_BddIndex_t));
00579 for (id=0; id <= bddManager->numVars; id++){
00580 totalBytes += bddManager->uniqueTable[id]->numBins*sizeof(int);;
00581 }
00582
00583 totalBytes += CalCacheTableMemoryConsumption(bddManager->cacheTable);
00584
00585
00586 totalBytes += bddManager->maxDepth*sizeof(CalHashTable_t **);
00587 for (depth = 0; depth < bddManager->depth; depth++){
00588 for (id=0; id <= bddManager->numVars; id++){
00589 if (bddManager->reqQue[depth][id]){
00590 totalBytes +=
00591 bddManager->reqQue[depth][id]->numBins*
00592 sizeof(CalBddNode_t*);
00593 }
00594 }
00595 }
00596
00597 totalBytes += sizeof(CalAssociation_t)*2;
00598
00599 totalBytes += CalBlockMemoryConsumption(bddManager->superBlock);
00600
00601 fprintf(fp, "Total memory consumed: %lu Pages (%lu Bytes)\n",
00602 numPages+totalBytes/PAGE_SIZE,
00603 PAGE_SIZE*numPages+totalBytes);
00604
00605 CalBddManagerGetCacheTableData(bddManager, &cacheSize,
00606 &cacheEntries, &cacheInsertions,
00607 &cacheLookups, &cacheHits, &cacheCollisions);
00608 fprintf(fp, "Cache Size: %lu\n", cacheSize);
00609 fprintf(fp, "Cache Entries: %lu\n", cacheEntries);
00610 fprintf(fp, "Cache Insertions: %lu\n", cacheInsertions);
00611 fprintf(fp, "Cache Collisions: %lu\n", cacheCollisions);
00612 fprintf(fp, "Cache Hits: %lu\n", cacheHits);
00613 if (cacheLookups){
00614 fprintf(fp, "Cache Lookup: %lu\n", cacheLookups);
00615 fprintf(fp, "Cache hit ratio: %-.2f\n", ((double)cacheHits)/cacheLookups);
00616 }
00617 fprintf(fp, "Number of nodes garbage collected: %lu\n",
00618 bddManager->numNodesFreed);
00619 fprintf(fp,"number of garbage collections: %d\n", bddManager->numGC);
00620 fprintf(fp,"number of dynamic reorderings: %d\n",
00621 bddManager->numReorderings);
00622 fprintf(fp,"number of trivial swaps: %ld\n", bddManager->numTrivialSwaps);
00623 fprintf(fp,"number of swaps in last reordering: %ld\n", bddManager->numSwaps);
00624 fprintf(fp,"garbage collection limit: %lu\n", bddManager->uniqueTableGCLimit);
00625 fflush(fp);
00626 }
00627
00639 void
00640 Cal_BddDynamicReordering(Cal_BddManager bddManager, int technique)
00641 {
00642 bddManager->reorderTechnique = technique;
00643 bddManager->dynamicReorderingEnableFlag = 1;
00644 }
00645
00657 void
00658 Cal_BddReorder(Cal_BddManager bddManager)
00659 {
00660 if ((bddManager->dynamicReorderingEnableFlag == 0) ||
00661 (bddManager->reorderTechnique == CAL_REORDER_NONE)){
00662 return;
00663 }
00664 CalCacheTableTwoFlush(bddManager->cacheTable);
00665 if (bddManager->reorderMethod == CAL_REORDER_METHOD_DF){
00666 CalBddReorderAuxDF(bddManager);
00667 }
00668 else if (bddManager->reorderMethod == CAL_REORDER_METHOD_BF){
00669 Cal_BddManagerGC(bddManager);
00670 CalBddReorderAuxBF(bddManager);
00671 }
00672 }
00673
00674
00687 int
00688 Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00689 {
00690 Cal_Bdd_t f;
00691 if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
00692 f = CalBddGetInternalBdd(bddManager, fUserBdd);
00693 return (CalBddTypeAux(bddManager, f));
00694 }
00695 return (CAL_BDD_TYPE_OVERFLOW);
00696 }
00706 long
00707 Cal_BddVars(Cal_BddManager bddManager)
00708 {
00709 return (bddManager->numVars);
00710 }
00711
00712
00724 long
00725 Cal_BddNodeLimit(
00726 Cal_BddManager bddManager,
00727 long newLimit)
00728 {
00729 long oldLimit;
00730
00731 oldLimit = bddManager->nodeLimit;
00732 if (newLimit < 0){
00733 newLimit=0;
00734 }
00735 bddManager->nodeLimit = newLimit;
00736 if (newLimit && (bddManager->uniqueTableGCLimit > newLimit)){
00737 bddManager->uniqueTableGCLimit = newLimit;
00738 }
00739 return (oldLimit);
00740 }
00741
00755 int
00756 Cal_BddOverflow(Cal_BddManager bddManager)
00757 {
00758 int result;
00759 result = bddManager->overflow;
00760 bddManager->overflow = 0;
00761 return (result);
00762 }
00763
00773 int
00774 Cal_BddIsCube(
00775 Cal_BddManager bddManager,
00776 Cal_Bdd fUserBdd)
00777 {
00778 Cal_Bdd_t f0, f1;
00779 Cal_Bdd_t f;
00780 f = CalBddGetInternalBdd(bddManager, fUserBdd);
00781 if (CalBddIsBddConst(f)){
00782 if (CalBddIsBddZero(bddManager, f)){
00783 CalBddFatalMessage("Cal_BddIsCube called with 0");
00784 }
00785 else return 1;
00786 }
00787
00788 CalBddGetThenBdd(f, f1);
00789 CalBddGetElseBdd(f, f0);
00790
00791
00792
00793 if (CalBddIsBddZero(bddManager, f1)){
00794 return (CalBddIsCubeStep(bddManager, f0));
00795 } else if (CalBddIsBddZero(bddManager, f0)){
00796 return (CalBddIsCubeStep(bddManager, f1));
00797 } else {
00798 return 0;
00799 }
00800 }
00801
00813 void *
00814 Cal_BddManagerGetHooks(Cal_BddManager bddManager)
00815 {
00816 return bddManager->hooks;
00817 }
00818
00830 void
00831 Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks)
00832 {
00833 bddManager->hooks = hooks;
00834 }
00835
00836
00837
00838
00839
00851 Cal_Bdd_t
00852 CalBddIf(Cal_BddManager bddManager, Cal_Bdd_t F)
00853 {
00854 if (CalBddIsBddConst(F)){
00855 CalBddWarningMessage("CalBddIf: argument is constant");
00856 }
00857 return bddManager->varBdds[CalBddGetBddId(F)];
00858 }
00859
00869 int
00870 CalBddIsCubeStep(Cal_BddManager bddManager, Cal_Bdd_t f)
00871 {
00872 Cal_Bdd_t f0, f1;
00873 if (CalBddIsBddConst(f)){
00874 if (CalBddIsBddZero(bddManager, f)){
00875 CalBddFatalMessage("Cal_BddIsCube called with 0");
00876 }
00877 else return 1;
00878 }
00879
00880 CalBddGetThenBdd(f, f1);
00881 CalBddGetElseBdd(f, f0);
00882
00883
00884
00885 if (CalBddIsBddZero(bddManager, f1)){
00886 return (CalBddIsCubeStep(bddManager, f0));
00887 } else if (CalBddIsBddZero(bddManager, f0)){
00888 return (CalBddIsCubeStep(bddManager, f1));
00889 } else {
00890 return 0;
00891 }
00892 }
00893
00903 int
00904 CalBddTypeAux(Cal_BddManager_t * bddManager, Cal_Bdd_t f)
00905 {
00906 Cal_Bdd_t thenBdd, elseBdd;
00907
00908 if (CalBddIsBddConst(f)){
00909 if (CalBddIsBddZero(bddManager, f)) return (CAL_BDD_TYPE_ZERO);
00910 if (CalBddIsBddOne(bddManager, f)) return (CAL_BDD_TYPE_ONE);
00911 }
00912 CalBddGetThenBdd(f, thenBdd);
00913 CalBddGetElseBdd(f, elseBdd);
00914 if (CalBddIsBddOne(bddManager, thenBdd) &&
00915 CalBddIsBddZero(bddManager, elseBdd))
00916 return CAL_BDD_TYPE_POSVAR;
00917 if (CalBddIsBddZero(bddManager, thenBdd) &&
00918 CalBddIsBddOne(bddManager, elseBdd))
00919 return (CAL_BDD_TYPE_NEGVAR);
00920 return (CAL_BDD_TYPE_NONTERMINAL);
00921 }
00922
00934 Cal_Bdd_t
00935 CalBddIdentity(Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd)
00936 {
00937 CalBddIcrRefCount(calBdd);
00938 return calBdd;
00939 }
00940
00941
00942
00943
00944
00956 static Cal_Bdd_t
00957 BddIntersectsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g)
00958 {
00959 Cal_Bdd_t f1, f2, g1, g2, result, temp;
00960 Cal_BddId_t topId;
00961
00962
00963 if (CalBddIsBddConst(f)){
00964 if (CalBddIsBddZero(bddManager, f)){
00965 return f;
00966 }
00967 else {
00968 return g;
00969 }
00970 }
00971 if (CalBddIsBddConst(g)){
00972 if (CalBddIsBddZero(bddManager, g)){
00973 return g;
00974 }
00975 else {
00976 return f;
00977 }
00978 }
00979 if (CalBddSameOrNegation(f, g)){
00980 if (CalBddIsEqual(f, g)){
00981 return f;
00982 }
00983 else
00984 return bddManager->bddZero;
00985 }
00986 if (CAL_BDD_OUT_OF_ORDER(f, g)) CAL_BDD_SWAP(f, g);
00987 CalBddGetMinId2(bddManager, f, g, topId);
00988 CalBddGetCofactors(f, topId, f1, f2);
00989 CalBddGetCofactors(g, topId, g1, g2);
00990 temp = BddIntersectsStep(bddManager, f1, g1);
00991 if (CalBddIsBddZero(bddManager, temp)){
00992 temp = BddIntersectsStep(bddManager, f2, g2);
00993 if (CalBddIsBddZero(bddManager, temp)){
00994 return bddManager->bddZero;
00995 }
00996 else{
00997 if(CalUniqueTableForIdFindOrAdd(bddManager,
00998 bddManager->uniqueTable[topId],
00999 bddManager->bddZero, temp,
01000 &result) == 0){
01001 CalBddIcrRefCount(temp);
01002 }
01003 }
01004 }
01005 else {
01006 if(CalUniqueTableForIdFindOrAdd(bddManager, bddManager->uniqueTable[topId],
01007 temp, bddManager->bddZero,&result) == 0){
01008 CalBddIcrRefCount(temp);
01009 }
01010 }
01011 return result;
01012 }
01013
01014
01015
01016
01017
01018
01019
01020
01021
01022
01023
01024
01025
01026
01027
01028
01029
01030
01031
01032
01033
01034
