src/calBdd/cal.h File Reference
#include <stdio.h>#include <stdlib.h>#include <string.h>#include <assert.h>#include <math.h>#include "calMem.h"
Go to the source code of this file.
Define Documentation
| #define Cal_BddNamingFnNone ((char *(*)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t))0) |
| #define Cal_BddTerminalIdFnNone ((char *(*)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t))0) |
| #define EXTERN extern |
CHeaderFile*****************************************************************
FileName [cal.h]
PackageName [cal]
Synopsis [Header CAL file for exported data structures and functions.]
Description []
SeeAlso [optional]
Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) 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.h,v 1.8 2002/09/08 21:22:16 fabio Exp
]
Typedef Documentation
| typedef struct CalBddNodeStruct* Cal_Bdd |
| typedef unsigned short int Cal_BddId_t |
| typedef unsigned short int Cal_BddIndex_t |
| typedef struct Cal_BddManagerStruct* Cal_BddManager |
| typedef struct Cal_BddManagerStruct Cal_BddManager_t |
| typedef enum Cal_BddOpEnum Cal_BddOp_t |
| typedef struct Cal_BlockStruct* Cal_Block |
| typedef char*(* Cal_TerminalIdFn_t)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t) |
| typedef char*(* Cal_VarNamingFn_t)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t) |
Enumeration Type Documentation
| enum Cal_BddOpEnum |
Function Documentation
| EXTERN int Cal_AssociationInit | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | associationInfoUserBdds, | |||
| int | pairs | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Creates or finds a variable association.]
Description [Creates or finds a variable association. The association is specified by associationInfo, which is a an array of BDD with Cal_BddNull(bddManager) as the end marker. If pairs is 0, the array is assumed to be an array of variables. In this case, each variable is paired with constant BDD one. Such an association may viewed as specifying a set of variables for use with routines such as Cal_BddExists. If pair is not 0, then the even numbered array elements should be variables and the odd numbered elements should be the BDDs which they are mapped to. In both cases, the return value is an integer identifier for this association. If the given association is equivalent to one which already exists, the same identifier is used for both, and the reference count of the association is increased by one.]
SideEffects [None]
SeeAlso [Cal_AssociationQuit]
Definition at line 106 of file calAssociation.c.
00109 { 00110 int i, numAssociations; 00111 CalAssociation_t *p, **q; 00112 Cal_Bdd_t f; 00113 Cal_Bdd_t *varAssociation; 00114 Cal_BddId_t j; 00115 long last; 00116 Cal_Bdd_t *associationInfo; 00117 00118 if (!CheckAssoc(bddManager, associationInfoUserBdds, pairs)){ 00119 return (-1); 00120 } 00121 00122 00123 /* First count the number of elements */ 00124 for (i=0; associationInfoUserBdds[i]; i++); 00125 if (pairs) numAssociations = i/2; 00126 else numAssociations = i; 00127 associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1); 00128 for (j=0; j < i; j++){ 00129 associationInfo[j] = 00130 CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]); 00131 } 00132 associationInfo[j] = bddManager->bddNull; 00133 00134 00135 varAssociation = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1); 00136 for(i = 0; i <= bddManager->maxNumVars; i++){ 00137 varAssociation[i] = bddManager->bddNull; 00138 } 00139 00140 00141 if(pairs){ 00142 for(i = 0; i < numAssociations; i++){ 00143 f = associationInfo[(i<<1)]; 00144 varAssociation[CalBddGetBddId(f)] = associationInfo[(i<<1)+1]; 00145 } 00146 } 00147 else{ 00148 for(i = 0; i < numAssociations; i++){ 00149 f=associationInfo[i]; 00150 varAssociation[CalBddGetBddId(f)] = CalBddOne(bddManager); 00151 } 00152 } 00153 /* Check for existence. */ 00154 for(p = bddManager->associationList; p; p = p->next){ 00155 if(AssociationIsEqual(bddManager, p->varAssociation, varAssociation)){ 00156 Cal_MemFree(varAssociation); 00157 Cal_MemFree(associationInfo); 00158 p->refCount++; 00159 return (p->id); 00160 } 00161 } 00162 /* Find the first unused id. */ 00163 for(q = &bddManager->associationList, p = *q, i = 0; 00164 p && p->id == i; q = &p->next, p = *q, ++i){ 00165 } 00166 /*p = Cal_MemAlloc(CalAssociation_t, 1);*/ 00167 /*p = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/ 00168 p = Cal_MemAlloc(CalAssociation_t, 1); 00169 p->id = i; 00170 p->next = *q; 00171 *q = p; 00172 p->varAssociation = varAssociation; 00173 last = -1; 00174 if(pairs){ 00175 for(i = 0; i < numAssociations; i++){ 00176 f = associationInfo[(i<<1)]; 00177 j = CalBddGetBddIndex(bddManager, f); 00178 if((long)j > last){ 00179 last = j; 00180 } 00181 } 00182 } 00183 else{ 00184 for(i = 0; i < numAssociations; i++){ 00185 f = associationInfo[i]; 00186 j = CalBddGetBddIndex(bddManager, f); 00187 if((long)j > last){ 00188 last = j; 00189 } 00190 } 00191 } 00192 p->lastBddIndex = last; 00193 p->refCount = 1; 00194 /* Protect BDDs in the association. */ 00195 if(pairs){ 00196 for(i = 0; i < numAssociations; i++){ 00197 f = associationInfo[(i<<1)+1]; 00198 CalBddIcrRefCount(f); 00199 } 00200 } 00201 Cal_MemFree(associationInfo); 00202 return p->id; 00203 }
| EXTERN void Cal_AssociationQuit | ( | Cal_BddManager | bddManager, | |
| int | associationId | |||
| ) |
Function********************************************************************
Synopsis [Deletes the variable association given by id]
Description [Decrements the reference count of the variable association with identifier id, and frees it if the reference count becomes zero.]
SideEffects [None]
SeeAlso [Cal_AssociationInit]
Definition at line 219 of file calAssociation.c.
00220 { 00221 Cal_BddId_t i; 00222 Cal_Bdd_t f; 00223 CalAssociation_t *p, **q; 00224 00225 if(bddManager->currentAssociation->id == associationId){ 00226 bddManager->currentAssociation = bddManager->tempAssociation; 00227 } 00228 for(q = &bddManager->associationList, p = *q; p; q = &p->next, p = *q){ 00229 if(p->id == associationId){ 00230 p->refCount--; 00231 if(!p->refCount){ 00232 /* Unprotect the BDDs in the association. */ 00233 for(i = 1; i <= bddManager->numVars; i++){ 00234 f = p->varAssociation[i]; 00235 if(!CalBddIsBddNull(bddManager, f)){ 00236 CalBddDcrRefCount(f); 00237 } 00238 } 00239 *q = p->next; 00240 Cal_MemFree(p->varAssociation); 00241 /*CAL_BDD_FREE_REC(bddManager, p, CalAssociation_t);*/ 00242 Cal_MemFree(p); 00243 CalCacheTableTwoFlushAssociationId(bddManager, associationId); 00244 } 00245 return; 00246 } 00247 } 00248 CalBddWarningMessage("Cal_AssociationQuit: no association with specified ID"); 00249 }
| EXTERN int Cal_AssociationSetCurrent | ( | Cal_BddManager | bddManager, | |
| int | associationId | |||
| ) |
Function********************************************************************
Synopsis [Sets the current variable association to the one given by id and returns the ID of the old association.]
Description [Sets the current variable association to the one given by id and returns the ID of the old association. An id of -1 indicates the temporary association]
SideEffects [None]
Definition at line 264 of file calAssociation.c.
00265 { 00266 int oldAssociationId; 00267 CalAssociation_t *p; 00268 00269 oldAssociationId = bddManager->currentAssociation->id; 00270 if(associationId != -1){ 00271 for(p = bddManager->associationList; p; p = p->next){ 00272 if(p->id == associationId){ 00273 bddManager->currentAssociation = p; 00274 return (oldAssociationId); 00275 } 00276 } 00277 CalBddWarningMessage( 00278 "Cal_AssociationSetCurrent: no variable association with specified ID.\n May have been discarded during dynamic reordering."); 00279 } 00280 bddManager->currentAssociation = bddManager->tempAssociation; 00281 return oldAssociationId; 00282 }
| EXTERN Cal_Bdd Cal_BddAnd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Returns the BDD for logical AND of argument BDDs]
Description [Returns the BDD for logical AND of f and g]
SideEffects [None]
Definition at line 90 of file calBddOp.c.
00094 { 00095 Cal_Bdd_t result; 00096 Cal_Bdd userResult; 00097 Cal_Bdd_t F, G; 00098 00099 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00100 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00101 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00102 result = CalBddOpBF(bddManager, CalOpAnd, F, G); 00103 } 00104 else { 00105 return (Cal_Bdd)0; 00106 } 00107 userResult = CalBddGetExternalBdd(bddManager, result); 00108 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00109 Cal_BddFree(bddManager, userResult); 00110 Cal_BddManagerGC(bddManager); 00111 return (Cal_Bdd) 0; 00112 } 00113 return userResult; 00114 }
| EXTERN Cal_Bdd Cal_BddBetween | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fMinUserBdd, | |||
| Cal_Bdd | fMaxUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns a minimal BDD whose function contains fMin and is contained in fMax.]
Description [Returns a minimal BDD f which is contains fMin and is contained in fMax ( fMin <= f <= fMax). This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step (Rk Rk-1' <= f <= Rk).]
SideEffects [None]
SeeAlso [Cal_BddReduce]
Definition at line 185 of file calReduce.c.
00187 { 00188 if (CalBddPreProcessing(bddManager, 2, fMinUserBdd, fMaxUserBdd)){ 00189 Cal_Bdd_t fMin = CalBddGetInternalBdd(bddManager, fMinUserBdd); 00190 Cal_Bdd_t fMax = CalBddGetInternalBdd(bddManager, fMaxUserBdd); 00191 Cal_Bdd_t fMaxNot, careSet, result; 00192 Cal_Bdd resultUserBdd; 00193 long fMinSize, fMaxSize, resultSize; 00194 00195 CalBddNot(fMax, fMaxNot); 00196 careSet = CalBddOpBF(bddManager, CalOpOr, fMin, fMaxNot); 00197 result = BddReduceBF(bddManager, CalOpCofactor, fMin, careSet); 00198 resultUserBdd = CalBddGetExternalBdd(bddManager, result); 00199 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00200 Cal_BddFree(bddManager, resultUserBdd); 00201 Cal_BddManagerGC(bddManager); 00202 return (Cal_Bdd) 0; 00203 } 00204 fMinSize = Cal_BddSize(bddManager, fMinUserBdd, 1); 00205 fMaxSize = Cal_BddSize(bddManager, fMaxUserBdd, 1); 00206 resultSize = Cal_BddSize(bddManager, resultUserBdd, 1); 00207 if (resultSize < fMinSize){ 00208 if (resultSize < fMaxSize){ 00209 return resultUserBdd; 00210 } 00211 else { 00212 Cal_BddFree(bddManager, resultUserBdd); 00213 return Cal_BddIdentity(bddManager, fMaxUserBdd); 00214 } 00215 } 00216 Cal_BddFree(bddManager, resultUserBdd); 00217 if (fMinSize < fMaxSize){ 00218 return Cal_BddIdentity(bddManager, fMinUserBdd); 00219 } 00220 else{ 00221 return Cal_BddIdentity(bddManager, fMaxUserBdd); 00222 } 00223 } 00224 return (Cal_Bdd) 0; 00225 }
| EXTERN Cal_Bdd Cal_BddCofactor | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | cUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Returns the generalized cofactor of BDD f with respect to BDD c.]
Description [Returns the generalized cofactor of BDD f with respect to BDD c. The constrain operator given by Coudert et al (ICCAD90) is used to find the generalized cofactor.]
SideEffects [None.]
SeeAlso [Cal_BddReduce]
Definition at line 100 of file calReduce.c.
00102 { 00103 Cal_Bdd_t result; 00104 Cal_Bdd userResult; 00105 if (CalBddPreProcessing(bddManager, 2, fUserBdd, cUserBdd)){ 00106 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00107 Cal_Bdd_t c = CalBddGetInternalBdd(bddManager, cUserBdd); 00108 result = BddCofactorBF(bddManager, CalOpCofactor, f, c); 00109 userResult = CalBddGetExternalBdd(bddManager, result); 00110 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00111 Cal_BddFree(bddManager, userResult); 00112 Cal_BddManagerGC(bddManager); 00113 return (Cal_Bdd) 0; 00114 } 00115 return userResult; 00116 } 00117 return (Cal_Bdd) 0; 00118 }
| EXTERN Cal_Bdd Cal_BddCompose | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd, | |||
| Cal_Bdd | hUserBdd | |||
| ) |
CFile***********************************************************************
FileName [calBddCompose.c]
PackageName [cal]
Synopsis [Routine for composing one BDD into another.]
Description []
SeeAlso []
Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@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
- calBddCompose.c,v 1.1.1.3 1998/05/04 00:58:50 hsv Exp
]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [composition - substitute a BDD variable by a function]
Description [Returns the BDD obtained by substituting a variable by a function]
SideEffects [None]
Definition at line 84 of file calBddCompose.c.
00086 { 00087 Cal_Bdd_t result; 00088 CalRequestNode_t *requestNode; 00089 Cal_Bdd_t F, G, H; 00090 00091 if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd) == 0){ 00092 result = bddManager->bddNull; 00093 } 00094 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00095 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00096 H = CalBddGetInternalBdd(bddManager, hUserBdd); 00097 00098 if(CalBddIsBddConst(G)){ 00099 CalBddNodeIcrRefCount(fUserBdd); 00100 return fUserBdd; 00101 } 00102 CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode); 00103 CalRequestNodePutF(requestNode, F); 00104 CalRequestNodePutG(requestNode, H); 00105 CalRequestNodePutNextRequestNode(requestNode, 0); 00106 bddManager->requestNodeListArray[0] = requestNode; 00107 /* 00108 ** We can achieve a superscalar compose operation, provided G 00109 ** is the same for all the compose operation 00110 */ 00111 00112 CalRequestNodeListCompose(bddManager, bddManager->requestNodeListArray[0], 00113 CalBddGetBddIndex(bddManager, G)); 00114 00115 CalRequestNodeGetThenRequest(requestNode, result); 00116 CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode); 00117 bddManager->requestNodeListArray[0] = Cal_Nil(CalRequestNode_t); 00118 00119 return CalBddGetExternalBdd(bddManager, result); 00120 }
| EXTERN int Cal_BddDependsOn | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | varUserBdd | |||
| ) |
Function********************************************************************
Name [Cal_BddDependsOn]
Synopsis [Returns 1 if f depends on var and returns 0 otherwise.]
Description [Returns 1 if f depends on var and returns 0 otherwise.]
SideEffects [None]
Definition at line 125 of file calBddSupport.c.
00127 { 00128 Cal_BddIndex_t bddIndex; 00129 Cal_Bdd_t f, var; 00130 00131 if(CalBddPreProcessing(bddManager, 2, fUserBdd, varUserBdd)){ 00132 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00133 var = CalBddGetInternalBdd(bddManager, varUserBdd); 00134 if(CalBddIsBddConst(var)){ 00135 return 1; 00136 } 00137 bddIndex = CalBddGetBddIndex(bddManager, var); 00138 CalBddDependsOnStep(bddManager, f, bddIndex, 1); 00139 return CalBddDependsOnStep(bddManager, f, bddIndex, 0); 00140 } 00141 return (0); 00142 }
| EXTERN int Cal_BddDumpBdd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd * | userVars, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Write a BDD to a file]
Description [Writes an encoded description of the BDD to the file given by fp. The argument vars should be a null-terminated array of variables that include the support of f . These variables need not be in order of increasing index. The function returns a nonzero value if f was written to the file successfully. ]
SideEffects [required]
SeeAlso [optional]
Definition at line 229 of file calDump.c.
00234 { 00235 long i; 00236 Cal_BddIndex_t *normalizedIndexes; 00237 Cal_BddIndex_t vIndex; 00238 Cal_Bdd_t f; 00239 Cal_BddIndex_t numberVars; 00240 Cal_Bdd *support; 00241 int ok; 00242 CalHashTable_t *h; 00243 int indexSize; 00244 long next; 00245 int nodeNumberSize; 00246 00247 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00248 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00249 for(i = 0; userVars[i]; ++i){ 00250 if(Cal_BddType(bddManager, userVars[i]) != CAL_BDD_TYPE_POSVAR){ 00251 CalBddWarningMessage("Cal_BddDumpBdd: support is not all positive variables"); 00252 return (0); 00253 } 00254 } 00255 normalizedIndexes = Cal_MemAlloc(Cal_BddIndex_t, bddManager->numVars); 00256 for(i = 0; i < bddManager->numVars; ++i){ 00257 normalizedIndexes[i] = CAL_BDD_CONST_INDEX; 00258 } 00259 for(i = 0; userVars[i]; ++i){ 00260 vIndex = Cal_BddGetIfIndex(bddManager, userVars[i]); 00261 if(normalizedIndexes[vIndex] != CAL_BDD_CONST_INDEX){ 00262 CalBddWarningMessage("Cal_BddDumpBdd: variables duplicated in support"); 00263 Cal_MemFree(normalizedIndexes); 00264 return 0; 00265 } 00266 normalizedIndexes[vIndex] = i; 00267 } 00268 numberVars = i; 00269 support = Cal_MemAlloc(Cal_Bdd, bddManager->numVars+1); 00270 Cal_BddSupport(bddManager, fUserBdd, support); 00271 ok = 1; 00272 for(i = 0; ok && support[i]; ++i){ 00273 if(normalizedIndexes[Cal_BddGetIfIndex(bddManager, support[i])] == CAL_BDD_CONST_INDEX){ 00274 CalBddWarningMessage("Cal_BddDumpBdd: incomplete support specified"); 00275 ok = 0; 00276 } 00277 } 00278 if(!ok){ 00279 Cal_MemFree(normalizedIndexes); 00280 Cal_MemFree(support); 00281 return 0; 00282 } 00283 Cal_MemFree(support); 00284 /* Everything checked now; barring I/O errors, we should be able to */ 00285 /* Write a valid output file. */ 00286 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00287 h = CalHashTableOneInit(bddManager, sizeof(long)); 00288 indexSize = BytesNeeded(numberVars+1); 00289 CalBddMarkSharedNodes(bddManager, f); 00290 next = 0; 00291 CalBddNumberSharedNodes(bddManager, f, h, &next); 00292 nodeNumberSize = BytesNeeded(next); 00293 Write(bddManager, MAGIC_COOKIE, sizeof(long), fp); 00294 Write(bddManager, (unsigned long)numberVars, sizeof(Cal_BddIndex_t), fp); 00295 Write(bddManager, (unsigned long)next, sizeof(long), fp); 00296 BddDumpBddStep(bddManager, f, fp, h, normalizedIndexes, indexSize, nodeNumberSize); 00297 CalHashTableOneQuit(h); 00298 Cal_MemFree(normalizedIndexes); 00299 return (1); 00300 } 00301 return (0); 00302 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN Cal_Bdd Cal_BddExists | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Returns the result of existentially quantifying some variables from the given BDD.]
Description [Returns the BDD for f with all the variables that are paired with something in the current variable association existentially quantified out.]
SideEffects [None.]
SeeAlso [Cal_BddRelProd]
Definition at line 110 of file calQuant.c.
00111 { 00112 Cal_Bdd_t result; 00113 Cal_Bdd userResult; 00114 00115 if (CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00116 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00117 CalAssociation_t *assoc = bddManager->currentAssociation; 00118 unsigned short opCode; 00119 00120 if (assoc->id == -1){ 00121 opCode = bddManager->tempOpCode--; 00122 } 00123 else { 00124 opCode = CAL_OP_QUANT + assoc->id; 00125 } 00126 if (bddManager->numNodes <= CAL_LARGE_BDD){ 00127 /* If number of nodes is small, call depth first routine. */ 00128 result = BddExistsStep(bddManager, f, opCode, assoc); 00129 } 00130 else { 00131 result = BddExistsBFPlusDF(bddManager, f, opCode, assoc); 00132 } 00133 userResult = CalBddGetExternalBdd(bddManager, result); 00134 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00135 Cal_BddFree(bddManager, userResult); 00136 Cal_BddManagerGC(bddManager); 00137 return (Cal_Bdd) 0; 00138 } 00139 return userResult; 00140 } 00141 return (Cal_Bdd) 0; 00142 }
| EXTERN Cal_Bdd Cal_BddForAll | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the result of universally quantifying some variables from the given BDD.]
Description [Returns the BDD for f with all the variables that are paired with something in the current variable association universally quantified out.]
SideEffects [None.]
Definition at line 208 of file calQuant.c.
00209 { 00210 Cal_Bdd_t result; 00211 Cal_Bdd userResult; 00212 00213 if (CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00214 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00215 CalAssociation_t *assoc = bddManager->currentAssociation; 00216 unsigned short opCode; 00217 00218 CalBddNot(f, f); 00219 if (assoc->id == -1){ 00220 opCode = bddManager->tempOpCode--; 00221 } 00222 else { 00223 opCode = CAL_OP_QUANT + assoc->id; 00224 } 00225 if (bddManager->numNodes <= CAL_LARGE_BDD){ 00226 /* If number of nodes is small, call depth first routine. */ 00227 result = BddExistsStep(bddManager, f, opCode, assoc); 00228 } 00229 else { 00230 result = BddExistsBFPlusDF(bddManager, f, opCode, assoc); 00231 } 00232 CalBddNot(result, result); 00233 userResult = CalBddGetExternalBdd(bddManager, result); 00234 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00235 Cal_BddFree(bddManager, userResult); 00236 Cal_BddManagerGC(bddManager); 00237 return (Cal_Bdd) 0; 00238 } 00239 return userResult; 00240 } 00241 return (Cal_Bdd) 0; 00242 }
| EXTERN 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 }
| EXTERN void Cal_BddFunctionPrint | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | userBdd, | |||
| char * | name | |||
| ) |
Function********************************************************************
Synopsis [Prints the function implemented by the argument BDD]
Description [Prints the function implemented by the argument BDD]
SideEffects [None]
Definition at line 128 of file calUtil.c.
00130 { 00131 Cal_Bdd_t calBdd; 00132 calBdd = CalBddGetInternalBdd(bddManager, userBdd); 00133 CalBddFunctionPrint(bddManager, calBdd, name); 00134 }
| EXTERN void Cal_BddFunctionProfile | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| long * | funcCounts | |||
| ) |
Function********************************************************************
Synopsis [Returns a "function profile" for f.]
Description [The nth entry of the function profile array is the number of subfunctions of f which may be obtained by restricting the variables whose index is less than n. An entry of zero indicates that f is independent of the variable with the corresponding index.]
SideEffects []
SeeAlso [optional]
Definition at line 257 of file calBddSize.c.
00259 { 00260 long i; 00261 Cal_BddIndex_t j; 00262 CalHashTable_t *h; 00263 Cal_Bdd_t f; 00264 00265 /* The number of subfunctions obtainable by restricting the */ 00266 /* variables of index < n is the number of subfunctions whose top */ 00267 /* variable has index n plus the number of subfunctions obtainable */ 00268 /* by restricting the variables of index < n+1 minus the number of */ 00269 /* these latter subfunctions whose highest reference is by a node at */ 00270 /* level n. */ 00271 /* The strategy will be to start with the number of subfunctions */ 00272 /* whose top variable has index n. We compute the highest level at */ 00273 /* which each subfunction is referenced. Then we work bottom up; at */ 00274 /* level n we add in the result from level n+1 and subtract the */ 00275 /* number of subfunctions whose highest reference is at level n. */ 00276 00277 Cal_BddProfile(bddManager, fUserBdd, funcCounts, 0); 00278 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00279 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00280 /* Encode the profile. The low bit of a count will be zero for */ 00281 /* those levels where f actually has a node. */ 00282 for(j = 0; j < bddManager->numVars; ++j){ 00283 if(!funcCounts[j]){ 00284 funcCounts[j] = 1; 00285 } 00286 else{ 00287 funcCounts[j] <<= 1; 00288 } 00289 } 00290 h = CalHashTableOneInit(bddManager, sizeof(int)); 00291 /* For each subfunction in f, compute the highest level where it is */ 00292 /* referenced. f itself is conceptually referenced at the highest */ 00293 /* possible level, which we represent by -1. */ 00294 i = -1; 00295 CalHashTableOneInsert(h, f, (char *)&i); 00296 BddHighestRefStep(bddManager, f, h); 00297 /* Walk through these results. For each subfunction, decrement the */ 00298 /* count at the highest level where it is referenced. */ 00299 BddDominatedStep(bddManager, f, funcCounts, h); 00300 CalHashTableOneQuit(h); 00301 /* Now add each level n+1 result to that of level n. */ 00302 for(i = bddManager->numVars-1, j = i+1; i>= 0; --i){ 00303 if(funcCounts[i] != 1){ 00304 funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j]; 00305 j = i; 00306 } 00307 else{ 00308 funcCounts[i] = 0; 00309 } 00310 } 00311 } 00312 }
| EXTERN void Cal_BddFunctionProfileMultiple | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | fUserBddArray, | |||
| long * | funcCounts | |||
| ) |
Function********************************************************************
Synopsis [Returns a "function profile" for fArray.]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 326 of file calBddSize.c.
00328 { 00329 long i; 00330 Cal_BddIndex_t j; 00331 Cal_Bdd_t *f, *fArray; 00332 CalHashTable_t *h; 00333 00334 CalBddArrayPreProcessing(bddManager, fUserBddArray); 00335 00336 for(i = 0; fUserBddArray[i]; ++i); 00337 00338 fArray = Cal_MemAlloc(Cal_Bdd_t, i+1); 00339 for (j=0; j < i; j++){ 00340 fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]); 00341 } 00342 fArray[j] = bddManager->bddNull; 00343 00344 /* See cmu_bdd_function_profile for the strategy involved here. */ 00345 Cal_BddProfileMultiple(bddManager, fUserBddArray, funcCounts, 0); 00346 for(j = 0; j < bddManager->numVars; ++j){ 00347 if(!funcCounts[j]){ 00348 funcCounts[j] = 1; 00349 } 00350 else{ 00351 funcCounts[j] <<= 1; 00352 } 00353 } 00354 h = CalHashTableOneInit(bddManager, sizeof(int)); 00355 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00356 BddHighestRefStep(bddManager, *f, h); 00357 } 00358 i = -1; 00359 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00360 CalHashTableOneInsert(h, *f, (char *)&i); 00361 } 00362 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00363 BddDominatedStep(bddManager, *f, funcCounts, h); 00364 } 00365 CalHashTableOneQuit(h); 00366 for(i = bddManager->numVars-1, j = i+1; i >= 0; --i){ 00367 if(funcCounts[i] != 1){ 00368 funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j]; 00369 j = i; 00370 } 00371 else{ 00372 funcCounts[i] = 0; 00373 } 00374 } 00375 Cal_MemFree(fArray); 00376 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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.]
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN int Cal_BddIsEqual | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | userBdd1, | |||
| Cal_Bdd | userBdd2 | |||
| ) |
AutomaticStart
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 []
| EXTERN int Cal_BddIsProvisional | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | userBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns 1, if the given user BDD contains provisional BDD node.]
Description [Returns 1, if the given user BDD contains provisional BDD node.]
SideEffects [None.]
SeeAlso []
Definition at line 344 of file calPipeline.c.
00345 { 00346 Cal_Bdd_t internalBdd = CalBddGetInternalBdd(bddManager, userBdd); 00347 return CalBddIsMarked(internalBdd); 00348 }
| EXTERN Cal_Bdd Cal_BddITE | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd, | |||
| Cal_Bdd | hUserBdd | |||
| ) |
CFile***********************************************************************
FileName [calBddITE.c]
PackageName [cal]
Synopsis [Routine for computing ITE of 3 BDD operands.]
Description []
SeeAlso [optional]
Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@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
- calBddITE.c,v 1.1.1.3 1998/05/04 00:58:51 hsv Exp
]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Returns the BDD for logical If-Then-Else
Description [Returns the BDD for the logical operation IF f THEN g ELSE h
- f g + f' h]
SideEffects [None]
SeeAlso [Cal_BddAnd, Cal_BddNand, Cal_BddOr, Cal_BddNor, Cal_BddXor, Cal_BddXnor]
Definition at line 88 of file calBddITE.c.
00090 { 00091 Cal_Bdd_t result; 00092 Cal_Bdd userResult; 00093 Cal_Bdd_t F, G, H; 00094 if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd)){ 00095 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00096 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00097 H = CalBddGetInternalBdd(bddManager, hUserBdd); 00098 result = CalBddOpITEBF(bddManager, F, G, H); 00099 } 00100 else { 00101 return (Cal_Bdd) 0; 00102 } 00103 userResult = CalBddGetExternalBdd(bddManager, result); 00104 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00105 Cal_BddFree(bddManager, userResult); 00106 Cal_BddManagerGC(bddManager); 00107 return (Cal_Bdd) 0; 00108 } 00109 return userResult; 00110 }
| EXTERN Cal_Bdd Cal_BddManagerCreateNewVarAfter | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | userBdd | |||
| ) |
Function********************************************************************
Synopsis [Creates and returns a new variable after the specified one in the variable order.]
Description [Creates and returns a new variable after the specified one in the variable order.]
SideEffects [None]
Definition at line 488 of file calBddManager.c.
00490 { 00491 Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd); 00492 if (CalBddIsBddConst(calBdd)){ 00493 return Cal_BddManagerCreateNewVarLast(bddManager); 00494 } 00495 else{ 00496 return CalBddGetExternalBdd(bddManager, 00497 CalBddManagerCreateNewVar(bddManager, 00498 CalBddGetBddIndex(bddManager, calBdd)+1)); 00499 } 00500 }
| EXTERN Cal_Bdd Cal_BddManagerCreateNewVarBefore | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | userBdd | |||
| ) |
Function********************************************************************
Synopsis [Creates and returns a new variable before the specified one in the variable order.]
Description [Creates and returns a new variable before the specified one in the variable order.]
SideEffects [None]
Definition at line 461 of file calBddManager.c.
00463 { 00464 Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd); 00465 if (CalBddIsBddConst(calBdd)){ 00466 return Cal_BddManagerCreateNewVarLast(bddManager); 00467 } 00468 else{ 00469 return CalBddGetExternalBdd(bddManager, 00470 CalBddManagerCreateNewVar(bddManager, 00471 CalBddGetBddIndex(bddManager, 00472 calBdd))); 00473 } 00474 }
| EXTERN Cal_Bdd Cal_BddManagerCreateNewVarFirst | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Creates and returns a new variable at the start of the variable order.]
Description [Creates and returns a new variable at the start of the variable order.]
SideEffects [None]
Definition at line 421 of file calBddManager.c.
00422 { 00423 return CalBddGetExternalBdd(bddManager, CalBddManagerCreateNewVar(bddManager, 00424 (Cal_BddIndex_t)0)); 00425 }
| EXTERN Cal_Bdd Cal_BddManagerCreateNewVarLast | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Creates and returns a new variable at the end of the variable order.]
Description [Creates and returns a new variable at the end of the variable order.]
SideEffects [None]
Definition at line 439 of file calBddManager.c.
00440 { 00441 return CalBddGetExternalBdd(bddManager, 00442 CalBddManagerCreateNewVar(bddManager, 00443 (Cal_BddIndex_t) 00444 bddManager->numVars)); 00445 }
| EXTERN int Cal_BddManagerGC | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Invokes the garbage collection at the manager level.]
Description [For each variable in the increasing id free nodes with reference count equal to zero freeing a node results in decrementing reference count of then and else nodes by one.]
SideEffects [None.]
Definition at line 110 of file calGC.c.
00111 { 00112 Cal_BddIndex_t index; 00113 Cal_BddId_t id; 00114 int numNodesFreed; 00115 /* unsigned long origNodes = bddManager->numNodes; */ 00116 00117 if (bddManager->numPeakNodes < (bddManager->numNodes + 00118 bddManager->numForwardedNodes)){ 00119 bddManager->numPeakNodes = bddManager->numNodes + 00120 bddManager->numForwardedNodes ; 00121 } 00122 00123 CalHashTableGC(bddManager, bddManager->uniqueTable[0]); 00124 for(index = 0; index < bddManager->numVars; index++){ 00125 id = bddManager->indexToId[index]; 00126 numNodesFreed = CalHashTableGC(bddManager, bddManager->uniqueTable[id]); 00127 bddManager->numNodes -= numNodesFreed; 00128 bddManager->numNodesFreed += numNodesFreed; 00129 } 00130 /* Free the cache entries related to unused BDD nodes */ 00131 /* The assumption is that during CalHashTableGC, the freed BDD nodes 00132 are marked. However, since they are not touched after being put 00133 on the free list, the mark should be unaffected and can be used 00134 for cleaning up the cache table. 00135 */ 00136 CalCacheTableTwoGCFlush(bddManager->cacheTable); 00137 bddManager->numGC++; 00138 return 0; 00139 }
| EXTERN void* Cal_BddManagerGetHooks | ( | Cal_BddManager | bddManager | ) |
| EXTERN unsigned long Cal_BddManagerGetNumNodes | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Returns the number of BDD nodes]
Description [Returns the number of BDD nodes]
SideEffects [None]
SeeAlso [Cal_BddTotalSize]
Definition at line 402 of file calBddManager.c.
00403 { 00404 return bddManager->numNodes; 00405 }
| EXTERN Cal_Bdd Cal_BddManagerGetVarWithId | ( | Cal_BddManager | bddManager, | |
| Cal_BddId_t | id | |||
| ) |
Function********************************************************************
Synopsis [Returns the variable with the specified id, null if no such variable exists]
Description [Returns the variable with the specified id, null if no such variable exists]
SideEffects [None]
SeeAlso [optional]
Definition at line 539 of file calBddManager.c.
00540 { 00541 if (id <= 0 || id > bddManager->numVars){ 00542 CalBddWarningMessage("Id out of range"); 00543 return (Cal_Bdd) 0; 00544 } 00545 return CalBddGetExternalBdd(bddManager, bddManager->varBdds[id]); 00546 }
| EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex | ( | Cal_BddManager | bddManager, | |
| Cal_BddIndex_t | index | |||
| ) |
Function********************************************************************
Synopsis [Returns the variable with the specified index, null if no such variable exists]
Description [Returns the variable with the specified index, null if no such variable exists]
SideEffects [None]
Definition at line 515 of file calBddManager.c.
00516 { 00517 if (index >= bddManager->numVars){ 00518 CalBddWarningMessage("Index out of range"); 00519 return (Cal_Bdd) 0; 00520 } 00521 return CalBddGetExternalBdd(bddManager, 00522 bddManager->varBdds[bddManager->indexToId[index]]); 00523 }
| EXTERN Cal_BddManager Cal_BddManagerInit | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Creates and initializes a new BDD manager.]
Description [Initializes and allocates fields of the BDD manager. Some of the fields are initialized for maxNumVars+1 or numVars+1, whereas some of them are initialized for maxNumVars or numVars. The first kind of fields are associated with the id of a variable and the second ones are with the index of the variable.]
SideEffects [None]
SeeAlso [Cal_BddManagerQuit]
Definition at line 152 of file calBddManager.c.
00153 { 00154 Cal_BddManager_t *bddManager; 00155 int i; 00156 CalBddNode_t *bddNode; 00157 Cal_Bdd_t resultBdd; 00158 00159 00160 bddManager = Cal_MemAlloc(Cal_BddManager_t, 1); 00161 00162 bddManager->numVars = 0; 00163 00164 bddManager->maxNumVars = 30; 00165 00166 bddManager->varBdds = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1); 00167 00168 bddManager->pageManager1 = CalPageManagerInit(4); 00169 bddManager->pageManager2 = CalPageManagerInit(NUM_PAGES_PER_SEGMENT); 00170 00171 bddManager->nodeManagerArray = Cal_MemAlloc(CalNodeManager_t*, bddManager->maxNumVars+1); 00172 00173 bddManager->nodeManagerArray[0] = CalNodeManagerInit(bddManager->pageManager1); 00174 bddManager->uniqueTable = Cal_MemAlloc(CalHashTable_t *, 00175 bddManager->maxNumVars+1); 00176 bddManager->uniqueTable[0] = CalHashTableInit(bddManager, 0); 00177 00178 /* Constant One */ 00179 CalBddPutBddId(bddManager->bddOne, CAL_BDD_CONST_ID); 00180 CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode); 00181 CalBddPutBddNode(bddManager->bddOne, bddNode); 00182 /* ~0x0 put so that the node is not mistaken for forwarded node */ 00183 CalBddPutThenBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0); 00184 CalBddPutElseBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0); 00185 CalBddPutRefCount(bddManager->bddOne, CAL_MAX_REF_COUNT); 00186 CalBddNot(bddManager->bddOne, bddManager->bddZero); 00187 00188 /* Create a user BDD */ 00189 CalHashTableAddDirectAux(bddManager->uniqueTable[0], bddManager->bddOne, 00190 bddManager->bddOne, &resultBdd); 00191 CalBddPutRefCount(resultBdd, CAL_MAX_REF_COUNT); 00192 bddManager->userOneBdd = CalBddGetBddNode(resultBdd); 00193 bddManager->userZeroBdd = CalBddNodeNot(bddManager->userOneBdd); 00194 00195 /* Null BDD */ 00196 CalBddPutBddId(bddManager->bddNull, CAL_BDD_NULL_ID); 00197 CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode); 00198 CalBddPutBddNode(bddManager->bddNull, bddNode); 00199 /* ~0x10 put so that the node is not mistaken for forwarded node or 00200 the constant nodes. */ 00201 CalBddPutThenBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10); 00202 CalBddPutElseBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10); 00203 CalBddPutRefCount(bddManager->bddNull, CAL_MAX_REF_COUNT); 00204 /* Put in the unique table, so that it gets locked */ 00205 /*CalHashTableAddDirect(bddManager->uniqueTable[0], bddNode);*/ 00206 00207 bddManager->indexToId = Cal_MemAlloc(Cal_BddId_t, bddManager->maxNumVars); 00208 bddManager->idToIndex = Cal_MemAlloc(Cal_BddIndex_t, bddManager->maxNumVars+1); 00209 bddManager->idToIndex[CAL_BDD_CONST_ID] = CAL_BDD_CONST_INDEX; 00210 00211 bddManager->depth = DEFAULT_DEPTH; 00212 bddManager->maxDepth = DEFAULT_MAX_DEPTH; 00213 bddManager->pipelineState = READY; 00214 bddManager->pipelineDepth = PIPELINE_EXECUTION_DEPTH; 00215 bddManager->currentPipelineDepth = 0; 00216 bddManager->pipelineFn = CalOpAnd; 00217 00218 00219 bddManager->reqQue = Cal_MemAlloc(CalHashTable_t **, bddManager->maxDepth); 00220 bddManager->cacheTable = CalCacheTableTwoInit(bddManager); 00221 00222 for (i=0; i < bddManager->maxDepth; i++){ 00223 bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, 00224 bddManager->maxNumVars+1); 00225 bddManager->reqQue[i][0] = CalHashTableInit(bddManager, 0); 00226 } 00227 00228 bddManager->requestNodeListArray = Cal_MemAlloc(CalRequestNode_t*, 00229 MAX_INSERT_DEPTH); 00230 for(i = 0; i < MAX_INSERT_DEPTH; i++){ 00231 bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t); 00232 } 00233 bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t); 00234 00235 /* Garbage collection related information */ 00236 bddManager->numNodes = bddManager->numPeakNodes = 1; 00237 bddManager->numNodesFreed = 0; 00238 bddManager->gcCheck = CAL_GC_CHECK; 00239 bddManager->uniqueTableGCLimit = CAL_MIN_GC_LIMIT; 00240 bddManager->numGC = 0; 00241 bddManager->gcMode = 1; 00242 bddManager->nodeLimit = 0; 00243 bddManager->overflow = 0; 00244 bddManager->repackAfterGCThreshold = CAL_REPACK_AFTER_GC_THRESHOLD; 00245 00246 00247 /* Special functions */ 00248 bddManager->TransformFn = BddDefaultTransformFn; 00249 bddManager->transformEnv = 0; 00250 00251 00252 /* Association related information */ 00253 bddManager->associationList = Cal_Nil(CalAssociation_t); 00254 /*bddManager->tempAssociation = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/ 00255 bddManager->tempAssociation = Cal_MemAlloc(CalAssociation_t, 1); 00256 bddManager->tempAssociation->id = -1; 00257 bddManager->tempAssociation->lastBddIndex = -1; 00258 bddManager->tempAssociation->varAssociation = 00259 Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1); 00260 for(i = 0; i < bddManager->maxNumVars+1; i++){ 00261 bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull; 00262 } 00263 bddManager->tempOpCode = -1; 00264 bddManager->currentAssociation = bddManager->tempAssociation; 00265 00266 /* BDD reordering related information */ 00267 bddManager->dynamicReorderingEnableFlag = 1; 00268 bddManager->reorderMethod = CAL_REORDER_METHOD_DF; 00269 bddManager->reorderTechnique = CAL_REORDER_NONE; 00270 bddManager->numForwardedNodes = 0; 00271 bddManager->numReorderings = 0; 00272 bddManager->maxNumVarsSiftedPerReordering = 1000; 00273 bddManager->maxNumSwapsPerReordering = 2000000; 00274 bddManager->numSwaps = 0; 00275 bddManager->numTrivialSwaps = 0; 00276 bddManager->maxSiftingGrowth = 2.0; 00277 bddManager->reorderingThreshold = CAL_BDD_REORDER_THRESHOLD; 00278 bddManager->maxForwardedNodes = CAL_NUM_FORWARDED_NODES_LIMIT; 00279 bddManager->tableRepackThreshold = CAL_TABLE_REPACK_THRESHOLD; 00280 00281 00282 /*bddManager->superBlock = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/ 00283 bddManager->superBlock = Cal_MemAlloc(Cal_Block_t, 1); 00284 bddManager->superBlock->numChildren=0; 00285 bddManager->superBlock->children=0; 00286 bddManager->superBlock->reorderable=1; 00287 bddManager->superBlock->firstIndex= -1; 00288 bddManager->superBlock->lastIndex=0; 00289 00290 bddManager->hooks = Cal_Nil(void); 00291 00292 return bddManager; 00293 }
| EXTERN int Cal_BddManagerQuit | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Frees the BDD manager and all the associated allocations]
Description [Frees the BDD manager and all the associated allocations]
SideEffects [None]
SeeAlso [Cal_BddManagerInit]
Definition at line 307 of file calBddManager.c.
00308 { 00309 int i, j; 00310 00311 if(bddManager == Cal_Nil(Cal_BddManager_t)) return 1; 00312 00313 for (i=0; i < bddManager->maxDepth; i++){ 00314 for (j=0; j <= bddManager->numVars; j++){ 00315 CalHashTableQuit(bddManager, bddManager->reqQue[i][j]); 00316 } 00317 Cal_MemFree(bddManager->reqQue[i]); 00318 } 00319 00320 for (i=0; i <= bddManager->numVars; i++){ 00321 CalHashTableQuit(bddManager, bddManager->uniqueTable[i]); 00322 CalNodeManagerQuit(bddManager->nodeManagerArray[i]); 00323 } 00324 00325 CalCacheTableTwoQuit(bddManager->cacheTable); 00326 Cal_MemFree(bddManager->tempAssociation->varAssociation); 00327 /*CAL_BDD_FREE_REC(bddManager, bddManager->tempAssociation, CalAssociation_t);*/ 00328 Cal_MemFree(bddManager->tempAssociation); 00329 /*CAL_BDD_FREE_REC(bddManager, bddManager->superBlock, Cal_Block_t);*/ 00330 CalFreeBlockRecursively(bddManager->superBlock); 00331 CalAssociationListFree(bddManager); 00332 Cal_MemFree(bddManager->varBdds); 00333 Cal_MemFree(bddManager->indexToId); 00334 Cal_MemFree(bddManager->idToIndex); 00335 Cal_MemFree(bddManager->uniqueTable); 00336 Cal_MemFree(bddManager->reqQue); 00337 Cal_MemFree(bddManager->requestNodeListArray); 00338 Cal_MemFree(bddManager->nodeManagerArray); 00339 CalPageManagerQuit(bddManager->pageManager1); 00340 CalPageManagerQuit(bddManager->pageManager2); 00341 Cal_MemFree(bddManager); 00342 00343 return 0; 00344 }
| EXTERN void Cal_BddManagerSetGCLimit | ( | Cal_BddManager | manager | ) |
Function********************************************************************
Synopsis [Sets the limit of the garbage collection.]
Description [It tries to set the limit at twice the number of nodes in the manager at the current point. However, the limit is not allowed to fall below the MIN_GC_LIMIT or to exceed the value of node limit (if one exists).]
SideEffects [None.]
Definition at line 154 of file calGC.c.
00155 { 00156 manager->uniqueTableGCLimit = ((manager->numNodes) << 1); 00157 if(manager->uniqueTableGCLimit < CAL_MIN_GC_LIMIT){ 00158 manager->uniqueTableGCLimit = CAL_MIN_GC_LIMIT; 00159 } 00160 if (manager->nodeLimit && (manager->uniqueTableGCLimit > 00161 manager->nodeLimit)){ 00162 manager->uniqueTableGCLimit = manager->nodeLimit; 00163 } 00164 }
| EXTERN 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 }
| EXTERN void Cal_BddManagerSetParameters | ( | Cal_BddManager | bddManager, | |
| long | reorderingThreshold, | |||
| long | maxForwardedNodes, | |||
| double | repackAfterGCThreshold, | |||
| double | tableRepackThreshold | |||
| ) |
Function********************************************************************
Synopsis [Sets appropriate fields of BDD Manager.]
Description [This function is used to set the parameters which are used to control the reordering process. "reorderingThreshold" determines the number of nodes below which reordering will NOT be invoked, "maxForwardedNodes" determines the maximum number of forwarded nodes which are allowed (at that point the cleanup must be done), and "repackingThreshold" determines the fraction of the page utilized below which repacking has to be invoked. These parameters have different effect on the computational and memory usage aspects of reordeing. For instance, higher value of "maxForwardedNodes" will result in process consuming more memory, and a lower value on the other hand would invoke the cleanup process repeatedly resulting in increased computation.]
SideEffects [Sets appropriate fields of BDD Manager]
SeeAlso []
Definition at line 369 of file calBddManager.c.
00374 { 00375 if (reorderingThreshold >= 0){ 00376 bddManager->reorderingThreshold = reorderingThreshold; 00377 } 00378 if (maxForwardedNodes >= 0){ 00379 bddManager->maxForwardedNodes = maxForwardedNodes; 00380 } 00381 if (repackAfterGCThreshold >= 0.0){ 00382 bddManager->repackAfterGCThreshold = (float) repackAfterGCThreshold; 00383 } 00384 if (tableRepackThreshold >= 0.0){ 00385 bddManager->tableRepackThreshold = (float) tableRepackThreshold; 00386 } 00387 }
| EXTERN Cal_Bdd Cal_BddMultiwayAnd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBddArray | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical AND of argument BDDs]
Description [Returns the BDD for logical AND of set of BDDs in the bddArray]
SideEffects [None]
Definition at line 448 of file calBddOp.c.
00449 { 00450 int i, numBdds = 0; 00451 Cal_Bdd_t result; 00452 Cal_Bdd_t *calBddArray; 00453 Cal_Bdd userBdd; 00454 00455 for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){ 00456 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){ 00457 return (Cal_Bdd) 0; 00458 } 00459 } 00460 00461 if (numBdds == 0){ 00462 CalBddWarningMessage("Multiway AND called with 0 length array"); 00463 return (Cal_Bdd) 0; 00464 } 00465 else if (numBdds == 1){ 00466 return Cal_BddIdentity(bddManager, userBddArray[0]); 00467 } 00468 else{ 00469 calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1); 00470 for (i = 0; i < numBdds; i++){ 00471 calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]); 00472 } 00473 result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpAnd); 00474 Cal_MemFree(calBddArray); 00475 } 00476 return CalBddGetExternalBdd(bddManager, result); 00477 }
| EXTERN Cal_Bdd Cal_BddMultiwayOr | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBddArray | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical OR of argument BDDs]
Description [Returns the BDD for logical OR of set of BDDs in the bddArray]
SideEffects [None]
Definition at line 489 of file calBddOp.c.
00490 { 00491 int i, numBdds = 0; 00492 Cal_Bdd_t result; 00493 Cal_Bdd_t *calBddArray; 00494 Cal_Bdd userBdd; 00495 00496 for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){ 00497 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){ 00498 return (Cal_Bdd) 0; 00499 } 00500 } 00501 00502 if (numBdds == 0){ 00503 CalBddWarningMessage("Multiway OR called with 0 length array"); 00504 return (Cal_Bdd) 0; 00505 } 00506 else if (numBdds == 1){ 00507 return Cal_BddIdentity(bddManager, userBddArray[0]); 00508 } 00509 else{ 00510 calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1); 00511 for (i = 0; i < numBdds; i++){ 00512 calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]); 00513 } 00514 result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpOr); 00515 Cal_MemFree(calBddArray); 00516 } 00517 return CalBddGetExternalBdd(bddManager, result); 00518 }
| EXTERN Cal_Bdd Cal_BddMultiwayXor | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBddArray | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical XOR of argument BDDs]
Description [Returns the BDD for logical XOR of set of BDDs in the bddArray]
SideEffects [None]
Definition at line 530 of file calBddOp.c.
00531 { 00532 int i, numBdds = 0; 00533 Cal_Bdd_t result; 00534 Cal_Bdd_t *calBddArray; 00535 Cal_Bdd userBdd; 00536 00537 for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){ 00538 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){ 00539 return (Cal_Bdd) 0; 00540 } 00541 } 00542 00543 if (numBdds == 0){ 00544 CalBddWarningMessage("Multiway OR called with 0 length array"); 00545 return (Cal_Bdd) 0; 00546 } 00547 else if (numBdds == 1){ 00548 return Cal_BddIdentity(bddManager, userBddArray[0]); 00549 } 00550 else{ 00551 calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1); 00552 for (i = 0; i < numBdds; i++){ 00553 calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]); 00554 } 00555 result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpXor); 00556 Cal_MemFree(calBddArray); 00557 } 00558 return CalBddGetExternalBdd(bddManager, result); 00559 }
| EXTERN Cal_Bdd Cal_BddNand | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical NAND of argument BDDs]
Description [Returns the BDD for logical NAND of f and g]
SideEffects [None]
Definition at line 126 of file calBddOp.c.
00130 { 00131 Cal_Bdd_t result; 00132 Cal_Bdd_t F, G; 00133 Cal_Bdd userResult; 00134 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00135 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00136 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00137 result = CalBddOpBF(bddManager, CalOpNand, F, G); 00138 } 00139 else{ 00140 return (Cal_Bdd) 0; 00141 } 00142 userResult = CalBddGetExternalBdd(bddManager, result); 00143 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00144 Cal_BddFree(bddManager, userResult); 00145 Cal_BddManagerGC(bddManager); 00146 return (Cal_Bdd) 0; 00147 } 00148 return userResult; 00149 }
| EXTERN Cal_Block Cal_BddNewVarBlock | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | variable, | |||
| long | length | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Creates and returns a variable block used for controlling dynamic reordering.]
Description [The block is specified by passing the first variable and the length of the block. The "length" number of consecutive variables starting from "variable" are put in the block.]
SideEffects [A new block is created.]
SeeAlso []
Definition at line 89 of file calBlk.c.
00090 { 00091 Cal_Block b; 00092 Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, variable); 00093 00094 if (CalBddTypeAux(bddManager, calBdd) != CAL_BDD_TYPE_POSVAR) { 00095 CalBddWarningMessage("Cal_BddNewVarBlock: second argument is not a positive variable\n"); 00096 if (CalBddIsBddConst(calBdd)){ 00097 return (Cal_Block) 0; 00098 } 00099 } 00100 00101 /*b = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/ 00102 b = Cal_MemAlloc(Cal_Block_t, 1); 00103 b->reorderable = 0; 00104 b->firstIndex = bddManager->idToIndex[calBdd.bddId]; 00105 if (length <= 0) { 00106 CalBddWarningMessage("Cal_BddNewVarBlock: invalid final argument"); 00107 length = 1; 00108 } 00109 b->lastIndex = b->firstIndex + length - 1; 00110 if (b->lastIndex >= bddManager->numVars) { 00111 CalBddWarningMessage("Cal_BddNewVarBlock: range covers non-existent variables"); 00112 b->lastIndex = bddManager->numVars - 1; 00113 } 00114 AddBlock(bddManager->superBlock, b); 00115 return (b); 00116 }
| EXTERN 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 }
| EXTERN Cal_Bdd Cal_BddNor | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical NOR of argument BDDs]
Description [Returns the BDD for logical NOR of f and g]
SideEffects [None]
Definition at line 195 of file calBddOp.c.
00198 { 00199 Cal_Bdd_t result; 00200 Cal_Bdd userResult; 00201 Cal_Bdd_t F, G; 00202 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00203 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00204 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00205 result = CalBddOpBF(bddManager, CalOpOr, F, G); 00206 CalBddNot(result, result); 00207 } 00208 else{ 00209 return (Cal_Bdd) 0; 00210 } 00211 userResult = CalBddGetExternalBdd(bddManager, result); 00212 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00213 Cal_BddFree(bddManager, userResult); 00214 Cal_BddManagerGC(bddManager); 00215 return (Cal_Bdd) 0; 00216 } 00217 return userResult; 00218 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN Cal_Bdd Cal_BddOr | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical OR of argument BDDs]
Description [Returns the BDD for logical OR of f and g]
SideEffects [None]
Definition at line 161 of file calBddOp.c.
00164 { 00165 Cal_Bdd_t result; 00166 Cal_Bdd_t F, G; 00167 Cal_Bdd userResult; 00168 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00169 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00170 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00171 result = CalBddOpBF(bddManager, CalOpOr, F, G); 00172 } 00173 else{ 00174 return (Cal_Bdd) 0; 00175 } 00176 userResult = CalBddGetExternalBdd(bddManager, result); 00177 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00178 Cal_BddFree(bddManager, userResult); 00179 Cal_BddManagerGC(bddManager); 00180 return (Cal_Bdd) 0; 00181 } 00182 return userResult; 00183 }
| EXTERN 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]
| EXTERN Cal_Bdd* Cal_BddPairwiseAnd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBddArray | |||
| ) |
Function********************************************************************
Synopsis [Returns an array of BDDs obtained by logical AND of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]
Description [Returns an array of BDDs obtained by logical AND of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]
SideEffects [None]
SeeAlso [Cal_BddPairwiseOr]
Definition at line 303 of file calBddOp.c.
00304 { 00305 int i, num; 00306 Cal_Bdd_t *bddArray; 00307 Cal_Bdd_t *resultArray; 00308 Cal_Bdd userBdd; 00309 Cal_Bdd *userResultArray; 00310 00311 for (num = 0; (userBdd = userBddArray[num]); num++){ 00312 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){ 00313 return Cal_Nil(Cal_Bdd); 00314 } 00315 } 00316 if ((num == 0) || (num%2 != 0)){ 00317 fprintf(stdout,"Odd number of arguments passed to array AND\n"); 00318 return Cal_Nil(Cal_Bdd); 00319 } 00320 bddArray = Cal_MemAlloc(Cal_Bdd_t, num); 00321 for (i = 0; i < num; i++){ 00322 bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]); 00323 } 00324 resultArray = BddArrayOpBF(bddManager, bddArray, num, CalOpAnd); 00325 userResultArray = Cal_MemAlloc(Cal_Bdd, num/2); 00326 for (i=0; i<num/2; i++){ 00327 userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]); 00328 } 00329 Cal_MemFree(bddArray); 00330 Cal_MemFree(resultArray); 00331 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00332 for (i=0; i<num/2; i++){ 00333 Cal_BddFree(bddManager, userResultArray[i]); 00334 userResultArray[i] = (Cal_Bdd) 0; 00335 } 00336 Cal_BddManagerGC(bddManager); 00337 return userResultArray; 00338 } 00339 return userResultArray; 00340 }
| EXTERN Cal_Bdd* Cal_BddPairwiseOr | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBddArray | |||
| ) |
Function********************************************************************
Synopsis [Returns an array of BDDs obtained by logical OR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]
Description [Returns an array of BDDs obtained by logical OR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]
SideEffects [None]
SeeAlso [Cal_BddPairwiseAnd]
Definition at line 358 of file calBddOp.c.
00359 { 00360 int i, num=0; 00361 Cal_Bdd_t *bddArray; 00362 Cal_Bdd_t *resultArray; 00363 Cal_Bdd userBdd; 00364 Cal_Bdd *userResultArray; 00365 00366 for (num = 0; (userBdd = userBddArray[num]); num++){ 00367 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){ 00368 return Cal_Nil(Cal_Bdd); 00369 } 00370 } 00371 if ((num == 0) || (num%2 != 0)){ 00372 fprintf(stdout,"Odd number of arguments passed to array OR\n"); 00373 return Cal_Nil(Cal_Bdd); 00374 } 00375 bddArray = Cal_MemAlloc(Cal_Bdd_t, num); 00376 for (i = 0; i < num; i++){ 00377 bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]); 00378 } 00379 resultArray = BddArrayOpBF(bddManager, bddArray, num, CalOpOr); 00380 userResultArray = Cal_MemAlloc(Cal_Bdd, num/2); 00381 for (i=0; i<num/2; i++){ 00382 userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]); 00383 } 00384 Cal_MemFree(bddArray); 00385 Cal_MemFree(resultArray); 00386 return userResultArray; 00387 }
| EXTERN Cal_Bdd* Cal_BddPairwiseXor | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBddArray | |||
| ) |
Function********************************************************************
Synopsis [Returns an array of BDDs obtained by logical XOR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]
Description [Returns an array of BDDs obtained by logical XOR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]
SideEffects [None]
SeeAlso [Cal_BddPairwiseAnd]
Definition at line 405 of file calBddOp.c.
00406 { 00407 int i, num=0; 00408 Cal_Bdd_t *bddArray; 00409 Cal_Bdd_t *resultArray; 00410 Cal_Bdd userBdd; 00411 Cal_Bdd *userResultArray; 00412 00413 for (num = 0; (userBdd = userBddArray[num]); num++){ 00414 if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){ 00415 return Cal_Nil(Cal_Bdd); 00416 } 00417 } 00418 if ((num == 0) || (num%2 != 0)){ 00419 fprintf(stdout,"Odd number of arguments passed to array OR\n"); 00420 return Cal_Nil(Cal_Bdd); 00421 } 00422 bddArray = Cal_MemAlloc(Cal_Bdd_t, num); 00423 for (i = 0; i < num; i++){ 00424 bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]); 00425 } 00426 resultArray = BddArrayOpBF(bddManager, bddArray, num, CalOpXor); 00427 userResultArray = Cal_MemAlloc(Cal_Bdd, num/2); 00428 for (i=0; i<num/2; i++){ 00429 userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]); 00430 } 00431 Cal_MemFree(bddArray); 00432 Cal_MemFree(resultArray); 00433 return userResultArray; 00434 }
| EXTERN void Cal_BddPrintBdd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_VarNamingFn_t | VarNamingFn, | |||
| Cal_TerminalIdFn_t | TerminalIdFn, | |||
| Cal_Pointer_t | env, | |||
| FILE * | fp | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints a BDD in the human readable form.]
Description [Prints a human-readable representation of the BDD f to the file given by fp. The namingFn should be a pointer to a function taking a bddManager, a BDD and the pointer given by env. This function should return either a null pointer or a srting that is the name of the supplied variable. If it returns a null pointer, a default name is generated based on the index of the variable. It is also legal for naminFN to e null; in this case, default names are generated for all variables. The macro bddNamingFnNone is a null pointer of suitable type. terminalIdFn should be apointer to a function taking a bddManager and two longs. plus the pointer given by the env. It should return either a null pointer. If it returns a null pointer, or if terminalIdFn is null, then default names are generated for the terminals. The macro bddTerminalIdFnNone is a null pointer of suitable type.]
SideEffects [None.]
Definition at line 111 of file calPrint.c.
00115 { 00116 long next; 00117 CalHashTable_t *hashTable; 00118 00119 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager,fUserBdd); 00120 CalBddMarkSharedNodes(bddManager, f); 00121 hashTable = CalHashTableOneInit(bddManager, sizeof(long)); 00122 next = 0; 00123 CalBddNumberSharedNodes(bddManager, f, hashTable, &next); 00124 BddPrintBddStep(bddManager, f, VarNamingFn, TerminalIdFn, env, fp, 00125 hashTable, 0); 00126 CalHashTableOneQuit(hashTable); 00127 }
| EXTERN void Cal_BddPrintFunctionProfile | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | f, | |||
| Cal_VarNamingFn_t | varNamingProc, | |||
| char * | env, | |||
| int | lineLength, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Cal_BddPrintFunctionProfile is like Cal_BddPrintProfile except it displays a function profile for f]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 161 of file calPrintProfile.c.
00167 { 00168 long *levelCounts; 00169 if (CalBddPreProcessing(bddManager, 1, f)){ 00170 return; 00171 } 00172 levelCounts = Cal_MemAlloc(long, bddManager->numVars+1); 00173 Cal_BddFunctionProfile(bddManager, f, levelCounts); 00174 CalBddPrintProfileAux(bddManager, levelCounts, varNamingProc, env, 00175 lineLength, fp); 00176 Cal_MemFree(levelCounts); 00177 }
| EXTERN void Cal_BddPrintFunctionProfileMultiple | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBdds, | |||
| Cal_VarNamingFn_t | varNamingProc, | |||
| char * | env, | |||
| int | lineLength, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Cal_BddPrintFunctionProfileMultiple is like Cal_BddPrintFunctionProfile except for multiple BDDs]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 193 of file calPrintProfile.c.
00199 { 00200 long *levelCounts; 00201 if (CalBddArrayPreProcessing(bddManager, userBdds) == 0){ 00202 return; 00203 } 00204 levelCounts = Cal_MemAlloc(long, bddManager->numVars+1); 00205 Cal_BddFunctionProfileMultiple(bddManager, userBdds, levelCounts); 00206 CalBddPrintProfileAux(bddManager, levelCounts, varNamingProc, env, lineLength, fp); 00207 Cal_MemFree(levelCounts); 00208 }
| EXTERN void Cal_BddPrintProfile | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_VarNamingFn_t | varNamingProc, | |||
| char * | env, | |||
| int | lineLength, | |||
| FILE * | fp | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Displays the node profile for f on fp. lineLength specifies the maximum line length. varNamingFn is as in Cal_BddPrintBdd.]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 95 of file calPrintProfile.c.
00101 { 00102 long *levelCounts; 00103 00104 if (CalBddPreProcessing(bddManager, 1, fUserBdd) == 0){ 00105 return; 00106 } 00107 levelCounts = Cal_MemAlloc(long, bddManager->numVars+1); 00108 Cal_BddProfile(bddManager, fUserBdd, levelCounts, 1); 00109 CalBddPrintProfileAux(bddManager, levelCounts, varNamingProc, env, 00110 lineLength, fp); 00111 Cal_MemFree(levelCounts); 00112 }
| EXTERN void Cal_BddPrintProfileMultiple | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userBdds, | |||
| Cal_VarNamingFn_t | varNamingProc, | |||
| char * | env, | |||
| int | lineLength, | |||
| FILE * | fp | |||
| ) |
Function********************************************************************
Synopsis [Cal_BddPrintProfileMultiple is like Cal_BddPrintProfile except it displays the profile for a set of BDDs]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 127 of file calPrintProfile.c.
00134 { 00135 long *levelCounts; 00136 00137 if (CalBddArrayPreProcessing(bddManager, userBdds) == 0){ 00138 return; 00139 } 00140 levelCounts = Cal_MemAlloc(long, bddManager->numVars+1); 00141 Cal_BddProfileMultiple(bddManager, userBdds, levelCounts, 1); 00142 CalBddPrintProfileAux(bddManager, levelCounts, varNamingProc, env, lineLength, fp); 00143 Cal_MemFree(levelCounts); 00144 }
| EXTERN void Cal_BddProfile | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| long * | levelCounts, | |||
| int | negout | |||
| ) |
Function********************************************************************
Synopsis [Returns a "node profile" of f, i.e., the number of nodes at each level in f.]
Description [negout is as in Cal_BddSize. levelCounts should be an array of size Cal_BddVars(bddManager)+1 to hold the profile.]
SideEffects [None]
SeeAlso [optional]
Definition at line 180 of file calBddSize.c.
00182 { 00183 Cal_BddIndex_t i; 00184 Cal_Bdd_t f, g; 00185 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00186 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00187 for(i = 0; i <= bddManager->numVars; i++){ 00188 levelCounts[i] = 0l; 00189 } 00190 g = CalBddOne(bddManager); 00191 CalBddPutMark(g, 0); 00192 BddMarkBdd(f); 00193 BddProfileStep(bddManager, f, levelCounts, countingFns[!negout]); 00194 } 00195 }
| EXTERN void Cal_BddProfileMultiple | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | fUserBddArray, | |||
| long * | levelCounts, | |||
| int | negout | |||
| ) |
Function********************************************************************
Synopsis []
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 210 of file calBddSize.c.
00212 { 00213 Cal_Bdd_t *f, *fArray; 00214 Cal_Bdd_t g; 00215 int i, j; 00216 00217 CalBddArrayPreProcessing(bddManager, fUserBddArray); 00218 00219 for(i = 0; fUserBddArray[i]; ++i); 00220 00221 fArray = Cal_MemAlloc(Cal_Bdd_t, i+1); 00222 for (j=0; j < i; j++){ 00223 fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]); 00224 } 00225 fArray[j] = bddManager->bddNull; 00226 00227 for(i = 0; i <= bddManager->numVars; i++){ 00228 levelCounts[i] = 0l; 00229 } 00230 g = CalBddOne(bddManager); 00231 CalBddPutMark(g, 0); 00232 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00233 BddMarkBdd(*f); 00234 } 00235 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00236 BddProfileStep(bddManager, *f, levelCounts, countingFns[!negout]); 00237 } 00238 Cal_MemFree(fArray); 00239 }
| EXTERN Cal_Bdd Cal_BddReduce | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | cUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns a BDD which agrees with f for all valuations which satisfy c.]
Description [Returns a BDD which agrees with f for all valuations which satisfy c. The result is usually smaller in terms of number of BDD nodes than f. This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step.]
SideEffects [None]
SeeAlso [Cal_BddCofactor]
Definition at line 138 of file calReduce.c.
00140 { 00141 if (CalBddPreProcessing(bddManager, 2, fUserBdd, cUserBdd)){ 00142 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00143 Cal_Bdd_t c = CalBddGetInternalBdd(bddManager, cUserBdd); 00144 Cal_Bdd_t result; 00145 Cal_Bdd userResult; 00146 00147 result = BddReduceBF(bddManager, CalOpCofactor, f, c); 00148 userResult = CalBddGetExternalBdd(bddManager, result); 00149 00150 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00151 Cal_BddFree(bddManager, userResult); 00152 Cal_BddManagerGC(bddManager); 00153 return (Cal_Bdd) 0; 00154 } 00155 if (Cal_BddSize(bddManager, userResult, 1) < 00156 Cal_BddSize(bddManager, fUserBdd, 1)){ 00157 return userResult; 00158 } 00159 else{ 00160 Cal_BddFree(bddManager, userResult); 00161 return Cal_BddIdentity(bddManager, fUserBdd); 00162 } 00163 } 00164 return (Cal_Bdd) 0; 00165 }
| EXTERN Cal_Bdd Cal_BddRelProd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the result of taking the logical AND of the argument BDDs and existentially quantifying some variables from the product.]
Description [Returns the BDD for the logical AND of f and g with all the variables that are paired with something in the current variable association existentially quantified out.]
SideEffects [None.]
Definition at line 159 of file calQuant.c.
00160 { 00161 Cal_Bdd_t result; 00162 Cal_Bdd userResult; 00163 00164 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00165 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00166 Cal_Bdd_t g = CalBddGetInternalBdd(bddManager, gUserBdd); 00167 CalAssociation_t *assoc = bddManager->currentAssociation; 00168 unsigned short opCode; 00169 00170 if (bddManager->currentAssociation->id == -1){ 00171 opCode = bddManager->tempOpCode--; 00172 bddManager->tempOpCode--; 00173 } 00174 else { 00175 opCode = CAL_OP_REL_PROD + assoc->id; 00176 } 00177 if (bddManager->numNodes <= CAL_LARGE_BDD){ 00178 /* If number of nodes is small, call depth first routine. */ 00179 result = BddRelProdStep(bddManager, f, g, opCode, assoc); 00180 } 00181 else { 00182 result = BddRelProdBFPlusDF(bddManager, f, g, opCode, assoc); 00183 } 00184 userResult = CalBddGetExternalBdd(bddManager, result); 00185 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00186 Cal_BddFree(bddManager, userResult); 00187 Cal_BddManagerGC(bddManager); 00188 return (Cal_Bdd) 0; 00189 } 00190 return userResult; 00191 } 00192 return (Cal_Bdd) 0; 00193 }
| EXTERN 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 }
| EXTERN Cal_Bdd Cal_BddSatisfy | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Name [Cal_BddSatisfy]
Synopsis [Returns a BDD which implies f, true for some valuation on which f is true, and which has at most one node at each level]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 97 of file calBddSatisfy.c.
00098 { 00099 Cal_Bdd_t f; 00100 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00101 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00102 if(CalBddIsBddZero(bddManager, f)){ 00103 CalBddWarningMessage("Cal_BddSatisfy: argument is false"); 00104 return (fUserBdd); 00105 } 00106 f = BddSatisfyStep(bddManager, f); 00107 return CalBddGetExternalBdd(bddManager, f); 00108 } 00109 return (Cal_Bdd) 0; 00110 }
| EXTERN double Cal_BddSatisfyingFraction | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the fraction of valuations which make f true. (Note that this fraction is independent of whatever set of variables f is supposed to be a function of)]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 179 of file calBddSatisfy.c.
00180 { 00181 double fraction; 00182 CalHashTable_t *hashTable; 00183 Cal_Bdd_t f; 00184 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00185 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00186 hashTable = CalHashTableOneInit(bddManager, sizeof(double)); 00187 fraction = BddSatisfyingFractionStep(bddManager, f, hashTable); 00188 CalHashTableOneQuit(hashTable); 00189 return fraction; 00190 } 00191 return 0.0; 00192 }
| EXTERN Cal_Bdd Cal_BddSatisfySupport | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
Function********************************************************************
Name [Cal_BddSatisfySupport]
Synopsis [Returns a special cube contained in f.]
Description [The returned BDD which implies f, is true for some valuation on which f is true, which has at most one node at each level, and which has exactly one node corresponding to each variable which is associated with something in the current variable association.]
SideEffects [required]
SeeAlso [optional]
Definition at line 131 of file calBddSatisfy.c.
00132 { 00133 Cal_BddId_t *support, *p; 00134 long i; 00135 Cal_Bdd_t result; 00136 Cal_Bdd_t f; 00137 00138 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00139 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00140 if(CalBddIsBddZero(bddManager, f)){ 00141 CalBddWarningMessage("Cal_BddSatisfySupport: argument is false"); 00142 return (fUserBdd); 00143 } 00144 support = Cal_MemAlloc(Cal_BddId_t, bddManager->numVars+1); 00145 for(i = 1, p = support; i <= bddManager->numVars; i++){ 00146 if(!CalBddIsBddNull(bddManager, 00147 bddManager->currentAssociation->varAssociation[i])){ 00148 *p = bddManager->idToIndex[i]; 00149 ++p; 00150 } 00151 } 00152 *p = 0; 00153 qsort(support, (unsigned)(p - support), sizeof(Cal_BddId_t), IndexCmp); 00154 while(p != support){ 00155 --p; 00156 *p = bddManager->indexToId[*p]; 00157 } 00158 result = BddSatisfySupportStep(bddManager, f, support); 00159 Cal_MemFree(support); 00160 return CalBddGetExternalBdd(bddManager, result); 00161 } 00162 return (Cal_Bdd) 0; 00163 }
| EXTERN void Cal_BddSetGCMode | ( | Cal_BddManager | bddManager, | |
| int | gcMode | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.]
Description [Sets the garbage collection mode, 0 means the garbage collection should be turned off, 1 means garbage collection should be on.]
SideEffects [None.]
Definition at line 90 of file calGC.c.
00093 { 00094 bddManager->gcMode = gcMode; 00095 }
| EXTERN long Cal_BddSize | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| int | negout | |||
| ) |
Function********************************************************************
Synopsis [Returns the number of nodes in f when negout is nonzero. If negout is zero, we pretend that the BDDs don't have negative-output pointers.]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 104 of file calBddSize.c.
00105 { 00106 Cal_Bdd_t f, g; 00107 00108 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00109 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00110 g = CalBddOne(bddManager); 00111 CalBddPutMark(g, 0); 00112 BddMarkBdd(f); 00113 return BddSizeStep(f, countingFns[!negout]); 00114 } 00115 return (0l); 00116 }
| EXTERN long Cal_BddSizeMultiple | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | fUserBddArray, | |||
| int | negout | |||
| ) |
Function********************************************************************
Synopsis [The routine is like Cal_BddSize, but takes a null-terminated array of BDDs and accounts for sharing of nodes.]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 132 of file calBddSize.c.
00134 { 00135 long size; 00136 Cal_Bdd_t *f; 00137 Cal_Bdd_t g; 00138 Cal_Bdd_t *fArray; 00139 int i, j; 00140 00141 if (CalBddArrayPreProcessing(bddManager, fUserBddArray) == 0){ 00142 return -1; 00143 } 00144 00145 for(i = 0; fUserBddArray[i]; ++i); 00146 00147 fArray = Cal_MemAlloc(Cal_Bdd_t, i+1); 00148 for (j=0; j < i; j++){ 00149 fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]); 00150 } 00151 fArray[j] = bddManager->bddNull; 00152 00153 g = CalBddOne(bddManager); 00154 CalBddPutMark(g, 0); 00155 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00156 BddMarkBdd(*f); 00157 } 00158 size = 0l; 00159 for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){ 00160 size += BddSizeStep(*f, countingFns[!negout]); 00161 } 00162 Cal_MemFree(fArray); 00163 return size; 00164 }
| EXTERN 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 }
| EXTERN Cal_Bdd Cal_BddSubstitute | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Substitute a set of variables by functions]
Description [Returns a BDD for f using the substitution defined by current variable association. Each variable is replaced by its associated BDDs. The substitution is effective simultaneously]
SideEffects [None]
SeeAlso [Cal_BddCompose]
Definition at line 93 of file calBddSubstitute.c.
00094 { 00095 CalRequest_t result; 00096 int bddId, bddIndex, lastIndex; 00097 CalHashTable_t *hashTable; 00098 CalHashTable_t *uniqueTableForId; 00099 CalHashTable_t **reqQueForSubstitute = bddManager->reqQue[0]; 00100 CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 00101 Cal_Bdd_t f; 00102 00103 if (CalBddPreProcessing(bddManager, 1, fUserBdd) == 0){ 00104 return (Cal_Bdd) 0; 00105 } 00106 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00107 if(CalBddIsBddConst(f)){ 00108 return CalBddGetExternalBdd(bddManager, f); 00109 } 00110 00111 CalHashTableFindOrAdd(reqQueForSubstitute[CalBddGetBddId(f)], f, 00112 bddManager->bddNull, &result); 00113 00114 /* ReqQueApply */ 00115 lastIndex = bddManager->currentAssociation->lastBddIndex; 00116 for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){ 00117 bddId = bddManager->indexToId[bddIndex]; 00118 hashTable = reqQueForSubstitute[bddId]; 00119 if(hashTable->numEntries){ 00120 CalHashTableSubstituteApply(bddManager, hashTable, lastIndex, 00121 reqQueForSubstitute); 00122 } 00123 } 00124 00125 /* ReqQueReduce */ 00126 for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){ 00127 bddId = bddManager->indexToId[bddIndex]; 00128 uniqueTableForId = bddManager->uniqueTable[bddId]; 00129 hashTable = reqQueForSubstitute[bddId]; 00130 if(hashTable->numEntries){ 00131 CalHashTableSubstituteReduce(bddManager, hashTable, 00132 reqQueForITE, uniqueTableForId); 00133 } 00134 } 00135 00136 CalRequestIsForwardedTo(result); 00137 00138 /* ReqQueCleanUp */ 00139 for(bddId = 1; bddId <= bddManager->numVars; bddId++){ 00140 CalHashTableCleanUp(reqQueForSubstitute[bddId]); 00141 } 00142 00143 return CalBddGetExternalBdd(bddManager, result); 00144 }
| EXTERN void Cal_BddSupport | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd * | support | |||
| ) |
AutomaticEnd Function********************************************************************
Name [Cal_BddSupport]
Synopsis [returns the support of f as a null-terminated array of variables]
Description [optional]
SideEffects [None]
SeeAlso [optional]
Definition at line 92 of file calBddSupport.c.
00094 { 00095 if(CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00096 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00097 Cal_Bdd_t *internalSupport = Cal_MemAlloc(Cal_Bdd_t, bddManager->numVars+1); 00098 Cal_Bdd_t *end; 00099 int i = 0; 00100 end = CalBddSupportStep(bddManager, f, internalSupport); 00101 *end = CalBddNull(bddManager); 00102 CalBddUnmarkNodes(bddManager, f); 00103 while (CalBddIsBddNull(bddManager, internalSupport[i]) == 0){ 00104 *support = CalBddGetExternalBdd(bddManager, internalSupport[i]); 00105 support++; 00106 i++; 00107 } 00108 Cal_MemFree(internalSupport); 00109 } 00110 *support = (Cal_Bdd) 0; 00111 }
| EXTERN Cal_Bdd Cal_BddSwapVars | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd, | |||
| Cal_Bdd | hUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Return a function obtained by swapping two variables]
Description [Returns the BDD obtained by simultaneously substituting variable g by variable h and variable h and variable g in the BDD f]
SideEffects [None]
SeeAlso [Cal_BddSubstitute]
Definition at line 92 of file calBddSwapVars.c.
00095 { 00096 Cal_Bdd_t f,g,h,tmpBdd; 00097 Cal_BddIndex_t gIndex, hIndex; 00098 CalRequest_t result; 00099 int bddId, bddIndex; 00100 CalHashTable_t *hashTable; 00101 CalHashTable_t *uniqueTableForId; 00102 CalHashTable_t **reqQueForSwapVars = bddManager->reqQue[0]; 00103 CalHashTable_t **reqQueForSwapVarsPlus = bddManager->reqQue[1]; 00104 CalHashTable_t **reqQueForSwapVarsMinus = bddManager->reqQue[2]; 00105 CalHashTable_t **reqQueForCompose = bddManager->reqQue[3]; 00106 CalHashTable_t **reqQueForITE = bddManager->reqQue[4]; 00107 00108 if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd) == 0){ 00109 return (Cal_Bdd) 0; 00110 } 00111 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00112 g = CalBddGetInternalBdd(bddManager, gUserBdd); 00113 h = CalBddGetInternalBdd(bddManager, hUserBdd); 00114 00115 if(CalBddIsBddConst(g) || CalBddIsBddConst(h)){ 00116 CalBddWarningMessage("Unacceptable arguments for Cal_BddSwapVars"); 00117 return (Cal_Bdd) 0; 00118 } 00119 if(CalBddIsEqual(g, h)){ 00120 /* 00121 CalBddIcrRefCount(f); 00122 */ 00123 return CalBddGetExternalBdd(bddManager, f); 00124 } 00125 if(CalBddGetBddIndex(bddManager, g) > CalBddGetBddIndex(bddManager, h)){ 00126 tmpBdd = g; 00127 g = h; 00128 h = tmpBdd; 00129 } 00130 00131 gIndex = CalBddGetBddIndex(bddManager, g); 00132 hIndex = CalBddGetBddIndex(bddManager, h); 00133 00134 CalBddGetMinId2(bddManager, f, g, bddId); 00135 CalHashTableFindOrAdd(reqQueForSwapVars[bddId], f, 00136 bddManager->bddNull, &result); 00137 00138 /* ReqQueApply */ 00139 for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){ 00140 bddId = bddManager->indexToId[bddIndex]; 00141 hashTable = reqQueForSwapVars[bddId]; 00142 if(hashTable->numEntries){ 00143 CalHashTableSwapVarsApply(bddManager, hashTable, gIndex, hIndex, 00144 reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus, 00145 reqQueForCompose, reqQueForITE); 00146 } 00147 hashTable = reqQueForSwapVarsPlus[bddId]; 00148 if(hashTable->numEntries){ 00149 CalHashTableSwapVarsPlusApply(bddManager, hashTable, hIndex, 00150 reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus, 00151 reqQueForCompose); 00152 } 00153 hashTable = reqQueForSwapVarsMinus[bddId]; 00154 if(hashTable->numEntries){ 00155 CalHashTableSwapVarsMinusApply(bddManager, hashTable, hIndex, 00156 reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus, 00157 reqQueForCompose); 00158 } 00159 hashTable = reqQueForCompose[bddId]; 00160 if(hashTable->numEntries){ 00161 CalHashTableComposeApply(bddManager, hashTable, hIndex, 00162 reqQueForCompose, reqQueForITE); 00163 } 00164 hashTable = reqQueForITE[bddId]; 00165 if(hashTable->numEntries){ 00166 CalHashTableITEApply(bddManager, hashTable, reqQueForITE); 00167 } 00168 } 00169 00170 /* ReqQueReduce */ 00171 for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){ 00172 bddId = bddManager->indexToId[bddIndex]; 00173 uniqueTableForId = bddManager->uniqueTable[bddId]; 00174 hashTable = reqQueForSwapVars[bddId]; 00175 if(hashTable->numEntries){ 00176 CalHashTableReduce(bddManager, hashTable, uniqueTableForId); 00177 } 00178 hashTable = reqQueForSwapVarsPlus[bddId]; 00179 if(hashTable->numEntries){ 00180 CalHashTableReduce(bddManager, hashTable, uniqueTableForId); 00181 } 00182 hashTable = reqQueForSwapVarsMinus[bddId]; 00183 if(hashTable->numEntries){ 00184 CalHashTableReduce(bddManager, hashTable, uniqueTableForId); 00185 } 00186 hashTable = reqQueForCompose[bddId]; 00187 if(hashTable->numEntries){ 00188 CalHashTableReduce(bddManager, hashTable, uniqueTableForId); 00189 } 00190 hashTable = reqQueForITE[bddId]; 00191 if(hashTable->numEntries){ 00192 CalHashTableReduce(bddManager, hashTable, uniqueTableForId); 00193 } 00194 } 00195 00196 CalRequestIsForwardedTo(result); 00197 00198 /* ReqQueCleanUp */ 00199 for(bddId = 1; bddId <= bddManager->numVars; bddId++){ 00200 CalHashTableCleanUp(reqQueForSwapVars[bddId]); 00201 CalHashTableCleanUp(reqQueForSwapVarsPlus[bddId]); 00202 CalHashTableCleanUp(reqQueForSwapVarsMinus[bddId]); 00203 CalHashTableCleanUp(reqQueForCompose[bddId]); 00204 CalHashTableCleanUp(reqQueForITE[bddId]); 00205 } 00206 return CalBddGetExternalBdd(bddManager, result); 00207 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN 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 }
| EXTERN Cal_Bdd Cal_BddUndumpBdd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | userVars, | |||
| FILE * | fp, | |||
| int * | error | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Reads a BDD from a file]
Description [Loads an encoded description of a BDD from the file given by fp. The argument vars should be a null terminated array of variables that will become the support of the BDD. As in Cal_BddDumpBdd, these need not be in the order of increasing index. If the same array of variables in used in dumping and undumping, the BDD returned will be equal to the one that was dumped. More generally, if array v1 is used when dumping, and the array v2 is used when undumping, the BDD returned will be equal to the original BDD with the ith variable in v2 substituted for the ith variable in v1 for all i. Null BDD is returned in the operation fails for reason (node limit reached, I/O error, invalid file format, etc.). In this case, an error code is stored in error. the code will be one of the following. CAL_BDD_UNDUMP_FORMAT Invalid file format CAL_BDD_UNDUMP_OVERFLOW Node limit exceeded CAL_BDD_UNDUMP_IOERROR File I/O error CAL_BDD_UNDUMP_EOF Unexpected EOF]
SideEffects [required]
SeeAlso [optional]
Definition at line 121 of file calDump.c.
00126 { 00127 long i,j; 00128 Cal_BddIndex_t numberVars; 00129 long numberShared; 00130 int indexSize; 00131 int nodeNumberSize; 00132 Cal_Bdd_t *shared; 00133 long sharedSoFar; 00134 Cal_Bdd_t v; 00135 Cal_Bdd_t result; 00136 Cal_Bdd_t *vars; 00137 00138 *error = 0; 00139 for(i = 0; userVars[i]; ++i){ 00140 if(Cal_BddType(bddManager, userVars[i]) != CAL_BDD_TYPE_POSVAR){ 00141 CalBddWarningMessage("Cal_BddUndumpBdd: support is not all positive variables"); 00142 return (Cal_Bdd) 0; 00143 } 00144 } 00145 vars = Cal_MemAlloc(Cal_Bdd_t, i); 00146 for (j=0; j < i; j++){ 00147 vars[j] = CalBddGetInternalBdd(bddManager,userVars[j]); 00148 } 00149 00150 if(Read(error, sizeof(long), fp) != MAGIC_COOKIE){ 00151 if(!*error){ 00152 *error = CAL_BDD_UNDUMP_FORMAT; 00153 } 00154 Cal_MemFree(vars); 00155 return (Cal_Bdd) 0; 00156 } 00157 numberVars = Read(error, sizeof(Cal_BddIndex_t), fp); 00158 if(*error){ 00159 Cal_MemFree(vars); 00160 return (Cal_Bdd) 0; 00161 } 00162 if(numberVars != i){ 00163 *error = CAL_BDD_UNDUMP_FORMAT; 00164 Cal_MemFree(vars); 00165 return (Cal_Bdd) 0; 00166 } 00167 numberShared = Read(error, sizeof(long), fp); 00168 if(*error){ 00169 Cal_MemFree(vars); 00170 return (Cal_Bdd) 0; 00171 } 00172 indexSize = BytesNeeded(numberVars+1); 00173 nodeNumberSize = BytesNeeded(numberShared); 00174 if(numberShared < 0){ 00175 *error = CAL_BDD_UNDUMP_FORMAT; 00176 Cal_MemFree(vars); 00177 return (Cal_Bdd) 0; 00178 } 00179 shared = Cal_MemAlloc(Cal_Bdd_t, numberShared); 00180 for(i = 0; i < numberShared; ++i){ 00181 shared[i] = CalBddNull(bddManager); 00182 } 00183 sharedSoFar = 0; 00184 result = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared, 00185 numberShared, &sharedSoFar, indexSize, nodeNumberSize, error); 00186 Cal_MemFree(vars); 00187 00188 for(i = 0; i < numberShared; ++i){ 00189 v = shared[i]; 00190 if(!CalBddIsBddNull(bddManager, v)){ 00191 CalBddFree(v); 00192 } 00193 } 00194 if(!*error && sharedSoFar != numberShared){ 00195 *error = CAL_BDD_UNDUMP_FORMAT; 00196 } 00197 Cal_MemFree(shared); 00198 if(*error){ 00199 if(!CalBddIsBddNull(bddManager, result)){ 00200 CalBddFree(result); 00201 } 00202 return (Cal_Bdd) 0; 00203 } 00204 /* 00205 * Decrement the reference count of result by 1. Since it has 00206 * already been incremented in BddUndumpBddStep. 00207 */ 00208 CalBddDcrRefCount(result); 00209 return CalBddGetExternalBdd(bddManager, result); 00210 }
| EXTERN 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 }
| EXTERN void Cal_BddVarBlockReorderable | ( | Cal_BddManager | bddManager, | |
| Cal_Block | block, | |||
| int | reorderable | |||
| ) |
Function********************************************************************
Synopsis [Sets the reoderability of a particular block.]
Description [If a block is reorderable, the child blocks are recursively involved in swapping.]
SideEffects [None.]
SeeAlso []
Definition at line 130 of file calBlk.c.
00132 { 00133 block->reorderable = reorderable; 00134 }
| EXTERN long Cal_BddVars | ( | Cal_BddManager | bddManager | ) |
| EXTERN Cal_Bdd Cal_BddVarSubstitute | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Substitute a set of variables by set of another variables.]
Description [Returns a BDD for f using the substitution defined by current variable association. It is assumed that each variable is replaced by another variable. For the substitution of a variable by a function, use Cal_BddSubstitute instead.]
SideEffects [None]
SeeAlso [Cal_BddSubstitute]
Definition at line 93 of file calBddVarSubstitute.c.
00094 { 00095 CalRequest_t result; 00096 Cal_Bdd userResult; 00097 00098 if (CalBddPreProcessing(bddManager, 1, fUserBdd)){ 00099 Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd); 00100 CalAssociation_t *assoc = bddManager->currentAssociation; 00101 unsigned short opCode; 00102 if (assoc->id == -1){ 00103 opCode = bddManager->tempOpCode--; 00104 } 00105 else { 00106 opCode = CAL_OP_VAR_SUBSTITUTE + assoc->id; 00107 } 00108 result = CalBddVarSubstitute(bddManager, f, opCode, assoc); 00109 userResult = CalBddGetExternalBdd(bddManager, result); 00110 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00111 Cal_BddFree(bddManager, userResult); 00112 Cal_BddManagerGC(bddManager); 00113 return (Cal_Bdd) 0; 00114 } 00115 return userResult; 00116 } 00117 return (Cal_Bdd) 0; 00118 }
| EXTERN Cal_Bdd Cal_BddXnor | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical exclusive NOR of argument BDDs]
Description [Returns the BDD for logical exclusive NOR of f and g]
SideEffects [None]
Definition at line 264 of file calBddOp.c.
00265 { 00266 Cal_Bdd_t result; 00267 Cal_Bdd userResult; 00268 Cal_Bdd_t F, G; 00269 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00270 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00271 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00272 result = CalBddOpBF(bddManager, CalOpXor, F, G); 00273 CalBddNot(result, result); 00274 } 00275 else{ 00276 return (Cal_Bdd) 0; 00277 } 00278 userResult = CalBddGetExternalBdd(bddManager, result); 00279 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00280 Cal_BddFree(bddManager, userResult); 00281 Cal_BddManagerGC(bddManager); 00282 return (Cal_Bdd) 0; 00283 } 00284 return userResult; 00285 }
| EXTERN Cal_Bdd Cal_BddXor | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Returns the BDD for logical exclusive OR of argument BDDs]
Description [Returns the BDD for logical exclusive OR of f and g]
SideEffects [None]
Definition at line 230 of file calBddOp.c.
00233 { 00234 Cal_Bdd_t result; 00235 Cal_Bdd userResult; 00236 Cal_Bdd_t F, G; 00237 if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){ 00238 F = CalBddGetInternalBdd(bddManager, fUserBdd); 00239 G = CalBddGetInternalBdd(bddManager, gUserBdd); 00240 result = CalBddOpBF(bddManager, CalOpXor, F, G); 00241 } 00242 else{ 00243 return (Cal_Bdd) 0; 00244 } 00245 userResult = CalBddGetExternalBdd(bddManager, result); 00246 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00247 Cal_BddFree(bddManager, userResult); 00248 Cal_BddManagerGC(bddManager); 00249 return (Cal_Bdd) 0; 00250 } 00251 return userResult; 00252 }
| EXTERN 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 }
| EXTERN void Cal_ImageDump | ( | Cal_BddManager_t * | bddManager, | |
| FILE * | fp | |||
| ) |
AutomaticStart AutomaticEnd
Definition at line 91 of file calUtil.c.
00092 { 00093 00094 CalPageManager_t *pageManager; 00095 int i, j; 00096 char *segment, c; 00097 int count = NUM_PAGES_PER_SEGMENT * PAGE_SIZE; 00098 00099 pageManager = bddManager->pageManager1; 00100 for(i = 0; i < pageManager->numSegments; i++){ 00101 segment = (char *) pageManager->pageSegmentArray[i]; 00102 for(j = 1; j <= count; j++){ 00103 c = segment[j]; 00104 fprintf(fp, "%c", j%64?c:'\n'); 00105 } 00106 } 00107 pageManager = bddManager->pageManager2; 00108 for(i = 0; i < pageManager->numSegments; i++){ 00109 segment = (char *) pageManager->pageSegmentArray[i]; 00110 for(j = 1; j <= count; j++){ 00111 c = segment[j]; 00112 fprintf(fp, "%c", j%64?c:'\n'); 00113 } 00114 } 00115 }
| EXTERN Cal_Address_t Cal_MemAllocation | ( | void | ) |
Function********************************************************************
Synopsis [Returns the memory allocated.]
Description [Returns the memory allocated.]
SideEffects [required]
SeeAlso [optional]
Definition at line 180 of file calMem.c.
00181 { 00182 return (blockAllocation); 00183 }
| EXTERN void Cal_MemFatal | ( | char * | message | ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints an error message and exits.]
Description [Prints an error message and exits.]
SideEffects [required]
SeeAlso [optional]
Definition at line 162 of file calMem.c.
00163 { 00164 fprintf(stderr, "Memory management library: error: %s\n", message); 00165 exit(1); 00166 }
| EXTERN void Cal_MemFreeBlock | ( | Cal_Pointer_t | p | ) |
Function********************************************************************
Synopsis [Frees the block.]
Description [Frees the block.]
SideEffects [required]
SeeAlso [optional]
Definition at line 277 of file calMem.c.
00278 { 00279 Block b; 00280 00281 if (!p) return; 00282 b = (Block) ((Cal_Address_t)p-HEADER_SIZE); 00283 if (!b->used) Cal_MemFatal("Cal_MemFreeBlock: block not in use"); 00284 if (b->sizeIndex < 0 || b->sizeIndex > MAX_SIZEINDEX) Cal_MemFatal("Cal_MemFreeBlock: invalid block header"); 00285 MergeAndFree(b); 00286 }
| EXTERN void Cal_MemFreeRec | ( | Cal_RecMgr | mgr, | |
| Cal_Pointer_t | rec | |||
| ) |
Function********************************************************************
Synopsis [Frees a record managed by the indicated record manager. ]
Description [Frees a record managed by the indicated record manager. ]
SideEffects [required]
SeeAlso [optional]
Definition at line 412 of file calMem.c.
00413 { 00414 #if defined(DEBUG_MEM) 00415 if (mgr->size >= sizeof(long)+sizeof(List_t)) 00416 if (*(long *)(sizeof(List_t)+(Cal_Address_t)rec) == MAGIC_COOKIE) 00417 fprintf(stderr, "record at 0x%lx may already be freed\n", (Cal_Address_t)rec); 00418 #endif 00419 ((List)rec)->next=mgr->free; 00420 #if defined(DEBUG_MEM) 00421 if (mgr->size >= sizeof(long)+sizeof(List_t)) 00422 *(long *)(sizeof(List_t)+(Cal_Address_t)rec)=MAGIC_COOKIE; 00423 #endif 00424 mgr->free=(List)rec; 00425 }
| EXTERN void Cal_MemFreeRecMgr | ( | Cal_RecMgr | mgr | ) |
Function********************************************************************
Synopsis [Frees all the storage associated with the specified record manager.]
Description [Frees all the storage associated with the specified record manager.]
SideEffects [required]
SeeAlso [optional]
Definition at line 470 of file calMem.c.
00471 { 00472 List p, q; 00473 for (p=mgr->blocks; p; p=q){ 00474 q=p->next; 00475 Cal_MemFreeBlock((Cal_Pointer_t)p); 00476 } 00477 Cal_MemFreeBlock((Cal_Pointer_t)mgr); 00478 }
| EXTERN Cal_Pointer_t Cal_MemGetBlock | ( | Cal_Address_t | size | ) |
Function********************************************************************
Synopsis [Allocates a new block of the specified size.]
Description [Allocates a new block of the specified size.]
SideEffects [required]
SeeAlso [optional]
Definition at line 197 of file calMem.c.
00198 { 00199 int i; 00200 int sizeIndex; 00201 int allocSizeIndex; 00202 int newSeg; 00203 Cal_Address_t allocSize; 00204 Cal_Pointer_t sbrkRet; 00205 Block b; 00206 00207 if ((sizeIndex = BlockSizeIndex(size)) < 0) return ((Cal_Pointer_t)0); 00208 00209 /* Find smallest free block which is large enough. */ 00210 for (i = sizeIndex; i <= MAX_SIZEINDEX && !avail[i]; ++i); 00211 if (i > MAX_SIZEINDEX) { 00212 /* We must get more storage; don't allocate less than */ 00213 /* 2^MIN_ALLOC_SIZE_INDEX */ 00214 if (sizeIndex < MIN_ALLOC_SIZEINDEX) allocSizeIndex=MIN_ALLOC_SIZEINDEX; 00215 else allocSizeIndex=sizeIndex; 00216 allocSize=((Cal_Address_t)1 << allocSizeIndex); 00217 00218 /* Pad current segment to be a multiple of 2^allocSizeIndex in */ 00219 /* length. */ 00220 allocSize += ((currSeg->limit + allocSize - 1) & 00221 ~(allocSize - 1)) - currSeg->limit; 00222 if ((sbrkRet=(Cal_Pointer_t)SBRK(0)) != 00223 (Cal_Pointer_t)((Cal_Address_t)currSeg->baseAddress+currSeg->limit) || 00224 allocSize+currSeg->limit > MAX_SEG_SIZE) { 00225 00226 /* Segment is too large or someone else has moved the break. */ 00227 /* Pad to get to appropriate boundary. */ 00228 allocSize=CAL_ROUNDUP((Cal_Address_t)sbrkRet)-(Cal_Address_t)sbrkRet; 00229 00230 /* Pad allocation request with storage for new segment */ 00231 /* information and indicate that a new segment must be */ 00232 /* created. */ 00233 allocSize+=((Cal_Address_t)1 << allocSizeIndex)+CAL_ROUNDUP(sizeof(Segment_t)); 00234 newSeg=1; 00235 } 00236 else newSeg=0; 00237 sbrkRet=(Cal_Pointer_t)SBRK(allocSize); 00238 if (sbrkRet == (Cal_Pointer_t) -1) Cal_MemFatal("Cal_MemGetBlock: allocation failed"); 00239 blockAllocation += allocSize; 00240 if (newSeg){ 00241 currSeg = (Segment) CAL_ROUNDUP((Cal_Address_t)sbrkRet); 00242 currSeg->baseAddress=(Cal_Pointer_t)((Cal_Address_t)currSeg+CAL_ROUNDUP(sizeof(Segment_t))); 00243 currSeg->limit=0; 00244 /* Readjust allocation size. */ 00245 allocSize=(1l << allocSizeIndex); 00246 } 00247 /* Carve allocated space up into blocks and add to free lists. */ 00248 while (allocSize){ 00249 size = allocSize - (allocSize & (allocSize-1)); 00250 b = (Block) ((Cal_Address_t)currSeg->baseAddress+currSeg->limit); 00251 b->sizeIndex = CeilingLog2(size); 00252 b->seg = currSeg; 00253 AddToFreeList(b); 00254 currSeg->limit += size; 00255 allocSize -= size; 00256 } 00257 /* Find free block of appropriate size. */ 00258 for (i=sizeIndex; i <= MAX_SIZEINDEX && !avail[i]; ++i); 00259 } 00260 b = RemoveFromFreeList(avail[i]); 00261 TrimToSize(b, sizeIndex); 00262 return ((Cal_Pointer_t)((Cal_Address_t)b + HEADER_SIZE)); 00263 }
| EXTERN Cal_Pointer_t Cal_MemNewRec | ( | Cal_RecMgr | mgr | ) |
Function********************************************************************
Synopsis [Allocates a record from the specified record manager. ]
Description [Allocates a record from the specified record manager. ]
SideEffects [required]
SeeAlso [optional]
Definition at line 355 of file calMem.c.
00356 { 00357 int i; 00358 Cal_Pointer_t p; 00359 List new_; 00360 00361 if (!mgr->free) { 00362 /* Allocate a new block. */ 00363 new_ = (List) Cal_MemGetBlock(ALLOC_SIZE); 00364 mgr->numBlocks++; 00365 new_->next=mgr->blocks; 00366 mgr->blocks=new_; 00367 mgr->free=(List)((Cal_Address_t)new_+CAL_ROUNDUP(sizeof(List_t))); 00368 p=(Cal_Pointer_t)(mgr->free); 00369 /* Carve the block into pieces. */ 00370 for (i=1; i < mgr->recsPerBlock; ++i) { 00371 ((List)p)->next=(List)((Cal_Address_t)p+mgr->size); 00372 #if defined(DEBUG_MEM) 00373 if (mgr->size >= sizeof(long)+sizeof(List_t)) 00374 *(long *)(sizeof(List_t)+(Cal_Address_t)p)=MAGIC_COOKIE; 00375 #endif 00376 p=(Cal_Pointer_t)((Cal_Address_t)p+mgr->size); 00377 } 00378 ((List)p)->next=0; 00379 #if defined(DEBUG_MEM) 00380 if (mgr->size >= sizeof(long)+sizeof(List_t)){ 00381 *(long *)(sizeof(List_t)+(Cal_Address_t)p)=MAGIC_COOKIE; 00382 } 00383 #endif 00384 } 00385 new_ = mgr->free; 00386 #if defined(DEBUG_MEM) 00387 if (mgr->size >= sizeof(long)+sizeof(List_t)){ 00388 if (*(long *)(sizeof(List_t)+(Cal_Address_t)new_) != MAGIC_COOKIE) 00389 fprintf(stderr, "record at 0x%lx may be in use\n", (Cal_Address_t)new_); 00390 else 00391 *(long *)(sizeof(struct 00392 list_)+(Cal_Address_t)new)=MAGIC_COOKIE1; 00393 } 00394 #endif 00395 mgr->free = mgr->free->next; 00396 return ((Cal_Pointer_t)new_); 00397 }
| EXTERN Cal_RecMgr Cal_MemNewRecMgr | ( | int | size | ) |
Function********************************************************************
Synopsis [Creates a new record manager with the given record size.]
Description [Creates a new record manager with the given record size.]
SideEffects [required]
SeeAlso [optional]
Definition at line 441 of file calMem.c.
00442 { 00443 Cal_RecMgr mgr; 00444 00445 if (size < sizeof(List_t)) size=sizeof(List_t); 00446 size=CAL_ROUNDUP(size); 00447 if (size > ALLOC_SIZE-CAL_ROUNDUP(sizeof(List_t))) 00448 Cal_MemFatal("Cal_MemNewRecMgr: record size too large"); 00449 mgr = (Cal_RecMgr)Cal_MemGetBlock((Cal_Address_t)sizeof(Cal_RecMgr_t)); 00450 mgr->size=size; 00451 mgr->recsPerBlock=(ALLOC_SIZE-CAL_ROUNDUP(sizeof(List_t)))/size; 00452 mgr->free=0; 00453 mgr->blocks=0; 00454 mgr->numBlocks = 0; 00455 return (mgr); 00456 }
| EXTERN Cal_Pointer_t Cal_MemResizeBlock | ( | Cal_Pointer_t | p, | |
| Cal_Address_t | newSize | |||
| ) |
Function********************************************************************
Synopsis [Expands or contracts the block to a new size. We try to avoid moving the block if possible. ]
Description [Expands or contracts the block to a new size. We try to avoid moving the block if possible. ]
SideEffects [required]
SeeAlso [optional]
Definition at line 304 of file calMem.c.
00305 { 00306 int newSizeIndex; 00307 Block b; 00308 Block bb; 00309 Cal_Pointer_t q; 00310 Cal_Address_t oldSize; 00311 00312 if (!p) return (Cal_MemGetBlock(newSize)); 00313 b = (Block) ((Cal_Address_t)p - HEADER_SIZE); 00314 if (!b->used) Cal_MemFatal("Cal_MemResizeBlock: block not in use"); 00315 if (b->sizeIndex < 0 || b->sizeIndex > MAX_SIZEINDEX){ 00316 Cal_MemFatal("Cal_MemResizeBlock: invalid block header"); 00317 } 00318 if ((newSizeIndex = BlockSizeIndex(newSize)) < 0){ 00319 Cal_MemFreeBlock(p); 00320 return ((Cal_Pointer_t)0); 00321 } 00322 if (b->sizeIndex >= newSizeIndex){ 00323 /* Shrink block. */ 00324 TrimToSize(b, newSizeIndex); 00325 return (p); 00326 } 00327 oldSize=(1l << b->sizeIndex) - HEADER_SIZE; 00328 /* Try to expand by adding buddies at higher addresses. */ 00329 for (bb=Buddy(b); 00330 bb && (Cal_Address_t)b < (Cal_Address_t)bb && !bb->used && bb->sizeIndex == b->sizeIndex; 00331 bb=Buddy(b)) { 00332 RemoveFromFreeList(bb); 00333 if (++(b->sizeIndex) == newSizeIndex) return (p); 00334 } 00335 /* Couldn't expand all the way to needed size; allocate a new block */ 00336 /* and move the contents of the old one. */ 00337 q = (Cal_Pointer_t) Cal_MemGetBlock(newSize); 00338 Cal_MemCopy(q, p, oldSize); 00339 MergeAndFree(b); 00340 return (q); 00341 }
| EXTERN int Cal_PerformanceTest | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | outputBddArray, | |||
| int | numFunctions, | |||
| int | iteration, | |||
| int | seed, | |||
| int | andPerformanceFlag, | |||
| int | multiwayPerformanceFlag, | |||
| int | onewayPerformanceFlag, | |||
| int | quantifyPerformanceFlag, | |||
| int | composePerformanceFlag, | |||
| int | relprodPerformanceFlag, | |||
| int | swapPerformanceFlag, | |||
| int | substitutePerformanceFlag, | |||
| int | sanityCheckFlag, | |||
| int | computeMemoryOverheadFlag, | |||
| int | superscalarFlag | |||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Main routine for testing performances of various routines.]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 114 of file calPerformanceTest.c.
00125 { 00126 00127 CalUtilSRandom((long)seed); 00128 00129 ITERATION = iteration; 00130 fprintf(stdout,"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"); 00131 fprintf(stdout, "Performing %d iterations for each function\n", iteration); 00132 Cal_BddSetGCMode(bddManager, 0); 00133 #ifdef QUANTIFY 00134 quantify_start_recording_data(); 00135 #endif 00136 00137 #ifdef PURECOV 00138 purecov_clear_data(); 00139 #endif 00140 00141 if (relprodPerformanceFlag){ 00142 CalPerformanceTestRelProd(bddManager, outputBddArray, numFunctions, 1, 1, 00143 1, 1); 00144 CalUtilSRandom((long)seed); 00145 00146 } 00147 if (sanityCheckFlag == 1){ 00148 CalQuantifySanityCheck(bddManager, outputBddArray, 00149 numFunctions); 00150 CalUtilSRandom((long)seed); 00151 } 00152 if (quantifyPerformanceFlag){ 00153 CalPerformanceTestQuantifyAllTogether(bddManager, outputBddArray, 00154 numFunctions, 1, 1, 1); 00155 CalUtilSRandom((long)seed); 00156 /* 00157 CalPerformanceTestNonSuperscalarQuant(bddManager, outputBddArray, numFunctions); 00158 CalUtilSRandom((long)seed); 00159 */ 00160 } 00161 00162 if (multiwayPerformanceFlag){ 00163 CalPerformanceTestMultiway(bddManager, outputBddArray, numFunctions); 00164 CalUtilSRandom((long)seed); 00165 } 00166 if (onewayPerformanceFlag){ 00167 CalPerformanceTestOneway(bddManager, outputBddArray, numFunctions); 00168 CalUtilSRandom((long)seed); 00169 } 00170 if (andPerformanceFlag){ 00171 CalPerformanceTestAnd(bddManager, outputBddArray, numFunctions); 00172 CalUtilSRandom((long)seed); 00173 } 00174 if (composePerformanceFlag){ 00175 CalPerformanceTestCompose(bddManager, outputBddArray, numFunctions); 00176 CalUtilSRandom((long)seed); 00177 } 00178 if (swapPerformanceFlag){ 00179 CalPerformanceTestSwapVars(bddManager, outputBddArray, numFunctions); 00180 CalUtilSRandom((long)seed); 00181 } 00182 if (substitutePerformanceFlag){ 00183 CalPerformanceTestSubstitute(bddManager, outputBddArray, numFunctions); 00184 CalUtilSRandom((long)seed); 00185 } 00186 #ifdef COMPUTE_MEMORY_OVERHEAD 00187 if (computeMemoryOverheadFlag){ 00188 CalPerformaceMemoryOverhead(bddManager, outputBddArray, numFunctions); 00189 CalUtilSRandom((long)seed); 00190 } 00191 #endif 00192 if (superscalarFlag){ 00193 CalPerformaceTestSuperscalar(bddManager, outputBddArray, numFunctions); 00194 CalUtilSRandom((long)seed); 00195 CalPerformanceTestNonSuperscalar(bddManager, outputBddArray, numFunctions); 00196 CalUtilSRandom((long)seed); 00197 } 00198 #ifdef QUANTIFY 00199 quantify_stop_recording_data(); 00200 #endif 00201 #ifdef PURECOV 00202 purecov_save_data(); 00203 purecov_disable_save(); 00204 #endif 00205 fprintf(stdout,"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"); 00206 Cal_BddSetGCMode(bddManager, 1); 00207 return 0; 00208 }
| EXTERN Cal_Bdd Cal_PipelineCreateProvisionalBdd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | fUserBdd, | |||
| Cal_Bdd | gUserBdd | |||
| ) |
Function********************************************************************
Synopsis [Create a provisional BDD in the pipeline.]
Description [The provisional BDD is automatically freed once the pipeline is quitted.]
SideEffects []
SeeAlso []
Definition at line 170 of file calPipeline.c.
00172 { 00173 int insertDepth, operandDepth; 00174 CalRequestNode_t *requestNode; 00175 Cal_Bdd_t provisionalBdd, f, g; 00176 Cal_BddId_t bddId; 00177 Cal_Bdd userNode; 00178 00179 insertDepth = 0; 00180 00181 f = CalBddGetInternalBdd(bddManager, fUserBdd); 00182 g = CalBddGetInternalBdd(bddManager, gUserBdd); 00183 if(bddManager->pipelineState != CREATE){ 00184 CalBddWarningMessage("Provisional Bdd not created: Pipeline is not initialized"); 00185 return (Cal_Bdd) 0; 00186 } 00187 if(CalBddIsMarked(f)){ 00188 CalBddGetDepth(f, operandDepth); 00189 if(insertDepth <= operandDepth){ 00190 insertDepth = operandDepth + 1; 00191 } 00192 } 00193 if(CalBddIsMarked(g)){ 00194 CalBddGetDepth(g, operandDepth); 00195 if(insertDepth <= operandDepth){ 00196 insertDepth = operandDepth + 1; 00197 } 00198 } 00199 if (bddManager->pipelineDepth <= insertDepth){ 00200 bddManager->pipelineDepth = insertDepth + 1; 00201 } 00202 if (insertDepth >= MAX_INSERT_DEPTH){ 00203 CalBddWarningMessage("Provisional Bdd not created"); 00204 CalBddWarningMessage("Maximum pipeline depth is reached"); 00205 return (Cal_Bdd) 0; 00206 } 00207 00208 CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode); 00209 CalRequestNodePutF(requestNode, f); 00210 CalRequestNodePutG(requestNode, g); 00211 CalRequestNodeMark(requestNode); 00212 CalRequestNodePutDepth(requestNode, insertDepth); 00213 CalRequestNodePutNextRequestNode(requestNode, 00214 bddManager->requestNodeListArray[insertDepth]); 00215 bddManager->requestNodeListArray[insertDepth] = requestNode; 00216 00217 CalBddGetMinId2(bddManager, f, g, bddId); 00218 CalBddPutBddId(provisionalBdd, bddId); 00219 CalBddPutBddNode(provisionalBdd, (CalBddNode_t *)requestNode); 00220 00221 CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], userNode); 00222 CalBddNodePutThenBdd(userNode, provisionalBdd); 00223 CalBddNodePutElseBdd(userNode, bddManager->bddOne); 00224 CalBddNodePutNextBddNode(userNode, 00225 bddManager->userProvisionalNodeList); 00226 bddManager->userProvisionalNodeList = userNode; 00227 CalBddNodeIcrRefCount(userNode); 00228 return userNode; 00229 }
| EXTERN int Cal_PipelineExecute | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Executes a pipeline.]
Description [All the results are computed. User should update the BDDs of interest. Eventually this feature would become transparent.]
SideEffects [required]
SeeAlso [optional]
Definition at line 244 of file calPipeline.c.
00245 { 00246 CalRequestNode_t **requestNodeListArray, *node, *nextNode; 00247 int i; 00248 Cal_Bdd_t thenBdd; 00249 int automaticDepthControlFlag = 0; 00250 int pipelineDepth; 00251 00252 if(bddManager->pipelineState != CREATE){ 00253 CalBddWarningMessage("Pipeline cannot be executed"); 00254 return 0; 00255 } 00256 00257 /* Check if we need to control the depth value using some heuristic */ 00258 if (bddManager->depth == 0) automaticDepthControlFlag = 1; 00259 00260 requestNodeListArray = bddManager->requestNodeListArray; 00261 pipelineDepth = bddManager->pipelineDepth; 00262 while(pipelineDepth){ 00263 if (automaticDepthControlFlag){ 00264 if (bddManager->numNodes < 10000) bddManager->depth = 4; 00265 else if (bddManager->numNodes < 100000) bddManager->depth = 2; 00266 else bddManager->depth = 1; 00267 } 00268 if(bddManager->depth > pipelineDepth){ 00269 bddManager->depth = pipelineDepth; 00270 } 00271 CalRequestNodeListArrayOp(bddManager, requestNodeListArray, 00272 bddManager->pipelineFn); 00273 pipelineDepth -= bddManager->depth; 00274 00275 /* Lock the results, in case garbage collection needs to be 00276 invoked */ 00277 for (i=0; i<bddManager->depth; i++){ 00278 for (node = requestNodeListArray[i]; node; node = nextNode){ 00279 nextNode = CalBddNodeGetNextBddNode(node); 00280 CalBddNodeGetThenBdd(node, thenBdd); 00281 CalBddIcrRefCount(thenBdd); 00282 } 00283 } 00284 /* Save the current pipelineDepth */ 00285 bddManager->currentPipelineDepth = pipelineDepth; 00286 if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){ 00287 /* Abort, may be we should clean up a little bit */ 00288 fprintf(stderr,"Bdd Overflow: Aborting\n"); 00289 return 0; 00290 } 00291 requestNodeListArray += bddManager->depth; 00292 } 00293 /* Need to decrement the reference counts */ 00294 for (i=0; i<bddManager->pipelineDepth; i++){ 00295 for (node=bddManager->requestNodeListArray[i]; node; node = nextNode){ 00296 nextNode = CalBddNodeGetNextBddNode(node); 00297 CalBddNodeGetThenBdd(node, thenBdd); 00298 CalBddDcrRefCount(thenBdd); 00299 } 00300 } 00301 bddManager->pipelineState = UPDATE; 00302 return 1; 00303 }
| EXTERN int Cal_PipelineInit | ( | Cal_BddManager | bddManager, | |
| Cal_BddOp_t | bddOp | |||
| ) |
Function********************************************************************
Synopsis [Initialize a BDD pipeline.]
Description [All the operations for this pipeline must be of the same kind.]
SideEffects [None.]
SeeAlso []
Definition at line 130 of file calPipeline.c.
00131 { 00132 CalBddPostProcessing(bddManager); 00133 if(bddManager->pipelineState != READY){ 00134 CalBddWarningMessage("Pipeline cannot be initialized"); 00135 return 0; 00136 } 00137 else{ 00138 bddManager->pipelineState = CREATE; 00139 switch(bddOp){ 00140 case CAL_AND : 00141 bddManager->pipelineFn = CalOpAnd; 00142 break; 00143 case CAL_OR : 00144 bddManager->pipelineFn = CalOpOr; 00145 break; 00146 case CAL_XOR : 00147 bddManager->pipelineFn = CalOpXor; 00148 break; 00149 default : 00150 CalBddWarningMessage("Unknown Bdd Operation type"); 00151 return 0; 00152 } 00153 return 1; 00154 } 00155 }
| EXTERN void Cal_PipelineQuit | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Resets the pipeline freeing all resources.]
Description [The user must make sure to update all provisional BDDs of interest before calling this routine.]
SideEffects []
SeeAlso []
Definition at line 363 of file calPipeline.c.
00364 { 00365 CalRequestNode_t *requestNode, *next; 00366 int i; 00367 00368 bddManager->pipelineState = READY; 00369 for(i = 0; i < bddManager->pipelineDepth; i++){ 00370 for(requestNode = bddManager->requestNodeListArray[i], 00371 bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t); 00372 requestNode != Cal_Nil(CalRequestNode_t); 00373 requestNode = next){ 00374 next = CalRequestNodeGetNextRequestNode(requestNode); 00375 CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode); 00376 } 00377 bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t); 00378 } 00379 bddManager->pipelineDepth = 0; 00380 for (requestNode = bddManager->userProvisionalNodeList; requestNode; 00381 requestNode = next){ 00382 next = CalRequestNodeGetNextRequestNode(requestNode); 00383 CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], 00384 requestNode); 00385 } 00386 bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t); 00387 }
| EXTERN void Cal_PipelineSetDepth | ( | Cal_BddManager | bddManager, | |
| int | depth | |||
| ) |
CFile***********************************************************************
FileName [calPipeline.c]
PackageName [cal]
Synopsis [Routines for creating and managing the pipelined BDD operations.]
Description [Eventually we would like to have this feature transparent to the user.]
SeeAlso [optional]
Author [ Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) Jagesh 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
- calPipeline.c,v 1.1.1.3 1998/05/04 00:59:01 hsv Exp
]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Set depth of a BDD pipeline.]
Description [The "depth" determines the amount of dependency we would allow in pipelined computation.]
SideEffects [None.]
SeeAlso []
Definition at line 91 of file calPipeline.c.
00092 { 00093 int i, j; 00094 if(depth > 6){ 00095 CalBddWarningMessage("PipelineDepth can not exceed 6\n"); 00096 CalBddWarningMessage("setting PipelineDepth to 6\n"); 00097 depth = 6; 00098 } 00099 if(bddManager->maxDepth < depth){ 00100 int oldMaxDepth = bddManager->maxDepth; 00101 bddManager->depth = bddManager->maxDepth = depth; 00102 bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue, 00103 bddManager->maxDepth); 00104 for(i = oldMaxDepth; i < bddManager->maxDepth; i++){ 00105 bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1); 00106 for(j = 0; j < bddManager->numVars+1; j++){ 00107 bddManager->reqQue[i][j] = 00108 CalHashTableInit(bddManager, j); 00109 } 00110 } 00111 } 00112 else{ 00113 bddManager->depth = depth; 00114 } 00115 }
| EXTERN Cal_Bdd Cal_PipelineUpdateProvisionalBdd | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd | provisionalBdd | |||
| ) |
Function********************************************************************
Synopsis [Update a provisional Bdd obtained during pipelining.]
Description [The provisional BDD is automatically freed after quitting pipeline.]
SideEffects []
SeeAlso []
Definition at line 318 of file calPipeline.c.
00320 { 00321 Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, provisionalBdd); 00322 if(bddManager->pipelineState != UPDATE){ 00323 CalBddWarningMessage("Provisional Bdd cannot be updated"); 00324 return (Cal_Bdd) 0; 00325 } 00326 CalBddGetThenBdd(calBdd, calBdd); 00327 return CalBddGetExternalBdd(bddManager, calBdd); 00328 }
| EXTERN void Cal_TempAssociationAugment | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | associationInfoUserBdds, | |||
| int | pairs | |||
| ) |
Function********************************************************************
Synopsis [Adds to the temporary variable association.]
Description [Pairs is 0 if the information represents only a list of variables rather than a full association.]
SideEffects [None]
Definition at line 296 of file calAssociation.c.
00299 { 00300 int i, j, numAssociations; 00301 Cal_Bdd_t f; 00302 long last; 00303 Cal_Bdd_t *associationInfo; 00304 00305 if (CheckAssoc(bddManager, associationInfoUserBdds, pairs) == 0) { 00306 return; 00307 } 00308 00309 /*while (associationInfoUserBdds[i++]);*/ 00310 for (i=0; associationInfoUserBdds[i]; i++); 00311 if (pairs) numAssociations = i/2; 00312 else numAssociations = i; 00313 associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1); 00314 for (j=0; j < i; j++){ 00315 associationInfo[j] = 00316 CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]); 00317 } 00318 associationInfo[j] = bddManager->bddNull; 00319 00320 last = bddManager->tempAssociation->lastBddIndex; 00321 if(pairs){ 00322 for(i = 0; i < numAssociations; i++){ 00323 f = associationInfo[(i<<1)]; 00324 j = CalBddGetBddId(f); 00325 if(bddManager->idToIndex[j] > last){ 00326 last = bddManager->idToIndex[j]; 00327 } 00328 f = bddManager->tempAssociation->varAssociation[j]; 00329 if(!CalBddIsBddNull(bddManager, f)){ 00330 CalBddDcrRefCount(f); 00331 } 00332 f = associationInfo[(i<<1)+1]; 00333 bddManager->tempAssociation->varAssociation[j] = f; 00334 /* Protect BDDs in the association. */ 00335 CalBddIcrRefCount(f); 00336 } 00337 } 00338 else{ 00339 for(i = 0; i < numAssociations; i++){ 00340 f = associationInfo[i]; 00341 j = CalBddGetBddId(f); 00342 if(bddManager->idToIndex[j] > last){ 00343 last = bddManager->idToIndex[j]; 00344 } 00345 f = bddManager->tempAssociation->varAssociation[j]; 00346 if(!CalBddIsBddNull(bddManager, f)){ 00347 CalBddDcrRefCount(f); 00348 } 00349 bddManager->tempAssociation->varAssociation[j] = CalBddOne(bddManager); 00350 } 00351 } 00352 bddManager->tempAssociation->lastBddIndex = last; 00353 Cal_MemFree(associationInfo); 00354 }
| EXTERN void Cal_TempAssociationInit | ( | Cal_BddManager | bddManager, | |
| Cal_Bdd * | associationInfoUserBdds, | |||
| int | pairs | |||
| ) |
Function********************************************************************
Synopsis [Sets the temporary variable association.]
Description [Pairs is 0 if the information represents only a list of variables rather than a full association.]
SideEffects [None]
Definition at line 369 of file calAssociation.c.
00372 { 00373 long i; 00374 Cal_Bdd_t f; 00375 00376 /* Clean up old temporary association. */ 00377 for(i = 1; i <= bddManager->numVars; i++){ 00378 f = bddManager->tempAssociation->varAssociation[i]; 00379 if(!CalBddIsBddNull(bddManager, f)){ 00380 CalBddDcrRefCount(f); 00381 bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull; 00382 } 00383 } 00384 bddManager->tempAssociation->lastBddIndex = -1; 00385 Cal_TempAssociationAugment(bddManager, associationInfoUserBdds, pairs); 00386 }
| EXTERN void Cal_TempAssociationQuit | ( | Cal_BddManager | bddManager | ) |
Function********************************************************************
Synopsis [Cleans up temporary association]
Description [Cleans up temporary associationoptional]
SideEffects [None]
Definition at line 398 of file calAssociation.c.
00399 { 00400 int i; 00401 Cal_Bdd_t f; 00402 00403 /* Clean up old temporary association. */ 00404 for(i = 1; i <= bddManager->numVars; i++){ 00405 f = bddManager->tempAssociation->varAssociation[i]; 00406 if(!CalBddIsBddNull(bddManager, f)){ 00407 CalBddDcrRefCount(f); 00408 bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull; 00409 } 00410 } 00411 bddManager->tempAssociation->lastBddIndex = -1; 00412 }
