ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraBdd.h
Go to the documentation of this file.
1
28
29#ifndef ABC__misc__extra__extra_bdd_h
30#define ABC__misc__extra__extra_bdd_h
31
32
33#ifdef _WIN32
34#define inline __inline // compatible with MS VS 6.0
35#endif
36
37/*---------------------------------------------------------------------------*/
38/* Nested includes */
39/*---------------------------------------------------------------------------*/
40
41#include <stdio.h>
42#include <stdlib.h>
43#include <string.h>
44#include <assert.h>
45
46#include "misc/st/st.h"
47#include "bdd/cudd/cuddInt.h"
48#include "misc/extra/extra.h"
49
50
51ABC_NAMESPACE_HEADER_START
52
53
54/*---------------------------------------------------------------------------*/
55/* Constant declarations */
56/*---------------------------------------------------------------------------*/
57
58/*---------------------------------------------------------------------------*/
59/* Stucture declarations */
60/*---------------------------------------------------------------------------*/
61
62/*---------------------------------------------------------------------------*/
63/* Type declarations */
64/*---------------------------------------------------------------------------*/
65
66/*---------------------------------------------------------------------------*/
67/* Variable declarations */
68/*---------------------------------------------------------------------------*/
69
70/*---------------------------------------------------------------------------*/
71/* Macro declarations */
72/*---------------------------------------------------------------------------*/
73
74/* constants of the manager */
75#define b0 Cudd_Not((dd)->one)
76#define b1 (dd)->one
77#define z0 (dd)->zero
78#define z1 (dd)->one
79#define a0 (dd)->zero
80#define a1 (dd)->one
81
82// hash key macros
83#define hashKey1(a,TSIZE) \
84((ABC_PTRUINT_T)(a) % TSIZE)
85
86#define hashKey2(a,b,TSIZE) \
87(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
88
89#define hashKey3(a,b,c,TSIZE) \
90(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
91
92#define hashKey4(a,b,c,d,TSIZE) \
93((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
94 (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
95
96#define hashKey5(a,b,c,d,e,TSIZE) \
97(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
98 (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
99
100/*===========================================================================*/
101/* Various Utilities */
102/*===========================================================================*/
103
104/*=== extraBddAuto.c ========================================================*/
105
106extern DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc );
107extern DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
108extern DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG );
109extern DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
110extern DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc );
111extern DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
112extern DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc );
113
114extern DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
115extern DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace );
116
117extern DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace );
118extern DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
119extern DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace );
120extern DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
121extern DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace );
122
123extern DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
124extern DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA );
125extern DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
126extern DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
127
128extern DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
129extern DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
130
131/*=== extraBddCas.c =============================================================*/
132
133/* performs the binary encoding of the set of function using the given vars */
134extern DdNode * Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
135/* solves the column encoding problem using a sophisticated method */
136extern DdNode * Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
137/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
138extern st__table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
139/* collects the nodes under the cut starting from the given set of ADD nodes */
140extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
141/* find the profile of a DD (the number of edges crossing each level) */
142extern int Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
143
144/*=== extraBddImage.c ================================================================*/
145
146typedef struct Extra_ImageTree_t_ Extra_ImageTree_t;
147extern Extra_ImageTree_t * Extra_bddImageStart(
148 DdManager * dd, DdNode * bCare,
149 int nParts, DdNode ** pbParts,
150 int nVars, DdNode ** pbVars, int fVerbose );
151extern DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
152extern void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
153extern DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree );
154
155typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t;
156extern Extra_ImageTree2_t * Extra_bddImageStart2(
157 DdManager * dd, DdNode * bCare,
158 int nParts, DdNode ** pbParts,
159 int nVars, DdNode ** pbVars, int fVerbose );
160extern DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
161extern void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
162extern DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
163
164/*=== extraBddMisc.c ========================================================*/
165
166extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
167extern DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
168extern DdNode * Extra_bddRemapUp( DdManager * dd, DdNode * bF );
169extern DdNode * Extra_bddMove( DdManager * dd, DdNode * bF, int nVars );
170extern DdNode * extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag );
171extern void Extra_StopManager( DdManager * dd );
172extern void Extra_bddPrint( DdManager * dd, DdNode * F );
173extern void Extra_bddPrintSupport( DdManager * dd, DdNode * F );
174extern void extraDecomposeCover( DdManager* dd, DdNode* zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 );
175extern int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp );
176extern int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar );
177extern int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 );
178extern int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax );
179extern int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall );
180extern int * Extra_SupportArray( DdManager * dd, DdNode * F, int * support );
181extern int * Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
182extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
183extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
184extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
185extern DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
186extern DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f );
187extern int Extra_bddIsVar( DdNode * bFunc );
188extern DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars );
189extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars );
190extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars );
191extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F );
192extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
193extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
194extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
195extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
196extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar );
197extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
198extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide );
199extern void Extra_zddDumpPla( DdManager * dd, DdNode * zCover, int nVars, char * pFileName );
200
201/* build the set of all tuples of K variables out of N */
202extern DdNode * Extra_bddTuples( DdManager * dd, int K, DdNode * bVarsN );
203extern DdNode * extraBddTuples( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
204
205#ifndef ABC_PRB
206#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
207#endif
208
209/*=== extraMaxMin.c ==============================================================*/
210
211/* maximal/minimimal */
212extern DdNode * Extra_zddMaximal (DdManager *dd, DdNode *S);
213extern DdNode * extraZddMaximal (DdManager *dd, DdNode *S);
214extern DdNode * Extra_zddMinimal (DdManager *dd, DdNode *S);
215extern DdNode * extraZddMinimal (DdManager *dd, DdNode *S);
216/* maximal/minimal of the union of two sets of subsets */
217extern DdNode * Extra_zddMaxUnion (DdManager *dd, DdNode *S, DdNode *T);
218extern DdNode * extraZddMaxUnion (DdManager *dd, DdNode *S, DdNode *T);
219extern DdNode * Extra_zddMinUnion (DdManager *dd, DdNode *S, DdNode *T);
220extern DdNode * extraZddMinUnion (DdManager *dd, DdNode *S, DdNode *T);
221/* dot/cross products */
222extern DdNode * Extra_zddDotProduct (DdManager *dd, DdNode *S, DdNode *T);
223extern DdNode * extraZddDotProduct (DdManager *dd, DdNode *S, DdNode *T);
224extern DdNode * Extra_zddCrossProduct (DdManager *dd, DdNode *S, DdNode *T);
225extern DdNode * extraZddCrossProduct (DdManager *dd, DdNode *S, DdNode *T);
226extern DdNode * Extra_zddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T);
227extern DdNode * extraZddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T);
228
229/*=== extraBddSet.c ==============================================================*/
230
231/* subset/supset operations */
232extern DdNode * Extra_zddSubSet (DdManager *dd, DdNode *X, DdNode *Y);
233extern DdNode * extraZddSubSet (DdManager *dd, DdNode *X, DdNode *Y);
234extern DdNode * Extra_zddSupSet (DdManager *dd, DdNode *X, DdNode *Y);
235extern DdNode * extraZddSupSet (DdManager *dd, DdNode *X, DdNode *Y);
236extern DdNode * Extra_zddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y);
237extern DdNode * extraZddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y);
238extern DdNode * Extra_zddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y);
239extern DdNode * extraZddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y);
240extern DdNode * Extra_zddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y);
241extern DdNode * extraZddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y);
242/* check whether the empty combination belongs to the set of subsets */
243extern int Extra_zddEmptyBelongs (DdManager *dd, DdNode* zS);
244/* check whether the set consists of one subset only */
245extern int Extra_zddIsOneSubset (DdManager *dd, DdNode* zS);
246
247/*=== extraBddKmap.c ================================================================*/
248
249/* displays the Karnaugh Map of a function */
250extern void Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
251/* displays the Karnaugh Map of a relation */
252extern void Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
253
254/*=== extraBddSymm.c =================================================================*/
255
256typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t;
257struct Extra_SymmInfo_t_ {
258 int nVars; // the number of variables in the support
259 int nVarsMax; // the number of variables in the DD manager
260 int nSymms; // the number of pair-wise symmetries
261 int nNodes; // the number of nodes in a ZDD (if applicable)
262 int * pVars; // the list of all variables present in the support
263 char ** pSymms; // the symmetry information
264};
265
266/* computes the classical symmetry information for the function - recursive */
267extern Extra_SymmInfo_t * Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
268/* computes the classical symmetry information for the function - using naive approach */
269extern Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
270extern int Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
271
272/* allocates the data structure */
273extern Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars );
274/* deallocates the data structure */
275extern void Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
276/* print the contents the data structure */
277extern void Extra_SymmPairsPrint( Extra_SymmInfo_t * );
278/* converts the ZDD into the Extra_SymmInfo_t structure */
279extern Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
280
281/* computes the classical symmetry information as a ZDD */
282extern DdNode * Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
283extern DdNode * extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
284/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
285extern DdNode * Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
286extern DdNode * extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
287/* converts a set of variables into a set of singleton subsets */
288extern DdNode * Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
289extern DdNode * extraZddGetSingletons( DdManager * dd, DdNode * bVars );
290/* filters the set of variables using the support of the function */
291extern DdNode * Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
292extern DdNode * extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
293
294/* checks the possibility that the two vars are symmetric */
295extern int Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
296extern DdNode * extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
297
298/* build the set of all tuples of K variables out of N from the BDD cube */
299extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
300extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
301/* selects one subset from a ZDD representing the set of subsets */
302extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
303extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
304
305/*=== extraBddUnate.c =================================================================*/
306
307extern DdNode * Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut );
308extern DdNode * Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut );
309extern DdNode * Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut );
310
311/*=== extraBddUnate.c =================================================================*/
312
313typedef struct Extra_UnateVar_t_ Extra_UnateVar_t;
314struct Extra_UnateVar_t_ {
315 unsigned iVar : 30; // index of the variable
316 unsigned Pos : 1; // 1 if positive unate
317 unsigned Neg : 1; // 1 if negative unate
318};
319
320typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t;
321struct Extra_UnateInfo_t_ {
322 int nVars; // the number of variables in the support
323 int nVarsMax; // the number of variables in the DD manager
324 int nUnate; // the number of unate variables
325 Extra_UnateVar_t * pVars; // the array of variables present in the support
326};
327
328/* allocates the data structure */
329extern Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars );
330/* deallocates the data structure */
331extern void Extra_UnateInfoDissolve( Extra_UnateInfo_t * );
332/* print the contents the data structure */
333extern void Extra_UnateInfoPrint( Extra_UnateInfo_t * );
334/* converts the ZDD into the Extra_SymmInfo_t structure */
335extern Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars );
336/* naive check of unateness of one variable */
337extern int Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar );
338
339/* computes the unateness information for the function */
340extern Extra_UnateInfo_t * Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc );
341extern Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc );
342
343/* computes the classical symmetry information as a ZDD */
344extern DdNode * Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
345extern DdNode * extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
346
347/* converts a set of variables into a set of singleton subsets */
348extern DdNode * Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
349extern DdNode * extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars );
350
352
353
354
355ABC_NAMESPACE_HEADER_END
356
357
358
359#endif /* __EXTRA_H__ */
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition abc_namespaces.h:51
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition abc_namespaces.h:50
Code
#define Code
Definition deflate.h:76
Extra_bddBitsToCube
DdNode * Extra_bddBitsToCube(DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
Definition extraBddMisc.c:730
Extra_bddSpaceEquationsPos
DdNode * Extra_bddSpaceEquationsPos(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:387
Extra_zddNotSubSet
DdNode * Extra_zddNotSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:165
Extra_zddMaximal
DdNode * Extra_zddMaximal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:101
extraZddMaximal
DdNode * extraZddMaximal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:294
Extra_SymmInfo_t
struct Extra_SymmInfo_t_ Extra_SymmInfo_t
Definition extraBdd.h:256
Extra_bddImageCompute2
DdNode * Extra_bddImageCompute2(Extra_ImageTree2_t *pTree, DdNode *bCare)
Definition extraBddImage.c:1108
extraZddSelectOneSubset
DdNode * extraZddSelectOneSubset(DdManager *dd, DdNode *zS)
Definition extraBddSymm.c:1419
extraBddCheckVarsSymmetric
DdNode * extraBddCheckVarsSymmetric(DdManager *dd, DdNode *bF, DdNode *bVars)
Definition extraBddSymm.c:1169
extraZddMinimal
DdNode * extraZddMinimal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:373
Extra_SymmPairsComputeNaive
Extra_SymmInfo_t * Extra_SymmPairsComputeNaive(DdManager *dd, DdNode *bFunc)
Definition extraBddSymm.c:396
Extra_ImageTree_t
struct Extra_ImageTree_t_ Extra_ImageTree_t
Definition extraBdd.h:146
Extra_bddSpaceFromFunction
DdNode * Extra_bddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition extraBddAuto.c:253
Extra_UnateInfoDissolve
void Extra_UnateInfoDissolve(Extra_UnateInfo_t *)
Definition extraBddUnate.c:178
extraDecomposeCover
void extraDecomposeCover(DdManager *dd, DdNode *zC, DdNode **zC0, DdNode **zC1, DdNode **zC2)
Definition extraBddMisc.c:1217
Extra_zddEmptyBelongs
int Extra_zddEmptyBelongs(DdManager *dd, DdNode *zS)
Definition extraBddSet.c:265
Extra_zddSymmPairsCompute
DdNode * Extra_zddSymmPairsCompute(DdManager *dd, DdNode *bF, DdNode *bVars)
Definition extraBddSymm.c:105
extraZddMaxNotSupSet
DdNode * extraZddMaxNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:799
Extra_UnateComputeFast
Extra_UnateInfo_t * Extra_UnateComputeFast(DdManager *dd, DdNode *bFunc)
Definition extraBddUnate.c:73
extraBddSpaceFromMatrixPos
DdNode * extraBddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:1333
extraZddMaxDotProduct
DdNode * extraZddMaxDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:938
Extra_bddImageStart2
Extra_ImageTree2_t * Extra_bddImageStart2(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition extraBddImage.c:1066
Extra_bddSpaceFromMatrixPos
DdNode * Extra_bddSpaceFromMatrixPos(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:431
Extra_bddNodePathsUnderCut
st__table * Extra_bddNodePathsUnderCut(DdManager *dd, DdNode *bFunc, int CutLevel)
Definition extraBddCas.c:263
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition extraBddMisc.c:223
extraZddSubSet
DdNode * extraZddSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:319
Extra_bddComputeCube
DdNode * Extra_bddComputeCube(DdManager *dd, DdNode **bXVars, int nVars)
Definition extraBddMisc.c:1001
Extra_bddReduceVarSet
DdNode * Extra_bddReduceVarSet(DdManager *dd, DdNode *bVars, DdNode *bF)
Definition extraBddSymm.c:181
extraZddGetSingletons
DdNode * extraZddGetSingletons(DdManager *dd, DdNode *bVars)
Definition extraBddSymm.c:1001
Extra_bddCreateOr
DdNode * Extra_bddCreateOr(DdManager *dd, int nVars)
Definition extraBddMisc.c:883
Extra_UnateInfo_t
struct Extra_UnateInfo_t_ Extra_UnateInfo_t
Definition extraBdd.h:320
Extra_bddSuppSize
int Extra_bddSuppSize(DdManager *dd, DdNode *bSupp)
Definition extraBddMisc.c:321
Extra_bddCheckVarsSymmetric
int Extra_bddCheckVarsSymmetric(DdManager *dd, DdNode *bF, int iVar1, int iVar2)
Definition extraBddSymm.c:360
extraBddSpaceEquationsPos
DdNode * extraBddSpaceEquationsPos(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:1071
Extra_zddPrimes
DdNode * Extra_zddPrimes(DdManager *dd, DdNode *F)
Definition extraBddMisc.c:933
extraZddNotSubSet
DdNode * extraZddNotSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:550
Extra_bddVarIsInCube
int Extra_bddVarIsInCube(DdNode *bCube, int iVar)
Definition extraBddMisc.c:1056
Extra_bddSuppOverlapping
int Extra_bddSuppOverlapping(DdManager *dd, DdNode *S1, DdNode *S2)
Definition extraBddMisc.c:365
extraBddSpaceCanonVars
DdNode * extraBddSpaceCanonVars(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:1000
Extra_bddCreateAnd
DdNode * Extra_bddCreateAnd(DdManager *dd, int nVars)
Definition extraBddMisc.c:858
Extra_bddIsVar
int Extra_bddIsVar(DdNode *bFunc)
Definition extraBddMisc.c:839
Extra_bddSupportNegativeCube
DdNode * Extra_bddSupportNegativeCube(DdManager *dd, DdNode *f)
Definition extraBddMisc.c:764
extraBddReduceVarSet
DdNode * extraBddReduceVarSet(DdManager *dd, DdNode *bVars, DdNode *bF)
Definition extraBddSymm.c:1062
Extra_bddSuppContainVar
int Extra_bddSuppContainVar(DdManager *dd, DdNode *bS, DdNode *bVar)
Definition extraBddMisc.c:346
Extra_bddImageRead
DdNode * Extra_bddImageRead(Extra_ImageTree_t *pTree)
Definition extraBddImage.c:292
Extra_bddImageTreeDelete2
void Extra_bddImageTreeDelete2(Extra_ImageTree2_t *pTree)
Definition extraBddImage.c:1128
Extra_UnateInfoCreateFromZdd
Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd(DdManager *dd, DdNode *zUnate, DdNode *bVars)
Definition extraBddUnate.c:227
Extra_TransferPermute
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition extraBddMisc.c:87
extraZddNotSupSet
DdNode * extraZddNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:676
Extra_bddCreateExor
DdNode * Extra_bddCreateExor(DdManager *dd, int nVars)
Definition extraBddMisc.c:908
Extra_bddImageStart
Extra_ImageTree_t * Extra_bddImageStart(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition extraBddImage.c:156
Extra_UnateComputeSlow
Extra_UnateInfo_t * Extra_UnateComputeSlow(DdManager *dd, DdNode *bFunc)
Definition extraBddUnate.c:293
Extra_bddPrint
void Extra_bddPrint(DdManager *dd, DdNode *F)
Definition extraBddMisc.c:246
extraZddGetSymmetricVars
DdNode * extraZddGetSymmetricVars(DdManager *dd, DdNode *bF, DdNode *bG, DdNode *bVars)
Definition extraBddSymm.c:804
Extra_bddTuples
DdNode * Extra_bddTuples(DdManager *dd, int K, DdNode *bVarsN)
Definition extraBddMisc.c:2691
Extra_zddNotSupSet
DdNode * Extra_zddNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:198
extraZddSymmPairsCompute
DdNode * extraZddSymmPairsCompute(DdManager *dd, DdNode *bF, DdNode *bVars)
Definition extraBddSymm.c:580
Extra_bddSpaceCanonVars
DdNode * Extra_bddSpaceCanonVars(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:316
Extra_bddCheckUnateNaive
int Extra_bddCheckUnateNaive(DdManager *dd, DdNode *bF, int iVar)
Definition extraBddUnate.c:338
Extra_bddPermuteArray
void Extra_bddPermuteArray(DdManager *dd, DdNode **bNodesIn, DdNode **bNodesOut, int nNodes, int *permut)
Definition extraBddMisc.c:961
Extra_zddDotProduct
DdNode * Extra_zddDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:208
Extra_bddSpaceFromFunctionNeg
DdNode * Extra_bddSpaceFromFunctionNeg(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:295
Extra_bddSpaceExorGates
DdNode ** Extra_bddSpaceExorGates(DdManager *dd, DdNode *bFuncRed, DdNode *zEquations)
Definition extraBddAuto.c:497
extraZddDotProduct
DdNode * extraZddDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:672
extraBddTuples
DdNode * extraBddTuples(DdManager *dd, DdNode *bVarsK, DdNode *bVarsN)
Definition extraBddMisc.c:2597
Extra_zddMinimal
DdNode * Extra_zddMinimal(DdManager *dd, DdNode *S)
Definition extraBddMaxMin.c:127
Extra_ImageTree2_t
struct Extra_ImageTree2_t_ Extra_ImageTree2_t
Definition extraBdd.h:155
Extra_ProfileWidth
int Extra_ProfileWidth(DdManager *dd, DdNode *F, int *Profile, int CutLevel)
Definition extraBddCas.c:519
Extra_bddSpaceFromMatrixNeg
DdNode * Extra_bddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:452
extraBddSpaceFromMatrixNeg
DdNode * extraBddSpaceFromMatrixNeg(DdManager *dd, DdNode *zA)
Definition extraBddAuto.c:1451
Extra_zddMaxUnion
DdNode * Extra_zddMaxUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:153
Extra_PrintKMapRelation
void Extra_PrintKMapRelation(FILE *pFile, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nXVars, int nYVars, DdNode **XVars, DdNode **YVars)
Definition extraBddKmap.c:581
Extra_TransferPermuteTime
DdNode * Extra_TransferPermuteTime(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute, int TimeOut)
Definition extraBddTime.c:150
Extra_UnateInfoAllocate
Extra_UnateInfo_t * Extra_UnateInfoAllocate(int nVars)
Definition extraBddUnate.c:155
Extra_bddRemapUp
DdNode * Extra_bddRemapUp(DdManager *dd, DdNode *bF)
Definition extraBddMisc.c:145
Extra_zddUnateInfoCompute
DdNode * Extra_zddUnateInfoCompute(DdManager *dd, DdNode *bF, DdNode *bVars)
Definition extraBddUnate.c:105
Extra_bddSpaceFromFunctionPos
DdNode * Extra_bddSpaceFromFunctionPos(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:274
Extra_zddTuplesFromBdd
DdNode * Extra_zddTuplesFromBdd(DdManager *dd, int K, DdNode *bVarsN)
Definition extraBddSymm.c:488
Extra_bddComputeRangeCube
DdNode * Extra_bddComputeRangeCube(DdManager *dd, int iStart, int iStop)
Definition extraBddMisc.c:699
Extra_bddFindOneCube
DdNode * Extra_bddFindOneCube(DdManager *dd, DdNode *bF)
Definition extraBddMisc.c:605
extraZddSupSet
DdNode * extraZddSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:430
Extra_bddMove
DdNode * Extra_bddMove(DdManager *dd, DdNode *bF, int nVars)
Definition extraBddMisc.c:187
Extra_bddSuppDifferentVars
int Extra_bddSuppDifferentVars(DdManager *dd, DdNode *S1, DdNode *S2, int DiffMax)
Definition extraBddMisc.c:393
Extra_UnateVar_t
struct Extra_UnateVar_t_ Extra_UnateVar_t
Definition extraBdd.h:313
Extra_bddSpaceEquations
DdNode * Extra_bddSpaceEquations(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:361
extraZddCrossProduct
DdNode * extraZddCrossProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:799
Extra_VectorSupportArray
int * Extra_VectorSupportArray(DdManager *dd, DdNode **F, int n, int *support)
Definition extraBddMisc.c:572
Extra_SymmPairsCreateFromZdd
Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd(DdManager *dd, DdNode *zPairs, DdNode *bVars)
Definition extraBddSymm.c:288
Extra_bddAndTime
DdNode * Extra_bddAndTime(DdManager *dd, DdNode *f, DdNode *g, int TimeOut)
Definition extraBddTime.c:83
Extra_bddAndPermute
DdNode * Extra_bddAndPermute(DdManager *ddF, DdNode *bF, DdManager *ddG, DdNode *bG, int *pPermute)
Definition extraBddMisc.c:1090
extraZddGetSingletonsBoth
DdNode * extraZddGetSingletonsBoth(DdManager *dd, DdNode *bVars)
Definition extraBddUnate.c:570
Extra_TransferLevelByLevel
DdNode * Extra_TransferLevelByLevel(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition extraBddMisc.c:112
Extra_zddIsOneSubset
int Extra_zddIsOneSubset(DdManager *dd, DdNode *zS)
Definition extraBddSet.c:288
Extra_bddNodePathsUnderCutArray
int Extra_bddNodePathsUnderCutArray(DdManager *dd, DdNode **paNodes, DdNode **pbCubes, int nNodes, DdNode **paNodesRes, DdNode **pbCubesRes, int CutLevel)
Definition extraBddCas.c:355
extraBddSpaceFromFunctionPos
DdNode * extraBddSpaceFromFunctionPos(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:738
Extra_SymmPairsCompute
Extra_SymmInfo_t * Extra_SymmPairsCompute(DdManager *dd, DdNode *bFunc)
Definition extraBddSymm.c:73
Extra_zddGetSymmetricVars
DdNode * Extra_zddGetSymmetricVars(DdManager *dd, DdNode *bF, DdNode *bG, DdNode *bVars)
Definition extraBddSymm.c:130
extraZddMinUnion
DdNode * extraZddMinUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:564
Extra_zddMinUnion
DdNode * Extra_zddMinUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:180
Extra_zddGetSingletons
DdNode * Extra_zddGetSingletons(DdManager *dd, DdNode *bVars)
Definition extraBddSymm.c:157
extraBddSpaceFromFunction
DdNode * extraBddSpaceFromFunction(DdManager *dd, DdNode *bF, DdNode *bG)
Definition extraBddAuto.c:562
Extra_zddGetSingletonsBoth
DdNode * Extra_zddGetSingletonsBoth(DdManager *dd, DdNode *bVars)
Definition extraBddUnate.c:131
Extra_SymmPairsPrint
void Extra_SymmPairsPrint(Extra_SymmInfo_t *)
Definition extraBddSymm.c:257
Extra_bddImageTreeDelete
void Extra_bddImageTreeDelete(Extra_ImageTree_t *pTree)
Definition extraBddImage.c:273
Extra_SymmPairsDissolve
void Extra_SymmPairsDissolve(Extra_SymmInfo_t *)
Definition extraBddSymm.c:238
extraBddSpaceFromFunctionNeg
DdNode * extraBddSpaceFromFunctionNeg(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:869
Extra_PrintKMap
void Extra_PrintKMap(FILE *pFile, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nVars, DdNode **XVars, int fSuppType, char **pVarNames)
Definition extraBddKmap.c:201
extraBddSpaceEquationsNeg
DdNode * extraBddSpaceEquationsNeg(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:1201
Extra_zddSelectOneSubset
DdNode * Extra_zddSelectOneSubset(DdManager *dd, DdNode *zS)
Definition extraBddSymm.c:546
extraZddMaxUnion
DdNode * extraZddMaxUnion(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:454
Extra_bddCountCubes
int Extra_bddCountCubes(DdManager *dd, DdNode **pFuncs, int nFuncs, int fMode, int nLimit, int *pGuide)
Definition extraBddMisc.c:1485
Extra_zddSupSet
DdNode * Extra_zddSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:133
extraZddUnateInfoCompute
DdNode * extraZddUnateInfoCompute(DdManager *dd, DdNode *bF, DdNode *bVars)
Definition extraBddUnate.c:385
Extra_zddMaxNotSupSet
DdNode * Extra_zddMaxNotSupSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:232
Extra_bddSpaceReduce
DdNode * Extra_bddSpaceReduce(DdManager *dd, DdNode *bFunc, DdNode *bCanonVars)
Definition extraBddAuto.c:337
Extra_bddImageCompute
DdNode * Extra_bddImageCompute(Extra_ImageTree_t *pTree, DdNode *bCare)
Definition extraBddImage.c:220
Extra_bddEncodingBinary
DdNode * Extra_bddEncodingBinary(DdManager *dd, DdNode **pbFuncs, int nFuncs, DdNode **pbVars, int nVars)
Definition extraBddCas.c:138
extraZddTuplesFromBdd
DdNode * extraZddTuplesFromBdd(DdManager *dd, DdNode *bVarsK, DdNode *bVarsN)
Definition extraBddSymm.c:1341
Extra_zddMaxDotProduct
DdNode * Extra_zddMaxDotProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:263
Extra_UnateInfoPrint
void Extra_UnateInfoPrint(Extra_UnateInfo_t *)
Definition extraBddUnate.c:195
Extra_zddCrossProduct
DdNode * Extra_zddCrossProduct(DdManager *dd, DdNode *S, DdNode *T)
Definition extraBddMaxMin.c:236
Extra_bddImageRead2
DdNode * Extra_bddImageRead2(Extra_ImageTree2_t *pTree)
Definition extraBddImage.c:1150
Extra_SupportArray
int * Extra_SupportArray(DdManager *dd, DdNode *F, int *support)
Definition extraBddMisc.c:537
extraBddMove
DdNode * extraBddMove(DdManager *dd, DdNode *bF, DdNode *bFlag)
Definition extraBddMisc.c:1128
Extra_bddGetOneCube
DdNode * Extra_bddGetOneCube(DdManager *dd, DdNode *bFunc)
Definition extraBddMisc.c:645
Extra_bddCheckVarsSymmetricNaive
int Extra_bddCheckVarsSymmetricNaive(DdManager *dd, DdNode *bF, int iVar1, int iVar2)
Definition extraBddSymm.c:443
Extra_bddEncodingNonStrict
DdNode * Extra_bddEncodingNonStrict(DdManager *dd, DdNode **pbColumns, int nColumns, DdNode *bVarsCol, DdNode **pCVars, int nMulti, int *pSimple)
Definition extraBddCas.c:184
Extra_zddSubSet
DdNode * Extra_zddSubSet(DdManager *dd, DdNode *X, DdNode *Y)
Definition extraBddSet.c:100
Extra_bddSpaceEquationsNeg
DdNode * Extra_bddSpaceEquationsNeg(DdManager *dd, DdNode *bSpace)
Definition extraBddAuto.c:409
Extra_bddSpaceFromFunctionFast
DdNode * Extra_bddSpaceFromFunctionFast(DdManager *dd, DdNode *bFunc)
Definition extraBddAuto.c:153
extraBddChangePolarity
DdNode * extraBddChangePolarity(DdManager *dd, DdNode *bFunc, DdNode *bVars)
Definition extraBddMisc.c:2041
Extra_bddAndAbstractTime
DdNode * Extra_bddAndAbstractTime(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int TimeOut)
Definition extraBddTime.c:117
Extra_bddSuppCheckContainment
int Extra_bddSuppCheckContainment(DdManager *dd, DdNode *bL, DdNode *bH, DdNode **bLarge, DdNode **bSmall)
Definition extraBddMisc.c:443
Extra_SymmPairsAllocate
Extra_SymmInfo_t * Extra_SymmPairsAllocate(int nVars)
Definition extraBddSymm.c:207
Extra_bddPrintSupport
void Extra_bddPrintSupport(DdManager *dd, DdNode *F)
Definition extraBddMisc.c:302
Extra_bddChangePolarity
DdNode * Extra_bddChangePolarity(DdManager *dd, DdNode *bFunc, DdNode *bVars)
Definition extraBddMisc.c:1029
Extra_zddDumpPla
void Extra_zddDumpPla(DdManager *dd, DdNode *zCover, int nVars, char *pFileName)
Definition extraBddMisc.c:2307
Extra_ImageTree2_t_
Definition extraBddImage.c:1048
Extra_ImageTree2_t_::dd
DdManager * dd
Definition extraBddImage.c:1049
Extra_ImageTree2_t_::bCube
DdNode * bCube
Definition extraBddImage.c:1051
Extra_ImageTree_t_
Definition extraBddImage.c:44
Extra_ImageTree_t_::fVerbose
int fVerbose
Definition extraBddImage.c:48
Extra_SymmInfo_t_
Definition extraBdd.h:257
Extra_SymmInfo_t_::nNodes
int nNodes
Definition extraBdd.h:261
Extra_SymmInfo_t_::nVars
int nVars
Definition extraBdd.h:258
Extra_SymmInfo_t_::pVars
int * pVars
Definition extraBdd.h:262
Extra_SymmInfo_t_::nSymms
int nSymms
Definition extraBdd.h:260
Extra_SymmInfo_t_::pSymms
char ** pSymms
Definition extraBdd.h:263
Extra_SymmInfo_t_::nVarsMax
int nVarsMax
Definition extraBdd.h:259
Extra_UnateInfo_t_
Definition extraBdd.h:321
Extra_UnateInfo_t_::pVars
Extra_UnateVar_t * pVars
Definition extraBdd.h:325
Extra_UnateInfo_t_::nUnate
int nUnate
Definition extraBdd.h:324
Extra_UnateInfo_t_::nVars
int nVars
Definition extraBdd.h:322
Extra_UnateInfo_t_::nVarsMax
int nVarsMax
Definition extraBdd.h:323
Extra_UnateVar_t_
Definition extraBdd.h:314
Extra_UnateVar_t_::Pos
unsigned Pos
Definition extraBdd.h:316
Extra_UnateVar_t_::Neg
unsigned Neg
Definition extraBdd.h:317
Extra_UnateVar_t_::iVar
unsigned iVar
Definition extraBdd.h:315
cube
Definition exor.h:123
st__table
Definition st.h:52