abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bdcCore.c File Reference
#include "bdcInt.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Bdc_Fun_t
Bdc_ManFunc (Bdc_Man_t *p, int i)
 DECLARATIONS ///. More...
 
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 ///. More...
 
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)
 

Function Documentation

void* Bdc_FuncCopy ( Bdc_Fun_t p)

Definition at line 52 of file bdcCore.c.

52 { return p->pCopy; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Bdc_FuncCopyInt ( Bdc_Fun_t p)

Definition at line 53 of file bdcCore.c.

53 { return p->iCopy; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Bdc_Fun_t* Bdc_FuncFanin0 ( Bdc_Fun_t p)

Definition at line 50 of file bdcCore.c.

50 { return p->pFan0; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Bdc_Fun_t* Bdc_FuncFanin1 ( Bdc_Fun_t p)

Definition at line 51 of file bdcCore.c.

51 { return p->pFan1; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Bdc_FuncSetCopy ( Bdc_Fun_t p,
void *  pCopy 
)

Definition at line 54 of file bdcCore.c.

54 { p->pCopy = pCopy; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Bdc_FuncSetCopyInt ( Bdc_Fun_t p,
int  iCopy 
)

Definition at line 55 of file bdcCore.c.

55 { p->iCopy = iCopy; }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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;
80  // memory
81  p->vMemory = Vec_IntStart( 8 * p->nWords * p->nNodesAlloc );
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
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 }
char * memset()
Bdc_Isf_t IsfOR
Definition: bdcInt.h:107
Vec_Ptr_t * vTruths
Definition: bdcInt.h:100
Vec_Int_t * vMemory
Definition: bdcInt.h:111
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int nVarsMax
Definition: bdc.h:48
unsigned * puTemp2
Definition: bdcInt.h:102
unsigned * puTemp4
Definition: bdcInt.h:104
Bdc_Isf_t * pIsfAR
Definition: bdcInt.h:109
Bdc_Isf_t IsfAR
Definition: bdcInt.h:109
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Bdc_Par_t * pPars
Definition: bdcInt.h:84
unsigned * puTemp3
Definition: bdcInt.h:103
Vec_Int_t * vSpots
Definition: bdcInt.h:98
static Vec_Ptr_t * Vec_PtrAllocTruthTables(int nVars)
Definition: vecPtr.h:1065
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
unsigned * puTemp1
Definition: bdcInt.h:101
Bdc_Isf_t * pIsfOL
Definition: bdcInt.h:106
Bdc_Fun_t ** pTable
Definition: bdcInt.h:96
Bdc_Fun_t * pNodes
Definition: bdcInt.h:90
Bdc_Isf_t * pIsfOR
Definition: bdcInt.h:107
int nNodesAlloc
Definition: bdcInt.h:91
Bdc_Isf_t * pIsfAL
Definition: bdcInt.h:108
#define assert(ex)
Definition: util_old.h:213
int nTableSize
Definition: bdcInt.h:97
Bdc_Isf_t IsfOL
Definition: bdcInt.h:106
Bdc_Isf_t IsfAL
Definition: bdcInt.h:108
int nDivsLimit
Definition: bdcInt.h:88
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int nWords
Definition: bdcInt.h:86
static void Bdc_IsfStart(Bdc_Man_t *p, Bdc_Isf_t *pF)
Definition: bdcInt.h:131
int Bdc_ManAndNum ( Bdc_Man_t p)

Definition at line 49 of file bdcCore.c.

49 { return p->nNodes-p->nVars-1;}
int nVars
Definition: bdcInt.h:85
int nNodes
Definition: bdcInt.h:92
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 }
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
int nVars
Definition: bdcInt.h:85
int nNodesNew
Definition: bdcInt.h:93
int numCalls
Definition: bdcInt.h:113
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
void Bdc_ManPrepare(Bdc_Man_t *p, Vec_Ptr_t *vDivs)
Definition: bdcCore.c:147
static abctime Abc_Clock()
Definition: abc_global.h:279
unsigned * puOff
Definition: bdcInt.h:78
Bdc_Fun_t * Bdc_ManDecompose_rec(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
MACRO DEFINITIONS ///.
Definition: bdcDec.c:675
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Bdc_Fun_t * pRoot
Definition: bdcInt.h:94
void Bdc_SuppMinimize(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
Definition: bdcDec.c:87
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
int nNodesMax
Definition: bdcInt.h:87
static void Kit_TruthSharp(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:397
unsigned * puOn
Definition: bdcInt.h:77
Bdc_Fun_t * pNodes
Definition: bdcInt.h:90
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
static Bdc_Fun_t * Bdc_Not(Bdc_Fun_t *p)
Definition: bdc.h:56
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
abctime timeTotal
Definition: bdcInt.h:125
int Bdc_ManNodeVerify(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Fun_t *pFunc)
Definition: bdcDec.c:600
int nWords
Definition: bdcInt.h:86
int numNodes
Definition: bdcInt.h:114
static void Bdc_IsfStart(Bdc_Man_t *p, Bdc_Isf_t *pF)
Definition: bdcInt.h:131
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 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Counter
Definition: bdc.h:45
void Bdc_ManFree(Bdc_Man_t *p)
Definition: bdcCore.c:113
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
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
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
Bdc_Fun_t * pRoot
Definition: bdcInt.h:94
static int Bdc_FunId(Bdc_Man_t *p, Bdc_Fun_t *pFun)
Definition: bdcInt.h:130
static int Bdc_IsComplement(Bdc_Fun_t *p)
Definition: bdc.h:54
static Bdc_Fun_t * Bdc_Regular(Bdc_Fun_t *p)
Definition: bdc.h:55
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 }
void Bdc_ManDecPrint_rec(Bdc_Man_t *p, Bdc_Fun_t *pNode)
Definition: bdcCore.c:233
Bdc_Fun_t * Bdc_FuncFanin1(Bdc_Fun_t *p)
Definition: bdcCore.c:51
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
static int Bdc_FunId(Bdc_Man_t *p, Bdc_Fun_t *pFun)
Definition: bdcInt.h:130
static int Bdc_IsComplement(Bdc_Fun_t *p)
Definition: bdc.h:54
Bdc_Fun_t * Bdc_FuncFanin0(Bdc_Fun_t *p)
Definition: bdcCore.c:50
#define assert(ex)
Definition: util_old.h:213
static Bdc_Fun_t * Bdc_Regular(Bdc_Fun_t *p)
Definition: bdc.h:55
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 }
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
Bdc_Fun_t * pRoot
Definition: bdcInt.h:94
static int Bdc_FunId(Bdc_Man_t *p, Bdc_Fun_t *pFun)
Definition: bdcInt.h:130
Bdc_Fun_t * pNodes
Definition: bdcInt.h:90
static int Bdc_IsComplement(Bdc_Fun_t *p)
Definition: bdc.h:54
int nNodes
Definition: bdcInt.h:92
static Bdc_Fun_t * Bdc_Regular(Bdc_Fun_t *p)
Definition: bdc.h:55
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 }
Vec_Ptr_t * vTruths
Definition: bdcInt.h:100
abctime timeCache
Definition: bdcInt.h:121
Vec_Int_t * vMemory
Definition: bdcInt.h:111
int fVerbose
Definition: bdc.h:49
abctime timeCheck
Definition: bdcInt.h:122
abctime timeMuxes
Definition: bdcInt.h:123
int numReuse
Definition: bdcInt.h:119
Bdc_Par_t * pPars
Definition: bdcInt.h:84
int numCalls
Definition: bdcInt.h:113
Vec_Int_t * vSpots
Definition: bdcInt.h:98
abctime timeSupps
Definition: bdcInt.h:124
unsigned * puTemp1
Definition: bdcInt.h:101
int numWeaks
Definition: bdcInt.h:118
int numOrs
Definition: bdcInt.h:117
Bdc_Fun_t ** pTable
Definition: bdcInt.h:96
int numAnds
Definition: bdcInt.h:116
Bdc_Fun_t * pNodes
Definition: bdcInt.h:90
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_PRT(a, t)
Definition: abc_global.h:220
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
abctime timeTotal
Definition: bdcInt.h:125
int numMuxes
Definition: bdcInt.h:115
int numNodes
Definition: bdcInt.h:114
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
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); }
static Bdc_Fun_t * Bdc_FunWithId(Bdc_Man_t *p, int Id)
Definition: bdcInt.h:129
int Bdc_ManNodeNum ( Bdc_Man_t p)

Definition at line 48 of file bdcCore.c.

48 { return p->nNodes; }
int nNodes
Definition: bdcInt.h:92
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 }
Vec_Ptr_t * vTruths
Definition: bdcInt.h:100
Vec_Int_t * vMemory
Definition: bdcInt.h:111
void Bdc_TableClear(Bdc_Man_t *p)
Definition: bdcTable.c:120
static void Kit_TruthFill(unsigned *pOut, int nVars)
Definition: kit.h:367
void Bdc_TableAdd(Bdc_Man_t *p, Bdc_Fun_t *pFunc)
Definition: bdcTable.c:101
int nVars
Definition: bdcInt.h:85
int nNodesNew
Definition: bdcInt.h:93
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Bdc_Fun_t * Bdc_FunNew(Bdc_Man_t *p)
Definition: bdcInt.h:128
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
int nNodes
Definition: bdcInt.h:92
#define assert(ex)
Definition: util_old.h:213
int nDivsLimit
Definition: bdcInt.h:88
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int nWords
Definition: bdcInt.h:86
Bdc_Fun_t* Bdc_ManRoot ( Bdc_Man_t p)

Definition at line 47 of file bdcCore.c.

47 { return p->pRoot; }
Bdc_Fun_t * pRoot
Definition: bdcInt.h:94