ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bdcSpfd.c File Reference
#include "bdcInt.h"
#include "aig/aig/aig.h"
#include "misc/extra/extra.h"
Include dependency graph for bdcSpfd.c:

Go to the source code of this file.

Classes

struct  Bdc_Nod_t_
 
struct  Bdc_Ent_t_
 

Macros

#define BDC_TERM   0x1FFFFFFF
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t
 DECLARATIONS ///.
 
typedef struct Bdc_Ent_t_ Bdc_Ent_t
 

Functions

int Bdc_SpfdAdjCost (word t)
 
void Abc_Show6VarFunc (word F0, word F1)
 
void Bdc_SpfdPrint_rec (Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
 FUNCTION DEFINITIONS ///.
 
void Bdc_SpfdPrint (Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels, word Truth)
 
void Bdc_SpfdDecompose (word Truth, int nVars, int nCands, int nGatesMax)
 
void Bdc_SpfdDecomposeTest_ ()
 
int Bdc_SpfdMark0 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
int Bdc_SpfdMark1 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
void Bdc_SpfdUnmark0 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
void Bdc_SpfdUnmark1 (Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
 
int Bdc_SpfdCheckOverlap (Bdc_Ent_t *p, Bdc_Ent_t *pEnt0, Bdc_Ent_t *pEnt1)
 
int Bdc_SpfdHashValue (word t, int Size)
 
int * Bdc_SpfdHashLookup (Bdc_Ent_t *p, int Size, word t)
 
Vec_Wrd_tBdc_SpfdDecomposeTest__ (Vec_Int_t **pvWeights)
 
Vec_Wrd_tBdc_SpfdReadFiles5 (Vec_Int_t **pvWeights)
 
Vec_Wrd_tBdc_SpfdReadFiles6 (Vec_Int_t **pvWeights)
 
int Bdc_SpfdComputeCost (word f, int i, Vec_Int_t *vWeights)
 
word Bdc_SpfdFindBest (Vec_Wrd_t *vDivs, Vec_Int_t *vWeights, word F0, word F1, int *pCost)
 
int Bdc_SpfdDecomposeTestOne (word t, Vec_Wrd_t *vDivs, Vec_Int_t *vWeights)
 
void Bdc_SpfdDecomposeTest44 ()
 
void Bdc_SpfdDecomposeTest3 ()
 
void Bdc_SpfdDecomposeTest8 ()
 
void Bdc_SpfdDecomposeTest ()
 

Macro Definition Documentation

◆ BDC_TERM

#define BDC_TERM   0x1FFFFFFF

Definition at line 415 of file bdcSpfd.c.

Typedef Documentation

◆ Bdc_Ent_t

typedef struct Bdc_Ent_t_ Bdc_Ent_t

Definition at line 399 of file bdcSpfd.c.

◆ Bdc_Nod_t

typedef typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t

DECLARATIONS ///.

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

FileName [bdcSpfd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Truth-table-based bi-decomposition engine.]

Synopsis [The gateway to bi-decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 30, 2007.]

Revision [

Id
bdcSpfd.c,v 1.00 2007/01/30 00:00:00 alanmi Exp

]

Definition at line 32 of file bdcSpfd.c.

Function Documentation

◆ Abc_Show6VarFunc()

void Abc_Show6VarFunc ( word F0,
word F1 )
extern

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

Synopsis [Prints K-map of 6-var function represented by truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2007 of file abcPrint.c.

2008{
2009 // order of cells in the Karnaugh map
2010// int Cells[8] = { 0, 1, 3, 2, 6, 7, 5, 4 };
2011 int Cells[8] = { 0, 4, 6, 2, 3, 7, 5, 1 };
2012 // intermediate variables
2013 int s; // symbol counter
2014 int h; // horizontal coordinate;
2015 int v; // vertical coordinate;
2016 assert( (F0 & F1) == 0 );
2017
2018 // output minterms above
2019 for ( s = 0; s < 4; s++ )
2020 printf( " " );
2021 printf( " " );
2022 for ( h = 0; h < 8; h++ )
2023 {
2024 for ( s = 0; s < 3; s++ )
2025 printf( "%d", ((Cells[h] >> (2-s)) & 1) );
2026 printf( " " );
2027 }
2028 printf( "\n" );
2029
2030 // output horizontal line above
2031 for ( s = 0; s < 4; s++ )
2032 printf( " " );
2033 printf( "+" );
2034 for ( h = 0; h < 8; h++ )
2035 {
2036 for ( s = 0; s < 3; s++ )
2037 printf( "-" );
2038 printf( "+" );
2039 }
2040 printf( "\n" );
2041
2042 // output lines with function values
2043 for ( v = 0; v < 8; v++ )
2044 {
2045 for ( s = 0; s < 3; s++ )
2046 printf( "%d", ((Cells[v] >> (2-s)) & 1) );
2047 printf( " |" );
2048
2049 for ( h = 0; h < 8; h++ )
2050 {
2051 printf( " " );
2052 if ( ((F0 >> ((Cells[v]*8)+Cells[h])) & 1) )
2053 printf( "0" );
2054 else if ( ((F1 >> ((Cells[v]*8)+Cells[h])) & 1) )
2055 printf( "1" );
2056 else
2057 printf( " " );
2058 printf( " |" );
2059 }
2060 printf( "\n" );
2061
2062 // output horizontal line above
2063 for ( s = 0; s < 4; s++ )
2064 printf( " " );
2065// printf( "%c", v == 7 ? '+' : '|' );
2066 printf( "+" );
2067 for ( h = 0; h < 8; h++ )
2068 {
2069 for ( s = 0; s < 3; s++ )
2070 printf( "-" );
2071// printf( "%c", v == 7 ? '+' : '|' );
2072 printf( "%c", (v == 7 || h == 7) ? '+' : '|' );
2073 }
2074 printf( "\n" );
2075 }
2076}
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Bdc_SpfdAdjCost()

int Bdc_SpfdAdjCost ( word t)

Definition at line 83 of file bdcSpfd.c.

84{
85 word c0, c1;
86 int v, Cost = 0;
87 for ( v = 0; v < 6; v++ )
88 {
89 c0 = Bdc_Cof6( t, v, 0 );
90 c1 = Bdc_Cof6( t, v, 1 );
91 Cost += Bdc_CountOnes( c0 ^ c1 );
92 }
93 return Cost;
94}
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Here is the caller graph for this function:

◆ Bdc_SpfdCheckOverlap()

int Bdc_SpfdCheckOverlap ( Bdc_Ent_t * p,
Bdc_Ent_t * pEnt0,
Bdc_Ent_t * pEnt1 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file bdcSpfd.c.

481{
482 int RetValue;
483 RetValue = Bdc_SpfdMark0( p, pEnt0 );
484 assert( RetValue == 0 );
485 RetValue = Bdc_SpfdMark1( p, pEnt1 );
486 Bdc_SpfdUnmark0( p, pEnt0 );
487 Bdc_SpfdUnmark1( p, pEnt1 );
488 return RetValue;
489}
void Bdc_SpfdUnmark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:459
int Bdc_SpfdMark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:429
void Bdc_SpfdUnmark0(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:451
int Bdc_SpfdMark1(Bdc_Ent_t *p, Bdc_Ent_t *pEnt)
Definition bdcSpfd.c:440
Cube * p
Definition exorList.c:222
Here is the call graph for this function:

◆ Bdc_SpfdComputeCost()

int Bdc_SpfdComputeCost ( word f,
int i,
Vec_Int_t * vWeights )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 787 of file bdcSpfd.c.

788{
789 int Ones = Bdc_CountOnes(f);
790 if ( Ones == 0 )
791 return -1;
792 return 7*Ones + 10*(8 - Vec_IntEntry(vWeights, i));
793// return Bdc_CountOnes(f);
794}
Here is the caller graph for this function:

◆ Bdc_SpfdDecompose()

void Bdc_SpfdDecompose ( word Truth,
int nVars,
int nCands,
int nGatesMax )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file bdcSpfd.c.

179{
180 int nSize = nCands * nCands * (nGatesMax + 1) * 5;
181 Vec_Ptr_t * vLevels;
182 Vec_Int_t * vBegs, * vWeight;
183 Bdc_Nod_t * pNode, * pNode0, * pNode1, * pNode2;
184 int Count0, Count1, * pPerm;
185 int i, j, k, c, n;
186 abctime clk;
187 assert( nGatesMax < (1<<8) );
188 assert( nCands < (1<<12) );
189 assert( (1<<(nVars-1))*(1<<(nVars-1)) < (1<<12) ); // max SPFD
190
191 printf( "Storage size = %d (%d * %d * %d * %d).\n", nSize, nCands, nCands, nGatesMax + 1, 5 );
192
193 printf( "SPFD = %d.\n", Bdc_CountOnes(Truth) * Bdc_CountOnes(~Truth) );
194
195 // consider elementary functions
196 if ( Truth == 0 || Truth == ~0 )
197 {
198 printf( "Function is a constant.\n" );
199 return;
200 }
201 for ( i = 0; i < nVars; i++ )
202 if ( Truth == Truths[i] || Truth == ~Truths[i] )
203 {
204 printf( "Function is an elementary variable.\n" );
205 return;
206 }
207
208 // allocate
209 vLevels = Vec_PtrAlloc( 100 );
210 vBegs = Vec_IntAlloc( 100 );
211 vWeight = Vec_IntAlloc( 100 );
212
213 // initialize elementary variables
214 pNode = ABC_CALLOC( Bdc_Nod_t, (unsigned char)nVars );
215 for ( i = 0; i < nVars; i++ )
216 pNode[i].Truth = Truths[i];
217 for ( i = 0; i < nVars; i++ )
218 pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
219 Vec_PtrPush( vLevels, pNode );
220 Vec_IntPush( vBegs, nVars );
221
222 // the next level
223clk = Abc_Clock();
224 pNode0 = pNode;
225 pNode = ABC_CALLOC( Bdc_Nod_t, 5 * nVars * (nVars - 1) / 2 );
226 for ( c = i = 0; i < nVars; i++ )
227 for ( j = i+1; j < nVars; j++ )
228 {
229 pNode[c].Truth = pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
230 pNode[c].Truth = ~pNode0[i].Truth & pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
231 pNode[c].Truth = pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
232 pNode[c].Truth = ~pNode0[i].Truth & ~pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
233 pNode[c].Truth = pNode0[i].Truth ^ pNode0[j].Truth; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
234 }
235 assert( c == 5 * nVars * (nVars - 1) / 2 );
236 Vec_PtrPush( vLevels, pNode );
237 Vec_IntPush( vBegs, c );
238 for ( i = 0; i < c; i++ )
239 {
240 pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
241//Bdc_SpfdPrint( pNode + i, 1, vLevels );
242 if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
243 {
244 printf( "Function can be implemented using 1 gate.\n" );
245 pNode = NULL;
246 goto cleanup;
247 }
248 }
249printf( "Selected %6d gates on level %2d. ", c, 1 );
250Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
251
252
253 // iterate through levels
254 pNode = ABC_CALLOC( Bdc_Nod_t, nSize );
255 for ( n = 2; n <= nGatesMax; n++ )
256 {
257clk = Abc_Clock();
258 c = 0;
259 pNode1 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, n-1 );
260 Count1 = Vec_IntEntry( vBegs, n-1 );
261 // go through previous levels
262 for ( k = 0; k < n-1; k++ )
263 {
264 pNode0 = (Bdc_Nod_t *)Vec_PtrEntry( vLevels, k );
265 Count0 = Vec_IntEntry( vBegs, k );
266 for ( i = 0; i < Count0; i++ )
267 for ( j = 0; j < Count1; j++ )
268 {
269 pNode[c].Truth = pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
270 pNode[c].Truth = ~pNode0[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
271 pNode[c].Truth = pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
272 pNode[c].Truth = ~pNode0[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
273 pNode[c].Truth = pNode0[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = k; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
274 }
275 assert( c < nSize );
276 }
277 // go through current level
278 for ( i = 0; i < Count1; i++ )
279 for ( j = i+1; j < Count1; j++ )
280 {
281 pNode[c].Truth = pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 0;
282 pNode[c].Truth = ~pNode1[i].Truth & pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 1;
283 pNode[c].Truth = pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 2;
284 pNode[c].Truth = ~pNode1[i].Truth & ~pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 3;
285 pNode[c].Truth = pNode1[i].Truth ^ pNode1[j].Truth; pNode[c].iFan0g = n-1; pNode[c].iFan1g = n-1; pNode[c].iFan0n = i; pNode[c].iFan1n = j; pNode[c++].Type = 4;
286 }
287 assert( c < nSize );
288 // sort
289 Vec_IntClear( vWeight );
290 for ( i = 0; i < c; i++ )
291 {
292 pNode[i].Weight = Bdc_CountSpfd( pNode[i].Truth, Truth );
293if ( pNode[i].Weight > 300 )
294Bdc_SpfdPrint( pNode + i, 1, vLevels, Truth );
295 Vec_IntPush( vWeight, pNode[i].Weight );
296
297 if ( Truth == pNode[i].Truth || Truth == ~pNode[i].Truth )
298 {
299 printf( "Function can be implemented using %d gates.\n", n );
300 Bdc_SpfdPrint( pNode + i, n, vLevels, Truth );
301 goto cleanup;
302 }
303 }
304 pPerm = Abc_MergeSortCost( Vec_IntArray(vWeight), c );
305 assert( Vec_IntEntry(vWeight, pPerm[0]) <= Vec_IntEntry(vWeight, pPerm[c-1]) );
306
307 printf( "Best SPFD = %d.\n", Vec_IntEntry(vWeight, pPerm[c-1]) );
308// for ( i = 0; i < c; i++ )
309//printf( "%d ", Vec_IntEntry(vWeight, pPerm[i]) );
310
311 // choose the best ones
312 pNode2 = ABC_CALLOC( Bdc_Nod_t, nCands );
313 for ( j = 0, i = c-1; i >= 0; i-- )
314 {
315 pNode2[j++] = pNode[pPerm[i]];
316 if ( j == nCands )
317 break;
318 }
319 ABC_FREE( pPerm );
320 Vec_PtrPush( vLevels, pNode2 );
321 Vec_IntPush( vBegs, j );
322
323printf( "Selected %6d gates (out of %6d) on level %2d. ", j, c, n );
324Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
325
326 for ( i = 0; i < 10; i++ )
327 Bdc_SpfdPrint( pNode2 + i, n, vLevels, Truth );
328 }
329
330cleanup:
331 ABC_FREE( pNode );
332 Vec_PtrForEachEntry( Bdc_Nod_t *, vLevels, pNode, i )
333 ABC_FREE( pNode );
334 Vec_PtrFree( vLevels );
335 Vec_IntFree( vBegs );
336 Vec_IntFree( vWeight );
337}
ABC_INT64_T abctime
Definition abc_global.h:332
int * Abc_MergeSortCost(int *pCosts, int nSize)
Definition utilSort.c:442
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
void Bdc_SpfdPrint(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels, word Truth)
Definition bdcSpfd.c:158
typedefABC_NAMESPACE_IMPL_START struct Bdc_Nod_t_ Bdc_Nod_t
DECLARATIONS ///.
Definition bdcSpfd.c:32
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdDecomposeTest()

void Bdc_SpfdDecomposeTest ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1135 of file bdcSpfd.c.

1136{
1137 int nSizeM = (1 << 26); // big array size
1138 int nSizeK = (1 << 3); // small array size
1139 Vec_Wrd_t * v1M, * v1K;
1140 int EntryM, EntryK;
1141 int i, k, Counter;
1142 abctime clk;
1143
1144 Aig_ManRandom64( 1 );
1145
1146 v1M = Vec_WrdAlloc( nSizeM );
1147 for ( i = 0; i < nSizeM; i++ )
1148 Vec_WrdPush( v1M, Aig_ManRandom64(0) );
1149
1150 v1K = Vec_WrdAlloc( nSizeK );
1151 for ( i = 0; i < nSizeK; i++ )
1152 Vec_WrdPush( v1K, Aig_ManRandom64(0) );
1153
1154 clk = Abc_Clock();
1155 Counter = 0;
1156// for ( i = 0; i < nSizeM; i++ )
1157// for ( k = 0; k < nSizeK; k++ )
1158// Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1159 Vec_WrdForEachEntry( v1M, EntryM, i )
1160 Vec_WrdForEachEntry( v1K, EntryK, k )
1161 Counter += ((EntryM & EntryK) == EntryK);
1162 printf( "Total = %8d. ", Counter );
1163 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1164
1165 clk = Abc_Clock();
1166 Counter = 0;
1167// for ( k = 0; k < nSizeK; k++ )
1168// for ( i = 0; i < nSizeM; i++ )
1169// Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1170 Vec_WrdForEachEntry( v1K, EntryK, k )
1171 Vec_WrdForEachEntry( v1M, EntryM, i )
1172 Counter += ((EntryM & EntryK) == EntryK);
1173 printf( "Total = %8d. ", Counter );
1174 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1175}
word Aig_ManRandom64(int fReset)
Definition aigUtil.c:1200
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42
Here is the call graph for this function:

◆ Bdc_SpfdDecomposeTest3()

void Bdc_SpfdDecomposeTest3 ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1028 of file bdcSpfd.c.

1029{
1030 int nSizeM = (1 << 26);
1031 int nSizeK = (1 << 3);
1032 Vec_Wrd_t * v1M;
1033 Vec_Wrd_t * v1K;
1034 int i, k, Counter;
1035 abctime clk;
1036// int EntryM, EntryK;
1037 Aig_ManRandom64( 1 );
1038
1039 v1M = Vec_WrdAlloc( nSizeM );
1040 for ( i = 0; i < nSizeM; i++ )
1041 Vec_WrdPush( v1M, Aig_ManRandom64(0) );
1042
1043 v1K = Vec_WrdAlloc( nSizeK );
1044 for ( i = 0; i < nSizeK; i++ )
1045 Vec_WrdPush( v1K, Aig_ManRandom64(0) );
1046
1047 clk = Abc_Clock();
1048 Counter = 0;
1049 for ( i = 0; i < nSizeM; i++ )
1050 for ( k = 0; k < nSizeK; k++ )
1051 Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1052// Vec_WrdForEachEntry( v1M, EntryM, i )
1053// Vec_WrdForEachEntry( v1K, EntryK, k )
1054// Counter += ((EntryM & EntryK) == EntryK);
1055
1056 printf( "Total = %8d. ", Counter );
1057 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1058
1059 clk = Abc_Clock();
1060 Counter = 0;
1061 for ( k = 0; k < nSizeK; k++ )
1062 for ( i = 0; i < nSizeM; i++ )
1063 Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]);
1064 printf( "Total = %8d. ", Counter );
1065 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1066
1067}
Here is the call graph for this function:

◆ Bdc_SpfdDecomposeTest44()

void Bdc_SpfdDecomposeTest44 ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 905 of file bdcSpfd.c.

906{
907// word t = 0x5052585a0002080a;
908
909 word t = ABC_CONST(0x9ef7a8d9c7193a0f);
910// word t = 0x6BFDA276C7193A0F;
911// word t = 0xA3756AFE0B1DF60B;
912
913// word t = 0xFEF7AEBFCE80AA0F;
914// word t = 0x9EF7FDBFC77F6F0F;
915// word t = 0xDEF7FDFF377F6FFF;
916
917// word t = 0x345D02736DB390A5; // xor with var 0
918
919// word t = 0x3EFDA2736D139A0F; // best solution after changes
920
921 Vec_Int_t * vWeights;
922 Vec_Wrd_t * vDivs;
923 word c0, c1, s, tt, tbest;
924 int i, j, Cost, CostBest = 100000;
925 abctime clk = Abc_Clock();
926
927 return;
928
929// printf( "%d\n", RAND_MAX );
930
931 vDivs = Bdc_SpfdDecomposeTest__( &vWeights );
932// vDivs = Bdc_SpfdReadFiles5( &vWeights );
933
934// Abc_Show6VarFunc( ~t, t );
935
936 // try function
937 tt = t;
938 Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
939 if ( CostBest > Cost )
940 {
941 CostBest = Cost;
942 tbest = tt;
943 }
944 printf( "\n" );
945
946 // try complemented output
947 for ( i = 0; i < 6; i++ )
948 {
949 tt = t ^ Truths[i];
950 Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
951 if ( CostBest > Cost )
952 {
953 CostBest = Cost;
954 tbest = tt;
955 }
956 }
957 printf( "\n" );
958
959 // try complemented input
960 for ( i = 0; i < 6; i++ )
961 for ( j = 0; j < 6; j++ )
962 {
963 if ( i == j )
964 continue;
965 c0 = Bdc_Cof6( t, i, 0 );
966 c1 = Bdc_Cof6( t, i, 1 );
967 s = Truths[i] ^ Truths[j];
968 tt = (~s & c0) | (s & c1);
969
970 Cost = Bdc_SpfdDecomposeTestOne( tt, vDivs, vWeights );
971 if ( CostBest > Cost )
972 {
973 CostBest = Cost;
974 tbest = tt;
975 }
976 }
977
978/*
979 for ( i = 0; i < 6; i++ )
980 for ( j = 0; j < 6; j++ )
981 {
982 if ( i == j )
983 continue;
984 c0 = Bdc_Cof6( t, i, 0 );
985 c1 = Bdc_Cof6( t, i, 1 );
986 s = Truths[i] ^ Truths[j];
987 tt = (~s & c0) | (s & c1);
988
989 for ( k = 0; k < 6; k++ )
990 for ( n = 0; n < 6; n++ )
991 {
992 if ( k == n )
993 continue;
994 c0 = Bdc_Cof6( tt, k, 0 );
995 c1 = Bdc_Cof6( tt, k, 1 );
996 s = Truths[k] ^ Truths[n];
997 ttt= (~s & c0) | (s & c1);
998
999 Cost = Bdc_SpfdDecomposeTestOne( ttt, vDivs, vWeights );
1000 if ( CostBest > Cost )
1001 {
1002 CostBest = Cost;
1003 tbest = ttt;
1004 }
1005 }
1006 }
1007*/
1008
1009 printf( "Best solution found with cost %d. ", CostBest );
1010 Extra_PrintHex( stdout, (unsigned *)&tbest, 6 ); //printf( "\n" );
1011 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1012
1013 Vec_WrdFree( vDivs );
1014 Vec_IntFree( vWeights );
1015}
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
Vec_Wrd_t * Bdc_SpfdDecomposeTest__(Vec_Int_t **pvWeights)
Definition bdcSpfd.c:577
int Bdc_SpfdDecomposeTestOne(word t, Vec_Wrd_t *vDivs, Vec_Int_t *vWeights)
Definition bdcSpfd.c:872
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Here is the call graph for this function:

◆ Bdc_SpfdDecomposeTest8()

void Bdc_SpfdDecomposeTest8 ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1080 of file bdcSpfd.c.

1081{
1082// word t = 0x9ef7a8d9c7193a0f;
1083// word t = 0x9EF7FDBFC77F6F0F;
1084 word t = ABC_CONST(0x513B57150819050F);
1085
1086 Vec_Int_t * vWeights;
1087 Vec_Wrd_t * vDivs;
1088 word Func, FuncBest;
1089 int Cost, CostBest = ABC_INFINITY;
1090 int i;
1091 abctime clk = Abc_Clock();
1092
1093// return;
1094
1095 vDivs = Bdc_SpfdReadFiles5( &vWeights );
1096
1097 printf( "Best init = %4d. ", Bdc_SpfdAdjCost(t) );
1098 Extra_PrintHex( stdout, (unsigned *)&t, 6 ); //printf( "\n" );
1099 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1100
1101 Vec_WrdForEachEntry( vDivs, Func, i )
1102 {
1103 Cost = Bdc_SpfdAdjCost( t ^ Func );
1104 if ( CostBest > Cost )
1105 {
1106 CostBest = Cost;
1107 FuncBest = Func;
1108 }
1109 }
1110
1111 printf( "Best cost = %4d. ", CostBest );
1112 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); //printf( "\n" );
1113 Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
1114
1115Abc_Show6VarFunc( 0, t );
1116Abc_Show6VarFunc( 0, FuncBest );
1117Abc_Show6VarFunc( 0, (FuncBest ^ t) );
1118
1119 FuncBest ^= t;
1120 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
1121
1122}
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
Vec_Wrd_t * Bdc_SpfdReadFiles5(Vec_Int_t **pvWeights)
Definition bdcSpfd.c:726
int Bdc_SpfdAdjCost(word t)
Definition bdcSpfd.c:83
void Abc_Show6VarFunc(word F0, word F1)
Definition abcPrint.c:2007
Here is the call graph for this function:

◆ Bdc_SpfdDecomposeTest_()

void Bdc_SpfdDecomposeTest_ ( )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file bdcSpfd.c.

352{
353 int fTry = 0;
354// word T[17];
355// int i;
356
357// word Truth = Truths[0] & ~Truths[3];
358// word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]) | (Truths[4] & Truths[5]);
359// word Truth = (Truths[0] & Truths[1]) | ((Truths[2] & ~Truths[3]) ^ (Truths[4] & ~Truths[5]));
360// word Truth = (Truths[0] & Truths[1]) | (Truths[2] & Truths[3]);
361// word Truth = 0x9ef7a8d9c7193a0f; // AAFFAAFF0A0F0A0F
362// word Truth = 0x34080226CD163000;
363 word Truth = ABC_CONST(0x5052585a0002080a);
364 int nVars = 6;
365 int nCands = 200;// 75;
366 int nGatesMax = 20;
367
368 if ( fTry )
369 Bdc_SpfdDecompose( Truth, nVars, nCands, nGatesMax );
370/*
371 for ( i = 0; i < 6; i++ )
372 T[i] = Truths[i];
373 T[7] = 0;
374 T[8] = ~T[1] & T[3];
375 T[9] = ~T[8] & T[0];
376 T[10] = T[1] & T[4];
377 T[11] = T[10] & T[2];
378 T[12] = T[11] & T[9];
379 T[13] = ~T[0] & T[5];
380 T[14] = T[2] & T[13];
381 T[15] = ~T[12] & ~T[14];
382 T[16] = ~T[15];
383// if ( T[16] != Truth )
384// printf( "Failed\n" );
385
386 for ( i = 0; i < 17; i++ )
387 {
388// printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], Truth) );
389 printf( "%2d = %3d ", i, Bdc_CountSpfd(T[i], T[16]) );
390 Extra_PrintBinary( stdout, (unsigned *)&T[i], 64 ); printf( "\n" );
391 }
392// Extra_PrintBinary( stdout, (unsigned *)&Truth, 64 ); printf( "\n" );
393*/
394}
void Bdc_SpfdDecompose(word Truth, int nVars, int nCands, int nGatesMax)
Definition bdcSpfd.c:178
Here is the call graph for this function:

◆ Bdc_SpfdDecomposeTest__()

Vec_Wrd_t * Bdc_SpfdDecomposeTest__ ( Vec_Int_t ** pvWeights)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 577 of file bdcSpfd.c.

578{
579// int nFuncs = 8000000; // the number of functions to compute
580// int nSize = 2777111; // the hash table size to use
581// int Limit = 6;
582
583// int nFuncs = 51000000; // the number of functions to compute
584// int nSize = 50331653; // the hash table size to use
585// int Limit = 6;
586
587 int nFuncs = 250000000; // the number of functions to compute
588 int nSize = 201326611; // the hash table size to use
589 int Limit = 6;
590
591 int * pPlace, i, n, m, k, s, fCompl;
592 abctime clk = Abc_Clock(), clk2;
593 Vec_Int_t * vStops;
594 Vec_Wrd_t * vTruths;
595 Vec_Int_t * vWeights;
596 Bdc_Ent_t * p, * q, * pBeg0, * pEnd0, * pBeg1, * pEnd1, * pThis0, * pThis1;
597 word t0, t1, t;
598 assert( nSize <= nFuncs );
599
600 printf( "Allocating %.2f MB of internal memory.\n", 1.0*sizeof(Bdc_Ent_t)*nFuncs/(1<<20) );
601
602 p = (Bdc_Ent_t *)calloc( nFuncs, sizeof(Bdc_Ent_t) );
603 memset( p, 255, sizeof(Bdc_Ent_t) );
604 p->iList = 0;
605 for ( q = p; q < p+nFuncs; q++ )
606 q->iList = 0;
607 q = p + 1;
608 printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
609
610 vTruths = Vec_WrdStart( nFuncs );
611 vWeights = Vec_IntStart( nFuncs );
612 Vec_WrdClear( vTruths );
613 Vec_IntClear( vWeights );
614
615 // create elementary vars
616 vStops = Vec_IntAlloc( 10 );
617 Vec_IntPush( vStops, 1 );
618 for ( i = 0; i < 6; i++ )
619 {
620 q->iFan0 = BDC_TERM;
621 q->iFan1 = i;
622 q->Truth = Truths[i];
623 pPlace = Bdc_SpfdHashLookup( p, nSize, q->Truth );
624 *pPlace = q-p;
625 q++;
626 Vec_WrdPush( vTruths, Truths[i] );
627 Vec_IntPush( vWeights, 0 );
628 }
629 Vec_IntPush( vStops, 7 );
630 printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
631
632 // create gates
633 for ( n = 0; n < Limit; n++ )
634 {
635 // try previous
636 for ( k = 0; k < Limit; k++ )
637 for ( m = 0; m < Limit; m++ )
638 {
639 if ( k + m != n || k > m )
640 continue;
641 // set the start and stop
642 pBeg0 = p + Vec_IntEntry( vStops, k );
643 pEnd0 = p + Vec_IntEntry( vStops, k+1 );
644 // set the start and stop
645 pBeg1 = p + Vec_IntEntry( vStops, m );
646 pEnd1 = p + Vec_IntEntry( vStops, m+1 );
647
648 clk2 = Abc_Clock();
649 printf( "Trying %7d x %7d. ", (int)(pEnd0-pBeg0), (int)(pEnd1-pBeg1) );
650 for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
651 for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
652 if ( k < m || pThis1 > pThis0 )
653// if ( n < 5 || Bdc_SpfdCheckOverlap(p, pThis0, pThis1) )
654 for ( s = 0; s < 5; s++ )
655 {
656 t0 = (s&1) ? ~pThis0->Truth : pThis0->Truth;
657 t1 = ((s>>1)&1) ? ~pThis1->Truth : pThis1->Truth;
658 t = ((s>>2)&1) ? t0 ^ t1 : t0 & t1;
659 fCompl = t & 1;
660 if ( fCompl )
661 t = ~t;
662 if ( t == 0 )
663 continue;
664 pPlace = Bdc_SpfdHashLookup( p, nSize, t );
665 if ( pPlace == NULL )
666 continue;
667 q->iFan0 = pThis0-p;
668 q->fCompl0 = s&1;
669 q->iFan1 = pThis1-p;
670 q->fCompl1 = (s>>1)&1;
671 q->fExor = (s>>2)&1;
672 q->Truth = t;
673 q->fCompl = fCompl;
674 *pPlace = q-p;
675 q++;
676 Vec_WrdPush( vTruths, t );
677// Vec_IntPush( vWeights, n == 5 ? n : n+1 );
678 Vec_IntPush( vWeights, n+1 );
679 if ( q-p == nFuncs )
680 {
681 printf( "Reached limit of %d functions.\n", nFuncs );
682 goto finish;
683 }
684 }
685 printf( "Added %d + %d + 1 = %d. Total = %8d. ", k, m, n+1, (int)(q-p) );
686 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
687 }
688 Vec_IntPush( vStops, q-p );
689 }
690 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
691
692
693 {
694 FILE * pFile = fopen( "func6v6n_bin.txt", "wb" );
695 fwrite( Vec_WrdArray(vTruths), sizeof(word), Vec_WrdSize(vTruths), pFile );
696 fclose( pFile );
697 }
698 {
699 FILE * pFile = fopen( "func6v6nW_bin.txt", "wb" );
700 fwrite( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
701 fclose( pFile );
702 }
703
704
705finish:
706 Vec_IntFree( vStops );
707 free( p );
708
709 *pvWeights = vWeights;
710// Vec_WrdFree( vTruths );
711 return vTruths;
712}
#define BDC_TERM
Definition bdcSpfd.c:415
int * Bdc_SpfdHashLookup(Bdc_Ent_t *p, int Size, word t)
Definition bdcSpfd.c:550
struct Bdc_Ent_t_ Bdc_Ent_t
Definition bdcSpfd.c:399
int iList
Definition bdcSpfd.c:411
unsigned fCompl1
Definition bdcSpfd.c:407
unsigned fCompl0
Definition bdcSpfd.c:403
word Truth
Definition bdcSpfd.c:412
unsigned fExor
Definition bdcSpfd.c:408
unsigned fCompl
Definition bdcSpfd.c:404
unsigned iFan0
Definition bdcSpfd.c:402
unsigned iFan1
Definition bdcSpfd.c:406
char * calloc()
char * memset()
VOID_HACK free()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdDecomposeTestOne()

int Bdc_SpfdDecomposeTestOne ( word t,
Vec_Wrd_t * vDivs,
Vec_Int_t * vWeights )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 872 of file bdcSpfd.c.

873{
874 word F1 = t;
875 word F0 = ~F1;
876 word Func;
877 int i, Cost = 0;
878 printf( "Trying: " );
879 Extra_PrintHex( stdout, (unsigned *)&t, 6 ); printf( "\n" );
880// Abc_Show6VarFunc( F0, F1 );
881 for ( i = 0; F0 && F1; i++ )
882 {
883 printf( "*** ITER %2d ", i );
884 Func = Bdc_SpfdFindBest( vDivs, vWeights, F0, F1, &Cost );
885 F0 &= ~Func;
886 F1 &= ~Func;
887// Abc_Show6VarFunc( F0, F1 );
888 }
889 Cost += (i-1);
890 printf( "Produce solution with cost %2d (with adj cost %4d).\n", Cost, Bdc_SpfdAdjCost(t) );
891 return Cost;
892}
word Bdc_SpfdFindBest(Vec_Wrd_t *vDivs, Vec_Int_t *vWeights, word F0, word F1, int *pCost)
Definition bdcSpfd.c:807
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdFindBest()

word Bdc_SpfdFindBest ( Vec_Wrd_t * vDivs,
Vec_Int_t * vWeights,
word F0,
word F1,
int * pCost )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 807 of file bdcSpfd.c.

808{
809 word Func, FuncBest;
810 int i, Cost, CostBest = -1, NumBest = -1;
811 Vec_WrdForEachEntry( vDivs, Func, i )
812 {
813 if ( (Func & F0) == 0 )
814 {
815 Cost = Bdc_SpfdComputeCost(Func & F1, i, vWeights);
816 if ( CostBest < Cost )
817 {
818 CostBest = Cost;
819 FuncBest = Func;
820 NumBest = i;
821 }
822 }
823 if ( (Func & F1) == 0 )
824 {
825 Cost = Bdc_SpfdComputeCost(Func & F0, i, vWeights);
826 if ( CostBest < Cost )
827 {
828 CostBest = Cost;
829 FuncBest = Func;
830 NumBest = i;
831 }
832 }
833 if ( (~Func & F0) == 0 )
834 {
835 Cost = Bdc_SpfdComputeCost(~Func & F1, i, vWeights);
836 if ( CostBest < Cost )
837 {
838 CostBest = Cost;
839 FuncBest = ~Func;
840 NumBest = i;
841 }
842 }
843 if ( (~Func & F1) == 0 )
844 {
845 Cost = Bdc_SpfdComputeCost(~Func & F0, i, vWeights);
846 if ( CostBest < Cost )
847 {
848 CostBest = Cost;
849 FuncBest = ~Func;
850 NumBest = i;
851 }
852 }
853 }
854 (*pCost) += Vec_IntEntry(vWeights, NumBest);
855 assert( CostBest > 0 );
856 printf( "Selected %8d with cost %2d and weight %d: ", NumBest, 0, Vec_IntEntry(vWeights, NumBest) );
857 Extra_PrintHex( stdout, (unsigned *)&FuncBest, 6 ); printf( "\n" );
858 return FuncBest;
859}
int Bdc_SpfdComputeCost(word f, int i, Vec_Int_t *vWeights)
Definition bdcSpfd.c:787
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdHashLookup()

int * Bdc_SpfdHashLookup ( Bdc_Ent_t * p,
int Size,
word t )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 550 of file bdcSpfd.c.

551{
552 Bdc_Ent_t * pBin = p + Bdc_SpfdHashValue( t, Size );
553 if ( pBin->iList == 0 )
554 return &pBin->iList;
555 for ( pBin = p + pBin->iList; ; pBin = p + pBin->iNext )
556 {
557 if ( pBin->Truth == t )
558 return NULL;
559 if ( pBin->iNext == 0 )
560 return &pBin->iNext;
561 }
562 assert( 0 );
563 return NULL;
564}
int Bdc_SpfdHashValue(word t, int Size)
Definition bdcSpfd.c:502
int iNext
Definition bdcSpfd.c:410
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdHashValue()

int Bdc_SpfdHashValue ( word t,
int Size )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 502 of file bdcSpfd.c.

503{
504 // http://planetmath.org/encyclopedia/GoodHashTablePrimes.html
505 // 53,
506 // 97,
507 // 193,
508 // 389,
509 // 769,
510 // 1543,
511 // 3079,
512 // 6151,
513 // 12289,
514 // 24593,
515 // 49157,
516 // 98317,
517 // 196613,
518 // 393241,
519 // 786433,
520 // 1572869,
521 // 3145739,
522 // 6291469,
523 // 12582917,
524 // 25165843,
525 // 50331653,
526 // 100663319,
527 // 201326611,
528 // 402653189,
529 // 805306457,
530 // 1610612741,
531 static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741};
532 unsigned char * s = (unsigned char *)&t;
533 unsigned i, Value = 0;
534 for ( i = 0; i < 8; i++ )
535 Value ^= BigPrimes[i] * s[i];
536 return Value % Size;
537}
Here is the caller graph for this function:

◆ Bdc_SpfdMark0()

int Bdc_SpfdMark0 ( Bdc_Ent_t * p,
Bdc_Ent_t * pEnt )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 429 of file bdcSpfd.c.

430{
431 if ( pEnt->iFan0 == BDC_TERM )
432 return 0;
433 if ( pEnt->fMark0 )
434 return 0;
435 pEnt->fMark0 = 1;
436 return pEnt->fMark1 +
437 Bdc_SpfdMark0(p, p + pEnt->iFan0) +
438 Bdc_SpfdMark0(p, p + pEnt->iFan1);
439}
unsigned fMark1
Definition bdcSpfd.c:409
unsigned fMark0
Definition bdcSpfd.c:405
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdMark1()

int Bdc_SpfdMark1 ( Bdc_Ent_t * p,
Bdc_Ent_t * pEnt )

Definition at line 440 of file bdcSpfd.c.

441{
442 if ( pEnt->iFan0 == BDC_TERM )
443 return 0;
444 if ( pEnt->fMark1 )
445 return 0;
446 pEnt->fMark1 = 1;
447 return pEnt->fMark0 +
448 Bdc_SpfdMark1(p, p + pEnt->iFan0) +
449 Bdc_SpfdMark1(p, p + pEnt->iFan1);
450}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdPrint()

void Bdc_SpfdPrint ( Bdc_Nod_t * pNode,
int Level,
Vec_Ptr_t * vLevels,
word Truth )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file bdcSpfd.c.

159{
160 word Diff = Truth ^ pNode->Truth;
161 Extra_PrintHex( stdout, (unsigned *)&pNode->Truth, 6 ); printf( " " );
162 Extra_PrintHex( stdout, (unsigned *)&Diff, 6 ); printf( " " );
163 Bdc_SpfdPrint_rec( pNode, Level, vLevels );
164 printf( " %d\n", pNode->Weight );
165}
void Bdc_SpfdPrint_rec(Bdc_Nod_t *pNode, int Level, Vec_Ptr_t *vLevels)
FUNCTION DEFINITIONS ///.
Definition bdcSpfd.c:114
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdPrint_rec()

void Bdc_SpfdPrint_rec ( Bdc_Nod_t * pNode,
int Level,
Vec_Ptr_t * vLevels )

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file bdcSpfd.c.

115{
116 assert( Level > 0 );
117 printf( "(" );
118
119 if ( pNode->Type & 1 )
120 printf( "!" );
121 if ( pNode->iFan0g == 0 )
122 printf( "%c", 'a' + pNode->iFan0n );
123 else
124 {
125 Bdc_Nod_t * pNode0 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan0g);
126 Bdc_SpfdPrint_rec( pNode0 + pNode->iFan0n, pNode->iFan0g, vLevels );
127 }
128
129 if ( pNode->Type & 4 )
130 printf( "+" );
131 else
132 printf( "*" );
133
134 if ( pNode->Type & 2 )
135 printf( "!" );
136 if ( pNode->iFan1g == 0 )
137 printf( "%c", 'a' + pNode->iFan1n );
138 else
139 {
140 Bdc_Nod_t * pNode1 = (Bdc_Nod_t *)Vec_PtrEntry(vLevels, pNode->iFan1g);
141 Bdc_SpfdPrint_rec( pNode1 + pNode->iFan1n, pNode->iFan1g, vLevels );
142 }
143
144 printf( ")" );
145}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdReadFiles5()

Vec_Wrd_t * Bdc_SpfdReadFiles5 ( Vec_Int_t ** pvWeights)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 726 of file bdcSpfd.c.

727{
728 Vec_Int_t * vWeights;
729 Vec_Wrd_t * vDivs;
730 FILE * pFile;
731 int RetValue;
732
733 vDivs = Vec_WrdStart( 3863759 );
734 pFile = fopen( "func6v5n_bin.txt", "rb" );
735 RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
736 fclose( pFile );
737
738 vWeights = Vec_IntStart( 3863759 );
739 pFile = fopen( "func6v5nW_bin.txt", "rb" );
740 RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
741 fclose( pFile );
742
743 *pvWeights = vWeights;
744 return vDivs;
745}
Here is the caller graph for this function:

◆ Bdc_SpfdReadFiles6()

Vec_Wrd_t * Bdc_SpfdReadFiles6 ( Vec_Int_t ** pvWeights)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 758 of file bdcSpfd.c.

759{
760 Vec_Int_t * vWeights;
761 Vec_Wrd_t * vDivs = Vec_WrdStart( 12776759 );
762 FILE * pFile = fopen( "func6v6n_bin.txt", "rb" );
763 int RetValue;
764 RetValue = fread( Vec_WrdArray(vDivs), sizeof(word), Vec_WrdSize(vDivs), pFile );
765 fclose( pFile );
766
767 vWeights = Vec_IntStart( 12776759 );
768 pFile = fopen( "func6v6nW_bin.txt", "rb" );
769 RetValue = fread( Vec_IntArray(vWeights), sizeof(int), Vec_IntSize(vWeights), pFile );
770 fclose( pFile );
771
772 *pvWeights = vWeights;
773 return vDivs;
774}

◆ Bdc_SpfdUnmark0()

void Bdc_SpfdUnmark0 ( Bdc_Ent_t * p,
Bdc_Ent_t * pEnt )

Definition at line 451 of file bdcSpfd.c.

452{
453 if ( pEnt->iFan0 == BDC_TERM )
454 return;
455 pEnt->fMark0 = 0;
456 Bdc_SpfdUnmark0( p, p + pEnt->iFan0 );
457 Bdc_SpfdUnmark0( p, p + pEnt->iFan1 );
458}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_SpfdUnmark1()

void Bdc_SpfdUnmark1 ( Bdc_Ent_t * p,
Bdc_Ent_t * pEnt )

Definition at line 459 of file bdcSpfd.c.

460{
461 if ( pEnt->iFan0 == BDC_TERM )
462 return;
463 pEnt->fMark1 = 0;
464 Bdc_SpfdUnmark1( p, p + pEnt->iFan0 );
465 Bdc_SpfdUnmark1( p, p + pEnt->iFan1 );
466}
Here is the call graph for this function:
Here is the caller graph for this function: