abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bdcDec.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bdcDec.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Truth-table-based bi-decomposition engine.]
8 
9  Synopsis [Decomposition procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 30, 2007.]
16 
17  Revision [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bdcInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Minimizes the support of the ISF.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
46 {
47  int v;
48  abctime clk = 0; // Suppress "might be used uninitialized"
49  if ( p->pPars->fVerbose )
50  clk = Abc_Clock();
51  // compute support
52  pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
53  Kit_TruthSupport( pIsf->puOff, p->nVars );
54  // go through the support variables
55  for ( v = 0; v < p->nVars; v++ )
56  {
57  if ( (pIsf->uSupp & (1 << v)) == 0 )
58  continue;
59  Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
60  Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
61  if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
62  continue;
63 // if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
64 // continue;
65  // remove the variable
66  Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
67  Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
68 // Kit_TruthExist( pIsf->puOn, p->nVars, v );
69 // Kit_TruthExist( pIsf->puOff, p->nVars, v );
70  pIsf->uSupp &= ~(1 << v);
71  }
72  if ( p->pPars->fVerbose )
73  p->timeSupps += Abc_Clock() - clk;
74 }
75 
76 /**Function*************************************************************
77 
78  Synopsis [Minimizes the support of the ISF.]
79 
80  Description []
81 
82  SideEffects []
83 
84  SeeAlso []
85 
86 ***********************************************************************/
87 void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
88 {
89  int v;
90  abctime clk = 0; // Suppress "might be used uninitialized"
91  if ( p->pPars->fVerbose )
92  clk = Abc_Clock();
93  // go through the support variables
94  pIsf->uSupp = 0;
95  for ( v = 0; v < p->nVars; v++ )
96  {
97  if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) &&
98  !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
99  continue;
100  if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
101  {
102  Kit_TruthExist( pIsf->puOn, p->nVars, v );
103  Kit_TruthExist( pIsf->puOff, p->nVars, v );
104  continue;
105  }
106  pIsf->uSupp |= (1 << v);
107  }
108  if ( p->pPars->fVerbose )
109  p->timeSupps += Abc_Clock() - clk;
110 }
111 
112 /**Function*************************************************************
113 
114  Synopsis [Updates the ISF of the right after the left was decompoosed.]
115 
116  Description []
117 
118  SideEffects []
119 
120  SeeAlso []
121 
122 ***********************************************************************/
123 int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type )
124 {
125  unsigned * puTruth = p->puTemp1;
126  // get the truth table of the left branch
127  if ( Bdc_IsComplement(pFunc0) )
128  Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars );
129  else
130  Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars );
131  // split into parts
132  if ( Type == BDC_TYPE_OR )
133  {
134 // Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
135 // Right.R = bdd_exist( R, setRightRes );
136 
137 // if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
138 // if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
139 // pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V ); Cudd_Ref( pR->Q );
140 // pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
141 
142 // assert( pR->R != b0 );
143 // return (int)( pR->Q == b0 );
144 
145  Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
146  Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
147  Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq );
148 // assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
149  assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
150  return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
151  }
152  else if ( Type == BDC_TYPE_AND )
153  {
154 // Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
155 // Right.Q = bdd_exist( Q, setRightRes );
156 
157 // if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
158 // if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
159 // pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V ); Cudd_Ref( pR->R );
160 // pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V ); Cudd_Ref( pR->Q );
161 
162 // assert( pR->Q != b0 );
163 // return (int)( pR->R == b0 );
164 
165  Kit_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars );
166  Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq );
167  Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq );
168 // assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
169  assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
170  return Kit_TruthIsConst0(pIsfR->puOff, p->nVars);
171  }
172  return 0;
173 }
174 
175 /**Function*************************************************************
176 
177  Synopsis [Checks existence of OR-bidecomposition.]
178 
179  Description []
180 
181  SideEffects []
182 
183  SeeAlso []
184 
185 ***********************************************************************/
186 static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars )
187 {
188  assert( nLeftVars > 0 );
189  assert( nRightVars > 0 );
190  // compute the decomposition coefficient
191  if ( nLeftVars >= nRightVars )
192  return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
193  else // if ( nLeftVars < nRightVars )
194  return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis [Checks existence of weak OR-bidecomposition.]
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
209 {
210  char pVars[16];
211  int v, nVars, Beg, End;
212 
213  assert( pIsfL->uSupp == 0 );
214  assert( pIsfR->uSupp == 0 );
215 
216  // fill in the variables
217  nVars = 0;
218  for ( v = 0; v < p->nVars; v++ )
219  if ( pIsf->uSupp & (1 << v) )
220  pVars[nVars++] = v;
221 
222  // try variable pairs
223  for ( Beg = 0; Beg < nVars; Beg++ )
224  {
225  Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] );
226  for ( End = nVars - 1; End > Beg; End-- )
227  {
228  Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] );
229  if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
230  {
231  pIsfL->uUniq = (1 << pVars[Beg]);
232  pIsfR->uUniq = (1 << pVars[End]);
233  return 1;
234  }
235  }
236  }
237  return 0;
238 }
239 
240 /**Function*************************************************************
241 
242  Synopsis [Checks existence of weak OR-bidecomposition.]
243 
244  Description []
245 
246  SideEffects []
247 
248  SeeAlso []
249 
250 ***********************************************************************/
251 int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
252 {
253  int v, VarCost;
254  int VarBest = -1; // Suppress "might be used uninitialized"
255  int Cost, VarCostBest = 0;
256 
257  for ( v = 0; v < p->nVars; v++ )
258  {
259  if ( (pIsf->uSupp & (1 << v)) == 0 )
260  continue;
261 // if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
262 // Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist );
263 // if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
264 
265  Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
266  if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
267  {
268  // measure the cost of this variable
269 // VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
270 // Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ );
271 // VarCost = Kit_TruthCountOnes( Univ, p->nVars );
272 // Cudd_RecursiveDeref( dd, Univ );
273 
274  Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
275  VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
276  if ( VarCost == 0 )
277  VarCost = 1;
278  if ( VarCostBest < VarCost )
279  {
280  VarCostBest = VarCost;
281  VarBest = v;
282  }
283  }
284  }
285 
286  // derive the components for weak-bi-decomposition if the variable is found
287  if ( VarCostBest )
288  {
289 // funQLeftRes = Q & bdd_exist( R, setRightORweak );
290 // Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp );
291 // pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q );
292 // Cudd_RecursiveDeref( dd, Temp );
293 
294  Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
295  Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
296 
297 // pL->R = pF->R; Cudd_Ref( pL->R );
298 // pL->V = VarBest; Cudd_Ref( pL->V );
299  Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
300  pIsfL->uUniq = (1 << VarBest);
301  pIsfR->uUniq = 0;
302 
303 // assert( pL->Q != b0 );
304 // assert( pL->R != b0 );
305 // assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
306 // assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
307 
308  // express cost in percents of the covered boolean space
309  Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
310  if ( Cost == 0 )
311  Cost = 1;
312  return Cost;
313  }
314  return 0;
315 }
316 
317 /**Function*************************************************************
318 
319  Synopsis [Checks existence of OR-bidecomposition.]
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
328 int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
329 {
330  unsigned uSupportRem;
331  int v, nLeftVars = 1, nRightVars = 1;
332  // clean the var sets
333  Bdc_IsfStart( p, pIsfL );
334  Bdc_IsfStart( p, pIsfR );
335  // check that the support is correct
336  assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) );
337  assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) );
338  // find initial variable sets
339  if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
340  return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
341  // prequantify the variables in the offset
342  Kit_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq );
343  Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq );
344  // go through the remaining variables
345  uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq;
346  for ( v = 0; v < p->nVars; v++ )
347  {
348  if ( (uSupportRem & (1 << v)) == 0 )
349  continue;
350  // prequantify this variable
351  Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
352  Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
353  if ( nLeftVars < nRightVars )
354  {
355 // if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
356 // if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
357  if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
358  {
359 // pL->V &= VarNew;
360  pIsfL->uUniq |= (1 << v);
361  nLeftVars++;
362  Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
363  }
364 // else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
365  else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
366  {
367 // pR->V &= VarNew;
368  pIsfR->uUniq |= (1 << v);
369  nRightVars++;
370  Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
371  }
372  }
373  else
374  {
375 // if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
376  if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
377  {
378 // pR->V &= VarNew;
379  pIsfR->uUniq |= (1 << v);
380  nRightVars++;
381  Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
382  }
383 // else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
384  else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
385  {
386 // pL->V &= VarNew;
387  pIsfL->uUniq |= (1 << v);
388  nLeftVars++;
389  Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
390  }
391  }
392  }
393 
394  // derive the functions Q and R for the left branch
395 // pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
396 // pL->R = bdd_exist( pF->R, pR->V );
397 
398 // Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( Temp );
399 // pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
400 // Cudd_RecursiveDeref( dd, Temp );
401 // pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R );
402 
403  Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
404  Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uUniq );
405  Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
406 
407 // assert( pL->Q != b0 );
408 // assert( pL->R != b0 );
409 // assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
410  assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
411  assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
412 // assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
413 
414  // derive the functions Q and R for the right branch
415 // Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp );
416 // pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
417 // Cudd_RecursiveDeref( dd, Temp );
418 // pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
419 
420  Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
421  Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
422  Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
423 
424  assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
425  assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
426 // assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
427 
428  assert( pIsfL->uUniq );
429  assert( pIsfR->uUniq );
430  return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );
431 }
432 
433 /**Function*************************************************************
434 
435  Synopsis [Performs one step of bi-decomposition.]
436 
437  Description []
438 
439  SideEffects []
440 
441  SeeAlso []
442 
443 ***********************************************************************/
444 Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
445 {
446  int WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR;
447 
448  Bdc_IsfClean( p->pIsfOL );
449  Bdc_IsfClean( p->pIsfOR );
450  Bdc_IsfClean( p->pIsfAL );
451  Bdc_IsfClean( p->pIsfAR );
452 
453  // perform OR decomposition
454  WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
455 
456  // perform AND decomposition
457  Bdc_IsfNot( pIsf );
458  WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
459  Bdc_IsfNot( pIsf );
460  Bdc_IsfNot( p->pIsfAL );
461  Bdc_IsfNot( p->pIsfAR );
462 
463  // check the case when decomposition does not exist
464  if ( WeightOr == 0 && WeightAnd == 0 )
465  {
466  Bdc_IsfCopy( pIsfL, p->pIsfOL );
467  Bdc_IsfCopy( pIsfR, p->pIsfOR );
468  return BDC_TYPE_MUX;
469  }
470  // check the hash table
471  assert( WeightOr || WeightAnd );
472  WeightOrL = WeightOrR = 0;
473  if ( WeightOr )
474  {
475  if ( p->pIsfOL->uUniq )
476  {
477  Bdc_SuppMinimize( p, p->pIsfOL );
478  WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
479  }
480  if ( p->pIsfOR->uUniq )
481  {
482  Bdc_SuppMinimize( p, p->pIsfOR );
483  WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
484  }
485  }
486  WeightAndL = WeightAndR = 0;
487  if ( WeightAnd )
488  {
489  if ( p->pIsfAL->uUniq )
490  {
491  Bdc_SuppMinimize( p, p->pIsfAL );
492  WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
493  }
494  if ( p->pIsfAR->uUniq )
495  {
496  Bdc_SuppMinimize( p, p->pIsfAR );
497  WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
498  }
499  }
500 
501  // check if there is any reuse for the components
502  if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
503  {
504  p->numReuse++;
505  p->numOrs++;
506  Bdc_IsfCopy( pIsfL, p->pIsfOL );
507  Bdc_IsfCopy( pIsfR, p->pIsfOR );
508  return BDC_TYPE_OR;
509  }
510  if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
511  {
512  p->numReuse++;
513  p->numAnds++;
514  Bdc_IsfCopy( pIsfL, p->pIsfAL );
515  Bdc_IsfCopy( pIsfR, p->pIsfAR );
516  return BDC_TYPE_AND;
517  }
518 
519  // compare the two-component costs
520  if ( WeightOr > WeightAnd )
521  {
522  if ( WeightOr < BDC_SCALE )
523  p->numWeaks++;
524  p->numOrs++;
525  Bdc_IsfCopy( pIsfL, p->pIsfOL );
526  Bdc_IsfCopy( pIsfR, p->pIsfOR );
527  return BDC_TYPE_OR;
528  }
529  if ( WeightAnd < BDC_SCALE )
530  p->numWeaks++;
531  p->numAnds++;
532  Bdc_IsfCopy( pIsfL, p->pIsfAL );
533  Bdc_IsfCopy( pIsfR, p->pIsfAR );
534  return BDC_TYPE_AND;
535 }
536 
537 /**Function*************************************************************
538 
539  Synopsis [Find variable that leads to minimum sum of support sizes.]
540 
541  Description []
542 
543  SideEffects []
544 
545  SeeAlso []
546 
547 ***********************************************************************/
548 int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
549 {
550  int Var, VarMin, nSuppMin, nSuppCur;
551  unsigned uSupp0, uSupp1;
552  abctime clk = 0; // Suppress "might be used uninitialized"
553  if ( p->pPars->fVerbose )
554  clk = Abc_Clock();
555  VarMin = -1;
556  nSuppMin = 1000;
557  for ( Var = 0; Var < p->nVars; Var++ )
558  {
559  if ( (pIsf->uSupp & (1 << Var)) == 0 )
560  continue;
561  Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, Var );
562  Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var );
563  Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, Var );
564  Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var );
565  uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars );
566  uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars );
567  nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1);
568  if ( nSuppMin > nSuppCur )
569  {
570  nSuppMin = nSuppCur;
571  VarMin = Var;
572  break;
573  }
574  }
575  if ( VarMin >= 0 )
576  {
577  Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, VarMin );
578  Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin );
579  Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, VarMin );
580  Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin );
581  Bdc_SuppMinimize( p, pIsfL );
582  Bdc_SuppMinimize( p, pIsfR );
583  }
584  if ( p->pPars->fVerbose )
585  p->timeMuxes += Abc_Clock() - clk;
586  return VarMin;
587 }
588 
589 /**Function*************************************************************
590 
591  Synopsis [Creates gates.]
592 
593  Description []
594 
595  SideEffects []
596 
597  SeeAlso []
598 
599 ***********************************************************************/
600 int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc )
601 {
602  unsigned * puTruth = p->puTemp1;
603  if ( Bdc_IsComplement(pFunc) )
604  Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars );
605  else
606  Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars );
607  return Bdc_TableCheckContainment( p, pIsf, puTruth );
608 }
609 
610 /**Function*************************************************************
611 
612  Synopsis [Creates gates.]
613 
614  Description []
615 
616  SideEffects []
617 
618  SeeAlso []
619 
620 ***********************************************************************/
621 Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type )
622 {
623  Bdc_Fun_t * pFunc;
624  pFunc = Bdc_FunNew( p );
625  if ( pFunc == NULL )
626  return NULL;
627  pFunc->Type = Type;
628  pFunc->pFan0 = pFunc0;
629  pFunc->pFan1 = pFunc1;
630  pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
631  // get the truth table of the left branch
632  if ( Bdc_IsComplement(pFunc0) )
633  Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars );
634  else
635  Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars );
636  // get the truth table of the right branch
637  if ( Bdc_IsComplement(pFunc1) )
638  Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars );
639  else
640  Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars );
641  // compute the function of node
642  if ( pFunc->Type == BDC_TYPE_AND )
643  {
644  Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
645  }
646  else if ( pFunc->Type == BDC_TYPE_OR )
647  {
648  Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
649  // transform to AND gate
650  pFunc->Type = BDC_TYPE_AND;
651  pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
652  pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
653  Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
654  pFunc = Bdc_Not(pFunc);
655  }
656  else
657  assert( 0 );
658  // add to table
659  Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars );
660  Bdc_TableAdd( p, Bdc_Regular(pFunc) );
661  return pFunc;
662 }
663 
664 /**Function*************************************************************
665 
666  Synopsis [Performs one step of bi-decomposition.]
667 
668  Description []
669 
670  SideEffects []
671 
672  SeeAlso []
673 
674 ***********************************************************************/
675 Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
676 {
677 // int static Counter = 0;
678 // int LocalCounter = Counter++;
679  Bdc_Type_t Type;
680  Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
681  Bdc_Isf_t IsfL, * pIsfL = &IsfL;
682  Bdc_Isf_t IsfB, * pIsfR = &IsfB;
683  int iVar;
684  abctime clk = 0; // Suppress "might be used uninitialized"
685 /*
686 printf( "Init function (%d):\n", LocalCounter );
687 Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
688 Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
689 */
690  // check computed results
691  assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
692  if ( p->pPars->fVerbose )
693  clk = Abc_Clock();
694  pFunc = Bdc_TableLookup( p, pIsf );
695  if ( p->pPars->fVerbose )
696  p->timeCache += Abc_Clock() - clk;
697  if ( pFunc )
698  return pFunc;
699  // decide on the decomposition type
700  if ( p->pPars->fVerbose )
701  clk = Abc_Clock();
702  Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
703  if ( p->pPars->fVerbose )
704  p->timeCheck += Abc_Clock() - clk;
705  if ( Type == BDC_TYPE_MUX )
706  {
707  if ( p->pPars->fVerbose )
708  clk = Abc_Clock();
709  iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
710  if ( p->pPars->fVerbose )
711  p->timeMuxes += Abc_Clock() - clk;
712  p->numMuxes++;
713  pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
714  pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
715  if ( pFunc0 == NULL || pFunc1 == NULL )
716  return NULL;
717  pFunc = Bdc_FunWithId( p, iVar + 1 );
718  pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND );
719  pFunc1 = Bdc_ManCreateGate( p, pFunc, pFunc1, BDC_TYPE_AND );
720  if ( pFunc0 == NULL || pFunc1 == NULL )
721  return NULL;
722  pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR );
723  }
724  else
725  {
726  pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
727  if ( pFunc0 == NULL )
728  return NULL;
729  // decompose the right branch
730  if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) )
731  {
732  p->nNodesNew--;
733  return pFunc0;
734  }
735  Bdc_SuppMinimize( p, pIsfR );
736  pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
737  if ( pFunc1 == NULL )
738  return NULL;
739  // create new gate
740  pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
741  }
742  return pFunc;
743 }
744 
745 ////////////////////////////////////////////////////////////////////////
746 /// END OF FILE ///
747 ////////////////////////////////////////////////////////////////////////
748 
749 
750 ABC_NAMESPACE_IMPL_END
751 
Bdc_Isf_t_
Definition: bdcInt.h:73
BDC_SCALE
#define BDC_SCALE
INCLUDES ///.
Definition: bdcInt.h:41
Bdc_DecomposeStepMux
int Bdc_DecomposeStepMux(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition: bdcDec.c:548
Bdc_Isf_t_::uSupp
unsigned uSupp
Definition: bdcInt.h:75
Bdc_Man_t_::timeCache
abctime timeCache
Definition: bdcInt.h:121
Bdc_Man_t_::vMemory
Vec_Int_t * vMemory
Definition: bdcInt.h:111
Bdc_DecomposeOr
int Bdc_DecomposeOr(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition: bdcDec.c:328
Bdc_Par_t_::fVerbose
int fVerbose
Definition: bdc.h:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Kit_TruthExistSet
void Kit_TruthExistSet(unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
Definition: kitTruth.c:793
Bdc_Man_t_::timeCheck
abctime timeCheck
Definition: bdcInt.h:122
Bdc_Man_t_::puTemp2
unsigned * puTemp2
Definition: bdcInt.h:102
Kit_TruthIsDisjoint3
static int Kit_TruthIsDisjoint3(unsigned *pIn1, unsigned *pIn2, unsigned *pIn3, int nVars)
Definition: kit.h:347
Bdc_TableAdd
void Bdc_TableAdd(Bdc_Man_t *p, Bdc_Fun_t *pFunc)
Definition: bdcTable.c:101
Bdc_Type_t
Bdc_Type_t
BASIC TYPES ///.
Definition: bdcInt.h:48
Bdc_Man_t_::nVars
int nVars
Definition: bdcInt.h:85
Kit_TruthIsImply
static int Kit_TruthIsImply(unsigned *pIn1, unsigned *pIn2, int nVars)
Definition: kit.h:331
Bdc_Man_t_::timeMuxes
abctime timeMuxes
Definition: bdcInt.h:123
Bdc_Man_t_::puTemp4
unsigned * puTemp4
Definition: bdcInt.h:104
Bdc_Man_t_::numReuse
int numReuse
Definition: bdcInt.h:119
Bdc_DecomposeGetCost
static int Bdc_DecomposeGetCost(Bdc_Man_t *p, int nLeftVars, int nRightVars)
Definition: bdcDec.c:186
Kit_TruthVarIsVacuous
int Kit_TruthVarIsVacuous(unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
Definition: kitTruth.c:625
Bdc_Man_t_::pIsfAR
Bdc_Isf_t * pIsfAR
Definition: bdcInt.h:109
Bdc_Man_t_::nNodesNew
int nNodesNew
Definition: bdcInt.h:93
Bdc_ManCreateGate
Bdc_Fun_t * Bdc_ManCreateGate(Bdc_Man_t *p, Bdc_Fun_t *pFunc0, Bdc_Fun_t *pFunc1, Bdc_Type_t Type)
Definition: bdcDec.c:621
Bdc_Man_t_::pPars
Bdc_Par_t * pPars
Definition: bdcInt.h:84
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Bdc_TableCheckContainment
int Bdc_TableCheckContainment(Bdc_Man_t *p, Bdc_Isf_t *pIsf, unsigned *puTruth)
DECLARATIONS ///.
Definition: bdcTable.c:45
Bdc_Man_t_::puTemp3
unsigned * puTemp3
Definition: bdcInt.h:103
Kit_TruthExist
void Kit_TruthExist(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:684
Bdc_Isf_t_::puOff
unsigned * puOff
Definition: bdcInt.h:78
Bdc_ManDecompose_rec
Bdc_Fun_t * Bdc_ManDecompose_rec(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
MACRO DEFINITIONS ///.
Definition: bdcDec.c:675
Bdc_Man_t_::timeSupps
abctime timeSupps
Definition: bdcInt.h:124
Kit_TruthAnd
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
Bdc_Fun_t
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition: bdc.h:42
Bdc_Man_t_::puTemp1
unsigned * puTemp1
Definition: bdcInt.h:101
Bdc_IsfClean
static void Bdc_IsfClean(Bdc_Isf_t *p)
Definition: bdcInt.h:132
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Kit_TruthCountOnes
static int Kit_TruthCountOnes(unsigned *pIn, int nVars)
Definition: kit.h:251
Bdc_Man_t_::numWeaks
int numWeaks
Definition: bdcInt.h:118
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
Bdc_SuppMinimize
void Bdc_SuppMinimize(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
Definition: bdcDec.c:87
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Kit_TruthIsDisjoint
static int Kit_TruthIsDisjoint(unsigned *pIn1, unsigned *pIn2, int nVars)
Definition: kit.h:339
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Kit_TruthSharp
static void Kit_TruthSharp(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:397
Bdc_Man_t_::numOrs
int numOrs
Definition: bdcInt.h:117
Bdc_Man_t_::pIsfOL
Bdc_Isf_t * pIsfOL
Definition: bdcInt.h:106
Bdc_Man_t_::numAnds
int numAnds
Definition: bdcInt.h:116
Bdc_Isf_t_::puOn
unsigned * puOn
Definition: bdcInt.h:77
Bdc_IsComplement
static int Bdc_IsComplement(Bdc_Fun_t *p)
Definition: bdc.h:54
Bdc_FunNew
static Bdc_Fun_t * Bdc_FunNew(Bdc_Man_t *p)
Definition: bdcInt.h:128
Bdc_DecomposeUpdateRight
int Bdc_DecomposeUpdateRight(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR, Bdc_Fun_t *pFunc0, Bdc_Type_t Type)
Definition: bdcDec.c:123
Kit_TruthExistNew
void Kit_TruthExistNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:738
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition: kitTruth.c:346
Bdc_Isf_t_::uUniq
unsigned uUniq
Definition: bdcInt.h:76
Bdc_Man_t_
Definition: bdcInt.h:81
Kit_TruthCopy
static void Kit_TruthCopy(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:355
Minisat::Var
int Var
Definition: SolverTypes.h:42
Bdc_FunWithId
static Bdc_Fun_t * Bdc_FunWithId(Bdc_Man_t *p, int Id)
Definition: bdcInt.h:129
Bdc_DecomposeFindInitialVarSet
int Bdc_DecomposeFindInitialVarSet(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition: bdcDec.c:208
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:270
Bdc_Not
static Bdc_Fun_t * Bdc_Not(Bdc_Fun_t *p)
Definition: bdc.h:56
Bdc_Man_t_::pIsfOR
Bdc_Isf_t * pIsfOR
Definition: bdcInt.h:107
Kit_TruthForallNew
void Kit_TruthForallNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:867
Bdc_Man_t_::pIsfAL
Bdc_Isf_t * pIsfAL
Definition: bdcInt.h:108
assert
#define assert(ex)
Definition: util_old.h:213
Kit_WordCountOnes
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
Bdc_TableLookup
Bdc_Fun_t * Bdc_TableLookup(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
Definition: bdcTable.c:62
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Bdc_SuppMinimize2
ABC_NAMESPACE_IMPL_START void Bdc_SuppMinimize2(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
DECLARATIONS ///.
Definition: bdcDec.c:45
Bdc_Man_t_::numMuxes
int numMuxes
Definition: bdcInt.h:115
Bdc_IsfNot
static void Bdc_IsfNot(Bdc_Isf_t *p)
Definition: bdcInt.h:134
Bdc_IsfCopy
static void Bdc_IsfCopy(Bdc_Isf_t *p, Bdc_Isf_t *q)
Definition: bdcInt.h:133
Bdc_Regular
static Bdc_Fun_t * Bdc_Regular(Bdc_Fun_t *p)
Definition: bdc.h:55
Bdc_ManNodeVerify
int Bdc_ManNodeVerify(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Fun_t *pFunc)
Definition: bdcDec.c:600
Bdc_DecomposeWeakOr
int Bdc_DecomposeWeakOr(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition: bdcDec.c:251
Kit_TruthOr
static void Kit_TruthOr(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:385
Bdc_DecomposeStep
Bdc_Type_t Bdc_DecomposeStep(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition: bdcDec.c:444
Bdc_Man_t_::nWords
int nWords
Definition: bdcInt.h:86
Bdc_IsfStart
static void Bdc_IsfStart(Bdc_Man_t *p, Bdc_Isf_t *pF)
Definition: bdcInt.h:131