PolyBoRi
|
00001 /* Copyright (c) 2005-2007 by The PolyBoRi Team */ 00002 00003 #ifndef EXTRA_FWD_HEADER 00004 #define EXTRA_FWD_HEADER 00005 #include <cudd.h> 00006 00007 extern "C"{ 00008 /* the result of this operation is primes contained in the product of cubes */ 00009 extern DdNode * Extra_zddPrimeProduct( DdManager *dd, DdNode * f, DdNode * g ); 00010 00011 /* an alternative implementation of the cover product */ 00012 extern DdNode * Extra_zddProductAlt( DdManager *dd, DdNode * f, DdNode * g ); 00013 00014 /* returns the set of cubes pair-wise unate with the given cube */ 00015 extern DdNode * Extra_zddCompatible( DdManager * dd, DdNode * zCover, DdNode * zCube ); 00016 00017 /* a wrapper for the call to Extra_zddIsop() */ 00018 extern DdNode * Extra_zddIsopCover( DdManager * dd, DdNode * F1, DdNode * F12 ); 00019 /* a wrapper for the call to Extra_zddIsopCover() and Extra_zddPrintCover() */ 00020 extern void Extra_zddIsopPrintCover( DdManager * dd, DdNode * F1, DdNode * F12 ); 00021 /* a simple cover computation (not ISOP) */ 00022 extern DdNode * Extra_zddSimplify( DdManager * dd, DdNode * F1, DdNode * F12 ); 00023 00024 /* an alternative ISOP cover computation (faster than Extra_zddIsop()) */ 00025 extern DdNode * Extra_zddIsopCoverAlt( DdManager * dd, DdNode * F1, DdNode * F12 ); 00026 00027 /* count the number of cubes in the ISOP without building the ISOP as a ZDD */ 00028 extern int Extra_zddIsopCubeNum( DdManager * dd, DdNode * F1, DdNode * F12 ); 00029 00030 00031 /* computes the disjoint cube cover produced by the bdd paths */ 00032 extern DdNode * Extra_zddDisjointCover( DdManager * dd, DdNode * F ); 00033 /* performs resolution on the set of clauses (S) w.r.t. variables in zdd Vars */ 00034 extern DdNode * Extra_zddResolve( DdManager * dd, DdNode * S, DdNode * Vars ); 00035 /* cubes from zC that are not contained by cubes from zD over area bA */ 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 /* finds cofactors of the cover w.r.t. the top-most variable without creating new nodes */ 00039 /* selects one cube from a ZDD representing the cube cover */ 00040 extern DdNode * Extra_zddSelectOneCube( DdManager * dd, DdNode * zS ); 00041 00042 /* selects one subset from a ZDD representing the set of subsets */ 00043 extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS ); 00044 00045 /* checks unateness of the cover */ 00046 extern int Extra_zddCheckUnateness( DdManager * dd, DdNode * zCover ); 00047 /* computes the BDD of the area covered by the max number of cubes in a ZDD. */ 00048 extern DdNode * Extra_zddGetMostCoveredArea( DdManager * dd, DdNode * zC, int * nOverlaps ); 00049 00050 00051 /*=== extraZddExor.c ==============================================================*/ 00052 00053 /* computes the Exclusive-OR-type union of two cube sets */ 00054 extern DdNode * Extra_zddUnionExor( DdManager * dd, DdNode * S, DdNode * T ); 00055 /* given two sets of cubes, computes the set of pair-wise supercubes */ 00056 extern DdNode * Extra_zddSupercubes( DdManager *dd, DdNode * zA, DdNode * zB ); 00057 00058 /* selects cubes from zA that have a distance-1 cube in zB */ 00059 extern DdNode * Extra_zddSelectDist1Cubes( DdManager *dd, DdNode * zA, DdNode * zB ); 00060 00061 /* computes the set of fast ESOP covers for the multi-output function */ 00062 extern int Extra_zddFastEsopCoverArray( DdManager * dd, DdNode ** bFs, DdNode ** zCs, int nFs ); 00063 /* computes a fast ESOP cover for the single-output function */ 00064 //extern DdNode * Extra_zddFastEsopCover( DdManager * dd, DdNode * bF, st_table * Visited, int * pnCubes ); 00065 00066 /*=== extraZddFactor.c ================================================================*/ 00067 00068 /* counting the number of literals in the factored form */ 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 /* computing a quick divisor */ 00073 extern DdNode * Extra_zddQuickDivisor( DdManager * dd, DdNode * zCover ); 00074 extern DdNode * Extra_zddLevel0Kernel( DdManager * dd, DdNode * zCover ); 00075 /* division with quotient and remainder */ 00076 extern void Extra_zddDivision( DdManager * dd, DdNode * zCover, DdNode * zDiv, DdNode ** zQuo, DdNode ** zRem ); 00077 /* the common cube */ 00078 extern DdNode * Extra_zddCommonCubeFast( DdManager * dd, DdNode * zCover ); 00079 /* the cube of literals that occur more than once */ 00080 extern DdNode * Extra_zddMoreThanOnceCubeFast( DdManager * dd, DdNode * zCover ); 00081 /* making the cover cube-free */ 00082 extern DdNode * Extra_zddMakeCubeFree( DdManager * dd, DdNode * zCover, int iZVar ); 00083 /* testing whether the cover is cube-free */ 00084 extern int Extra_zddTestCubeFree( DdManager * dd, DdNode * zCover ); 00085 00086 /* counts the number of literals in the simple cover */ 00087 extern int Extra_zddCountLiteralsSimple( DdManager * dd, DdNode * zCover ); 00088 /* tests whether the cover contains more than one cube */ 00089 extern int Extra_zddMoreThanOneCube( DdManager * dd, DdNode * zCover ); 00090 /* the cube from levels */ 00091 extern DdNode * Extra_zddCombinationFromLevels( DdManager * dd, int * pLevels, int nVars ); 00092 /* determines common literals */ 00093 extern int Extra_zddCommonLiterals( DdManager * dd, DdNode * zCover, int iZVar, int * pLevels, int * pLiterals ); 00094 /* determines the set of literals that occur more than once */ 00095 extern int Extra_zddMoreThanOneLiteralSet( DdManager * dd, DdNode * zCover, int StartLevel, int * pVars, int * pCounters ); 00096 /* tests whether the given literal literal occurs more than once */ 00097 extern int Extra_zddMoreThanOneLiteral( DdManager * dd, DdNode * zCover, int iZVar ); 00098 00099 00100 /*=== extraZddGraph.c ==============================================================*/ 00101 00102 /* construct the set of cliques */ 00103 extern DdNode * Extra_zddCliques( DdManager *dd, DdNode * G, int fMaximal ); 00104 /* construct the set of all maximal cliques */ 00105 extern DdNode * Extra_zddMaxCliques( DdManager *dd, DdNode * G ); 00106 /* incrementally contruct the set of cliques */ 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 /* computes an ISOP cover with a random ordering of variables */ 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 /*=== extraZddLitCount.c ==============================================================*/ 00126 00127 /* count the number of times each variable occurs in the combinations */ 00128 extern int * Extra_zddLitCount( DdManager * dd, DdNode * Set ); 00129 /* count the number of literals in one ZDD combination */ 00130 extern int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb ); 00131 00132 /*=== extraZddMaxMin.c ==============================================================*/ 00133 00134 /* maximal/minimimal */ 00135 extern DdNode * Extra_zddMaximal( DdManager *dd, DdNode * S ); 00136 00137 extern DdNode * Extra_zddMinimal( DdManager *dd, DdNode * S ); 00138 00139 /* maximal/minimal of the union of two sets of subsets */ 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 /* dot/cross products */ 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 /*=== extraZddMisc.c ==============================================================*/ 00155 00156 /* create the combination composed of a single ZDD variable */ 00157 extern DdNode * Extra_zddVariable( DdManager * dd, int iVar ); 00158 /* build a ZDD for a combination of variables */ 00159 extern DdNode * Extra_zddCombination( DdManager *dd, int* VarValues, int nVars ); 00160 00161 /* the set of all possible combinations of the given set of variables */ 00162 extern DdNode * Extra_zddUniverse( DdManager * dd, DdNode * VarSet ); 00163 00164 /* build the set of all tuples of K variables out of N */ 00165 extern DdNode * Extra_zddTuples( DdManager * dd, int K, DdNode * zVarsN ); 00166 00167 /* build the set of all tuples of K variables out of N from the BDD cube */ 00168 extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN ); 00169 00170 /* convert the set of singleton combinations into one combination */ 00171 extern DdNode * Extra_zddSinglesToComb( DdManager * dd, DdNode * Singles ); 00172 00173 /* returns the set of combinations containing the max/min number of elements */ 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 /* returns the random set of k combinations of n elements with average density d */ 00179 extern DdNode * Extra_zddRandomSet( DdManager * dd, int n, int k, double d ); 00180 /* other utilities */ 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 /*=== extraZddPermute.c ==============================================================*/ 00200 00201 /* quantifications */ 00202 extern DdNode * Extra_zddExistAbstract( DdManager *manager, DdNode * F, DdNode * cube ); 00203 00204 /* changes the value of several variables in the ZDD */ 00205 extern DdNode * Extra_zddChangeVars( DdManager *manager, DdNode * F, DdNode * cube ); 00206 00207 /* permutes variables in ZDD */ 00208 extern DdNode * Extra_zddPermute ( DdManager *dd, DdNode * N, int *permut ); 00209 /* computes combinations in F with vars in Cube having the negative polarity */ 00210 extern DdNode * Extra_zddCofactor0( DdManager * dd, DdNode * f, DdNode * cube ); 00211 00212 /* computes combinations in F with vars in Cube having the positive polarity */ 00213 extern DdNode * Extra_zddCofactor1( DdManager * dd, DdNode * f, DdNode * cube, int fIncludeVars ); 00214 00215 00216 /*=== extraZddSubSup.c ==============================================================*/ 00217 00218 /* subset/supset operations */ 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 /* check whether the empty combination belongs to the set of subsets */ 00230 extern int Extra_zddEmptyBelongs ( DdManager *dd, DdNode* zS ); 00231 /* check whether the set consists of one subset only */ 00232 extern int Extra_zddIsOneSubset( DdManager *dd, DdNode* zS ); 00233 00234 } 00235 00236 00237 #endif