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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Bdc_Fun_tBdc_ManFunc (Bdc_Man_t *p, int i)
 DECLARATIONS ///.
 
Bdc_Fun_tBdc_ManRoot (Bdc_Man_t *p)
 
int Bdc_ManNodeNum (Bdc_Man_t *p)
 
int Bdc_ManAndNum (Bdc_Man_t *p)
 
Bdc_Fun_tBdc_FuncFanin0 (Bdc_Fun_t *p)
 
Bdc_Fun_tBdc_FuncFanin1 (Bdc_Fun_t *p)
 
void * Bdc_FuncCopy (Bdc_Fun_t *p)
 
int Bdc_FuncCopyInt (Bdc_Fun_t *p)
 
void Bdc_FuncSetCopy (Bdc_Fun_t *p, void *pCopy)
 
void Bdc_FuncSetCopyInt (Bdc_Fun_t *p, int iCopy)
 
Bdc_Man_tBdc_ManAlloc (Bdc_Par_t *pPars)
 MACRO DEFINITIONS ///.
 
void Bdc_ManFree (Bdc_Man_t *p)
 
void Bdc_ManPrepare (Bdc_Man_t *p, Vec_Ptr_t *vDivs)
 
void Bdc_ManDecPrintSimple (Bdc_Man_t *p)
 
void Bdc_ManDecPrint_rec (Bdc_Man_t *p, Bdc_Fun_t *pNode)
 
void Bdc_ManDecPrint (Bdc_Man_t *p)
 
int Bdc_ManDecompose (Bdc_Man_t *p, unsigned *puFunc, unsigned *puCare, int nVars, Vec_Ptr_t *vDivs, int nNodesMax)
 
void Bdc_ManDecomposeTest (unsigned uTruth, int nVars)
 
int Bdc_ManBidecNodeNum (word *pFunc, word *pCare, int nVars, int fVerbose)
 
void Bdc_ManBidecResubInt (Bdc_Man_t *p, Vec_Int_t *vRes)
 
Vec_Int_tBdc_ManBidecResub (word *pFunc, word *pCare, int nVars)
 

Function Documentation

◆ Bdc_FuncCopy()

void * Bdc_FuncCopy ( Bdc_Fun_t * p)

Definition at line 52 of file bdcCore.c.

52{ return p->pCopy; }
Cube * p
Definition exorList.c:222

◆ Bdc_FuncCopyInt()

int Bdc_FuncCopyInt ( Bdc_Fun_t * p)

Definition at line 53 of file bdcCore.c.

53{ return p->iCopy; }

◆ Bdc_FuncFanin0()

Bdc_Fun_t * Bdc_FuncFanin0 ( Bdc_Fun_t * p)

Definition at line 50 of file bdcCore.c.

50{ return p->pFan0; }
Here is the caller graph for this function:

◆ Bdc_FuncFanin1()

Bdc_Fun_t * Bdc_FuncFanin1 ( Bdc_Fun_t * p)

Definition at line 51 of file bdcCore.c.

51{ return p->pFan1; }
Here is the caller graph for this function:

◆ Bdc_FuncSetCopy()

void Bdc_FuncSetCopy ( Bdc_Fun_t * p,
void * pCopy )

Definition at line 54 of file bdcCore.c.

54{ p->pCopy = pCopy; }
Here is the caller graph for this function:

◆ Bdc_FuncSetCopyInt()

void Bdc_FuncSetCopyInt ( Bdc_Fun_t * p,
int iCopy )

Definition at line 55 of file bdcCore.c.

55{ p->iCopy = iCopy; }
Here is the caller graph for this function:

◆ Bdc_ManAlloc()

Bdc_Man_t * Bdc_ManAlloc ( Bdc_Par_t * pPars)

MACRO DEFINITIONS ///.

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

Synopsis [Allocate resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file bdcCore.c.

69{
70 Bdc_Man_t * p;
71 p = ABC_ALLOC( Bdc_Man_t, 1 );
72 memset( p, 0, sizeof(Bdc_Man_t) );
73 assert( pPars->nVarsMax > 1 && pPars->nVarsMax < 16 );
74 p->pPars = pPars;
75 p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
76 p->nDivsLimit = 200;
77 // internal nodes
78 p->nNodesAlloc = 512;
79 p->pNodes = ABC_ALLOC( Bdc_Fun_t, p->nNodesAlloc );
80 // memory
81 p->vMemory = Vec_IntStart( 8 * p->nWords * p->nNodesAlloc );
82 Vec_IntClear(p->vMemory);
83 // set up hash table
84 p->nTableSize = (1 << p->pPars->nVarsMax);
85 p->pTable = ABC_ALLOC( Bdc_Fun_t *, p->nTableSize );
86 memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
87 p->vSpots = Vec_IntAlloc( 256 );
88 // truth tables
89 p->vTruths = Vec_PtrAllocTruthTables( p->pPars->nVarsMax );
90 p->puTemp1 = ABC_ALLOC( unsigned, 4 * p->nWords );
91 p->puTemp2 = p->puTemp1 + p->nWords;
92 p->puTemp3 = p->puTemp2 + p->nWords;
93 p->puTemp4 = p->puTemp3 + p->nWords;
94 // start the internal ISFs
95 p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL );
96 p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR );
97 p->pIsfAL = &p->IsfAL; Bdc_IsfStart( p, p->pIsfAL );
98 p->pIsfAR = &p->IsfAR; Bdc_IsfStart( p, p->pIsfAR );
99 return p;
100}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition bdc.h:42
struct Bdc_Man_t_ Bdc_Man_t
Definition bdc.h:43
int nVarsMax
Definition bdc.h:48
#define assert(ex)
Definition util_old.h:213
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_ManAndNum()

int Bdc_ManAndNum ( Bdc_Man_t * p)

Definition at line 49 of file bdcCore.c.

49{ return p->nNodes-p->nVars-1;}
Here is the caller graph for this function:

◆ Bdc_ManBidecNodeNum()

int Bdc_ManBidecNodeNum ( word * pFunc,
word * pCare,
int nVars,
int fVerbose )

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

Synopsis [Performs decomposition of one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file bdcCore.c.

379{
380 int nNodes;
381 Bdc_Man_t * pManDec;
382 Bdc_Par_t Pars = {0}, * pPars = &Pars;
383 pPars->nVarsMax = nVars;
384 pManDec = Bdc_ManAlloc( pPars );
385 Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 );
386 nNodes = Bdc_ManAndNum( pManDec );
387 if ( fVerbose )
388 Bdc_ManDecPrint( pManDec );
389 Bdc_ManFree( pManDec );
390 return nNodes;
391}
void Bdc_ManDecPrint(Bdc_Man_t *p)
Definition bdcCore.c:260
void Bdc_ManFree(Bdc_Man_t *p)
Definition bdcCore.c:113
int Bdc_ManAndNum(Bdc_Man_t *p)
Definition bdcCore.c:49
int Bdc_ManDecompose(Bdc_Man_t *p, unsigned *puFunc, unsigned *puCare, int nVars, Vec_Ptr_t *vDivs, int nNodesMax)
Definition bdcCore.c:291
Bdc_Man_t * Bdc_ManAlloc(Bdc_Par_t *pPars)
MACRO DEFINITIONS ///.
Definition bdcCore.c:68
struct Bdc_Par_t_ Bdc_Par_t
Definition bdc.h:44
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_ManBidecResub()

Vec_Int_t * Bdc_ManBidecResub ( word * pFunc,
word * pCare,
int nVars )

Definition at line 426 of file bdcCore.c.

427{
428 Vec_Int_t * vRes = NULL;
429 int nNodes;
430 Bdc_Man_t * pManDec;
431 Bdc_Par_t Pars = {0}, * pPars = &Pars;
432 pPars->nVarsMax = nVars;
433 pManDec = Bdc_ManAlloc( pPars );
434 Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 );
435 if ( pManDec->pRoot != NULL )
436 {
437 //Bdc_ManDecPrint( pManDec );
438 nNodes = Bdc_ManAndNum( pManDec );
439 vRes = Vec_IntAlloc( 2*nNodes + 1 );
440 Bdc_ManBidecResubInt( pManDec, vRes );
441 assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
442 }
443 Bdc_ManFree( pManDec );
444 return vRes;
445}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
void Bdc_ManBidecResubInt(Bdc_Man_t *p, Vec_Int_t *vRes)
Definition bdcCore.c:404
Bdc_Fun_t * pRoot
Definition bdcInt.h:94
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_ManBidecResubInt()

void Bdc_ManBidecResubInt ( Bdc_Man_t * p,
Vec_Int_t * vRes )

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

Synopsis [Performs decomposition of one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file bdcCore.c.

405{
406 int i, iRoot = Bdc_FunId(p,Bdc_Regular(p->pRoot)) - 1;
407 if ( iRoot == -1 )
408 Vec_IntPush( vRes, !Bdc_IsComplement(p->pRoot) );
409 else if ( iRoot < p->nVars )
410 Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) );
411 else
412 {
413 for ( i = p->nVars+1; i < p->nNodes; i++ )
414 {
415 Bdc_Fun_t * pNode = p->pNodes + i;
416 int iLit0 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) - 1, Bdc_IsComplement(pNode->pFan0) );
417 int iLit1 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) - 1, Bdc_IsComplement(pNode->pFan1) );
418 if ( iLit0 > iLit1 )
419 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
420 Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
421 }
422 assert( 2 + iRoot == p->nNodes );
423 Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) );
424 }
425}
Here is the caller graph for this function:

◆ Bdc_ManDecompose()

int Bdc_ManDecompose ( Bdc_Man_t * p,
unsigned * puFunc,
unsigned * puCare,
int nVars,
Vec_Ptr_t * vDivs,
int nNodesMax )

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

Synopsis [Performs decomposition of one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file bdcCore.c.

292{
293 Bdc_Isf_t Isf, * pIsf = &Isf;
294 abctime clk = Abc_Clock();
295 assert( nVars <= p->pPars->nVarsMax );
296 // set current manager parameters
297 p->nVars = nVars;
298 p->nWords = Kit_TruthWordNum( nVars );
299 p->nNodesMax = nNodesMax;
300 Bdc_ManPrepare( p, vDivs );
301 if ( puCare && Kit_TruthIsConst0( puCare, nVars ) )
302 {
303 p->pRoot = Bdc_Not(p->pNodes);
304 return 0;
305 }
306 // copy the function
307 Bdc_IsfStart( p, pIsf );
308 if ( puCare )
309 {
310 Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
311 Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
312 }
313 else
314 {
315 Kit_TruthCopy( pIsf->puOn, puFunc, p->nVars );
316 Kit_TruthNot( pIsf->puOff, puFunc, p->nVars );
317 }
318 Bdc_SuppMinimize( p, pIsf );
319 // call decomposition
320 p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
321 p->timeTotal += Abc_Clock() - clk;
322 p->numCalls++;
323 p->numNodes += p->nNodesNew;
324 if ( p->pRoot == NULL )
325 return -1;
326 if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) )
327 printf( "Bdc_ManDecompose(): Internal verification failed.\n" );
328// assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) );
329 return p->nNodesNew;
330}
ABC_INT64_T abctime
Definition abc_global.h:332
void Bdc_ManPrepare(Bdc_Man_t *p, Vec_Ptr_t *vDivs)
Definition bdcCore.c:147
int Bdc_ManNodeVerify(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Fun_t *pFunc)
Definition bdcDec.c:600
Bdc_Fun_t * Bdc_ManDecompose_rec(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
MACRO DEFINITIONS ///.
Definition bdcDec.c:675
void Bdc_SuppMinimize(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
Definition bdcDec.c:87
struct Bdc_Isf_t_ Bdc_Isf_t
Definition bdcInt.h:72
unsigned * puOn
Definition bdcInt.h:77
unsigned * puOff
Definition bdcInt.h:78
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_ManDecomposeTest()

void Bdc_ManDecomposeTest ( unsigned uTruth,
int nVars )

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

Synopsis [Performs decomposition of one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 343 of file bdcCore.c.

344{
345 static int Counter = 0;
346 static int Total = 0;
347 Bdc_Par_t Pars = {0}, * pPars = &Pars;
348 Bdc_Man_t * p;
349 int RetValue;
350// unsigned uCare = ~0x888f888f;
351 unsigned uCare = ~0;
352// unsigned uFunc = 0x88888888;
353// unsigned uFunc = 0xf888f888;
354// unsigned uFunc = 0x117e117e;
355// unsigned uFunc = 0x018b018b;
356 unsigned uFunc = uTruth;
357
358 pPars->nVarsMax = 8;
359 p = Bdc_ManAlloc( pPars );
360 RetValue = Bdc_ManDecompose( p, &uFunc, &uCare, nVars, NULL, 1000 );
361 Total += RetValue;
362 printf( "%5d : Nodes = %5d. Total = %8d.\n", ++Counter, RetValue, Total );
363// Bdc_ManDecPrint( p );
364 Bdc_ManFree( p );
365}
Here is the call graph for this function:

◆ Bdc_ManDecPrint()

void Bdc_ManDecPrint ( Bdc_Man_t * p)

Definition at line 260 of file bdcCore.c.

261{
262 Bdc_Fun_t * pRoot = Bdc_Regular(p->pRoot);
263
264 printf( "F = " );
265 if ( pRoot->Type == BDC_TYPE_CONST1 ) // constant 0
266 printf( "Constant %d", !Bdc_IsComplement(p->pRoot) );
267 else if ( pRoot->Type == BDC_TYPE_PI ) // literal
268 printf( "%s%d", Bdc_IsComplement(p->pRoot) ? "!" : "", Bdc_FunId(p,pRoot)-1 );
269 else
270 {
271 if ( Bdc_IsComplement(p->pRoot) )
272 printf( "!(" );
273 Bdc_ManDecPrint_rec( p, pRoot );
274 if ( Bdc_IsComplement(p->pRoot) )
275 printf( ")" );
276 }
277 printf( "\n" );
278}
void Bdc_ManDecPrint_rec(Bdc_Man_t *p, Bdc_Fun_t *pNode)
Definition bdcCore.c:233
@ BDC_TYPE_CONST1
Definition bdcInt.h:50
@ BDC_TYPE_PI
Definition bdcInt.h:51
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_ManDecPrint_rec()

void Bdc_ManDecPrint_rec ( Bdc_Man_t * p,
Bdc_Fun_t * pNode )

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

Synopsis [Prints bi-decomposition recursively.]

Description [This procedure prints bi-decomposition as a factored form. In doing so, logic sharing, if present, will be replicated several times.]

SideEffects []

SeeAlso []

Definition at line 233 of file bdcCore.c.

234{
235 if ( pNode->Type == BDC_TYPE_PI )
236 printf( "%c", 'a' + Bdc_FunId(p,pNode) - 1 );
237 else if ( pNode->Type == BDC_TYPE_AND )
238 {
239 Bdc_Fun_t * pNode0 = Bdc_FuncFanin0( pNode );
240 Bdc_Fun_t * pNode1 = Bdc_FuncFanin1( pNode );
241
242 if ( Bdc_IsComplement(pNode0) )
243 printf( "!" );
244 if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
245 printf( "(" );
246 Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode0) );
247 if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
248 printf( ")" );
249
250 if ( Bdc_IsComplement(pNode1) )
251 printf( "!" );
252 if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
253 printf( "(" );
254 Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode1) );
255 if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
256 printf( ")" );
257 }
258 else assert( 0 );
259}
Bdc_Fun_t * Bdc_FuncFanin0(Bdc_Fun_t *p)
Definition bdcCore.c:50
Bdc_Fun_t * Bdc_FuncFanin1(Bdc_Fun_t *p)
Definition bdcCore.c:51
@ BDC_TYPE_AND
Definition bdcInt.h:52
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bdc_ManDecPrintSimple()

void Bdc_ManDecPrintSimple ( Bdc_Man_t * p)

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

Synopsis [Prints bi-decomposition in a simple format.]

Description []

SideEffects []

SeeAlso []

Definition at line 199 of file bdcCore.c.

200{
201 Bdc_Fun_t * pNode;
202 int i;
203 printf( " 0 : Const 1\n" );
204 for ( i = 1; i < p->nNodes; i++ )
205 {
206 printf( " %d : ", i );
207 pNode = p->pNodes + i;
208 if ( pNode->Type == BDC_TYPE_PI )
209 printf( "PI " );
210 else
211 {
212 printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) );
213 printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) );
214 }
215// Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
216 printf( "\n" );
217 }
218 printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
219}

◆ Bdc_ManFree()

void Bdc_ManFree ( Bdc_Man_t * p)

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

Synopsis [Deallocate resynthesis manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file bdcCore.c.

114{
115 if ( p->pPars->fVerbose )
116 {
117 printf( "Bi-decomposition stats: Calls = %d. Nodes = %d. Reuse = %d.\n",
118 p->numCalls, p->numNodes, p->numReuse );
119 printf( "ANDs = %d. ORs = %d. Weak = %d. Muxes = %d. Memory = %.2f K\n",
120 p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) );
121 ABC_PRT( "Cache", p->timeCache );
122 ABC_PRT( "Check", p->timeCheck );
123 ABC_PRT( "Muxes", p->timeMuxes );
124 ABC_PRT( "Supps", p->timeSupps );
125 ABC_PRT( "TOTAL", p->timeTotal );
126 }
127 Vec_IntFree( p->vMemory );
128 Vec_IntFree( p->vSpots );
129 Vec_PtrFree( p->vTruths );
130 ABC_FREE( p->puTemp1 );
131 ABC_FREE( p->pNodes );
132 ABC_FREE( p->pTable );
133 ABC_FREE( p );
134}
#define ABC_PRT(a, t)
Definition abc_global.h:255
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the caller graph for this function:

◆ Bdc_ManFunc()

ABC_NAMESPACE_IMPL_START Bdc_Fun_t * Bdc_ManFunc ( Bdc_Man_t * p,
int i )

DECLARATIONS ///.

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

FileName [bdcCore.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
bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Accessing contents of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file bdcCore.c.

46{ return Bdc_FunWithId(p, i); }
Here is the caller graph for this function:

◆ Bdc_ManNodeNum()

int Bdc_ManNodeNum ( Bdc_Man_t * p)

Definition at line 48 of file bdcCore.c.

48{ return p->nNodes; }
Here is the caller graph for this function:

◆ Bdc_ManPrepare()

void Bdc_ManPrepare ( Bdc_Man_t * p,
Vec_Ptr_t * vDivs )

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

Synopsis [Clears the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file bdcCore.c.

148{
149 unsigned * puTruth;
150 Bdc_Fun_t * pNode;
151 int i;
152 Bdc_TableClear( p );
153 Vec_IntClear( p->vMemory );
154 // add constant 1 and elementary vars
155 p->nNodes = 0;
156 p->nNodesNew = - 1 - p->nVars - (vDivs? Vec_PtrSize(vDivs) : 0);
157 // add constant 1
158 pNode = Bdc_FunNew( p );
159 pNode->Type = BDC_TYPE_CONST1;
160 pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
161 Kit_TruthFill( pNode->puFunc, p->nVars );
162 pNode->uSupp = 0;
163 Bdc_TableAdd( p, pNode );
164 // add variables
165 for ( i = 0; i < p->nVars; i++ )
166 {
167 pNode = Bdc_FunNew( p );
168 pNode->Type = BDC_TYPE_PI;
169 pNode->puFunc = (unsigned *)Vec_PtrEntry( p->vTruths, i );
170 pNode->uSupp = (1 << i);
171 Bdc_TableAdd( p, pNode );
172 }
173 // add the divisors
174 if ( vDivs )
175 Vec_PtrForEachEntry( unsigned *, vDivs, puTruth, i )
176 {
177 pNode = Bdc_FunNew( p );
178 pNode->Type = BDC_TYPE_PI;
179 pNode->puFunc = puTruth;
180 pNode->uSupp = Kit_TruthSupport( puTruth, p->nVars );
181 Bdc_TableAdd( p, pNode );
182 if ( i == p->nDivsLimit )
183 break;
184 }
185 assert( p->nNodesNew == 0 );
186}
void Bdc_TableAdd(Bdc_Man_t *p, Bdc_Fun_t *pFunc)
Definition bdcTable.c:101
void Bdc_TableClear(Bdc_Man_t *p)
Definition bdcTable.c:120
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
#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_ManRoot()

Bdc_Fun_t * Bdc_ManRoot ( Bdc_Man_t * p)

Definition at line 47 of file bdcCore.c.

47{ return p->pRoot; }
Here is the caller graph for this function: