• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

extrafwd.h

Go to the documentation of this file.
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

Generated on Thu Feb 10 2011 for PolyBoRi by  doxygen 1.7.1