1 /**CFile****************************************************************
2
3 FileName [extraBddCas.c]
4
5 PackageName [extra]
6
7 Synopsis [Procedures related to LUT cascade synthesis.]
8
9 Author [Alan Mishchenko]
10
11 Affiliation [UC Berkeley]
12
13 Date [Ver. 2.0. Started - September 1, 2003.]
14
15 Revision [$Id: extraBddCas.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
16
17 ***********************************************************************/
18
19 #include "extraBdd.h"
20
21 ABC_NAMESPACE_IMPL_START
22
23
24 /*---------------------------------------------------------------------------*/
25 /* Constant declarations */
26 /*---------------------------------------------------------------------------*/
27
28 /*---------------------------------------------------------------------------*/
29 /* Stucture declarations */
30 /*---------------------------------------------------------------------------*/
31
32 /*---------------------------------------------------------------------------*/
33 /* Type declarations */
34 /*---------------------------------------------------------------------------*/
35
36 // the table to store cofactor operations
37 #define _TABLESIZE_COF 51113
38 typedef struct
39 {
40 unsigned Sign;
41 DdNode * Arg1;
42 } _HashEntry_cof;
43 _HashEntry_cof HHTable1[_TABLESIZE_COF];
44
45 // the table to store the result of computation of the number of minterms
46 #define _TABLESIZE_MINT 15113
47 typedef struct
48 {
49 DdNode * Arg1;
50 unsigned Arg2;
51 unsigned Res;
52 } _HashEntry_mint;
53 _HashEntry_mint HHTable2[_TABLESIZE_MINT];
54
55 typedef struct
56 {
57 int nEdges; // the number of in-coming edges of the node
58 DdNode * bSum; // the sum of paths of the incoming edges
59 } traventry;
60
61 // the signature used for hashing
62 static unsigned s_Signature = 1;
63
64 static int s_CutLevel = 0;
65
66 /*---------------------------------------------------------------------------*/
67 /* Variable declarations */
68 /*---------------------------------------------------------------------------*/
69
70 // because the proposed solution to the optimal encoding problem has exponential complexity
71 // we limit the depth of the branch and bound procedure to 5 levels
72 static int s_MaxDepth = 5;
73
74 static int s_nVarsBest; // the number of vars in the best ordering
75 static int s_VarOrderBest[32]; // storing the best ordering of vars in the "simple encoding"
76 static int s_VarOrderCur[32]; // storing the current ordering of vars
77
78 // the place to store the supports of the encoded function
79 static DdNode * s_Field[8][256]; // the size should be K, 2^K, where K is no less than MaxDepth
80 static DdNode * s_Encoded; // this is the original function
81 static DdNode * s_VarAll; // the set of all column variables
82 static int s_MultiStart; // the total number of encoding variables used
83 // the array field now stores the supports
84
85 static DdNode ** s_pbTemp; // the temporary storage for the columns
86
87 static int s_BackTracks;
88 static int s_BackTrackLimit = 100;
89
90 static DdNode * s_Terminal; // the terminal value for counting minterms
91
92
93 static int s_EncodingVarsLevel;
94
95
96 /*---------------------------------------------------------------------------*/
97 /* Macro declarations */
98 /*---------------------------------------------------------------------------*/
99
100
101 /**AutomaticStart*************************************************************/
102
103 /*---------------------------------------------------------------------------*/
104 /* Static function prototypes */
105 /*---------------------------------------------------------------------------*/
106
107 static DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars );
108 static void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level );
109 // functions called from EvaluateEncodings_rec()
110 static DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost );
111 static DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost );
112 unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll );
113 static unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max );
114
115 static void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st__table * Visited );
116 static void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st__table * Visited, st__table * CutNodes );
117
118 /**AutomaticEnd***************************************************************/
119
120
121 /*---------------------------------------------------------------------------*/
122 /* Definition of exported functions */
123 /*---------------------------------------------------------------------------*/
124
125 /**Function********************************************************************
126
127 Synopsis [Performs the binary encoding of the set of function using the given vars.]
128
129 Description [Performs a straight binary encoding of the set of functions using
130 the variable cubes formed from the given set of variables. ]
131
132 SideEffects []
133
134 SeeAlso []
135
136 ******************************************************************************/
137 DdNode *
Extra_bddEncodingBinary(DdManager * dd,DdNode ** pbFuncs,int nFuncs,DdNode ** pbVars,int nVars)138 Extra_bddEncodingBinary(
139 DdManager * dd,
140 DdNode ** pbFuncs, // pbFuncs is the array of columns to be encoded
141 int nFuncs, // nFuncs is the number of columns in the array
142 DdNode ** pbVars, // pbVars is the array of variables to use for the codes
143 int nVars ) // nVars is the column multiplicity, [log2(nFuncs)]
144 {
145 int i;
146 DdNode * bResult;
147 DdNode * bCube, * bTemp, * bProd;
148
149 assert( nVars >= Abc_Base2Log(nFuncs) );
150
151 bResult = b0; Cudd_Ref( bResult );
152 for ( i = 0; i < nFuncs; i++ )
153 {
154 bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 ); Cudd_Ref( bCube );
155 bProd = Cudd_bddAnd( dd, bCube, pbFuncs[i] ); Cudd_Ref( bProd );
156 Cudd_RecursiveDeref( dd, bCube );
157
158 bResult = Cudd_bddOr( dd, bProd, bTemp = bResult ); Cudd_Ref( bResult );
159 Cudd_RecursiveDeref( dd, bTemp );
160 Cudd_RecursiveDeref( dd, bProd );
161 }
162
163 Cudd_Deref( bResult );
164 return bResult;
165 } /* end of Extra_bddEncodingBinary */
166
167
168 /**Function********************************************************************
169
170 Synopsis [Solves the column encoding problem using a sophisticated method.]
171
172 Description [The encoding is based on the idea of deriving functions which
173 depend on only one variable, which corresponds to the case of non-disjoint
174 decompostion. It is assumed that the variables pCVars are ordered below the variables
175 representing the solumns, and the first variable pCVars[0] is the topmost one.]
176
177 SideEffects []
178
179 SeeAlso [Extra_bddEncodingBinary]
180
181 ******************************************************************************/
182
183 DdNode *
Extra_bddEncodingNonStrict(DdManager * dd,DdNode ** pbColumns,int nColumns,DdNode * bVarsCol,DdNode ** pCVars,int nMulti,int * pSimple)184 Extra_bddEncodingNonStrict(
185 DdManager * dd,
186 DdNode ** pbColumns, // pbColumns is the array of columns to be encoded;
187 int nColumns, // nColumns is the number of columns in the array
188 DdNode * bVarsCol, // bVarsCol is the cube of variables on which the columns depend
189 DdNode ** pCVars, // pCVars is the array of variables to use for the codes
190 int nMulti, // nMulti is the column multiplicity, [log2(nColumns)]
191 int * pSimple ) // pSimple gets the number of code variables taken from the input varibles without change
192 {
193 DdNode * bEncoded, * bResult;
194 int nVarsCol = Cudd_SupportSize(dd,bVarsCol);
195 abctime clk;
196
197 // cannot work with more that 32-bit codes
198 assert( nMulti < 32 );
199
200 // perform the preliminary encoding using the straight binary code
201 bEncoded = Extra_bddEncodingBinary( dd, pbColumns, nColumns, pCVars, nMulti ); Cudd_Ref( bEncoded );
202 //printf( "Node count = %d", Cudd_DagSize(bEncoded) );
203
204 // set the backgroup value for counting minterms
205 s_Terminal = b0;
206 // set the level of the encoding variables
207 s_EncodingVarsLevel = dd->invperm[pCVars[0]->index];
208
209 // the current number of backtracks
210 s_BackTracks = 0;
211 // the variables that are cofactored on the topmost level where everything starts (no vars)
212 s_Field[0][0] = b1;
213 // the size of the best set of "simple" encoding variables found so far
214 s_nVarsBest = 0;
215
216 // set the relation to be accessible to traversal procedures
217 s_Encoded = bEncoded;
218 // the set of all vars to be accessible to traversal procedures
219 s_VarAll = bVarsCol;
220 // the column multiplicity
221 s_MultiStart = nMulti;
222
223
224 clk = Abc_Clock();
225 // find the simplest encoding
226 if ( nColumns > 2 )
227 EvaluateEncodings_rec( dd, bVarsCol, nVarsCol, nMulti, 1 );
228 // printf( "The number of backtracks = %d\n", s_BackTracks );
229 // s_EncSearchTime += Abc_Clock() - clk;
230
231 // allocate the temporary storage for the columns
232 s_pbTemp = (DdNode **)ABC_ALLOC( char, nColumns * sizeof(DdNode *) );
233
234 // clk = Abc_Clock();
235 bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars ); Cudd_Ref( bResult );
236 // s_EncComputeTime += Abc_Clock() - clk;
237
238 // delocate the preliminarily encoded set
239 Cudd_RecursiveDeref( dd, bEncoded );
240 // Cudd_RecursiveDeref( dd, aEncoded );
241
242 ABC_FREE( s_pbTemp );
243
244 *pSimple = s_nVarsBest;
245 Cudd_Deref( bResult );
246 return bResult;
247 }
248
249 /**Function********************************************************************
250
251 Synopsis [Collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root.]
252
253 Description [The table returned contains the set of BDD nodes pointed to under the cut
254 and, for each node, the BDD of the sum of paths leading to this node from the root
255 The sums of paths in the table are referenced. CutLevel is the first DD level
256 considered to be under the cut.]
257
258 SideEffects []
259
260 SeeAlso [Extra_bddNodePaths]
261
262 ******************************************************************************/
Extra_bddNodePathsUnderCut(DdManager * dd,DdNode * bFunc,int CutLevel)263 st__table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel )
264 {
265 st__table * Visited; // temporary table to remember the visited nodes
266 st__table * CutNodes; // the result goes here
267 st__table * Result; // the result goes here
268 DdNode * aFunc;
269
270 s_CutLevel = CutLevel;
271
272 Result = st__init_table( st__ptrcmp, st__ptrhash);;
273 // the terminal cases
274 if ( Cudd_IsConstant( bFunc ) )
275 {
276 if ( bFunc == b1 )
277 {
278 st__insert( Result, (char*)b1, (char*)b1 );
279 Cudd_Ref( b1 );
280 Cudd_Ref( b1 );
281 }
282 else
283 {
284 st__insert( Result, (char*)b0, (char*)b0 );
285 Cudd_Ref( b0 );
286 Cudd_Ref( b0 );
287 }
288 return Result;
289 }
290
291 // create the ADD to simplify processing (no complemented edges)
292 aFunc = Cudd_BddToAdd( dd, bFunc ); Cudd_Ref( aFunc );
293
294 // Step 1: Start the tables and collect information about the nodes above the cut
295 // this information tells how many edges point to each node
296 Visited = st__init_table( st__ptrcmp, st__ptrhash);;
297 CutNodes = st__init_table( st__ptrcmp, st__ptrhash);;
298
299 CountNodeVisits_rec( dd, aFunc, Visited );
300
301 // Step 2: Traverse the BDD using the visited table and compute the sum of paths
302 CollectNodesAndComputePaths_rec( dd, aFunc, b1, Visited, CutNodes );
303
304 // at this point the table of cut nodes is ready and the table of visited is useless
305 {
306 st__generator * gen;
307 DdNode * aNode;
308 traventry * p;
309 st__foreach_item( Visited, gen, (const char**)&aNode, (char**)&p )
310 {
311 Cudd_RecursiveDeref( dd, p->bSum );
312 ABC_FREE( p );
313 }
314 st__free_table( Visited );
315 }
316
317 // go through the table CutNodes and create the BDD and the path to be returned
318 {
319 st__generator * gen;
320 DdNode * aNode, * bNode, * bSum;
321 st__foreach_item( CutNodes, gen, (const char**)&aNode, (char**)&bSum)
322 {
323 // aNode is not referenced, because aFunc is holding it
324 bNode = Cudd_addBddPattern( dd, aNode ); Cudd_Ref( bNode );
325 st__insert( Result, (char*)bNode, (char*)bSum );
326 // the new table takes both refs
327 }
328 st__free_table( CutNodes );
329 }
330
331 // dereference the ADD
332 Cudd_RecursiveDeref( dd, aFunc );
333
334 // return the table
335 return Result;
336
337 } /* end of Extra_bddNodePathsUnderCut */
338
339 /**Function********************************************************************
340
341 Synopsis [Collects the nodes under the cut in the ADD starting from the given set of ADD nodes.]
342
343 Description [Takes the array, paNodes, of ADD nodes to start the traversal,
344 the array, pbCubes, of BDD cubes to start the traversal with in each node,
345 and the number, nNodes, of ADD nodes and BDD cubes in paNodes and pbCubes.
346 Returns the number of columns found. Fills in paNodesRes (pbCubesRes)
347 with the set of ADD columns (BDD paths). These arrays should be allocated
348 by the user.]
349
350 SideEffects []
351
352 SeeAlso [Extra_bddNodePaths]
353
354 ******************************************************************************/
Extra_bddNodePathsUnderCutArray(DdManager * dd,DdNode ** paNodes,DdNode ** pbCubes,int nNodes,DdNode ** paNodesRes,DdNode ** pbCubesRes,int CutLevel)355 int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel )
356 {
357 st__table * Visited; // temporary table to remember the visited nodes
358 st__table * CutNodes; // the nodes under the cut go here
359 int i, Counter;
360
361 s_CutLevel = CutLevel;
362
363 // there should be some nodes
364 assert( nNodes > 0 );
365 if ( nNodes == 1 && Cudd_IsConstant( paNodes[0] ) )
366 {
367 if ( paNodes[0] == a1 )
368 {
369 paNodesRes[0] = a1; Cudd_Ref( a1 );
370 pbCubesRes[0] = pbCubes[0]; Cudd_Ref( pbCubes[0] );
371 }
372 else
373 {
374 paNodesRes[0] = a0; Cudd_Ref( a0 );
375 pbCubesRes[0] = pbCubes[0]; Cudd_Ref( pbCubes[0] );
376 }
377 return 1;
378 }
379
380 // Step 1: Start the table and collect information about the nodes above the cut
381 // this information tells how many edges point to each node
382 CutNodes = st__init_table( st__ptrcmp, st__ptrhash);;
383 Visited = st__init_table( st__ptrcmp, st__ptrhash);;
384
385 for ( i = 0; i < nNodes; i++ )
386 CountNodeVisits_rec( dd, paNodes[i], Visited );
387
388 // Step 2: Traverse the BDD using the visited table and compute the sum of paths
389 for ( i = 0; i < nNodes; i++ )
390 CollectNodesAndComputePaths_rec( dd, paNodes[i], pbCubes[i], Visited, CutNodes );
391
392 // at this point, the table of cut nodes is ready and the table of visited is useless
393 {
394 st__generator * gen;
395 DdNode * aNode;
396 traventry * p;
397 st__foreach_item( Visited, gen, (const char**)&aNode, (char**)&p )
398 {
399 Cudd_RecursiveDeref( dd, p->bSum );
400 ABC_FREE( p );
401 }
402 st__free_table( Visited );
403 }
404
405 // go through the table CutNodes and create the BDD and the path to be returned
406 {
407 st__generator * gen;
408 DdNode * aNode, * bSum;
409 Counter = 0;
410 st__foreach_item( CutNodes, gen, (const char**)&aNode, (char**)&bSum)
411 {
412 paNodesRes[Counter] = aNode; Cudd_Ref( aNode );
413 pbCubesRes[Counter] = bSum;
414 Counter++;
415 }
416 st__free_table( CutNodes );
417 }
418
419 // return the number of cofactors found
420 return Counter;
421
422 } /* end of Extra_bddNodePathsUnderCutArray */
423
424 /**Function*************************************************************
425
426 Synopsis [Collects all the BDD nodes into the table.]
427
428 Description []
429
430 SideEffects []
431
432 SeeAlso []
433
434 ***********************************************************************/
extraCollectNodes(DdNode * Func,st__table * tNodes)435 void extraCollectNodes( DdNode * Func, st__table * tNodes )
436 {
437 DdNode * FuncR;
438 FuncR = Cudd_Regular(Func);
439 if ( st__find_or_add( tNodes, (char*)FuncR, NULL ) )
440 return;
441 if ( cuddIsConstant(FuncR) )
442 return;
443 extraCollectNodes( cuddE(FuncR), tNodes );
444 extraCollectNodes( cuddT(FuncR), tNodes );
445 }
446
447 /**Function*************************************************************
448
449 Synopsis [Collects all the nodes of one DD into the table.]
450
451 Description []
452
453 SideEffects []
454
455 SeeAlso []
456
457 ***********************************************************************/
Extra_CollectNodes(DdNode * Func)458 st__table * Extra_CollectNodes( DdNode * Func )
459 {
460 st__table * tNodes;
461 tNodes = st__init_table( st__ptrcmp, st__ptrhash );
462 extraCollectNodes( Func, tNodes );
463 return tNodes;
464 }
465
466 /**Function*************************************************************
467
468 Synopsis [Updates the topmost level from which the given node is referenced.]
469
470 Description [Takes the table which maps each BDD nodes (including the constants)
471 into the topmost level on which this node counts as a cofactor. Takes the topmost
472 level, on which this node counts as a cofactor (see Extra_ProfileWidthFast().
473 Takes the node, for which the table entry should be updated.]
474
475 SideEffects []
476
477 SeeAlso []
478
479 ***********************************************************************/
extraProfileUpdateTopLevel(st__table * tNodeTopRef,int TopLevelNew,DdNode * node)480 void extraProfileUpdateTopLevel( st__table * tNodeTopRef, int TopLevelNew, DdNode * node )
481 {
482 int * pTopLevel;
483
484 if ( st__find_or_add( tNodeTopRef, (char*)node, (char***)&pTopLevel ) )
485 { // the node is already referenced
486 // the current top level should be updated if it is larger than the new level
487 if ( *pTopLevel > TopLevelNew )
488 *pTopLevel = TopLevelNew;
489 }
490 else
491 { // the node is not referenced
492 // its level should be set to the current new level
493 *pTopLevel = TopLevelNew;
494 }
495 }
496 /**Function*************************************************************
497
498 Synopsis [Fast computation of the BDD profile.]
499
500 Description [The array to store the profile is given by the user and should
501 contain at least as many entries as there is the maximum of the BDD/ZDD
502 size of the manager PLUS ONE.
503 When we say that the widths of the DD on level L is W, we mean the following.
504 Let us create the cut between the level L-1 and the level L and count the number
505 of different DD nodes pointed to across the cut. This number is the width W.
506 From this it follows the on level 0, the width is equal to the number of external
507 pointers to the considered DDs. If there is only one DD, then the profile on
508 level 0 is always 1. If this DD is rooted in the topmost variable, then the width
509 on level 1 is always 2, etc. The width at the level equal to dd->size is the
510 number of terminal nodes in the DD. (Because we consider the first level #0
511 and the last level #dd->size, the profile array should contain dd->size+1 entries.)
512 ]
513
514 SideEffects [This procedure will not work for BDDs w/ complement edges, only for ADDs and ZDDs]
515
516 SeeAlso []
517
518 ***********************************************************************/
Extra_ProfileWidth(DdManager * dd,DdNode * Func,int * pProfile,int CutLevel)519 int Extra_ProfileWidth( DdManager * dd, DdNode * Func, int * pProfile, int CutLevel )
520 {
521 st__generator * gen;
522 st__table * tNodeTopRef; // this table stores the top level from which this node is pointed to
523 st__table * tNodes;
524 DdNode * node;
525 DdNode * nodeR;
526 int LevelStart, Limit;
527 int i, size;
528 int WidthMax;
529
530 // start the mapping table
531 tNodeTopRef = st__init_table( st__ptrcmp, st__ptrhash);;
532 // add the topmost node to the profile
533 extraProfileUpdateTopLevel( tNodeTopRef, 0, Func );
534
535 // collect all nodes
536 tNodes = Extra_CollectNodes( Func );
537 // go though all the nodes and set the top level the cofactors are pointed from
538 // Cudd_ForeachNode( dd, Func, genDD, node )
539 st__foreach_item( tNodes, gen, (const char**)&node, NULL )
540 {
541 // assert( Cudd_Regular(node) ); // this procedure works only with ADD/ZDD (not BDD w/ compl.edges)
542 nodeR = Cudd_Regular(node);
543 if ( cuddIsConstant(nodeR) )
544 continue;
545 // this node is not a constant - consider its cofactors
546 extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddE(nodeR) );
547 extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddT(nodeR) );
548 }
549 st__free_table( tNodes );
550
551 // clean the profile
552 size = ddMax(dd->size, dd->sizeZ) + 1;
553 for ( i = 0; i < size; i++ )
554 pProfile[i] = 0;
555
556 // create the profile
557 st__foreach_item( tNodeTopRef, gen, (const char**)&node, (char**)&LevelStart )
558 {
559 nodeR = Cudd_Regular(node);
560 Limit = (cuddIsConstant(nodeR))? dd->size: dd->perm[nodeR->index];
561 for ( i = LevelStart; i <= Limit; i++ )
562 pProfile[i]++;
563 }
564
565 if ( CutLevel != -1 && CutLevel != 0 )
566 size = CutLevel;
567
568 // get the max width
569 WidthMax = 0;
570 for ( i = 0; i < size; i++ )
571 if ( WidthMax < pProfile[i] )
572 WidthMax = pProfile[i];
573
574 // deref the table
575 st__free_table( tNodeTopRef );
576
577 return WidthMax;
578 } /* end of Extra_ProfileWidth */
579
580
581 /*---------------------------------------------------------------------------*/
582 /* Definition of internal functions */
583 /*---------------------------------------------------------------------------*/
584
585 /*---------------------------------------------------------------------------*/
586 /* Definition of static functions */
587 /*---------------------------------------------------------------------------*/
588
589 /**Function********************************************************************
590
591 Synopsis [Computes the non-strict codes when evaluation is finished.]
592
593 Description [The information about the best code is stored in s_VarOrderBest,
594 which has s_nVarsBest entries.]
595
596 SideEffects [None]
597
598 ******************************************************************************/
CreateTheCodes_rec(DdManager * dd,DdNode * bEncoded,int Level,DdNode ** pCVars)599 DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars )
600 // bEncoded is the preliminarily encoded set of columns
601 // Level is the current level in the recursion
602 // pCVars are the variables to be used for encoding
603 {
604 DdNode * bRes;
605 if ( Level == s_nVarsBest )
606 { // the terminal case, when we need to remap the encoded function
607 // from the preliminary encoded variables to the new ones
608 st__table * CutNodes;
609 int nCols;
610 // double nMints;
611 /*
612 #ifdef _DEBUG
613
614 {
615 DdNode * bTemp;
616 // make sure that the given number of variables is enough
617 bTemp = Cudd_bddExistAbstract( dd, bEncoded, s_VarAll ); Cudd_Ref( bTemp );
618 // nMints = Cudd_CountMinterm( dd, bTemp, s_MultiStart );
619 nMints = Extra_CountMintermsSimple( bTemp, (1<<s_MultiStart) );
620 if ( nMints > Extra_Power2( s_MultiStart-Level ) )
621 { // the number of minterms is too large to encode the columns
622 // using the given minimum number of encoding variables
623 assert( 0 );
624 }
625 Cudd_RecursiveDeref( dd, bTemp );
626 }
627 #endif
628 */
629 // get the columns to be re-encoded
630 CutNodes = Extra_bddNodePathsUnderCut( dd, bEncoded, s_EncodingVarsLevel );
631 // LUT size is the cut level because because the temporary encoding variables
632 // are above the functional variables - this is not true!!!
633 // the temporary variables are below!
634
635 // put the entries from the table into the temporary array
636 {
637 st__generator * gen;
638 DdNode * bColumn, * bCode;
639 nCols = 0;
640 st__foreach_item( CutNodes, gen, (const char**)&bCode, (char**)&bColumn )
641 {
642 if ( bCode == b0 )
643 { // the unused part of the columns
644 Cudd_RecursiveDeref( dd, bColumn );
645 Cudd_RecursiveDeref( dd, bCode );
646 continue;
647 }
648 else
649 {
650 s_pbTemp[ nCols ] = bColumn; // takes ref
651 Cudd_RecursiveDeref( dd, bCode );
652 nCols++;
653 }
654 }
655 st__free_table( CutNodes );
656 // assert( nCols == (int)nMints );
657 }
658
659 // encode the columns
660 if ( s_MultiStart-Level == 0 ) // we reached the bottom level of recursion
661 {
662 assert( nCols == 1 );
663 // assert( (int)nMints == 1 );
664 bRes = s_pbTemp[0]; Cudd_Ref( bRes );
665 }
666 else
667 {
668 bRes = Extra_bddEncodingBinary( dd, s_pbTemp, nCols, pCVars+Level, s_MultiStart-Level ); Cudd_Ref( bRes );
669 }
670
671 // deref the columns
672 {
673 int i;
674 for ( i = 0; i < nCols; i++ )
675 Cudd_RecursiveDeref( dd, s_pbTemp[i] );
676 }
677 }
678 else
679 {
680 // cofactor the problem as specified in the best solution
681 DdNode * bCof0, * bCof1;
682 DdNode * bRes0, * bRes1;
683 DdNode * bProd0, * bProd1;
684 DdNode * bTemp;
685 DdNode * bVarNext = dd->vars[ s_VarOrderBest[Level] ];
686
687 bCof0 = Cudd_Cofactor( dd, bEncoded, Cudd_Not( bVarNext ) ); Cudd_Ref( bCof0 );
688 bCof1 = Cudd_Cofactor( dd, bEncoded, bVarNext ); Cudd_Ref( bCof1 );
689
690 // call recursively
691 bRes0 = CreateTheCodes_rec( dd, bCof0, Level+1, pCVars ); Cudd_Ref( bRes0 );
692 bRes1 = CreateTheCodes_rec( dd, bCof1, Level+1, pCVars ); Cudd_Ref( bRes1 );
693
694 Cudd_RecursiveDeref( dd, bCof0 );
695 Cudd_RecursiveDeref( dd, bCof1 );
696
697 // compose the result using the identity (bVarNext <=> pCVars[Level]) - this is wrong!
698 // compose the result as follows: x'y'F0 + xyF1
699 bProd0 = Cudd_bddAnd( dd, Cudd_Not(bVarNext), Cudd_Not(pCVars[Level]) ); Cudd_Ref( bProd0 );
700 bProd1 = Cudd_bddAnd( dd, bVarNext , pCVars[Level] ); Cudd_Ref( bProd1 );
701
702 bProd0 = Cudd_bddAnd( dd, bTemp = bProd0, bRes0 ); Cudd_Ref( bProd0 );
703 Cudd_RecursiveDeref( dd, bTemp );
704 Cudd_RecursiveDeref( dd, bRes0 );
705
706 bProd1 = Cudd_bddAnd( dd, bTemp = bProd1, bRes1 ); Cudd_Ref( bProd1 );
707 Cudd_RecursiveDeref( dd, bTemp );
708 Cudd_RecursiveDeref( dd, bRes1 );
709
710 bRes = Cudd_bddOr( dd, bProd0, bProd1 ); Cudd_Ref( bRes );
711
712 Cudd_RecursiveDeref( dd, bProd0 );
713 Cudd_RecursiveDeref( dd, bProd1 );
714 }
715 Cudd_Deref( bRes );
716 return bRes;
717 }
718
719 /**Function********************************************************************
720
721 Synopsis [Computes the current set of variables and counts the number of minterms.]
722
723 Description [Old implementation.]
724
725 SideEffects []
726
727 SeeAlso []
728
729 ******************************************************************************/
EvaluateEncodings_rec(DdManager * dd,DdNode * bVarsCol,int nVarsCol,int nMulti,int Level)730 void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level )
731 // bVarsCol is the set of remaining variables
732 // nVarsCol is the number of remaining variables
733 // nMulti is the number of encoding variables to be used
734 // Level is the level of recursion, from which this function is called
735 // if we successfully finish this procedure, Level also stands for how many encoding variabled we saved
736 {
737 int i, k;
738 int nEntries = (1<<(Level-1)); // the number of entries in the field of the previous level
739 DdNode * bVars0, * bVars1; // the cofactors
740 unsigned nMint0, nMint1; // the number of minterms
741 DdNode * bTempV;
742 DdNode * bVarTop;
743 int fBreak;
744
745
746 // there is no need to search above this level
747 if ( Level > s_MaxDepth )
748 return;
749
750 // if there are no variables left, quit the research
751 if ( bVarsCol == b1 )
752 return;
753
754 if ( s_BackTracks > s_BackTrackLimit )
755 return;
756
757 s_BackTracks++;
758
759 // otherwise, go through the remaining variables
760 for ( bTempV = bVarsCol; bTempV != b1; bTempV = cuddT(bTempV) )
761 {
762 // the currently tested variable
763 bVarTop = dd->vars[bTempV->index];
764
765 // put it into the array
766 s_VarOrderCur[Level-1] = bTempV->index;
767
768 // go through the entries and fill them out by cofactoring
769 fBreak = 0;
770 for ( i = 0; i < nEntries; i++ )
771 {
772 bVars0 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], Cudd_Not(bVarTop), &nMint0 );
773 Cudd_Ref( bVars0 );
774
775 if ( nMint0 > Extra_Power2( nMulti-1 ) )
776 {
777 // there is no way to encode - dereference and return
778 Cudd_RecursiveDeref( dd, bVars0 );
779 fBreak = 1;
780 break;
781 }
782
783 bVars1 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], bVarTop, &nMint1 );
784 Cudd_Ref( bVars1 );
785
786 if ( nMint1 > Extra_Power2( nMulti-1 ) )
787 {
788 // there is no way to encode - dereference and return
789 Cudd_RecursiveDeref( dd, bVars0 );
790 Cudd_RecursiveDeref( dd, bVars1 );
791 fBreak = 1;
792 break;
793 }
794
795 // otherwise, add these two cofactors
796 s_Field[Level][2*i + 0] = bVars0; // takes ref
797 s_Field[Level][2*i + 1] = bVars1; // takes ref
798 }
799
800 if ( !fBreak )
801 {
802 DdNode * bVarsRem;
803 // if we ended up here, it means that the cofactors w.r.t. variable bVarTop satisfy the condition
804 // save this situation
805 if ( s_nVarsBest < Level )
806 {
807 s_nVarsBest = Level;
808 // copy the variable assignment
809 for ( k = 0; k < Level; k++ )
810 s_VarOrderBest[k] = s_VarOrderCur[k];
811 }
812
813 // call recursively
814 // get the new variable set
815 if ( nMulti-1 > 0 )
816 {
817 bVarsRem = Cudd_bddExistAbstract( dd, bVarsCol, bVarTop ); Cudd_Ref( bVarsRem );
818 EvaluateEncodings_rec( dd, bVarsRem, nVarsCol-1, nMulti-1, Level+1 );
819 Cudd_RecursiveDeref( dd, bVarsRem );
820 }
821 }
822
823 // deref the contents of the array
824 for ( k = 0; k < i; k++ )
825 {
826 Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 0] );
827 Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 1] );
828 }
829
830 // if the solution is found, there is no need to continue
831 if ( s_nVarsBest == s_MaxDepth )
832 return;
833
834 // if the solution is found, there is no need to continue
835 if ( s_nVarsBest == s_MultiStart )
836 return;
837 }
838 // at this point, we have tried all possible directions in the space of variables
839 }
840
841 /**Function********************************************************************
842
843 Synopsis [Computes the current set of variables and counts the number of minterms.]
844
845 Description []
846
847 SideEffects []
848
849 SeeAlso []
850
851 ******************************************************************************/
ComputeVarSetAndCountMinterms(DdManager * dd,DdNode * bVars,DdNode * bVarTop,unsigned * Cost)852 DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost )
853 // takes bVars - the variables cofactored so far (some of them may be in negative polarity)
854 // bVarTop - the topmost variable w.r.t. which to cofactor (may be in negative polarity)
855 // returns the cost and the new set of variables (bVars & bVarTop)
856 {
857 DdNode * bVarsRes;
858
859 // get the resulting set of variables
860 bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop ); Cudd_Ref( bVarsRes );
861
862 // increment signature before calling Cudd_CountCofactorMinterms()
863 s_Signature++;
864 *Cost = Extra_CountCofactorMinterms( dd, s_Encoded, bVarsRes, s_VarAll );
865
866 Cudd_Deref( bVarsRes );
867 // s_CountCalls++;
868 return bVarsRes;
869 }
870
871 /**Function********************************************************************
872
873 Synopsis [Computes the current set of variables and counts the number of minterms.]
874
875 Description [The old implementation, which is approximately 4 times slower.]
876
877 SideEffects []
878
879 SeeAlso []
880
881 ******************************************************************************/
ComputeVarSetAndCountMinterms2(DdManager * dd,DdNode * bVars,DdNode * bVarTop,unsigned * Cost)882 DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost )
883 {
884 DdNode * bVarsRes;
885 DdNode * bCof, * bFun;
886
887 bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop ); Cudd_Ref( bVarsRes );
888
889 bCof = Cudd_Cofactor( dd, s_Encoded, bVarsRes ); Cudd_Ref( bCof );
890 bFun = Cudd_bddExistAbstract( dd, bCof, s_VarAll ); Cudd_Ref( bFun );
891 *Cost = (unsigned)Cudd_CountMinterm( dd, bFun, s_MultiStart );
892 Cudd_RecursiveDeref( dd, bFun );
893 Cudd_RecursiveDeref( dd, bCof );
894
895 Cudd_Deref( bVarsRes );
896 // s_CountCalls++;
897 return bVarsRes;
898 }
899
900
901 /**Function********************************************************************
902
903 Synopsis [Counts the number of encoding minterms pointed to by the cofactor of the function.]
904
905 Description []
906
907 SideEffects [None]
908
909 ******************************************************************************/
Extra_CountCofactorMinterms(DdManager * dd,DdNode * bFunc,DdNode * bVarsCof,DdNode * bVarsAll)910 unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll )
911 // this function computes how many minterms depending on the encoding variables
912 // are there in the cofactor of bFunc w.r.t. variables bVarsCof
913 // bFunc is assumed to depend on variables s_VarsAll
914 // the variables s_VarsAll should be ordered above the encoding variables
915 {
916 unsigned HKey;
917 DdNode * bFuncR;
918
919 // if the function is zero, there are no minterms
920 // if ( bFunc == b0 )
921 // return 0;
922
923 // if ( st__lookup(Visited, (char*)bFunc, NULL) )
924 // return 0;
925
926 // HKey = hashKey2c( s_Signature, bFuncR );
927 // if ( HHTable1[HKey].Sign == s_Signature && HHTable1[HKey].Arg1 == bFuncR ) // this node is visited
928 // return 0;
929
930
931 // check the hash-table
932 bFuncR = Cudd_Regular(bFunc);
933 // HKey = hashKey2( s_Signature, bFuncR, _TABLESIZE_COF );
934 HKey = hashKey2( s_Signature, bFunc, _TABLESIZE_COF );
935 for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF )
936 // if ( HHTable1[HKey].Arg1 == bFuncR ) // this node is visited
937 if ( HHTable1[HKey].Arg1 == bFunc ) // this node is visited
938 return 0;
939
940
941 // if the function is already the code
942 if ( dd->perm[bFuncR->index] >= s_EncodingVarsLevel )
943 {
944 // st__insert(Visited, (char*)bFunc, NULL);
945
946 // HHTable1[HKey].Sign = s_Signature;
947 // HHTable1[HKey].Arg1 = bFuncR;
948
949 assert( HHTable1[HKey].Sign != s_Signature );
950 HHTable1[HKey].Sign = s_Signature;
951 // HHTable1[HKey].Arg1 = bFuncR;
952 HHTable1[HKey].Arg1 = bFunc;
953
954 return Extra_CountMintermsSimple( bFunc, (1<<s_MultiStart) );
955 }
956 else
957 {
958 DdNode * bFunc0, * bFunc1;
959 DdNode * bVarsCof0, * bVarsCof1;
960 DdNode * bVarsCofR = Cudd_Regular(bVarsCof);
961 unsigned Res;
962
963 // get the levels
964 int LevelF = dd->perm[bFuncR->index];
965 int LevelC = cuddI(dd,bVarsCofR->index);
966 int LevelA = dd->perm[bVarsAll->index];
967
968 int LevelTop = LevelF;
969
970 if ( LevelTop > LevelC )
971 LevelTop = LevelC;
972
973 if ( LevelTop > LevelA )
974 LevelTop = LevelA;
975
976 // the top var in the function or in cofactoring vars always belongs to the set of all vars
977 assert( !( LevelTop == LevelF || LevelTop == LevelC ) || LevelTop == LevelA );
978
979 // cofactor the function
980 if ( LevelTop == LevelF )
981 {
982 if ( bFuncR != bFunc ) // bFunc is complemented
983 {
984 bFunc0 = Cudd_Not( cuddE(bFuncR) );
985 bFunc1 = Cudd_Not( cuddT(bFuncR) );
986 }
987 else
988 {
989 bFunc0 = cuddE(bFuncR);
990 bFunc1 = cuddT(bFuncR);
991 }
992 }
993 else // bVars is higher in the variable order
994 bFunc0 = bFunc1 = bFunc;
995
996 // cofactor the cube
997 if ( LevelTop == LevelC )
998 {
999 if ( bVarsCofR != bVarsCof ) // bFunc is complemented
1000 {
1001 bVarsCof0 = Cudd_Not( cuddE(bVarsCofR) );
1002 bVarsCof1 = Cudd_Not( cuddT(bVarsCofR) );
1003 }
1004 else
1005 {
1006 bVarsCof0 = cuddE(bVarsCofR);
1007 bVarsCof1 = cuddT(bVarsCofR);
1008 }
1009 }
1010 else // bVars is higher in the variable order
1011 bVarsCof0 = bVarsCof1 = bVarsCof;
1012
1013 // there are two cases:
1014 // (1) the top variable belongs to the cofactoring variables
1015 // (2) the top variable does not belong to the cofactoring variables
1016
1017 // (1) the top variable belongs to the cofactoring variables
1018 Res = 0;
1019 if ( LevelTop == LevelC )
1020 {
1021 if ( bVarsCof1 == b0 ) // this is a negative cofactor
1022 {
1023 if ( bFunc0 != b0 )
1024 Res = Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) );
1025 }
1026 else // this is a positive cofactor
1027 {
1028 if ( bFunc1 != b0 )
1029 Res = Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) );
1030 }
1031 }
1032 else
1033 {
1034 if ( bFunc0 != b0 )
1035 Res += Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) );
1036
1037 if ( bFunc1 != b0 )
1038 Res += Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) );
1039 }
1040
1041 // st__insert(Visited, (char*)bFunc, NULL);
1042
1043 // HHTable1[HKey].Sign = s_Signature;
1044 // HHTable1[HKey].Arg1 = bFuncR;
1045
1046 // skip through the entries with the same signatures
1047 // (these might have been created at the time of recursive calls)
1048 for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF );
1049 assert( HHTable1[HKey].Sign != s_Signature );
1050 HHTable1[HKey].Sign = s_Signature;
1051 // HHTable1[HKey].Arg1 = bFuncR;
1052 HHTable1[HKey].Arg1 = bFunc;
1053
1054 return Res;
1055 }
1056 }
1057
1058 /**Function********************************************************************
1059
1060 Synopsis [Counts the number of minterms.]
1061
1062 Description [This function counts minterms for functions up to 32 variables
1063 using a local cache. The terminal value (s_Termina) should be adjusted for
1064 BDDs and ADDs.]
1065
1066 SideEffects [None]
1067
1068 ******************************************************************************/
Extra_CountMintermsSimple(DdNode * bFunc,unsigned max)1069 unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max )
1070 {
1071 unsigned HKey;
1072
1073 // normalize
1074 if ( Cudd_IsComplement(bFunc) )
1075 return max - Extra_CountMintermsSimple( Cudd_Not(bFunc), max );
1076
1077 // now it is known that the function is not complemented
1078 if ( cuddIsConstant(bFunc) )
1079 return ((bFunc==s_Terminal)? 0: max);
1080
1081 // check cache
1082 HKey = hashKey2( bFunc, max, _TABLESIZE_MINT );
1083 if ( HHTable2[HKey].Arg1 == bFunc && HHTable2[HKey].Arg2 == max )
1084 return HHTable2[HKey].Res;
1085 else
1086 {
1087 // min = min0/2 + min1/2;
1088 unsigned min = (Extra_CountMintermsSimple( cuddE(bFunc), max ) >> 1) +
1089 (Extra_CountMintermsSimple( cuddT(bFunc), max ) >> 1);
1090
1091 HHTable2[HKey].Arg1 = bFunc;
1092 HHTable2[HKey].Arg2 = max;
1093 HHTable2[HKey].Res = min;
1094
1095 return min;
1096 }
1097 } /* end of Extra_CountMintermsSimple */
1098
1099
1100 /**Function********************************************************************
1101
1102 Synopsis [Visits the nodes.]
1103
1104 Description [Visits the nodes above the cut and the nodes pointed to below the cut;
1105 collects the visited nodes, counts how many times each node is visited, and sets
1106 the path-sum to be the constant zero BDD.]
1107
1108 SideEffects []
1109
1110 SeeAlso []
1111
1112 ******************************************************************************/
CountNodeVisits_rec(DdManager * dd,DdNode * aFunc,st__table * Visited)1113 void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st__table * Visited )
1114
1115 {
1116 traventry * p;
1117 char **slot;
1118 if ( st__find_or_add(Visited, (char*)aFunc, &slot) )
1119 { // the entry already exists
1120 p = (traventry*) *slot;
1121 // increment the counter of incoming edges
1122 p->nEdges++;
1123 return;
1124 }
1125 // this node has not been visited
1126 assert( !Cudd_IsComplement(aFunc) );
1127
1128 // create the new traversal entry
1129 p = (traventry *) ABC_ALLOC( char, sizeof(traventry) );
1130 // set the initial sum of edges to zero BDD
1131 p->bSum = b0; Cudd_Ref( b0 );
1132 // set the starting number of incoming edges
1133 p->nEdges = 1;
1134 // set this entry into the slot
1135 *slot = (char*)p;
1136
1137 // recur if the node is above the cut
1138 if ( cuddI(dd,aFunc->index) < s_CutLevel )
1139 {
1140 CountNodeVisits_rec( dd, cuddE(aFunc), Visited );
1141 CountNodeVisits_rec( dd, cuddT(aFunc), Visited );
1142 }
1143 } /* end of CountNodeVisits_rec */
1144
1145
1146 /**Function********************************************************************
1147
1148 Synopsis [Revisits the nodes and computes the paths.]
1149
1150 Description [This function visits the nodes above the cut having the goal of
1151 summing all the incomming BDD edges; when this function comes across the node
1152 below the cut, it saves this node in the CutNode table.]
1153
1154 SideEffects []
1155
1156 SeeAlso []
1157
1158 ******************************************************************************/
CollectNodesAndComputePaths_rec(DdManager * dd,DdNode * aFunc,DdNode * bCube,st__table * Visited,st__table * CutNodes)1159 void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st__table * Visited, st__table * CutNodes )
1160 {
1161 // find the node in the visited table
1162 DdNode * bTemp;
1163 traventry * p;
1164 char **slot;
1165 if ( st__find_or_add(Visited, (char*)aFunc, &slot) )
1166 { // the node is found
1167 // get the pointer to the traversal entry
1168 p = (traventry*) *slot;
1169
1170 // make sure that the counter of incoming edges is positive
1171 assert( p->nEdges > 0 );
1172
1173 // add the cube to the currently accumulated cubes
1174 p->bSum = Cudd_bddOr( dd, bTemp = p->bSum, bCube ); Cudd_Ref( p->bSum );
1175 Cudd_RecursiveDeref( dd, bTemp );
1176
1177 // decrement the number of visits
1178 p->nEdges--;
1179
1180 // if more visits to this node are expected, return
1181 if ( p->nEdges )
1182 return;
1183 else // if ( p->nEdges == 0 )
1184 { // this is the last visit - propagate the cube
1185
1186 // check where this node is
1187 if ( cuddI(dd,aFunc->index) < s_CutLevel )
1188 { // the node is above the cut
1189 DdNode * bCube0, * bCube1;
1190
1191 // get the top-most variable
1192 DdNode * bVarTop = dd->vars[aFunc->index];
1193
1194 // compute the propagated cubes
1195 bCube0 = Cudd_bddAnd( dd, p->bSum, Cudd_Not( bVarTop ) ); Cudd_Ref( bCube0 );
1196 bCube1 = Cudd_bddAnd( dd, p->bSum, bVarTop ); Cudd_Ref( bCube1 );
1197
1198 // call recursively
1199 CollectNodesAndComputePaths_rec( dd, cuddE(aFunc), bCube0, Visited, CutNodes );
1200 CollectNodesAndComputePaths_rec( dd, cuddT(aFunc), bCube1, Visited, CutNodes );
1201
1202 // dereference the cubes
1203 Cudd_RecursiveDeref( dd, bCube0 );
1204 Cudd_RecursiveDeref( dd, bCube1 );
1205 return;
1206 }
1207 else
1208 { // the node is below the cut
1209 // add this node to the cut node table, if it is not yet there
1210
1211 // DdNode * bNode;
1212 // bNode = Cudd_addBddPattern( dd, aFunc ); Cudd_Ref( bNode );
1213 if ( st__find_or_add(CutNodes, (char*)aFunc, &slot) )
1214 { // the node exists - should never happen
1215 assert( 0 );
1216 }
1217 *slot = (char*) p->bSum; Cudd_Ref( p->bSum );
1218 // the table takes the reference of bNode
1219 return;
1220 }
1221 }
1222 }
1223
1224 // the node does not exist in the visited table - should never happen
1225 assert(0);
1226
1227 } /* end of CollectNodesAndComputePaths_rec */
1228
1229
1230
1231 ////////////////////////////////////////////////////////////////////////
1232 /// END OF FILE ///
1233 ////////////////////////////////////////////////////////////////////////
1234 ABC_NAMESPACE_IMPL_END
1235
1236