src/calBdd/cal.c File Reference

#include "calInt.h"
Include dependency graph for cal.c:

Go to the source code of this file.

Functions

static Cal_Bdd_t BddIntersectsStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g)
int Cal_BddIsEqual (Cal_BddManager bddManager, Cal_Bdd userBdd1, Cal_Bdd userBdd2)
int Cal_BddIsBddOne (Cal_BddManager bddManager, Cal_Bdd userBdd)
int Cal_BddIsBddZero (Cal_BddManager bddManager, Cal_Bdd userBdd)
int Cal_BddIsBddNull (Cal_BddManager bddManager, Cal_Bdd userBdd)
int Cal_BddIsBddConst (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddIdentity (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddOne (Cal_BddManager bddManager)
Cal_Bdd Cal_BddZero (Cal_BddManager bddManager)
Cal_Bdd Cal_BddNot (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_BddId_t Cal_BddGetIfIndex (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_BddId_t Cal_BddGetIfId (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddIf (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddThen (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddElse (Cal_BddManager bddManager, Cal_Bdd userBdd)
void Cal_BddFree (Cal_BddManager bddManager, Cal_Bdd userBdd)
void Cal_BddUnFree (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddGetRegular (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd Cal_BddIntersects (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddImplies (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
unsigned long Cal_BddTotalSize (Cal_BddManager bddManager)
void Cal_BddStats (Cal_BddManager bddManager, FILE *fp)
void Cal_BddDynamicReordering (Cal_BddManager bddManager, int technique)
void Cal_BddReorder (Cal_BddManager bddManager)
int Cal_BddType (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
long Cal_BddVars (Cal_BddManager bddManager)
long Cal_BddNodeLimit (Cal_BddManager bddManager, long newLimit)
int Cal_BddOverflow (Cal_BddManager bddManager)
int Cal_BddIsCube (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
void * Cal_BddManagerGetHooks (Cal_BddManager bddManager)
void Cal_BddManagerSetHooks (Cal_BddManager bddManager, void *hooks)
Cal_Bdd_t CalBddIf (Cal_BddManager bddManager, Cal_Bdd_t F)
int CalBddIsCubeStep (Cal_BddManager bddManager, Cal_Bdd_t f)
int CalBddTypeAux (Cal_BddManager_t *bddManager, Cal_Bdd_t f)
Cal_Bdd_t CalBddIdentity (Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd)

Function Documentation

static Cal_Bdd_t BddIntersectsStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  g 
) [static]

CFile***********************************************************************

FileName [cal.c]

PackageName [cal]

Synopsis [Miscellaneous collection of exported BDD functions]

Description []

SeeAlso []

Author [ Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu ]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
cal.c,v 1.2 2009/04/11 23:43:52 fabio Exp

]AutomaticStart

Function********************************************************************

Synopsis [Recursive routine to returns a BDD that implies conjunction of argument BDDs]

Description [Recursive routine to returns a BDD that implies conjunction of argument BDDs]

SideEffects [None]

Definition at line 957 of file cal.c.

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 }

void Cal_BddDynamicReordering ( Cal_BddManager  bddManager,
int  technique 
)

Function********************************************************************

Synopsis [Specify dynamic reordering technique.]

Description [Selects the method for dynamic reordering.]

SideEffects [None]

SeeAlso [Cal_BddReorder]

Definition at line 640 of file cal.c.

00641 {
00642   bddManager->reorderTechnique = technique;
00643   bddManager->dynamicReorderingEnableFlag = 1;
00644 }

Cal_Bdd Cal_BddElse ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the negative cofactor of the argument BDD with respect to the top variable of the BDD.]

Description [Returns the negative cofactor of the argument BDD with respect to the top variable of the BDD.]

SideEffects [The reference count of the returned BDD is increased by 1.]

SeeAlso [Cal_BddThen]

Definition at line 365 of file cal.c.

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 }

void Cal_BddFree ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Frees the argument BDD.]

Description [Frees the argument BDD. It is an error to free a BDD more than once.]

SideEffects [The reference count of the argument BDD is decreased by 1.]

SeeAlso [Cal_BddUnFree]

Definition at line 390 of file cal.c.

00391 {
00392   /* Interface BDD reference count */
00393   CalBddNodeDcrRefCount(CAL_BDD_POINTER(userBdd));
00394 }

Cal_BddId_t Cal_BddGetIfId ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the id of the top variable of the argument BDD.]

Description [Returns the id of the top variable of the argument BDD.]

SideEffects [None]

SeeAlso [Cal_BddGetIfIndex]

Definition at line 286 of file cal.c.

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 }

Cal_BddId_t Cal_BddGetIfIndex ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the index of the top variable of the argument BDD.]

Description [Returns the index of the top variable of the argument BDD.]

SideEffects [None]

SeeAlso [Cal_BddGetIfId]

Definition at line 260 of file cal.c.

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 }

Cal_Bdd Cal_BddGetRegular ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns a BDD with positive from a given BDD with arbitrary phase]

Description [Returns a BDD with positive from a given BDD with arbitrary phase]

SideEffects [None.]

Definition at line 428 of file cal.c.

00429 {
00430   return CAL_BDD_POINTER(userBdd);
00431 }

Cal_Bdd Cal_BddIdentity ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the duplicate BDD of the argument BDD.]

Description [Returns the duplicate BDD of the argument BDD.]

SideEffects [The reference count of the BDD is increased by 1.]

SeeAlso [Cal_BddNot]

Definition at line 185 of file cal.c.

00186 {
00187   /* Interface BDD reference count */
00188   CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
00189   CalBddNodeIcrRefCount(bddNode);
00190   return userBdd;
00191 }

Cal_Bdd Cal_BddIf ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the BDD corresponding to the top variable of the argument BDD.]

Description [Returns the BDD corresponding to the top variable of the argument BDD.]

SideEffects [None.]

Definition at line 311 of file cal.c.

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 }

Cal_Bdd Cal_BddImplies ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  gUserBdd 
)

Function********************************************************************

Synopsis [Computes a BDD that implies conjunction of f and Cal_BddNot(g)]

Description [Computes a BDD that implies conjunction of f and Cal_BddNot(g)]

SideEffects [none]

SeeAlso [Cal_BddIntersects]

Definition at line 471 of file cal.c.

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 }

Cal_Bdd Cal_BddIntersects ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  gUserBdd 
)

Function********************************************************************

Synopsis [Computes a BDD that implies conjunction of f and g.]

Description [Computes a BDD that implies conjunction of f and g.]

SideEffects [None]

SeeAlso [Cal_BddImplies]

Definition at line 445 of file cal.c.

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 }

int Cal_BddIsBddConst ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is a constant, 0 otherwise.]

Description [Returns 1 if the argument BDD is either constant one or constant zero, otherwise returns 0.]

SideEffects [None.]

SeeAlso [Cal_BddIsBddOne, Cal_BddIsBddZero]

Definition at line 165 of file cal.c.

00168 {
00169   return ((userBdd == bddManager->userOneBdd) ||
00170           (userBdd == bddManager->userZeroBdd));
00171 }

int Cal_BddIsBddNull ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is NULL, 0 otherwise.]

Description [Returns 1 if the argument BDD is NULL, 0 otherwise.]

SideEffects [None.]

Definition at line 146 of file cal.c.

00147 {
00148   return (userBdd == 0);
00149 }

int Cal_BddIsBddOne ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is constant one, 0 otherwise.]

Description [Returns 1 if the argument BDD is constant one, 0 otherwise.]

SideEffects [None.]

SeeAlso [Cal_BddIsBddZero]

Definition at line 112 of file cal.c.

00113 {
00114   return (userBdd == bddManager->userOneBdd);
00115 }

int Cal_BddIsBddZero ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is constant zero, 0 otherwise.]

Description [Returns 1 if the argument BDD is constant zero, 0 otherwise.]

SideEffects [None.]

SeeAlso [Cal_BddIsBddOne]

Definition at line 129 of file cal.c.

00132 {
00133   return (userBdd == bddManager->userZeroBdd);
00134 }

int Cal_BddIsCube ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is a cube, 0 otherwise]

Description [Returns 1 if the argument BDD is a cube, 0 otherwise]

SideEffects [None]

Definition at line 774 of file cal.c.

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    * Exactly one branch of f must point to ZERO to be a cube.
00792    */
00793   if (CalBddIsBddZero(bddManager, f1)){
00794         return (CalBddIsCubeStep(bddManager, f0));
00795   } else if (CalBddIsBddZero(bddManager, f0)){
00796         return (CalBddIsCubeStep(bddManager, f1));
00797   } else { /* not a cube, because neither branch is zero */
00798         return 0;
00799   }
00800 }

int Cal_BddIsEqual ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd1,
Cal_Bdd  userBdd2 
)

AutomaticEnd Function********************************************************************

Synopsis [Returns 1 if argument BDDs are equal, 0 otherwise.]

Description [Returns 1 if argument BDDs are equal, 0 otherwise.]

SideEffects [None.]

SeeAlso []

Definition at line 95 of file cal.c.

00096 {
00097   return (userBdd1 == userBdd2);
00098 }

void* Cal_BddManagerGetHooks ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Returns the hooks field of the manager.]

Description [Returns the hooks field of the manager.]

SideEffects [None]

SeeAlso []

Definition at line 814 of file cal.c.

00815 {
00816   return bddManager->hooks;
00817 }

void Cal_BddManagerSetHooks ( Cal_BddManager  bddManager,
void *  hooks 
)

Function********************************************************************

Synopsis [Sets the hooks field of the manager.]

Description [Sets the hooks field of the manager.]

SideEffects [Hooks field changes. ]

SeeAlso []

Definition at line 831 of file cal.c.

00832 {
00833   bddManager->hooks = hooks;
00834 }

long Cal_BddNodeLimit ( Cal_BddManager  bddManager,
long  newLimit 
)

Function********************************************************************

Synopsis [Sets the node limit to new_limit and returns the old limit.]

Description [Sets the node limit to new_limit and returns the old limit.]

SideEffects [Threshold for garbage collection may change]

SeeAlso [Cal_BddManagerGC]

Definition at line 725 of file cal.c.

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 }

Cal_Bdd Cal_BddNot ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the complement of the argument BDD.]

Description [Returns the complement of the argument BDD.]

SideEffects [The reference count of the argument BDD is increased by 1.]

SeeAlso [Cal_BddIdentity]

Definition at line 240 of file cal.c.

00241 {
00242   /* Interface BDD reference count */
00243   CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
00244   CalBddNodeIcrRefCount(bddNode);
00245   return CalBddNodeNot(userBdd);
00246 }

Cal_Bdd Cal_BddOne ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Returns the BDD for the constant one]

Description [Returns the BDD for the constant one]

SideEffects [None]

SeeAlso [Cal_BddZero]

Definition at line 205 of file cal.c.

00206 {
00207   return bddManager->userOneBdd;
00208 }

int Cal_BddOverflow ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Returns 1 if the node limit has been exceeded, 0 otherwise. The overflow flag is cleared.]

Description [Returns 1 if the node limit has been exceeded, 0 otherwise. The overflow flag is cleared.]

SideEffects [None]

SeeAlso [Cal_BddNodeLimit]

Definition at line 756 of file cal.c.

00757 {
00758   int result;
00759   result = bddManager->overflow;
00760   bddManager->overflow = 0;
00761   return (result);
00762 }

void Cal_BddReorder ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Invoke the current dynamic reodering method.]

Description [Invoke the current dynamic reodering method.]

SideEffects [Index of a variable may change due to reodering]

SeeAlso [Cal_BddDynamicReordering]

Definition at line 658 of file cal.c.

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 }

void Cal_BddStats ( Cal_BddManager  bddManager,
FILE *  fp 
)

Function********************************************************************

Synopsis [Prints miscellaneous BDD statistics]

Description [Prints miscellaneous BDD statistics]

SideEffects [None]

Definition at line 516 of file cal.c.

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   /* Calculate the memory consumed */
00562   totalBytes =
00563       /* Over all bdd manager */
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       /* Page manager */
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   /* IndexToId and IdToIndex */
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   /* Cache Table */
00583   totalBytes += CalCacheTableMemoryConsumption(bddManager->cacheTable);
00584   
00585   /* Req que */
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   /* Association */
00597   totalBytes += sizeof(CalAssociation_t)*2;
00598   /* Block */
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 }

Cal_Bdd Cal_BddThen ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Returns the positive cofactor of the argument BDD with respect to the top variable of the BDD.]

Description [Returns the positive cofactor of the argument BDD with respect to the top variable of the BDD.]

SideEffects [The reference count of the returned BDD is increased by 1.]

SeeAlso [Cal_BddElse]

Definition at line 339 of file cal.c.

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 }

unsigned long Cal_BddTotalSize ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Returns the number of nodes in the Unique table]

Description [Returns the number of nodes in the Unique table]

SideEffects [None]

SeeAlso [Cal_BddManagerGetNumNodes]

Definition at line 500 of file cal.c.

00501 {
00502   return Cal_BddManagerGetNumNodes(bddManager);
00503 }

int Cal_BddType ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

Function********************************************************************

Synopsis [Returns type of a BDD ( 0, 1, +var, -var, ovrflow, nonterminal)]

Description [Returns BDD_TYPE_ZERO if f is false, BDD_TYPE_ONE if f is true, BDD_TYPE_POSVAR is f is an unnegated variable, BDD_TYPE_NEGVAR if f is a negated variable, BDD_TYPE_OVERFLOW if f is null, and BDD_TYPE_NONTERMINAL otherwise.]

SideEffects [None]

Definition at line 688 of file cal.c.

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 }

void Cal_BddUnFree ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

Function********************************************************************

Synopsis [Unfrees the argument BDD.]

Description [Unfrees the argument BDD. It is an error to pass a BDD with reference count of zero to be unfreed.]

SideEffects [The reference count of the argument BDD is increased by 1.]

SeeAlso [Cal_BddFree]

Definition at line 410 of file cal.c.

00411 {
00412   /* Interface BDD reference count */
00413   CalBddNode_t *bddNode = CAL_BDD_POINTER(userBdd);
00414   CalBddNodeIcrRefCount(bddNode);
00415 }

long Cal_BddVars ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Returns the number of BDD variables]

Description [Returns the number of BDD variables]

SideEffects [None]

Definition at line 707 of file cal.c.

00708 {
00709   return (bddManager->numVars);
00710 }

Cal_Bdd Cal_BddZero ( Cal_BddManager  bddManager  ) 

Function********************************************************************

Synopsis [Returns the BDD for the constant zero]

Description [Returns the BDD for the constant zero]

SideEffects [None]

SeeAlso [Cal_BddOne]

Definition at line 222 of file cal.c.

00223 {
00224   return bddManager->userZeroBdd;
00225 }

Cal_Bdd_t CalBddIdentity ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  calBdd 
)

Function********************************************************************

Synopsis [Returns the duplicate BDD of the argument BDD.]

Description [Returns the duplicate BDD of the argument BDD.]

SideEffects [The reference count of the BDD is increased by 1.]

SeeAlso [Cal_BddNot]

Definition at line 935 of file cal.c.

00936 {
00937   CalBddIcrRefCount(calBdd);
00938   return calBdd;
00939 }

Cal_Bdd_t CalBddIf ( Cal_BddManager  bddManager,
Cal_Bdd_t  F 
)

Function********************************************************************

Synopsis [Returns the BDD corresponding to the top variable of the argument BDD.]

Description [Returns the BDD corresponding to the top variable of the argument BDD.]

SideEffects [None.]

Definition at line 852 of file cal.c.

00853 {
00854   if (CalBddIsBddConst(F)){
00855     CalBddWarningMessage("CalBddIf: argument is constant");
00856   }
00857   return bddManager->varBdds[CalBddGetBddId(F)];
00858 }

int CalBddIsCubeStep ( Cal_BddManager  bddManager,
Cal_Bdd_t  f 
)

Function********************************************************************

Synopsis [Returns 1 if the argument BDD is a cube, 0 otherwise]

Description [Returns 1 if the argument BDD is a cube, 0 otherwise]

SideEffects [None]

Definition at line 870 of file cal.c.

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    * Exactly one branch of f must point to ZERO to be a cube.
00884    */
00885   if (CalBddIsBddZero(bddManager, f1)){
00886         return (CalBddIsCubeStep(bddManager, f0));
00887   } else if (CalBddIsBddZero(bddManager, f0)){
00888         return (CalBddIsCubeStep(bddManager, f1));
00889   } else { /* not a cube, because neither branch is zero */
00890         return 0;
00891   }
00892 }

int CalBddTypeAux ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f 
)

Function********************************************************************

Synopsis [Returns the BDD type by recursively traversing the argument BDD]

Description [Returns the BDD type by recursively traversing the argument BDD]

SideEffects [None]

Definition at line 904 of file cal.c.

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 }

Generated on Tue Jan 12 13:57:09 2010 for glu-2.2 by  doxygen 1.6.1