src/misc/extra/extraBddCas.c File Reference

#include "extra.h"

Include dependency graph for extraBddCas.c:

Data Structures
struct	_HashEntry_cof
struct	_HashEntry_mint
struct	traventry
Defines
#define	_TABLESIZE_COF 51113
#define	_TABLESIZE_MINT 15113
Functions
static DdNode *	CreateTheCodes_rec (DdManager dd, DdNode bEncoded, int Level, DdNode **pCVars)
static void	EvaluateEncodings_rec (DdManager dd, DdNode bVarsCol, int nVarsCol, int nMulti, int Level)
static DdNode *	ComputeVarSetAndCountMinterms (DdManager dd, DdNode bVars, DdNode bVarTop, unsigned Cost)
static DdNode *	ComputeVarSetAndCountMinterms2 (DdManager dd, DdNode bVars, DdNode bVarTop, unsigned Cost)
unsigned	Extra_CountCofactorMinterms (DdManager dd, DdNode bFunc, DdNode bVarsCof, DdNode bVarsAll)
static unsigned	Extra_CountMintermsSimple (DdNode *bFunc, unsigned max)
static void	CountNodeVisits_rec (DdManager dd, DdNode aFunc, st_table *Visited)
static void	CollectNodesAndComputePaths_rec (DdManager dd, DdNode aFunc, DdNode bCube, st_table Visited, st_table *CutNodes)
DdNode *	Extra_bddEncodingBinary (DdManager dd, DdNode pbFuncs, int nFuncs, DdNode *pbVars, int nVars)
DdNode *	Extra_bddEncodingNonStrict (DdManager dd, DdNode pbColumns, int nColumns, DdNode bVarsCol, DdNode *pCVars, int nMulti, int pSimple)
st_table *	Extra_bddNodePathsUnderCut (DdManager dd, DdNode bFunc, int CutLevel)
int	Extra_bddNodePathsUnderCutArray (DdManager dd, DdNode paNodes, DdNode pbCubes, int nNodes, DdNode paNodesRes, DdNode *pbCubesRes, int CutLevel)
void	extraCollectNodes (DdNode Func, st_table tNodes)
st_table *	Extra_CollectNodes (DdNode *Func)
void	extraProfileUpdateTopLevel (st_table tNodeTopRef, int TopLevelNew, DdNode node)
int	Extra_ProfileWidth (DdManager dd, DdNode Func, int *pProfile, int CutLevel)
Variables
_HashEntry_cof	HHTable1 [_TABLESIZE_COF]
_HashEntry_mint	HHTable2 [_TABLESIZE_MINT]
static unsigned	s_Signature = 1
static int	s_CutLevel = 0
static int	s_MaxDepth = 5
static int	s_nVarsBest
static int	s_VarOrderBest [32]
static int	s_VarOrderCur [32]
static DdNode *	s_Field [8][256]
static DdNode *	s_Encoded
static DdNode *	s_VarAll
static int	s_MultiStart
static DdNode **	s_pbTemp
static int	s_BackTracks
static int	s_BackTrackLimit = 100
static DdNode *	s_Terminal
static int	s_EncodingVarsLevel

Define Documentation

#define _TABLESIZE_COF 51113

CFile****************************************************************

FileName [extraBddCas.c]

PackageName [extra]

Synopsis [Procedures related to LUT cascade synthesis.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id: extraBddCas.c,v 1.0 2003/05/21 18:03:50 alanmi Exp

]

Definition at line 34 of file extraBddCas.c.

#define _TABLESIZE_MINT 15113

Definition at line 43 of file extraBddCas.c.

Function Documentation

void CollectNodesAndComputePaths_rec	(	DdManager *	dd,
		DdNode *	aFunc,
		DdNode *	bCube,
		st_table *	Visited,
		st_table *	CutNodes
	)			`[static]`

Function********************************************************************

Synopsis [Revisits the nodes and computes the paths.]

Description [This function visits the nodes above the cut having the goal of summing all the incomming BDD edges; when this function comes across the node below the cut, it saves this node in the CutNode table.]

SideEffects []

SeeAlso []

Definition at line 1156 of file extraBddCas.c.

01158 01159 01160 01161 01162 01163 01164 01165 01166 01167 01168 01169 01170 01171 01172 01173 01174 01175 01176 01177 01178 01179 01180 01181 01182 01183 01184 01185 01186 01187 01188 01189 01190 01191 01192 01193 01194 01195 01196 01197 01198 01199 01200 01201 01202 01203 01204 01205 01206 01207 01208 01209 01210 01211 01212 01213 01214 01215 01216 01217 01218 01219         } 01220 01221 01222 01223 01224

class="fragment">01157 { // find the node in the visited table DdNode * bTemp; traventry * p; char **slot; if ( st_find_or_add(Visited, (char*)aFunc, &slot) ) { // the node is found // get the pointer to the traversal entry p = (traventry*) *slot; // make sure that the counter of incoming edges is positive assert( p->nEdges > 0 ); // add the cube to the currently accumulated cubes p->bSum = Cudd_bddOr( dd, bTemp = p->bSum, bCube ); Cudd_Ref( p->bSum ); Cudd_RecursiveDeref( dd, bTemp ); // decrement the number of visits p->nEdges--; // if more visits to this node are expected, return if ( p->nEdges ) return; else // if ( p->nEdges == 0 ) { // this is the last visit - propagate the cube // check where this node is if ( cuddI(dd,aFunc->index) < s_CutLevel ) { // the node is above the cut DdNode * bCube0, * bCube1; // get the top-most variable DdNode * bVarTop = dd->vars[aFunc->index]; // compute the propagated cubes bCube0 = Cudd_bddAnd( dd, p->bSum, Cudd_Not( bVarTop ) ); Cudd_Ref( bCube0 ); bCube1 = Cudd_bddAnd( dd, p->bSum, bVarTop ); Cudd_Ref( bCube1 ); // call recursively CollectNodesAndComputePaths_rec( dd, cuddE(aFunc), bCube0, Visited, CutNodes ); CollectNodesAndComputePaths_rec( dd, cuddT(aFunc), bCube1, Visited, CutNodes ); // dereference the cubes Cudd_RecursiveDeref( dd, bCube0 ); Cudd_RecursiveDeref( dd, bCube1 ); return; } else { // the node is below the cut // add this node to the cut node table, if it is not yet there // DdNode * bNode; // bNode = Cudd_addBddPattern( dd, aFunc ); Cudd_Ref( bNode ); if ( st_find_or_add(CutNodes, (char*)aFunc, &slot) ) { // the node exists - should never happen assert( 0 ); } *slot = (char*) p->bSum; Cudd_Ref( p->bSum ); // the table takes the reference of bNode return; } } // the node does not exist in the visited table - should never happen assert(0); } /* end of CollectNodesAndComputePaths_rec */

DdNode * ComputeVarSetAndCountMinterms	(	DdManager *	dd,
		DdNode *	bVars,
		DdNode *	bVarTop,
		unsigned *	Cost
	)			`[static]`

Function********************************************************************

Synopsis [Computes the current set of variables and counts the number of minterms.]

Description []

SideEffects []

SeeAlso []

Definition at line 849 of file extraBddCas.c.

00853 {
00854         DdNode * bVarsRes;
00855 
00856         // get the resulting set of variables
00857         bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop );  Cudd_Ref( bVarsRes );
00858 
00859         // increment signature before calling Cudd_CountCofactorMinterms()
00860         s_Signature++;
00861         *Cost = Extra_CountCofactorMinterms( dd, s_Encoded, bVarsRes, s_VarAll );
00862 
00863         Cudd_Deref( bVarsRes );
00864 //      s_CountCalls++;
00865         return bVarsRes;
00866 }

DdNode * ComputeVarSetAndCountMinterms2	(	DdManager *	dd,
		DdNode *	bVars,
		DdNode *	bVarTop,
		unsigned *	Cost
	)			`[static]`

Function********************************************************************

Synopsis [Computes the current set of variables and counts the number of minterms.]

Description [The old implementation, which is approximately 4 times slower.]

SideEffects []

SeeAlso []

Definition at line 879 of file extraBddCas.c.

00880 {
00881         DdNode * bVarsRes;
00882         DdNode * bCof, * bFun;
00883 
00884         bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop );             Cudd_Ref( bVarsRes );
00885 
00886         bCof  = Cudd_Cofactor( dd, s_Encoded,  bVarsRes );        Cudd_Ref( bCof );
00887         bFun  = Cudd_bddExistAbstract( dd, bCof, s_VarAll );      Cudd_Ref( bFun );
00888         *Cost = (unsigned)Cudd_CountMinterm( dd, bFun, s_MultiStart );
00889         Cudd_RecursiveDeref( dd, bFun );
00890         Cudd_RecursiveDeref( dd, bCof );
00891 
00892         Cudd_Deref( bVarsRes );
00893 //      s_CountCalls++;
00894         return bVarsRes;
00895 }

void CountNodeVisits_rec	(	DdManager *	dd,
		DdNode *	aFunc,
		st_table *	Visited
	)			`[static]`

Function********************************************************************

Synopsis [Visits the nodes.]

Description [Visits the nodes above the cut and the nodes pointed to below the cut; collects the visited nodes, counts how many times each node is visited, and sets the path-sum to be the constant zero BDD.]

SideEffects []

SeeAlso []

Definition at line 1110 of file extraBddCas.c.

01112 {
01113         traventry * p;
01114         char **slot;
01115         if ( st_find_or_add(Visited, (char*)aFunc, &slot) )
01116         { // the entry already exists
01117                 p = (traventry*) *slot;
01118                 // increment the counter of incoming edges
01119                 p->nEdges++;
01120                 return; 
01121         }
01122         // this node has not been visited
01123         assert( !Cudd_IsComplement(aFunc) );
01124 
01125         // create the new traversal entry
01126         p = (traventry *) malloc( sizeof(traventry) );
01127         // set the initial sum of edges to zero BDD
01128         p->bSum = b0;   Cudd_Ref( b0 );
01129         // set the starting number of incoming edges
01130         p->nEdges = 1;
01131         // set this entry into the slot
01132         *slot = (char*)p;
01133 
01134         // recur if the node is above the cut
01135         if ( cuddI(dd,aFunc->index) < s_CutLevel )
01136         {
01137                 CountNodeVisits_rec( dd, cuddE(aFunc), Visited );
01138                 CountNodeVisits_rec( dd, cuddT(aFunc), Visited );
01139         }
01140 } /* end of CountNodeVisits_rec */

DdNode * CreateTheCodes_rec	(	DdManager *	dd,
		DdNode *	bEncoded,
		int	Level,
		DdNode **	pCVars
	)			`[static]`

AutomaticStart

Function********************************************************************

Synopsis [Computes the non-strict codes when evaluation is finished.]

Description [The information about the best code is stored in s_VarOrderBest, which has s_nVarsBest entries.]

SideEffects [None]

Definition at line 596 of file extraBddCas.c.

00600 {
00601         DdNode * bRes;
00602         if ( Level == s_nVarsBest )
00603         { // the terminal case, when we need to remap the encoded function 
00604                 // from the preliminary encoded variables to the new ones
00605                 st_table * CutNodes;
00606                 int nCols;
00607 //              double nMints;
00608 /*
00609 #ifdef _DEBUG
00610 
00611                 {
00612                 DdNode * bTemp;
00613                 // make sure that the given number of variables is enough
00614                 bTemp  = Cudd_bddExistAbstract( dd, bEncoded, s_VarAll );           Cudd_Ref( bTemp );
00615 //              nMints = Cudd_CountMinterm( dd, bTemp, s_MultiStart );
00616                 nMints = Extra_CountMintermsSimple( bTemp, (1<<s_MultiStart) );
00617                 if ( nMints > Extra_Power2( s_MultiStart-Level ) ) 
00618                 {  // the number of minterms is too large to encode the columns 
00619                    // using the given minimum number of encoding variables
00620                         assert( 0 );
00621                 }
00622                 Cudd_RecursiveDeref( dd, bTemp );
00623                 }
00624 #endif
00625 */
00626                 // get the columns to be re-encoded
00627                 CutNodes = Extra_bddNodePathsUnderCut( dd, bEncoded, s_EncodingVarsLevel );
00628                 // LUT size is the cut level because because the temporary encoding variables 
00629                 // are above the functional variables - this is not true!!!
00630                 // the temporary variables are below!
00631 
00632                 // put the entries from the table into the temporary array
00633                 { 
00634                         st_generator * gen;
00635                         DdNode * bColumn, * bCode;
00636                         nCols = 0;
00637                         st_foreach_item( CutNodes, gen, (char**)&bCode, (char**)&bColumn ) 
00638                         {
00639                                 if ( bCode == b0 )
00640                                 { // the unused part of the columns
00641                                         Cudd_RecursiveDeref( dd, bColumn );
00642                                         Cudd_RecursiveDeref( dd, bCode );
00643                                         continue;
00644                                 }
00645                                 else
00646                                 {
00647                                         s_pbTemp[ nCols ] = bColumn; // takes ref
00648                                         Cudd_RecursiveDeref( dd, bCode );
00649                                         nCols++;
00650                                 }
00651                         }
00652                         st_free_table( CutNodes );
00653 //                      assert( nCols == (int)nMints );
00654                 }
00655 
00656                 // encode the columns
00657                 if ( s_MultiStart-Level == 0 ) // we reached the bottom level of recursion
00658                 {
00659                         assert( nCols       == 1 );
00660 //                      assert( (int)nMints == 1 );
00661                         bRes = s_pbTemp[0];     Cudd_Ref( bRes );
00662                 }
00663                 else
00664                 {
00665                         bRes = Extra_bddEncodingBinary( dd, s_pbTemp, nCols, pCVars+Level, s_MultiStart-Level ); Cudd_Ref( bRes );
00666                 }
00667 
00668                 // deref the columns
00669                 {
00670                         int i;
00671                         for ( i = 0; i < nCols; i++ )
00672                                 Cudd_RecursiveDeref( dd, s_pbTemp[i] );
00673                 }
00674         }
00675         else
00676         {
00677                 // cofactor the problem as specified in the best solution
00678                 DdNode * bCof0,  * bCof1;
00679                 DdNode * bRes0,  * bRes1;
00680                 DdNode * bProd0, * bProd1;
00681                 DdNode * bTemp;
00682                 DdNode * bVarNext = dd->vars[ s_VarOrderBest[Level] ];
00683 
00684                 bCof0  = Cudd_Cofactor( dd, bEncoded,  Cudd_Not( bVarNext ) );   Cudd_Ref( bCof0 );
00685                 bCof1  = Cudd_Cofactor( dd, bEncoded,            bVarNext   );   Cudd_Ref( bCof1 );
00686 
00687                 // call recursively
00688                 bRes0 = CreateTheCodes_rec( dd, bCof0, Level+1, pCVars );  Cudd_Ref( bRes0 );
00689                 bRes1 = CreateTheCodes_rec( dd, bCof1, Level+1, pCVars );  Cudd_Ref( bRes1 );
00690 
00691                 Cudd_RecursiveDeref( dd, bCof0 );
00692                 Cudd_RecursiveDeref( dd, bCof1 );
00693 
00694                 // compose the result using the identity (bVarNext <=> pCVars[Level])  - this is wrong!
00695                 // compose the result as follows: x'y'F0 + xyF1
00696                 bProd0 = Cudd_bddAnd( dd, Cudd_Not(bVarNext), Cudd_Not(pCVars[Level]) );   Cudd_Ref( bProd0 );
00697                 bProd1 = Cudd_bddAnd( dd,          bVarNext ,          pCVars[Level]  );   Cudd_Ref( bProd1 );
00698 
00699                 bProd0 = Cudd_bddAnd( dd, bTemp = bProd0, bRes0 );   Cudd_Ref( bProd0 );
00700                 Cudd_RecursiveDeref( dd, bTemp );
00701                 Cudd_RecursiveDeref( dd, bRes0 );
00702 
00703                 bProd1 = Cudd_bddAnd( dd, bTemp = bProd1, bRes1 );   Cudd_Ref( bProd1 );
00704                 Cudd_RecursiveDeref( dd, bTemp );
00705                 Cudd_RecursiveDeref( dd, bRes1 );
00706 
00707                 bRes = Cudd_bddOr( dd, bProd0, bProd1 );             Cudd_Ref( bRes );
00708 
00709                 Cudd_RecursiveDeref( dd, bProd0 );
00710                 Cudd_RecursiveDeref( dd, bProd1 );
00711         }
00712         Cudd_Deref( bRes );
00713         return bRes;
00714 }

void EvaluateEncodings_rec	(	DdManager *	dd,
		DdNode *	bVarsCol,
		int	nVarsCol,
		int	nMulti,
		int	Level
	)			`[static]`

Function********************************************************************

Synopsis [Computes the current set of variables and counts the number of minterms.]

Description [Old implementation.]

SideEffects []

SeeAlso []

Definition at line 727 of file extraBddCas.c.

00733 {
00734         int i, k;
00735         int nEntries = (1<<(Level-1)); // the number of entries in the field of the previous level
00736         DdNode * bVars0, * bVars1; // the cofactors
00737         unsigned nMint0, nMint1;   // the number of minterms
00738         DdNode * bTempV;
00739         DdNode * bVarTop;
00740         int fBreak;
00741 
00742 
00743         // there is no need to search above this level
00744         if ( Level > s_MaxDepth )
00745                 return;
00746 
00747         // if there are no variables left, quit the research
00748         if ( bVarsCol == b1 )
00749                 return;
00750 
00751         if ( s_BackTracks > s_BackTrackLimit )
00752                 return;
00753 
00754         s_BackTracks++;
00755 
00756         // otherwise, go through the remaining variables
00757         for ( bTempV = bVarsCol; bTempV != b1; bTempV = cuddT(bTempV) )
00758         {
00759                 // the currently tested variable
00760                 bVarTop = dd->vars[bTempV->index];
00761 
00762                 // put it into the array
00763                 s_VarOrderCur[Level-1] = bTempV->index;
00764 
00765                 // go through the entries and fill them out by cofactoring
00766                 fBreak = 0;
00767                 for ( i = 0; i < nEntries; i++ )
00768                 {
00769                         bVars0 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], Cudd_Not(bVarTop), &nMint0 );
00770                         Cudd_Ref( bVars0 );
00771 
00772                         if ( nMint0 > Extra_Power2( nMulti-1 ) ) 
00773                         {
00774                                 // there is no way to encode - dereference and return
00775                                 Cudd_RecursiveDeref( dd, bVars0 );
00776                                 fBreak = 1;
00777                                 break;
00778                         }
00779 
00780                         bVars1 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], bVarTop, &nMint1 );
00781                         Cudd_Ref( bVars1 );
00782 
00783                         if ( nMint1 > Extra_Power2( nMulti-1 ) ) 
00784                         {
00785                                 // there is no way to encode - dereference and return
00786                                 Cudd_RecursiveDeref( dd, bVars0 );
00787                                 Cudd_RecursiveDeref( dd, bVars1 );
00788                                 fBreak = 1;
00789                                 break;
00790                         }
00791 
00792                         // otherwise, add these two cofactors
00793                         s_Field[Level][2*i + 0] = bVars0; // takes ref
00794                         s_Field[Level][2*i + 1] = bVars1; // takes ref
00795                 } 
00796 
00797                 if ( !fBreak )
00798                 {
00799                         DdNode * bVarsRem;
00800                         // if we ended up here, it means that the cofactors w.r.t. variable bVarTop satisfy the condition
00801                         // save this situation
00802                         if ( s_nVarsBest < Level )
00803                         {
00804                                 s_nVarsBest = Level;
00805                                 // copy the variable assignment
00806                                 for ( k = 0; k < Level; k++ )
00807                                         s_VarOrderBest[k] = s_VarOrderCur[k];
00808                         }
00809 
00810                         // call recursively
00811                         // get the new variable set
00812                         if ( nMulti-1 > 0 )
00813                         {
00814                                 bVarsRem = Cudd_bddExistAbstract( dd, bVarsCol, bVarTop );   Cudd_Ref( bVarsRem );
00815                                 EvaluateEncodings_rec( dd, bVarsRem, nVarsCol-1, nMulti-1, Level+1 );
00816                                 Cudd_RecursiveDeref( dd, bVarsRem );
00817                         }
00818                 }
00819 
00820                 // deref the contents of the array
00821                 for ( k = 0; k < i; k++ )
00822                 {
00823                         Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 0] );
00824                         Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 1] );
00825                 }
00826 
00827                 // if the solution is found, there is no need to continue
00828                 if ( s_nVarsBest == s_MaxDepth )
00829                         return;
00830 
00831                 // if the solution is found, there is no need to continue
00832                 if ( s_nVarsBest == s_MultiStart )
00833                         return;
00834         }
00835         // at this point, we have tried all possible directions in the space of variables
00836 }

DdNode* Extra_bddEncodingBinary	(	DdManager *	dd,
		DdNode **	pbFuncs,
		int	nFuncs,
		DdNode **	pbVars,
		int	nVars
	)

AutomaticEnd Function********************************************************************

Synopsis [Performs the binary encoding of the set of function using the given vars.]

Description [Performs a straight binary encoding of the set of functions using the variable cubes formed from the given set of variables. ]

SideEffects []

SeeAlso []

Definition at line 135 of file extraBddCas.c.

00141 {
00142         int i;
00143         DdNode * bResult;
00144         DdNode * bCube, * bTemp, * bProd;
00145 
00146         assert( nVars >= Extra_Base2Log(nFuncs) );
00147 
00148         bResult = b0;   Cudd_Ref( bResult );
00149         for ( i = 0; i < nFuncs; i++ )
00150         {
00151                 bCube   = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );   Cudd_Ref( bCube );
00152                 bProd   = Cudd_bddAnd( dd, bCube, pbFuncs[i] );         Cudd_Ref( bProd );
00153                 Cudd_RecursiveDeref( dd, bCube );
00154 
00155                 bResult = Cudd_bddOr( dd, bProd, bTemp = bResult );     Cudd_Ref( bResult );
00156                 Cudd_RecursiveDeref( dd, bTemp );
00157                 Cudd_RecursiveDeref( dd, bProd );
00158         }
00159 
00160         Cudd_Deref( bResult );
00161         return bResult;
00162 } /* end of Extra_bddEncodingBinary */

DdNode* Extra_bddEncodingNonStrict	(	DdManager *	dd,
		DdNode **	pbColumns,
		int	nColumns,
		DdNode *	bVarsCol,
		DdNode **	pCVars,
		int	nMulti,
		int *	pSimple
	)

Function********************************************************************

Synopsis [Solves the column encoding problem using a sophisticated method.]

Description [The encoding is based on the idea of deriving functions which depend on only one variable, which corresponds to the case of non-disjoint decompostion. It is assumed that the variables pCVars are ordered below the variables representing the solumns, and the first variable pCVars[0] is the topmost one.]

SideEffects []

SeeAlso [Extra_bddEncodingBinary]

Definition at line 181 of file extraBddCas.c.

00189 {
00190         DdNode * bEncoded, * bResult;
00191         int nVarsCol = Cudd_SupportSize(dd,bVarsCol);
00192         long clk;
00193 
00194         // cannot work with more that 32-bit codes
00195         assert( nMulti < 32 );
00196 
00197         // perform the preliminary encoding using the straight binary code
00198         bEncoded = Extra_bddEncodingBinary( dd, pbColumns, nColumns, pCVars, nMulti );   Cudd_Ref( bEncoded );
00199         //printf( "Node count = %d", Cudd_DagSize(bEncoded) );
00200 
00201         // set the backgroup value for counting minterms
00202         s_Terminal = b0;
00203         // set the level of the encoding variables
00204         s_EncodingVarsLevel = dd->invperm[pCVars[0]->index];
00205 
00206         // the current number of backtracks
00207         s_BackTracks = 0;
00208         // the variables that are cofactored on the topmost level where everything starts (no vars)
00209         s_Field[0][0] = b1;   
00210         // the size of the best set of "simple" encoding variables found so far
00211         s_nVarsBest   = 0;
00212 
00213     // set the relation to be accessible to traversal procedures
00214         s_Encoded = bEncoded;
00215         // the set of all vars to be accessible to traversal procedures
00216         s_VarAll  = bVarsCol;
00217         // the column multiplicity
00218         s_MultiStart  = nMulti;
00219 
00220 
00221         clk = clock();
00222         // find the simplest encoding
00223         if ( nColumns > 2 )
00224         EvaluateEncodings_rec( dd, bVarsCol, nVarsCol, nMulti, 1 );
00225 //      printf( "The number of backtracks = %d\n", s_BackTracks );
00226 //      s_EncSearchTime += clock() - clk;
00227 
00228         // allocate the temporary storage for the columns
00229         s_pbTemp = (DdNode **) malloc( nColumns * sizeof(DdNode *) );
00230 
00231 //      clk = clock();
00232         bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars );   Cudd_Ref( bResult );
00233 //      s_EncComputeTime += clock() - clk;
00234         
00235         // delocate the preliminarily encoded set
00236         Cudd_RecursiveDeref( dd, bEncoded );
00237 //      Cudd_RecursiveDeref( dd, aEncoded );
00238 
00239         free( s_pbTemp );
00240 
00241         *pSimple = s_nVarsBest;
00242         Cudd_Deref( bResult );
00243         return bResult;
00244 }

st_table* Extra_bddNodePathsUnderCut	(	DdManager *	dd,
		DdNode *	bFunc,
		int	CutLevel
	)

Function********************************************************************

Synopsis [Collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root.]

Description [The table returned contains the set of BDD nodes pointed to under the cut and, for each node, the BDD of the sum of paths leading to this node from the root The sums of paths in the table are referenced. CutLevel is the first DD level considered to be under the cut.]

SideEffects []

SeeAlso [Extra_bddNodePaths]

Definition at line 260 of file extraBddCas.c.

00261 {
00262         st_table * Visited;  // temporary table to remember the visited nodes
00263         st_table * CutNodes; // the result goes here
00264         st_table * Result; // the result goes here
00265         DdNode * aFunc;
00266 
00267         s_CutLevel = CutLevel;
00268 
00269         Result  = st_init_table(st_ptrcmp,st_ptrhash);
00270         // the terminal cases
00271         if ( Cudd_IsConstant( bFunc ) )
00272         {
00273                 if ( bFunc == b1 )
00274                 {
00275                         st_insert( Result, (char*)b1, (char*)b1 );
00276                         Cudd_Ref( b1 );
00277                         Cudd_Ref( b1 );
00278                 }
00279                 else
00280                 {
00281                         st_insert( Result, (char*)b0, (char*)b0 );
00282                         Cudd_Ref( b0 );
00283                         Cudd_Ref( b0 );
00284                 }
00285                 return Result;
00286         }
00287 
00288         // create the ADD to simplify processing (no complemented edges)
00289         aFunc = Cudd_BddToAdd( dd, bFunc );   Cudd_Ref( aFunc );
00290 
00291         // Step 1: Start the tables and collect information about the nodes above the cut 
00292         // this information tells how many edges point to each node
00293         Visited  = st_init_table(st_ptrcmp,st_ptrhash);
00294         CutNodes = st_init_table(st_ptrcmp,st_ptrhash);
00295 
00296         CountNodeVisits_rec( dd, aFunc, Visited );
00297 
00298         // Step 2: Traverse the BDD using the visited table and compute the sum of paths
00299         CollectNodesAndComputePaths_rec( dd, aFunc, b1, Visited, CutNodes );
00300 
00301         // at this point the table of cut nodes is ready and the table of visited is useless
00302         {
00303                 st_generator * gen;
00304                 DdNode * aNode;
00305                 traventry * p;
00306                 st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
00307                 {
00308                         Cudd_RecursiveDeref( dd, p->bSum );
00309                         free( p );
00310                 }
00311                 st_free_table( Visited );
00312         }
00313 
00314         // go through the table CutNodes and create the BDD and the path to be returned
00315         {
00316                 st_generator * gen;
00317                 DdNode * aNode, * bNode, * bSum;
00318                 st_foreach_item( CutNodes, gen, (char**)&aNode, (char**)&bSum) 
00319                 {
00320                         // aNode is not referenced, because aFunc is holding it
00321                         bNode = Cudd_addBddPattern( dd, aNode );  Cudd_Ref( bNode ); 
00322                         st_insert( Result, (char*)bNode, (char*)bSum );
00323                         // the new table takes both refs
00324                 }
00325                 st_free_table( CutNodes );
00326         }
00327 
00328         // dereference the ADD
00329         Cudd_RecursiveDeref( dd, aFunc );
00330 
00331         // return the table
00332         return Result;
00333 
00334 } /* end of Extra_bddNodePathsUnderCut */

int Extra_bddNodePathsUnderCutArray	(	DdManager *	dd,
		DdNode **	paNodes,
		DdNode **	pbCubes,
		int	nNodes,
		DdNode **	paNodesRes,
		DdNode **	pbCubesRes,
		int	CutLevel
	)

Function********************************************************************

Synopsis [Collects the nodes under the cut in the ADD starting from the given set of ADD nodes.]

Description [Takes the array, paNodes, of ADD nodes to start the traversal, the array, pbCubes, of BDD cubes to start the traversal with in each node, and the number, nNodes, of ADD nodes and BDD cubes in paNodes and pbCubes. Returns the number of columns found. Fills in paNodesRes (pbCubesRes) with the set of ADD columns (BDD paths). These arrays should be allocated by the user.]

SideEffects []

SeeAlso [Extra_bddNodePaths]

Definition at line 352 of file extraBddCas.c.

00353 {
00354         st_table * Visited;  // temporary table to remember the visited nodes
00355         st_table * CutNodes; // the nodes under the cut go here
00356         int i, Counter;
00357 
00358         s_CutLevel = CutLevel;
00359 
00360         // there should be some nodes
00361         assert( nNodes > 0 );
00362         if ( nNodes == 1 && Cudd_IsConstant( paNodes[0] ) )
00363         {
00364                 if ( paNodes[0] == a1 )
00365                 {
00366                         paNodesRes[0] = a1;          Cudd_Ref( a1 );
00367                         pbCubesRes[0] = pbCubes[0];  Cudd_Ref( pbCubes[0] );
00368                 }
00369                 else
00370                 {
00371                         paNodesRes[0] = a0;          Cudd_Ref( a0 );
00372                         pbCubesRes[0] = pbCubes[0];  Cudd_Ref( pbCubes[0] );
00373                 }
00374                 return 1;
00375         }
00376 
00377         // Step 1: Start the table and collect information about the nodes above the cut 
00378         // this information tells how many edges point to each node
00379         CutNodes = st_init_table(st_ptrcmp,st_ptrhash);
00380         Visited  = st_init_table(st_ptrcmp,st_ptrhash);
00381 
00382         for ( i = 0; i < nNodes; i++ )
00383                 CountNodeVisits_rec( dd, paNodes[i], Visited );
00384 
00385         // Step 2: Traverse the BDD using the visited table and compute the sum of paths
00386         for ( i = 0; i < nNodes; i++ )
00387                 CollectNodesAndComputePaths_rec( dd, paNodes[i], pbCubes[i], Visited, CutNodes );
00388 
00389         // at this point, the table of cut nodes is ready and the table of visited is useless
00390         {
00391                 st_generator * gen;
00392                 DdNode * aNode;
00393                 traventry * p;
00394                 st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
00395                 {
00396                         Cudd_RecursiveDeref( dd, p->bSum );
00397                         free( p );
00398                 }
00399                 st_free_table( Visited );
00400         }
00401 
00402         // go through the table CutNodes and create the BDD and the path to be returned
00403         {
00404                 st_generator * gen;
00405                 DdNode * aNode, * bSum;
00406                 Counter = 0;
00407                 st_foreach_item( CutNodes, gen, (char**)&aNode, (char**)&bSum) 
00408                 {
00409                         paNodesRes[Counter] = aNode;   Cudd_Ref( aNode ); 
00410                         pbCubesRes[Counter] = bSum;
00411                         Counter++;
00412                 }
00413                 st_free_table( CutNodes );
00414         }
00415 
00416         // return the number of cofactors found
00417         return Counter;
00418 
00419 } /* end of Extra_bddNodePathsUnderCutArray */

st_table* Extra_CollectNodes ( DdNode * Func )

Function*************************************************************

Synopsis [Collects all the nodes of one DD into the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file extraBddCas.c.

00456 {
00457         st_table * tNodes;
00458         tNodes = st_init_table( st_ptrcmp, st_ptrhash );
00459         extraCollectNodes( Func, tNodes );
00460         return tNodes;
00461 }

unsigned Extra_CountCofactorMinterms	(	DdManager *	dd,
		DdNode *	bFunc,
		DdNode *	bVarsCof,
		DdNode *	bVarsAll
	)

Function********************************************************************

Synopsis [Counts the number of encoding minterms pointed to by the cofactor of the function.]

Description []

SideEffects [None]

Definition at line 907 of file extraBddCas.c.

00912 {
00913         unsigned HKey;
00914         DdNode * bFuncR;
00915 
00916         // if the function is zero, there are no minterms
00917 //      if ( bFunc == b0 )
00918 //              return 0;
00919 
00920 //      if ( st_lookup(Visited, (char*)bFunc, NULL) )
00921 //              return 0;
00922 
00923 //      HKey = hashKey2c( s_Signature, bFuncR );
00924 //      if ( HHTable1[HKey].Sign == s_Signature && HHTable1[HKey].Arg1 == bFuncR ) // this node is visited
00925 //              return 0;
00926 
00927 
00928         // check the hash-table 
00929         bFuncR = Cudd_Regular(bFunc);
00930 //      HKey = hashKey2( s_Signature, bFuncR, _TABLESIZE_COF );
00931         HKey = hashKey2( s_Signature, bFunc, _TABLESIZE_COF );
00932         for ( ;  HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF )
00933 //              if ( HHTable1[HKey].Arg1 == bFuncR ) // this node is visited
00934                 if ( HHTable1[HKey].Arg1 == bFunc ) // this node is visited
00935                         return 0;
00936 
00937 
00938         // if the function is already the code
00939         if ( dd->perm[bFuncR->index] >= s_EncodingVarsLevel )
00940         {
00941 //              st_insert(Visited, (char*)bFunc, NULL);
00942 
00943 //              HHTable1[HKey].Sign = s_Signature;
00944 //              HHTable1[HKey].Arg1 = bFuncR;
00945 
00946                 assert( HHTable1[HKey].Sign != s_Signature );
00947                 HHTable1[HKey].Sign = s_Signature;
00948 //              HHTable1[HKey].Arg1 = bFuncR;
00949                 HHTable1[HKey].Arg1 = bFunc;
00950 
00951                 return Extra_CountMintermsSimple( bFunc, (1<<s_MultiStart) );
00952         }
00953         else
00954         {
00955                 DdNode * bFunc0,    * bFunc1;
00956                 DdNode * bVarsCof0, * bVarsCof1;
00957                 DdNode * bVarsCofR = Cudd_Regular(bVarsCof);
00958                 unsigned Res;
00959 
00960                 // get the levels
00961                 int LevelF = dd->perm[bFuncR->index];
00962                 int LevelC = cuddI(dd,bVarsCofR->index);
00963                 int LevelA = dd->perm[bVarsAll->index];
00964 
00965                 int LevelTop = LevelF;
00966 
00967                 if ( LevelTop > LevelC )
00968                          LevelTop = LevelC;
00969 
00970                 if ( LevelTop > LevelA )
00971                          LevelTop = LevelA;
00972 
00973                 // the top var in the function or in cofactoring vars always belongs to the set of all vars
00974                 assert( !( LevelTop == LevelF || LevelTop == LevelC ) || LevelTop == LevelA );
00975 
00976                 // cofactor the function
00977                 if ( LevelTop == LevelF )
00978                 {
00979                         if ( bFuncR != bFunc ) // bFunc is complemented 
00980                         {
00981                                 bFunc0 = Cudd_Not( cuddE(bFuncR) );
00982                                 bFunc1 = Cudd_Not( cuddT(bFuncR) );
00983                         }
00984                         else
00985                         {
00986                                 bFunc0 = cuddE(bFuncR);
00987                                 bFunc1 = cuddT(bFuncR);
00988                         }
00989                 }
00990                 else // bVars is higher in the variable order 
00991                         bFunc0 = bFunc1 = bFunc;
00992 
00993                 // cofactor the cube
00994                 if ( LevelTop == LevelC )
00995                 {
00996                         if ( bVarsCofR != bVarsCof ) // bFunc is complemented 
00997                         {
00998                                 bVarsCof0 = Cudd_Not( cuddE(bVarsCofR) );
00999                                 bVarsCof1 = Cudd_Not( cuddT(bVarsCofR) );
01000                         }
01001                         else
01002                         {
01003                                 bVarsCof0 = cuddE(bVarsCofR);
01004                                 bVarsCof1 = cuddT(bVarsCofR);
01005                         }
01006                 }
01007                 else // bVars is higher in the variable order 
01008                         bVarsCof0 = bVarsCof1 = bVarsCof;
01009 
01010                 // there are two cases: 
01011                 // (1) the top variable belongs to the cofactoring variables
01012                 // (2) the top variable does not belong to the cofactoring variables
01013 
01014                 // (1) the top variable belongs to the cofactoring variables
01015                 Res = 0;
01016                 if ( LevelTop == LevelC )
01017                 {
01018                         if ( bVarsCof1 == b0 ) // this is a negative cofactor
01019                         {
01020                                 if ( bFunc0 != b0 )
01021                                 Res = Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) );
01022                         }
01023                         else                        // this is a positive cofactor
01024                         {
01025                                 if ( bFunc1 != b0 )
01026                                 Res = Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) );
01027                         }
01028                 }
01029                 else
01030                 {
01031                         if ( bFunc0 != b0 )
01032                         Res += Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) );
01033                         
01034                         if ( bFunc1 != b0 )
01035                         Res += Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) );
01036                 }
01037 
01038 //              st_insert(Visited, (char*)bFunc, NULL);
01039 
01040 //              HHTable1[HKey].Sign = s_Signature;
01041 //              HHTable1[HKey].Arg1 = bFuncR;
01042 
01043                 // skip through the entries with the same signatures 
01044                 // (these might have been created at the time of recursive calls)
01045                 for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF );
01046                 assert( HHTable1[HKey].Sign != s_Signature );
01047                 HHTable1[HKey].Sign = s_Signature;
01048 //              HHTable1[HKey].Arg1 = bFuncR;
01049                 HHTable1[HKey].Arg1 = bFunc;
01050 
01051                 return Res;
01052         }
01053 }

unsigned Extra_CountMintermsSimple	(	DdNode *	bFunc,
		unsigned	max
	)			`[static]`

Function********************************************************************

Synopsis [Counts the number of minterms.]

Description [This function counts minterms for functions up to 32 variables using a local cache. The terminal value (s_Termina) should be adjusted for BDDs and ADDs.]

SideEffects [None]

Definition at line 1066 of file extraBddCas.c.

01067 {
01068         unsigned HKey;
01069 
01070         // normalize
01071         if ( Cudd_IsComplement(bFunc) )
01072                 return max - Extra_CountMintermsSimple( Cudd_Not(bFunc), max );
01073 
01074         // now it is known that the function is not complemented
01075         if ( cuddIsConstant(bFunc) )
01076                 return ((bFunc==s_Terminal)? 0: max);
01077 
01078         // check cache
01079         HKey = hashKey2( bFunc, max, _TABLESIZE_MINT );
01080         if ( HHTable2[HKey].Arg1 == bFunc && HHTable2[HKey].Arg2 == max )
01081                 return HHTable2[HKey].Res;
01082         else
01083         {
01084                 // min = min0/2 + min1/2;
01085                 unsigned min = (Extra_CountMintermsSimple( cuddE(bFunc), max ) >> 1) +
01086                                    (Extra_CountMintermsSimple( cuddT(bFunc), max ) >> 1);
01087 
01088                 HHTable2[HKey].Arg1 = bFunc;
01089                 HHTable2[HKey].Arg2 = max;
01090                 HHTable2[HKey].Res  = min;
01091 
01092                 return min;
01093         }
01094 }       /* end of Extra_CountMintermsSimple */

int Extra_ProfileWidth	(	DdManager *	dd,
		DdNode *	Func,
		int *	pProfile,
		int	CutLevel
	)

Function*************************************************************

Synopsis [Fast computation of the BDD profile.]

Description [The array to store the profile is given by the user and should contain at least as many entries as there is the maximum of the BDD/ZDD size of the manager PLUS ONE. When we say that the widths of the DD on level L is W, we mean the following. Let us create the cut between the level L-1 and the level L and count the number of different DD nodes pointed to across the cut. This number is the width W. From this it follows the on level 0, the width is equal to the number of external pointers to the considered DDs. If there is only one DD, then the profile on level 0 is always 1. If this DD is rooted in the topmost variable, then the width on level 1 is always 2, etc. The width at the level equal to dd->size is the number of terminal nodes in the DD. (Because we consider the first level #0 and the last level dd->size, the profile array should contain dd->size+1 entries.) ]

SideEffects [This procedure will not work for BDDs w/ complement edges, only for ADDs and ZDDs]

SeeAlso []

Definition at line 516 of file extraBddCas.c.

00517 {
00518         st_generator * gen;
00519         st_table * tNodeTopRef; // this table stores the top level from which this node is pointed to
00520         st_table * tNodes;
00521         DdNode * node;
00522         DdNode * nodeR;
00523         int LevelStart, Limit;
00524     int i, size;
00525         int WidthMax;
00526   
00527         // start the mapping table
00528         tNodeTopRef = st_init_table(st_ptrcmp,st_ptrhash);
00529         // add the topmost node to the profile
00530         extraProfileUpdateTopLevel( tNodeTopRef, 0, Func );
00531 
00532         // collect all nodes
00533         tNodes = Extra_CollectNodes( Func );
00534         // go though all the nodes and set the top level the cofactors are pointed from
00535 //      Cudd_ForeachNode( dd, Func, genDD, node )
00536         st_foreach_item( tNodes, gen, (char**)&node, NULL )
00537         {
00538 //              assert( Cudd_Regular(node) );  // this procedure works only with ADD/ZDD (not BDD w/ compl.edges)
00539                 nodeR = Cudd_Regular(node);
00540                 if ( cuddIsConstant(nodeR) )
00541                         continue;
00542                 // this node is not a constant - consider its cofactors
00543                 extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddE(nodeR) );
00544                 extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddT(nodeR) );
00545         }
00546         st_free_table( tNodes );
00547 
00548     // clean the profile
00549     size = ddMax(dd->size, dd->sizeZ) + 1;
00550     for ( i = 0; i < size; i++ ) 
00551                 pProfile[i] = 0;
00552 
00553         // create the profile
00554         st_foreach_item( tNodeTopRef, gen, (char**)&node, (char**)&LevelStart )
00555         {
00556                 nodeR = Cudd_Regular(node);
00557                 Limit = (cuddIsConstant(nodeR))? dd->size: dd->perm[nodeR->index];
00558                 for ( i = LevelStart; i <= Limit; i++ )
00559                         pProfile[i]++;
00560         }
00561 
00562         if ( CutLevel != -1 && CutLevel != 0  )
00563                 size = CutLevel;
00564 
00565         // get the max width
00566         WidthMax = 0;
00567     for ( i = 0; i < size; i++ ) 
00568                 if ( WidthMax < pProfile[i] )
00569                         WidthMax = pProfile[i];
00570 
00571         // deref the table
00572         st_free_table( tNodeTopRef );
00573 
00574         return WidthMax;
00575 } /* end of Extra_ProfileWidth */

void extraCollectNodes	(	DdNode *	Func,
		st_table *	tNodes
	)

Function*************************************************************

Synopsis [Collects all the BDD nodes into the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 432 of file extraBddCas.c.

00433 {
00434         DdNode * FuncR;
00435         FuncR = Cudd_Regular(Func);
00436         if ( st_find_or_add( tNodes, (char*)FuncR, NULL ) )
00437                 return;
00438         if ( cuddIsConstant(FuncR) )
00439                 return;
00440         extraCollectNodes( cuddE(FuncR), tNodes );
00441         extraCollectNodes( cuddT(FuncR), tNodes );
00442 }

void extraProfileUpdateTopLevel	(	st_table *	tNodeTopRef,
		int	TopLevelNew,
		DdNode *	node
	)

Function*************************************************************

Synopsis [Updates the topmost level from which the given node is referenced.]

Description [Takes the table which maps each BDD nodes (including the constants) into the topmost level on which this node counts as a cofactor. Takes the topmost level, on which this node counts as a cofactor (see Extra_ProfileWidthFast(). Takes the node, for which the table entry should be updated.]

SideEffects []

SeeAlso []

Definition at line 477 of file extraBddCas.c.

00478 {
00479         int * pTopLevel;
00480 
00481         if ( st_find_or_add( tNodeTopRef, (char*)node, (char***)&pTopLevel ) )
00482         { // the node is already referenced
00483                 // the current top level should be updated if it is larger than the new level
00484                 if ( *pTopLevel > TopLevelNew ) 
00485                          *pTopLevel = TopLevelNew;
00486         }
00487         else
00488         { // the node is not referenced
00489                 // its level should be set to the current new level
00490                 *pTopLevel = TopLevelNew;
00491         }
00492 }