glu-2.2: src/calBdd/cal.h Source File

00001 
00039 #ifndef _CAL
00040 #define _CAL
00041 #include <stdio.h>
00042 #include <stdlib.h>
00043 #include <string.h>
00044 #if HAVE_SYS_TYPES_H
00045 #  include <sys/types.h>
00046 #endif
00047 #if HAVE_SYS_TIME_H
00048 #  include <sys/time.h>
00049 #endif
00050 #if HAVE_SYS_RESOURCE_H
00051 #  include <sys/resource.h>
00052 #endif
00053 #if HAVE_UNISTD_H
00054 #  include <unistd.h>
00055 #endif
00056 #if HAVE_TIME_H
00057 #  include <time.h>
00058 #endif
00059 
00060 #include <assert.h>
00061 #include <math.h>
00062 
00063 #include "calMem.h"
00064 /*---------------------------------------------------------------------------*/
00065 /* Constant declarations                                                     */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 #ifndef EXTERN
00069 #  ifdef __cplusplus
00070 #    define EXTERN      extern "C"
00071 #  else
00072 #    define EXTERN      extern
00073 #  endif
00074 #endif
00075 
00076 #define CAL_BDD_TYPE_NONTERMINAL 0
00077 #define CAL_BDD_TYPE_ZERO 1
00078 #define CAL_BDD_TYPE_ONE 2
00079 #define CAL_BDD_TYPE_POSVAR 3
00080 #define CAL_BDD_TYPE_NEGVAR 4
00081 #define CAL_BDD_TYPE_OVERFLOW 5
00082 #define CAL_BDD_TYPE_CONSTANT 6
00083 
00084 #define CAL_BDD_UNDUMP_FORMAT 1
00085 #define CAL_BDD_UNDUMP_OVERFLOW 2
00086 #define CAL_BDD_UNDUMP_IOERROR 3
00087 #define CAL_BDD_UNDUMP_EOF 4
00088 
00089 #define CAL_REORDER_NONE 0
00090 #define CAL_REORDER_SIFT 1
00091 #define CAL_REORDER_WINDOW 2
00092 #define CAL_REORDER_METHOD_BF 0
00093 #define CAL_REORDER_METHOD_DF 1
00094 
00095 /*---------------------------------------------------------------------------*/
00096 /* Type declarations                                                         */
00097 /*---------------------------------------------------------------------------*/
00098 typedef struct Cal_BddManagerStruct *Cal_BddManager;
00099 typedef struct Cal_BddManagerStruct Cal_BddManager_t;
00100 typedef struct CalBddNodeStruct *Cal_Bdd;
00101 typedef unsigned short int Cal_BddId_t;
00102 typedef unsigned short int Cal_BddIndex_t;
00103 typedef char * (*Cal_VarNamingFn_t)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t); 
00104 typedef char * (*Cal_TerminalIdFn_t)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t);      
00105 typedef struct Cal_BlockStruct *Cal_Block;
00106 
00107 /*---------------------------------------------------------------------------*/
00108 /* Stucture declarations                                                     */
00109 /*---------------------------------------------------------------------------*/
00110 enum Cal_BddOpEnum {CAL_AND, CAL_OR, CAL_XOR};
00111 typedef enum Cal_BddOpEnum Cal_BddOp_t;
00112 
00113 
00114 /*---------------------------------------------------------------------------*/
00115 /* Variable declarations                                                     */
00116 /*---------------------------------------------------------------------------*/
00117 
00118 /*---------------------------------------------------------------------------*/
00119 /* Macro declarations                                                        */
00120 /*---------------------------------------------------------------------------*/
00121 #define Cal_BddNamingFnNone ((char *(*)(Cal_BddManager, Cal_Bdd, Cal_Pointer_t))0)
00122 #define Cal_BddTerminalIdFnNone ((char *(*)(Cal_BddManager, Cal_Address_t, Cal_Address_t, Cal_Pointer_t))0)
00123 #ifdef _CAL_DEBUG_
00124 #define Cal_Assert(valid) assert(valid)
00125 #else
00126 #define Cal_Assert(ignore) ((void)0)
00127 #endif
00128 
00129 
00130 
00133 /*---------------------------------------------------------------------------*/
00134 /* Function prototypes                                                       */
00135 /*---------------------------------------------------------------------------*/
00136 
00137 EXTERN int Cal_BddIsEqual(Cal_BddManager bddManager, Cal_Bdd userBdd1, Cal_Bdd userBdd2);
00138 EXTERN int Cal_BddIsBddOne(Cal_BddManager bddManager, Cal_Bdd userBdd);
00139 EXTERN int Cal_BddIsBddZero(Cal_BddManager bddManager, Cal_Bdd userBdd);
00140 EXTERN int Cal_BddIsBddNull(Cal_BddManager bddManager, Cal_Bdd userBdd);
00141 EXTERN int Cal_BddIsBddConst(Cal_BddManager bddManager, Cal_Bdd userBdd);
00142 EXTERN Cal_Bdd Cal_BddIdentity(Cal_BddManager bddManager, Cal_Bdd userBdd);
00143 EXTERN Cal_Bdd Cal_BddOne(Cal_BddManager bddManager);
00144 EXTERN Cal_Bdd Cal_BddZero(Cal_BddManager bddManager);
00145 EXTERN Cal_Bdd Cal_BddNot(Cal_BddManager bddManager, Cal_Bdd userBdd);
00146 EXTERN Cal_BddId_t Cal_BddGetIfIndex(Cal_BddManager bddManager, Cal_Bdd userBdd);
00147 EXTERN Cal_BddId_t Cal_BddGetIfId(Cal_BddManager bddManager, Cal_Bdd userBdd);
00148 EXTERN Cal_Bdd Cal_BddIf(Cal_BddManager bddManager, Cal_Bdd userBdd);
00149 EXTERN Cal_Bdd Cal_BddThen(Cal_BddManager bddManager, Cal_Bdd userBdd);
00150 EXTERN Cal_Bdd Cal_BddElse(Cal_BddManager bddManager, Cal_Bdd userBdd);
00151 EXTERN void Cal_BddFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
00152 EXTERN void Cal_BddUnFree(Cal_BddManager bddManager, Cal_Bdd userBdd);
00153 EXTERN Cal_Bdd Cal_BddGetRegular(Cal_BddManager bddManager, Cal_Bdd userBdd);
00154 EXTERN Cal_Bdd Cal_BddIntersects(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00155 EXTERN Cal_Bdd Cal_BddImplies(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00156 EXTERN unsigned long Cal_BddTotalSize(Cal_BddManager bddManager);
00157 EXTERN void Cal_BddStats(Cal_BddManager bddManager, FILE * fp);
00158 EXTERN void Cal_BddDynamicReordering(Cal_BddManager bddManager, int technique);
00159 EXTERN void Cal_BddReorder(Cal_BddManager bddManager);
00160 EXTERN int Cal_BddType(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00161 EXTERN long Cal_BddVars(Cal_BddManager bddManager);
00162 EXTERN long Cal_BddNodeLimit(Cal_BddManager bddManager, long newLimit);
00163 EXTERN int Cal_BddOverflow(Cal_BddManager bddManager);
00164 EXTERN int Cal_BddIsCube(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00165 EXTERN void * Cal_BddManagerGetHooks(Cal_BddManager bddManager);
00166 EXTERN void Cal_BddManagerSetHooks(Cal_BddManager bddManager, void *hooks);
00167 EXTERN int Cal_AssociationInit(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs);
00168 EXTERN void Cal_AssociationQuit(Cal_BddManager bddManager, int associationId);
00169 EXTERN int Cal_AssociationSetCurrent(Cal_BddManager bddManager, int associationId);
00170 EXTERN void Cal_TempAssociationAugment(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs);
00171 EXTERN void Cal_TempAssociationInit(Cal_BddManager bddManager, Cal_Bdd *associationInfoUserBdds, int pairs);
00172 EXTERN void Cal_TempAssociationQuit(Cal_BddManager bddManager);
00173 EXTERN Cal_Bdd Cal_BddCompose(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd);
00174 EXTERN Cal_Bdd Cal_BddITE(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd);
00175 EXTERN Cal_BddManager Cal_BddManagerInit(void);
00176 EXTERN int Cal_BddManagerQuit(Cal_BddManager bddManager);
00177 EXTERN void Cal_BddManagerSetParameters(Cal_BddManager bddManager, long reorderingThreshold, long maxForwardedNodes, double repackAfterGCThreshold, double tableRepackThreshold);
00178 EXTERN unsigned long Cal_BddManagerGetNumNodes(Cal_BddManager bddManager);
00179 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager);
00180 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager);
00181 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager, Cal_Bdd userBdd);
00182 EXTERN Cal_Bdd Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager, Cal_Bdd userBdd);
00183 EXTERN Cal_Bdd Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager, Cal_BddIndex_t index);
00184 EXTERN Cal_Bdd Cal_BddManagerGetVarWithId(Cal_BddManager bddManager, Cal_BddId_t id);
00185 EXTERN Cal_Bdd Cal_BddAnd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00186 EXTERN Cal_Bdd Cal_BddNand(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00187 EXTERN Cal_Bdd Cal_BddOr(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00188 EXTERN Cal_Bdd Cal_BddNor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00189 EXTERN Cal_Bdd Cal_BddXor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00190 EXTERN Cal_Bdd Cal_BddXnor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00191 EXTERN Cal_Bdd * Cal_BddPairwiseAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
00192 EXTERN Cal_Bdd * Cal_BddPairwiseOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
00193 EXTERN Cal_Bdd * Cal_BddPairwiseXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
00194 EXTERN Cal_Bdd Cal_BddMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
00195 EXTERN Cal_Bdd Cal_BddMultiwayOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
00196 EXTERN Cal_Bdd Cal_BddMultiwayXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray);
00197 EXTERN Cal_Bdd Cal_BddSatisfy(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00198 EXTERN Cal_Bdd Cal_BddSatisfySupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00199 EXTERN double Cal_BddSatisfyingFraction(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00200 EXTERN long Cal_BddSize(Cal_BddManager bddManager, Cal_Bdd fUserBdd, int negout);
00201 EXTERN long Cal_BddSizeMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, int negout);
00202 EXTERN void Cal_BddProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, long * levelCounts, int negout);
00203 EXTERN void Cal_BddProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long * levelCounts, int negout);
00204 EXTERN void Cal_BddFunctionProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, long * funcCounts);
00205 EXTERN void Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, long * funcCounts);
00206 EXTERN Cal_Bdd Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00207 EXTERN void Cal_BddSupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd *support);
00208 EXTERN int Cal_BddDependsOn(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd varUserBdd);
00209 EXTERN Cal_Bdd Cal_BddSwapVars(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd, Cal_Bdd hUserBdd);
00210 EXTERN Cal_Bdd Cal_BddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00211 EXTERN Cal_Block Cal_BddNewVarBlock(Cal_BddManager bddManager, Cal_Bdd variable, long length);
00212 EXTERN void Cal_BddVarBlockReorderable(Cal_BddManager bddManager, Cal_Block block, int reorderable);
00213 EXTERN Cal_Bdd Cal_BddUndumpBdd(Cal_BddManager bddManager, Cal_Bdd * userVars, FILE * fp, int * error);
00214 EXTERN int Cal_BddDumpBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd * userVars, FILE * fp);
00215 EXTERN void Cal_BddSetGCMode(Cal_BddManager bddManager, int gcMode);
00216 EXTERN int Cal_BddManagerGC(Cal_BddManager bddManager);
00217 EXTERN void Cal_BddManagerSetGCLimit(Cal_BddManager manager);
00218 EXTERN void Cal_MemFatal(char *message);
00219 EXTERN Cal_Address_t Cal_MemAllocation(void);
00220 EXTERN Cal_Pointer_t Cal_MemGetBlock(Cal_Address_t size);
00221 EXTERN void Cal_MemFreeBlock(Cal_Pointer_t p);
00222 EXTERN Cal_Pointer_t Cal_MemResizeBlock(Cal_Pointer_t p, Cal_Address_t newSize);
00223 EXTERN Cal_Pointer_t Cal_MemNewRec(Cal_RecMgr mgr);
00224 EXTERN void Cal_MemFreeRec(Cal_RecMgr mgr, Cal_Pointer_t rec);
00225 EXTERN Cal_RecMgr Cal_MemNewRecMgr(int size);
00226 EXTERN void Cal_MemFreeRecMgr(Cal_RecMgr mgr);
00227 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);
00228 EXTERN void Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth);
00229 EXTERN int Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp);
00230 EXTERN Cal_Bdd Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00231 EXTERN int Cal_PipelineExecute(Cal_BddManager bddManager);
00232 EXTERN Cal_Bdd Cal_PipelineUpdateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd provisionalBdd);
00233 EXTERN int Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd);
00234 EXTERN void Cal_PipelineQuit(Cal_BddManager bddManager);
00235 EXTERN void Cal_BddPrintBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t VarNamingFn, Cal_TerminalIdFn_t TerminalIdFn, Cal_Pointer_t env, FILE *fp);
00236 EXTERN void Cal_BddPrintProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
00237 EXTERN void Cal_BddPrintProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *userBdds, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
00238 EXTERN void Cal_BddPrintFunctionProfile(Cal_BddManager bddManager, Cal_Bdd f, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
00239 EXTERN void Cal_BddPrintFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *userBdds, Cal_VarNamingFn_t varNamingProc, char * env, int lineLength, FILE * fp);
00240 EXTERN Cal_Bdd Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00241 EXTERN Cal_Bdd Cal_BddRelProd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd);
00242 EXTERN Cal_Bdd Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd);
00243 EXTERN Cal_Bdd Cal_BddCofactor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd);
00244 EXTERN Cal_Bdd Cal_BddReduce(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd);
00245 EXTERN Cal_Bdd Cal_BddBetween(Cal_BddManager bddManager, Cal_Bdd fMinUserBdd, Cal_Bdd fMaxUserBdd);
00246 EXTERN void Cal_ImageDump(Cal_BddManager_t *bddManager, FILE *fp);
00247 EXTERN void Cal_BddFunctionPrint(Cal_BddManager bddManager, Cal_Bdd userBdd, char *name);
00248 
00251 #endif /* _CAL */