PolyBoRi
extrafwd.h
Go to the documentation of this file.
1 /* Copyright (c) 2005-2007 by The PolyBoRi Team */
2 
3 #ifndef EXTRA_FWD_HEADER
4 #define EXTRA_FWD_HEADER
5 #include <cudd.h>
6 
7 extern "C"{
8 /* the result of this operation is primes contained in the product of cubes */
9 extern DdNode * Extra_zddPrimeProduct( DdManager *dd, DdNode * f, DdNode * g );
10 
11 /* an alternative implementation of the cover product */
12 extern DdNode * Extra_zddProductAlt( DdManager *dd, DdNode * f, DdNode * g );
13 
14 /* returns the set of cubes pair-wise unate with the given cube */
15 extern DdNode * Extra_zddCompatible( DdManager * dd, DdNode * zCover, DdNode * zCube );
16 
17 /* a wrapper for the call to Extra_zddIsop() */
18 extern DdNode * Extra_zddIsopCover( DdManager * dd, DdNode * F1, DdNode * F12 );
19 /* a wrapper for the call to Extra_zddIsopCover() and Extra_zddPrintCover() */
20 extern void Extra_zddIsopPrintCover( DdManager * dd, DdNode * F1, DdNode * F12 );
21 /* a simple cover computation (not ISOP) */
22 extern DdNode * Extra_zddSimplify( DdManager * dd, DdNode * F1, DdNode * F12 );
23 
24 /* an alternative ISOP cover computation (faster than Extra_zddIsop()) */
25 extern DdNode * Extra_zddIsopCoverAlt( DdManager * dd, DdNode * F1, DdNode * F12 );
26 
27 /* count the number of cubes in the ISOP without building the ISOP as a ZDD */
28 extern int Extra_zddIsopCubeNum( DdManager * dd, DdNode * F1, DdNode * F12 );
29 
30 
31 /* computes the disjoint cube cover produced by the bdd paths */
32 extern DdNode * Extra_zddDisjointCover( DdManager * dd, DdNode * F );
33 /* performs resolution on the set of clauses (S) w.r.t. variables in zdd Vars */
34 extern DdNode * Extra_zddResolve( DdManager * dd, DdNode * S, DdNode * Vars );
35 /* cubes from zC that are not contained by cubes from zD over area bA */
36 extern DdNode * Extra_zddNotContainedCubesOverArea( DdManager * dd, DdNode * zC, DdNode * zD, DdNode * bA );
37 extern DdNode * extraZddNotContainedCubesOverArea( DdManager * dd, DdNode * zC, DdNode * zD, DdNode * bA );
38 /* finds cofactors of the cover w.r.t. the top-most variable without creating new nodes */
39 /* selects one cube from a ZDD representing the cube cover */
40 extern DdNode * Extra_zddSelectOneCube( DdManager * dd, DdNode * zS );
41 
42 /* selects one subset from a ZDD representing the set of subsets */
43 extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
44 
45 /* checks unateness of the cover */
46 extern int Extra_zddCheckUnateness( DdManager * dd, DdNode * zCover );
47 /* computes the BDD of the area covered by the max number of cubes in a ZDD. */
48 extern DdNode * Extra_zddGetMostCoveredArea( DdManager * dd, DdNode * zC, int * nOverlaps );
49 
50 
51 /*=== extraZddExor.c ==============================================================*/
52 
53 /* computes the Exclusive-OR-type union of two cube sets */
54 extern DdNode * Extra_zddUnionExor( DdManager * dd, DdNode * S, DdNode * T );
55 /* given two sets of cubes, computes the set of pair-wise supercubes */
56 extern DdNode * Extra_zddSupercubes( DdManager *dd, DdNode * zA, DdNode * zB );
57 
58 /* selects cubes from zA that have a distance-1 cube in zB */
59 extern DdNode * Extra_zddSelectDist1Cubes( DdManager *dd, DdNode * zA, DdNode * zB );
60 
61 /* computes the set of fast ESOP covers for the multi-output function */
62 extern int Extra_zddFastEsopCoverArray( DdManager * dd, DdNode ** bFs, DdNode ** zCs, int nFs );
63 /* computes a fast ESOP cover for the single-output function */
64 //extern DdNode * Extra_zddFastEsopCover( DdManager * dd, DdNode * bF, st_table * Visited, int * pnCubes );
65 
66 /*=== extraZddFactor.c ================================================================*/
67 
68 /* counting the number of literals in the factored form */
69 extern int Extra_bddFactoredFormLiterals( DdManager * dd, DdNode * bOnSet, DdNode * bOnDcSet );
70 extern DdNode * Extra_zddFactoredFormLiterals( DdManager * dd, DdNode * zCover );
71 extern DdNode * Extra_zddLFLiterals( DdManager * dd, DdNode * zCover, DdNode * zCube );
72 /* computing a quick divisor */
73 extern DdNode * Extra_zddQuickDivisor( DdManager * dd, DdNode * zCover );
74 extern DdNode * Extra_zddLevel0Kernel( DdManager * dd, DdNode * zCover );
75 /* division with quotient and remainder */
76 extern void Extra_zddDivision( DdManager * dd, DdNode * zCover, DdNode * zDiv, DdNode ** zQuo, DdNode ** zRem );
77 /* the common cube */
78 extern DdNode * Extra_zddCommonCubeFast( DdManager * dd, DdNode * zCover );
79 /* the cube of literals that occur more than once */
80 extern DdNode * Extra_zddMoreThanOnceCubeFast( DdManager * dd, DdNode * zCover );
81 /* making the cover cube-free */
82 extern DdNode * Extra_zddMakeCubeFree( DdManager * dd, DdNode * zCover, int iZVar );
83 /* testing whether the cover is cube-free */
84 extern int Extra_zddTestCubeFree( DdManager * dd, DdNode * zCover );
85 
86 /* counts the number of literals in the simple cover */
87 extern int Extra_zddCountLiteralsSimple( DdManager * dd, DdNode * zCover );
88 /* tests whether the cover contains more than one cube */
89 extern int Extra_zddMoreThanOneCube( DdManager * dd, DdNode * zCover );
90 /* the cube from levels */
91 extern DdNode * Extra_zddCombinationFromLevels( DdManager * dd, int * pLevels, int nVars );
92 /* determines common literals */
93 extern int Extra_zddCommonLiterals( DdManager * dd, DdNode * zCover, int iZVar, int * pLevels, int * pLiterals );
94 /* determines the set of literals that occur more than once */
95 extern int Extra_zddMoreThanOneLiteralSet( DdManager * dd, DdNode * zCover, int StartLevel, int * pVars, int * pCounters );
96 /* tests whether the given literal literal occurs more than once */
97 extern int Extra_zddMoreThanOneLiteral( DdManager * dd, DdNode * zCover, int iZVar );
98 
99 
100 /*=== extraZddGraph.c ==============================================================*/
101 
102 /* construct the set of cliques */
103 extern DdNode * Extra_zddCliques( DdManager *dd, DdNode * G, int fMaximal );
104 /* construct the set of all maximal cliques */
105 extern DdNode * Extra_zddMaxCliques( DdManager *dd, DdNode * G );
106 /* incrementally contruct the set of cliques */
107 extern DdNode * Extra_zddIncremCliques( DdManager *dd, DdNode * G, DdNode * C );
108 
109 
110 
111 
112 
113 extern DdNode * Extra_zddIsopCoverAllVars( DdManager * dd, DdNode * F1, DdNode * F12 );
114 
115 
116 extern DdNode * Extra_zddIsopCoverUnateVars( DdManager * dd, DdNode * F1, DdNode * F12 );
117 
118 
119 /* computes an ISOP cover with a random ordering of variables */
120 extern DdNode * Extra_zddIsopCoverRandom( DdManager * dd, DdNode * F1, DdNode * F12 );
121 
122 extern DdNode * Extra_zddIsopCoverReduced( DdManager * dd, DdNode * F1, DdNode * F12 );
123 
124 
125 /*=== extraZddLitCount.c ==============================================================*/
126 
127 /* count the number of times each variable occurs in the combinations */
128 extern int * Extra_zddLitCount( DdManager * dd, DdNode * Set );
129 /* count the number of literals in one ZDD combination */
130 extern int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb );
131 
132 /*=== extraZddMaxMin.c ==============================================================*/
133 
134 /* maximal/minimimal */
135 extern DdNode * Extra_zddMaximal( DdManager *dd, DdNode * S );
136 
137 extern DdNode * Extra_zddMinimal( DdManager *dd, DdNode * S );
138 
139 /* maximal/minimal of the union of two sets of subsets */
140 extern DdNode * Extra_zddMaxUnion( DdManager *dd, DdNode * S, DdNode * T );
141 
142 extern DdNode * Extra_zddMinUnion( DdManager *dd, DdNode * S, DdNode * T );
143 
144 /* dot/cross products */
145 extern DdNode * Extra_zddDotProduct( DdManager *dd, DdNode * S, DdNode * T );
146 
147 extern DdNode * Extra_zddExorProduct( DdManager *dd, DdNode * S, DdNode * T );
148 
149 extern DdNode * Extra_zddCrossProduct( DdManager *dd, DdNode * S, DdNode * T );
150 
151 extern DdNode * Extra_zddMaxDotProduct( DdManager *dd, DdNode * S, DdNode * T );
152 
153 
154 /*=== extraZddMisc.c ==============================================================*/
155 
156 /* create the combination composed of a single ZDD variable */
157 extern DdNode * Extra_zddVariable( DdManager * dd, int iVar );
158 /* build a ZDD for a combination of variables */
159 extern DdNode * Extra_zddCombination( DdManager *dd, int* VarValues, int nVars );
160 
161 /* the set of all possible combinations of the given set of variables */
162 extern DdNode * Extra_zddUniverse( DdManager * dd, DdNode * VarSet );
163 
164 /* build the set of all tuples of K variables out of N */
165 extern DdNode * Extra_zddTuples( DdManager * dd, int K, DdNode * zVarsN );
166 
167 /* build the set of all tuples of K variables out of N from the BDD cube */
168 extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
169 
170 /* convert the set of singleton combinations into one combination */
171 extern DdNode * Extra_zddSinglesToComb( DdManager * dd, DdNode * Singles );
172 
173 /* returns the set of combinations containing the max/min number of elements */
174 extern DdNode * Extra_zddMaximum( DdManager * dd, DdNode * S, int * nVars );
175 
176 extern DdNode * Extra_zddMinimum( DdManager * dd, DdNode * S, int * nVars );
177 
178 /* returns the random set of k combinations of n elements with average density d */
179 extern DdNode * Extra_zddRandomSet( DdManager * dd, int n, int k, double d );
180 /* other utilities */
181 extern DdNode * Extra_zddCoveredByArea( DdManager *dd, DdNode * zC, DdNode * bA );
182 
183 extern DdNode * Extra_zddNotCoveredByCover( DdManager *dd, DdNode * zC, DdNode * zD );
184 
185 extern DdNode * Extra_zddOverlappingWithArea( DdManager *dd, DdNode * zC, DdNode * bA );
186 
187 extern DdNode * Extra_zddConvertToBdd( DdManager *dd, DdNode * zC );
188 
189 extern DdNode * Extra_zddConvertToBddUnate( DdManager *dd, DdNode * zC );
190 
191 extern DdNode * Extra_zddConvertEsopToBdd( DdManager *dd, DdNode * zC );
192 
193 extern DdNode * Extra_zddConvertToBddAndAdd( DdManager *dd, DdNode * zC, DdNode * bA );
194 
195 extern DdNode * Extra_zddSingleCoveredArea( DdManager *dd, DdNode * zC );
196 
197 extern DdNode * Extra_zddConvertBddCubeIntoZddCube( DdManager *dd, DdNode * bCube );
198 
199 /*=== extraZddPermute.c ==============================================================*/
200 
201 /* quantifications */
202 extern DdNode * Extra_zddExistAbstract( DdManager *manager, DdNode * F, DdNode * cube );
203 
204 /* changes the value of several variables in the ZDD */
205 extern DdNode * Extra_zddChangeVars( DdManager *manager, DdNode * F, DdNode * cube );
206 
207 /* permutes variables in ZDD */
208 extern DdNode * Extra_zddPermute ( DdManager *dd, DdNode * N, int *permut );
209 /* computes combinations in F with vars in Cube having the negative polarity */
210 extern DdNode * Extra_zddCofactor0( DdManager * dd, DdNode * f, DdNode * cube );
211 
212 /* computes combinations in F with vars in Cube having the positive polarity */
213 extern DdNode * Extra_zddCofactor1( DdManager * dd, DdNode * f, DdNode * cube, int fIncludeVars );
214 
215 
216 /*=== extraZddSubSup.c ==============================================================*/
217 
218 /* subset/supset operations */
219 extern DdNode * Extra_zddSubSet ( DdManager *dd, DdNode * X, DdNode * Y );
220 
221 extern DdNode * Extra_zddSupSet ( DdManager *dd, DdNode * X, DdNode * Y );
222 
223 extern DdNode * Extra_zddNotSubSet( DdManager *dd, DdNode * X, DdNode * Y );
224 
225 extern DdNode * Extra_zddNotSupSet( DdManager *dd, DdNode * X, DdNode * Y );
226 
227 extern DdNode * Extra_zddMaxNotSupSet( DdManager *dd, DdNode * X, DdNode * Y );
228 
229 /* check whether the empty combination belongs to the set of subsets */
230 extern int Extra_zddEmptyBelongs ( DdManager *dd, DdNode* zS );
231 /* check whether the set consists of one subset only */
232 extern int Extra_zddIsOneSubset( DdManager *dd, DdNode* zS );
233 
234 }
235 
236 
237 #endif