00001
00002
00003 #ifndef EXTRA_FWD_HEADER
00004 #define EXTRA_FWD_HEADER
00005 #include <cudd.h>
00006
00007 extern "C"{
00008
00009 extern DdNode * Extra_zddPrimeProduct( DdManager *dd, DdNode * f, DdNode * g );
00010
00011
00012 extern DdNode * Extra_zddProductAlt( DdManager *dd, DdNode * f, DdNode * g );
00013
00014
00015 extern DdNode * Extra_zddCompatible( DdManager * dd, DdNode * zCover, DdNode * zCube );
00016
00017
00018 extern DdNode * Extra_zddIsopCover( DdManager * dd, DdNode * F1, DdNode * F12 );
00019
00020 extern void Extra_zddIsopPrintCover( DdManager * dd, DdNode * F1, DdNode * F12 );
00021
00022 extern DdNode * Extra_zddSimplify( DdManager * dd, DdNode * F1, DdNode * F12 );
00023
00024
00025 extern DdNode * Extra_zddIsopCoverAlt( DdManager * dd, DdNode * F1, DdNode * F12 );
00026
00027
00028 extern int Extra_zddIsopCubeNum( DdManager * dd, DdNode * F1, DdNode * F12 );
00029
00030
00031
00032 extern DdNode * Extra_zddDisjointCover( DdManager * dd, DdNode * F );
00033
00034 extern DdNode * Extra_zddResolve( DdManager * dd, DdNode * S, DdNode * Vars );
00035
00036 extern DdNode * Extra_zddNotContainedCubesOverArea( DdManager * dd, DdNode * zC, DdNode * zD, DdNode * bA );
00037 extern DdNode * extraZddNotContainedCubesOverArea( DdManager * dd, DdNode * zC, DdNode * zD, DdNode * bA );
00038
00039
00040 extern DdNode * Extra_zddSelectOneCube( DdManager * dd, DdNode * zS );
00041
00042
00043 extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
00044
00045
00046 extern int Extra_zddCheckUnateness( DdManager * dd, DdNode * zCover );
00047
00048 extern DdNode * Extra_zddGetMostCoveredArea( DdManager * dd, DdNode * zC, int * nOverlaps );
00049
00050
00051
00052
00053
00054 extern DdNode * Extra_zddUnionExor( DdManager * dd, DdNode * S, DdNode * T );
00055
00056 extern DdNode * Extra_zddSupercubes( DdManager *dd, DdNode * zA, DdNode * zB );
00057
00058
00059 extern DdNode * Extra_zddSelectDist1Cubes( DdManager *dd, DdNode * zA, DdNode * zB );
00060
00061
00062 extern int Extra_zddFastEsopCoverArray( DdManager * dd, DdNode ** bFs, DdNode ** zCs, int nFs );
00063
00064
00065
00066
00067
00068
00069 extern int Extra_bddFactoredFormLiterals( DdManager * dd, DdNode * bOnSet, DdNode * bOnDcSet );
00070 extern DdNode * Extra_zddFactoredFormLiterals( DdManager * dd, DdNode * zCover );
00071 extern DdNode * Extra_zddLFLiterals( DdManager * dd, DdNode * zCover, DdNode * zCube );
00072
00073 extern DdNode * Extra_zddQuickDivisor( DdManager * dd, DdNode * zCover );
00074 extern DdNode * Extra_zddLevel0Kernel( DdManager * dd, DdNode * zCover );
00075
00076 extern void Extra_zddDivision( DdManager * dd, DdNode * zCover, DdNode * zDiv, DdNode ** zQuo, DdNode ** zRem );
00077
00078 extern DdNode * Extra_zddCommonCubeFast( DdManager * dd, DdNode * zCover );
00079
00080 extern DdNode * Extra_zddMoreThanOnceCubeFast( DdManager * dd, DdNode * zCover );
00081
00082 extern DdNode * Extra_zddMakeCubeFree( DdManager * dd, DdNode * zCover, int iZVar );
00083
00084 extern int Extra_zddTestCubeFree( DdManager * dd, DdNode * zCover );
00085
00086
00087 extern int Extra_zddCountLiteralsSimple( DdManager * dd, DdNode * zCover );
00088
00089 extern int Extra_zddMoreThanOneCube( DdManager * dd, DdNode * zCover );
00090
00091 extern DdNode * Extra_zddCombinationFromLevels( DdManager * dd, int * pLevels, int nVars );
00092
00093 extern int Extra_zddCommonLiterals( DdManager * dd, DdNode * zCover, int iZVar, int * pLevels, int * pLiterals );
00094
00095 extern int Extra_zddMoreThanOneLiteralSet( DdManager * dd, DdNode * zCover, int StartLevel, int * pVars, int * pCounters );
00096
00097 extern int Extra_zddMoreThanOneLiteral( DdManager * dd, DdNode * zCover, int iZVar );
00098
00099
00100
00101
00102
00103 extern DdNode * Extra_zddCliques( DdManager *dd, DdNode * G, int fMaximal );
00104
00105 extern DdNode * Extra_zddMaxCliques( DdManager *dd, DdNode * G );
00106
00107 extern DdNode * Extra_zddIncremCliques( DdManager *dd, DdNode * G, DdNode * C );
00108
00109
00110
00111
00112
00113 extern DdNode * Extra_zddIsopCoverAllVars( DdManager * dd, DdNode * F1, DdNode * F12 );
00114
00115
00116 extern DdNode * Extra_zddIsopCoverUnateVars( DdManager * dd, DdNode * F1, DdNode * F12 );
00117
00118
00119
00120 extern DdNode * Extra_zddIsopCoverRandom( DdManager * dd, DdNode * F1, DdNode * F12 );
00121
00122 extern DdNode * Extra_zddIsopCoverReduced( DdManager * dd, DdNode * F1, DdNode * F12 );
00123
00124
00125
00126
00127
00128 extern int * Extra_zddLitCount( DdManager * dd, DdNode * Set );
00129
00130 extern int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb );
00131
00132
00133
00134
00135 extern DdNode * Extra_zddMaximal( DdManager *dd, DdNode * S );
00136
00137 extern DdNode * Extra_zddMinimal( DdManager *dd, DdNode * S );
00138
00139
00140 extern DdNode * Extra_zddMaxUnion( DdManager *dd, DdNode * S, DdNode * T );
00141
00142 extern DdNode * Extra_zddMinUnion( DdManager *dd, DdNode * S, DdNode * T );
00143
00144
00145 extern DdNode * Extra_zddDotProduct( DdManager *dd, DdNode * S, DdNode * T );
00146
00147 extern DdNode * Extra_zddExorProduct( DdManager *dd, DdNode * S, DdNode * T );
00148
00149 extern DdNode * Extra_zddCrossProduct( DdManager *dd, DdNode * S, DdNode * T );
00150
00151 extern DdNode * Extra_zddMaxDotProduct( DdManager *dd, DdNode * S, DdNode * T );
00152
00153
00154
00155
00156
00157 extern DdNode * Extra_zddVariable( DdManager * dd, int iVar );
00158
00159 extern DdNode * Extra_zddCombination( DdManager *dd, int* VarValues, int nVars );
00160
00161
00162 extern DdNode * Extra_zddUniverse( DdManager * dd, DdNode * VarSet );
00163
00164
00165 extern DdNode * Extra_zddTuples( DdManager * dd, int K, DdNode * zVarsN );
00166
00167
00168 extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
00169
00170
00171 extern DdNode * Extra_zddSinglesToComb( DdManager * dd, DdNode * Singles );
00172
00173
00174 extern DdNode * Extra_zddMaximum( DdManager * dd, DdNode * S, int * nVars );
00175
00176 extern DdNode * Extra_zddMinimum( DdManager * dd, DdNode * S, int * nVars );
00177
00178
00179 extern DdNode * Extra_zddRandomSet( DdManager * dd, int n, int k, double d );
00180
00181 extern DdNode * Extra_zddCoveredByArea( DdManager *dd, DdNode * zC, DdNode * bA );
00182
00183 extern DdNode * Extra_zddNotCoveredByCover( DdManager *dd, DdNode * zC, DdNode * zD );
00184
00185 extern DdNode * Extra_zddOverlappingWithArea( DdManager *dd, DdNode * zC, DdNode * bA );
00186
00187 extern DdNode * Extra_zddConvertToBdd( DdManager *dd, DdNode * zC );
00188
00189 extern DdNode * Extra_zddConvertToBddUnate( DdManager *dd, DdNode * zC );
00190
00191 extern DdNode * Extra_zddConvertEsopToBdd( DdManager *dd, DdNode * zC );
00192
00193 extern DdNode * Extra_zddConvertToBddAndAdd( DdManager *dd, DdNode * zC, DdNode * bA );
00194
00195 extern DdNode * Extra_zddSingleCoveredArea( DdManager *dd, DdNode * zC );
00196
00197 extern DdNode * Extra_zddConvertBddCubeIntoZddCube( DdManager *dd, DdNode * bCube );
00198
00199
00200
00201
00202 extern DdNode * Extra_zddExistAbstract( DdManager *manager, DdNode * F, DdNode * cube );
00203
00204
00205 extern DdNode * Extra_zddChangeVars( DdManager *manager, DdNode * F, DdNode * cube );
00206
00207
00208 extern DdNode * Extra_zddPermute ( DdManager *dd, DdNode * N, int *permut );
00209
00210 extern DdNode * Extra_zddCofactor0( DdManager * dd, DdNode * f, DdNode * cube );
00211
00212
00213 extern DdNode * Extra_zddCofactor1( DdManager * dd, DdNode * f, DdNode * cube, int fIncludeVars );
00214
00215
00216
00217
00218
00219 extern DdNode * Extra_zddSubSet ( DdManager *dd, DdNode * X, DdNode * Y );
00220
00221 extern DdNode * Extra_zddSupSet ( DdManager *dd, DdNode * X, DdNode * Y );
00222
00223 extern DdNode * Extra_zddNotSubSet( DdManager *dd, DdNode * X, DdNode * Y );
00224
00225 extern DdNode * Extra_zddNotSupSet( DdManager *dd, DdNode * X, DdNode * Y );
00226
00227 extern DdNode * Extra_zddMaxNotSupSet( DdManager *dd, DdNode * X, DdNode * Y );
00228
00229
00230 extern int Extra_zddEmptyBelongs ( DdManager *dd, DdNode* zS );
00231
00232 extern int Extra_zddIsOneSubset( DdManager *dd, DdNode* zS );
00233
00234 }
00235
00236
00237 #endif