abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
utilTruth.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [utilTruth.h]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Truth table manipulation.]
8 
9  Synopsis [Truth table manipulation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - October 28, 2012.]
16 
17  Revision [$Id: utilTruth.h,v 1.00 2012/10/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__misc__util__utilTruth_h
22 #define ABC__misc__util__utilTruth_h
23 
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// PARAMETERS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 ABC_NAMESPACE_HEADER_START
33 
34 ////////////////////////////////////////////////////////////////////////
35 /// BASIC TYPES ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 static word s_Truths6[6] = {
39  ABC_CONST(0xAAAAAAAAAAAAAAAA),
40  ABC_CONST(0xCCCCCCCCCCCCCCCC),
41  ABC_CONST(0xF0F0F0F0F0F0F0F0),
42  ABC_CONST(0xFF00FF00FF00FF00),
43  ABC_CONST(0xFFFF0000FFFF0000),
44  ABC_CONST(0xFFFFFFFF00000000)
45 };
46 
47 static word s_Truths6Neg[6] = {
48  ABC_CONST(0x5555555555555555),
49  ABC_CONST(0x3333333333333333),
50  ABC_CONST(0x0F0F0F0F0F0F0F0F),
51  ABC_CONST(0x00FF00FF00FF00FF),
52  ABC_CONST(0x0000FFFF0000FFFF),
53  ABC_CONST(0x00000000FFFFFFFF)
54 };
55 
56 static word s_TruthXors[6] = {
57  ABC_CONST(0x0000000000000000),
58  ABC_CONST(0x6666666666666666),
59  ABC_CONST(0x6969696969696969),
60  ABC_CONST(0x6996699669966996),
61  ABC_CONST(0x6996966969969669),
62  ABC_CONST(0x6996966996696996)
63 };
64 
65 static word s_PMasks[5][3] = {
66  { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
67  { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
68  { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
69  { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
70  { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
71 };
72 
73 static word Ps_PMasks[5][6][3] = {
74  {
75  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 0 0
76  { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) }, // 0 1
77  { ABC_CONST(0xA5A5A5A5A5A5A5A5), ABC_CONST(0x0A0A0A0A0A0A0A0A), ABC_CONST(0x5050505050505050) }, // 0 2
78  { ABC_CONST(0xAA55AA55AA55AA55), ABC_CONST(0x00AA00AA00AA00AA), ABC_CONST(0x5500550055005500) }, // 0 3
79  { ABC_CONST(0xAAAA5555AAAA5555), ABC_CONST(0x0000AAAA0000AAAA), ABC_CONST(0x5555000055550000) }, // 0 4
80  { ABC_CONST(0xAAAAAAAA55555555), ABC_CONST(0x00000000AAAAAAAA), ABC_CONST(0x5555555500000000) } // 0 5
81  },
82  {
83  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 1 0
84  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 1 1
85  { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) }, // 1 2
86  { ABC_CONST(0xCC33CC33CC33CC33), ABC_CONST(0x00CC00CC00CC00CC), ABC_CONST(0x3300330033003300) }, // 1 3
87  { ABC_CONST(0xCCCC3333CCCC3333), ABC_CONST(0x0000CCCC0000CCCC), ABC_CONST(0x3333000033330000) }, // 1 4
88  { ABC_CONST(0xCCCCCCCC33333333), ABC_CONST(0x00000000CCCCCCCC), ABC_CONST(0x3333333300000000) } // 1 5
89  },
90  {
91  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 2 0
92  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 2 1
93  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 2 2
94  { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) }, // 2 3
95  { ABC_CONST(0xF0F00F0FF0F00F0F), ABC_CONST(0x0000F0F00000F0F0), ABC_CONST(0x0F0F00000F0F0000) }, // 2 4
96  { ABC_CONST(0xF0F0F0F00F0F0F0F), ABC_CONST(0x00000000F0F0F0F0), ABC_CONST(0x0F0F0F0F00000000) } // 2 5
97  },
98  {
99  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 0
100  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 1
101  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 2
102  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 3 3
103  { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) }, // 3 4
104  { ABC_CONST(0xFF00FF0000FF00FF), ABC_CONST(0x00000000FF00FF00), ABC_CONST(0x00FF00FF00000000) } // 3 5
105  },
106  {
107  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 0
108  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 1
109  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 2
110  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 3
111  { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) }, // 4 4
112  { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) } // 4 5
113  }
114 };
115 
116 // the bit count for the first 256 integer numbers
117 static int Abc_TtBitCount8[256] = {
118  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
119  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
120  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
121  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
122  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
123  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
124  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
125  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
126 };
127 static inline int Abc_TtBitCount16( int i ) { return Abc_TtBitCount8[i & 0xFF] + Abc_TtBitCount8[i >> 8]; }
128 
129 ////////////////////////////////////////////////////////////////////////
130 /// MACRO DEFINITIONS ///
131 ////////////////////////////////////////////////////////////////////////
132 
133 ////////////////////////////////////////////////////////////////////////
134 /// FUNCTION DECLARATIONS ///
135 ////////////////////////////////////////////////////////////////////////
136 
137 /**Function*************************************************************
138 
139  Synopsis []
140 
141  Description []
142 
143  SideEffects []
144 
145  SeeAlso []
146 
147 ***********************************************************************/
148 // read/write/flip i-th bit of a bit string table:
149 static inline int Abc_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (i & 63)) & 1; }
150 static inline void Abc_TtSetBit( word * p, int i ) { p[i>>6] |= (((word)1)<<(i & 63)); }
151 static inline void Abc_TtXorBit( word * p, int i ) { p[i>>6] ^= (((word)1)<<(i & 63)); }
152 
153 // read/write k-th digit d of a hexadecimal number:
154 static inline int Abc_TtGetHex( word * p, int k ) { return (int)(p[k>>4] >> ((k<<2) & 63)) & 15; }
155 static inline void Abc_TtSetHex( word * p, int k, int d ) { p[k>>4] |= (((word)d)<<((k<<2) & 63)); }
156 static inline void Abc_TtXorHex( word * p, int k, int d ) { p[k>>4] ^= (((word)d)<<((k<<2) & 63)); }
157 
158 /**Function*************************************************************
159 
160  Synopsis []
161 
162  Description []
163 
164  SideEffects []
165 
166  SeeAlso []
167 
168 ***********************************************************************/
169 static inline int Abc_TtWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); }
170 static inline int Abc_TtByteNum( int nVars ) { return nVars <= 3 ? 1 : 1 << (nVars-3); }
171 static inline int Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 << (nVars-2); }
172 
173 /**Function*************************************************************
174 
175  Synopsis [Bit mask.]
176 
177  Description []
178 
179  SideEffects []
180 
181  SeeAlso []
182 
183 ***********************************************************************/
184 static inline word Abc_Tt6Mask( int nBits ) { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits); }
185 
186 /**Function*************************************************************
187 
188  Synopsis []
189 
190  Description []
191 
192  SideEffects []
193 
194  SeeAlso []
195 
196 ***********************************************************************/
197 static inline void Abc_TtClear( word * pOut, int nWords )
198 {
199  int w;
200  for ( w = 0; w < nWords; w++ )
201  pOut[w] = 0;
202 }
203 static inline void Abc_TtFill( word * pOut, int nWords )
204 {
205  int w;
206  for ( w = 0; w < nWords; w++ )
207  pOut[w] = ~(word)0;
208 }
209 static inline void Abc_TtUnit( word * pOut, int nWords )
210 {
211  int w;
212  for ( w = 0; w < nWords; w++ )
213  pOut[w] = s_Truths6[0];
214 }
215 static inline void Abc_TtNot( word * pOut, int nWords )
216 {
217  int w;
218  for ( w = 0; w < nWords; w++ )
219  pOut[w] = ~pOut[w];
220 }
221 static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
222 {
223  int w;
224  if ( fCompl )
225  for ( w = 0; w < nWords; w++ )
226  pOut[w] = ~pIn[w];
227  else
228  for ( w = 0; w < nWords; w++ )
229  pOut[w] = pIn[w];
230 }
231 static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
232 {
233  int w;
234  if ( fCompl )
235  for ( w = 0; w < nWords; w++ )
236  pOut[w] = ~(pIn1[w] & pIn2[w]);
237  else
238  for ( w = 0; w < nWords; w++ )
239  pOut[w] = pIn1[w] & pIn2[w];
240 }
241 static inline void Abc_TtSharp( word * pOut, word * pIn1, word * pIn2, int nWords )
242 {
243  int w;
244  for ( w = 0; w < nWords; w++ )
245  pOut[w] = pIn1[w] & ~pIn2[w];
246 }
247 static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
248 {
249  int w;
250  for ( w = 0; w < nWords; w++ )
251  pOut[w] = pIn1[w] | pIn2[w];
252 }
253 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
254 {
255  int w;
256  if ( fCompl )
257  for ( w = 0; w < nWords; w++ )
258  pOut[w] = pIn1[w] ^ ~pIn2[w];
259  else
260  for ( w = 0; w < nWords; w++ )
261  pOut[w] = pIn1[w] ^ pIn2[w];
262 }
263 static inline void Abc_TtMux( word * pOut, word * pCtrl, word * pIn1, word * pIn0, int nWords )
264 {
265  int w;
266  for ( w = 0; w < nWords; w++ )
267  pOut[w] = (pCtrl[w] & pIn1[w]) | (~pCtrl[w] & pIn0[w]);
268 }
269 static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
270 {
271  int w;
272  for ( w = 0; w < nWords; w++ )
273  if ( pIn1[w] != pIn2[w] )
274  return 0;
275  return 1;
276 }
277 static inline int Abc_TtCompare( word * pIn1, word * pIn2, int nWords )
278 {
279  int w;
280  for ( w = 0; w < nWords; w++ )
281  if ( pIn1[w] != pIn2[w] )
282  return (pIn1[w] < pIn2[w]) ? -1 : 1;
283  return 0;
284 }
285 static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords )
286 {
287  int w;
288  for ( w = nWords - 1; w >= 0; w-- )
289  if ( pIn1[w] != pIn2[w] )
290  return (pIn1[w] < pIn2[w]) ? -1 : 1;
291  return 0;
292 }
293 static inline int Abc_TtIsConst0( word * pIn1, int nWords )
294 {
295  int w;
296  for ( w = 0; w < nWords; w++ )
297  if ( pIn1[w] )
298  return 0;
299  return 1;
300 }
301 static inline int Abc_TtIsConst1( word * pIn1, int nWords )
302 {
303  int w;
304  for ( w = 0; w < nWords; w++ )
305  if ( ~pIn1[w] )
306  return 0;
307  return 1;
308 }
309 static inline void Abc_TtConst0( word * pIn1, int nWords )
310 {
311  int w;
312  for ( w = 0; w < nWords; w++ )
313  pIn1[w] = 0;
314 }
315 static inline void Abc_TtConst1( word * pIn1, int nWords )
316 {
317  int w;
318  for ( w = 0; w < nWords; w++ )
319  pIn1[w] = ~(word)0;
320 }
321 
322 /**Function*************************************************************
323 
324  Synopsis [Compute elementary truth tables.]
325 
326  Description []
327 
328  SideEffects []
329 
330  SeeAlso []
331 
332 ***********************************************************************/
333 static inline void Abc_TtElemInit( word ** pTtElems, int nVars )
334 {
335  int i, k, nWords = Abc_TtWordNum( nVars );
336  for ( i = 0; i < nVars; i++ )
337  if ( i < 6 )
338  for ( k = 0; k < nWords; k++ )
339  pTtElems[i][k] = s_Truths6[i];
340  else
341  for ( k = 0; k < nWords; k++ )
342  pTtElems[i][k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
343 }
344 static inline void Abc_TtElemInit2( word * pTtElems, int nVars )
345 {
346  int i, k, nWords = Abc_TtWordNum( nVars );
347  for ( i = 0; i < nVars; i++ )
348  {
349  word * pTruth = pTtElems + i * nWords;
350  if ( i < 6 )
351  for ( k = 0; k < nWords; k++ )
352  pTruth[k] = s_Truths6[i];
353  else
354  for ( k = 0; k < nWords; k++ )
355  pTruth[k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
356  }
357 }
358 
359 /**Function*************************************************************
360 
361  Synopsis []
362 
363  Description []
364 
365  SideEffects []
366 
367  SeeAlso []
368 
369 ***********************************************************************/
370 static inline word Abc_Tt6Cofactor0( word t, int iVar )
371 {
372  assert( iVar >= 0 && iVar < 6 );
373  return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
374 }
375 static inline word Abc_Tt6Cofactor1( word t, int iVar )
376 {
377  assert( iVar >= 0 && iVar < 6 );
378  return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
379 }
380 
381 static inline void Abc_TtCofactor0p( word * pOut, word * pIn, int nWords, int iVar )
382 {
383  if ( nWords == 1 )
384  pOut[0] = ((pIn[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pIn[0] & s_Truths6Neg[iVar]);
385  else if ( iVar <= 5 )
386  {
387  int w, shift = (1 << iVar);
388  for ( w = 0; w < nWords; w++ )
389  pOut[w] = ((pIn[w] & s_Truths6Neg[iVar]) << shift) | (pIn[w] & s_Truths6Neg[iVar]);
390  }
391  else // if ( iVar > 5 )
392  {
393  word * pLimit = pIn + nWords;
394  int i, iStep = Abc_TtWordNum(iVar);
395  for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
396  for ( i = 0; i < iStep; i++ )
397  {
398  pOut[i] = pIn[i];
399  pOut[i + iStep] = pIn[i];
400  }
401  }
402 }
403 static inline void Abc_TtCofactor1p( word * pOut, word * pIn, int nWords, int iVar )
404 {
405  if ( nWords == 1 )
406  pOut[0] = (pIn[0] & s_Truths6[iVar]) | ((pIn[0] & s_Truths6[iVar]) >> (1 << iVar));
407  else if ( iVar <= 5 )
408  {
409  int w, shift = (1 << iVar);
410  for ( w = 0; w < nWords; w++ )
411  pOut[w] = (pIn[w] & s_Truths6[iVar]) | ((pIn[w] & s_Truths6[iVar]) >> shift);
412  }
413  else // if ( iVar > 5 )
414  {
415  word * pLimit = pIn + nWords;
416  int i, iStep = Abc_TtWordNum(iVar);
417  for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
418  for ( i = 0; i < iStep; i++ )
419  {
420  pOut[i] = pIn[i + iStep];
421  pOut[i + iStep] = pIn[i + iStep];
422  }
423  }
424 }
425 static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
426 {
427  if ( nWords == 1 )
428  pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]);
429  else if ( iVar <= 5 )
430  {
431  int w, shift = (1 << iVar);
432  for ( w = 0; w < nWords; w++ )
433  pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
434  }
435  else // if ( iVar > 5 )
436  {
437  word * pLimit = pTruth + nWords;
438  int i, iStep = Abc_TtWordNum(iVar);
439  for ( ; pTruth < pLimit; pTruth += 2*iStep )
440  for ( i = 0; i < iStep; i++ )
441  pTruth[i + iStep] = pTruth[i];
442  }
443 }
444 static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
445 {
446  if ( nWords == 1 )
447  pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
448  else if ( iVar <= 5 )
449  {
450  int w, shift = (1 << iVar);
451  for ( w = 0; w < nWords; w++ )
452  pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
453  }
454  else // if ( iVar > 5 )
455  {
456  word * pLimit = pTruth + nWords;
457  int i, iStep = Abc_TtWordNum(iVar);
458  for ( ; pTruth < pLimit; pTruth += 2*iStep )
459  for ( i = 0; i < iStep; i++ )
460  pTruth[i] = pTruth[i + iStep];
461  }
462 }
463 
464 /**Function*************************************************************
465 
466  Synopsis [Checks pairs of cofactors w.r.t. two variables.]
467 
468  Description []
469 
470  SideEffects []
471 
472  SeeAlso []
473 
474 ***********************************************************************/
475 static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int jVar, int Num1, int Num2 )
476 {
477  assert( Num1 < Num2 && Num2 < 4 );
478  assert( iVar < jVar );
479  if ( nWords == 1 )
480  {
481  word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
482  int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
483  int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
484  return ((pTruth[0] >> shift1) & Mask) == ((pTruth[0] >> shift2) & Mask);
485  }
486  if ( jVar <= 5 )
487  {
488  word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
489  int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
490  int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
491  int w;
492  for ( w = 0; w < nWords; w++ )
493  if ( ((pTruth[w] >> shift1) & Mask) != ((pTruth[w] >> shift2) & Mask) )
494  return 0;
495  return 1;
496  }
497  if ( iVar <= 5 && jVar > 5 )
498  {
499  word * pLimit = pTruth + nWords;
500  int j, jStep = Abc_TtWordNum(jVar);
501  int shift1 = (Num1 & 1) * (1 << iVar);
502  int shift2 = (Num2 & 1) * (1 << iVar);
503  int Offset1 = (Num1 >> 1) * jStep;
504  int Offset2 = (Num2 >> 1) * jStep;
505  for ( ; pTruth < pLimit; pTruth += 2*jStep )
506  for ( j = 0; j < jStep; j++ )
507  if ( ((pTruth[j + Offset1] >> shift1) & s_Truths6Neg[iVar]) != ((pTruth[j + Offset2] >> shift2) & s_Truths6Neg[iVar]) )
508  return 0;
509  return 1;
510  }
511  {
512  word * pLimit = pTruth + nWords;
513  int j, jStep = Abc_TtWordNum(jVar);
514  int i, iStep = Abc_TtWordNum(iVar);
515  int Offset1 = (Num1 >> 1) * jStep + (Num1 & 1) * iStep;
516  int Offset2 = (Num2 >> 1) * jStep + (Num2 & 1) * iStep;
517  for ( ; pTruth < pLimit; pTruth += 2*jStep )
518  for ( i = 0; i < jStep; i += 2*iStep )
519  for ( j = 0; j < iStep; j++ )
520  if ( pTruth[Offset1 + i + j] != pTruth[Offset2 + i + j] )
521  return 0;
522  return 1;
523  }
524 }
525 
526 
527 /**Function*************************************************************
528 
529  Synopsis []
530 
531  Description []
532 
533  SideEffects []
534 
535  SeeAlso []
536 
537 ***********************************************************************/
538 static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == 0; }
539 static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar]; }
540 static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0; }
541 static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar]; }
542 static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return (~t & s_Truths6Neg[iVar]) == ((t >> (1 << iVar)) & s_Truths6Neg[iVar]); }
543 static inline int Abc_Tt6Cof0EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == ((t2 >> (1 << iVar)) & s_Truths6Neg[iVar]); }
544 static inline int Abc_Tt6Cof0EqualCof0( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == (t2 & s_Truths6Neg[iVar]); }
545 static inline int Abc_Tt6Cof1EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6[iVar]) == (t2 & s_Truths6[iVar]); }
546 
547 /**Function*************************************************************
548 
549  Synopsis []
550 
551  Description []
552 
553  SideEffects []
554 
555  SeeAlso []
556 
557 ***********************************************************************/
558 static inline int Abc_TtTruthIsConst0( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != 0 ) return 0; return 1; }
559 static inline int Abc_TtTruthIsConst1( word * p, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if ( p[w] != ~(word)0 ) return 0; return 1; }
560 
561 static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar )
562 {
563  if ( iVar < 6 )
564  {
565  int i;
566  for ( i = 0; i < nWords; i++ )
567  if ( t[i] & s_Truths6Neg[iVar] )
568  return 0;
569  return 1;
570  }
571  else
572  {
573  int i, Step = (1 << (iVar - 6));
574  word * tLimit = t + nWords;
575  for ( ; t < tLimit; t += 2*Step )
576  for ( i = 0; i < Step; i++ )
577  if ( t[i] )
578  return 0;
579  return 1;
580  }
581 }
582 static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar )
583 {
584  if ( iVar < 6 )
585  {
586  int i;
587  for ( i = 0; i < nWords; i++ )
588  if ( (t[i] & s_Truths6Neg[iVar]) != s_Truths6Neg[iVar] )
589  return 0;
590  return 1;
591  }
592  else
593  {
594  int i, Step = (1 << (iVar - 6));
595  word * tLimit = t + nWords;
596  for ( ; t < tLimit; t += 2*Step )
597  for ( i = 0; i < Step; i++ )
598  if ( ~t[i] )
599  return 0;
600  return 1;
601  }
602 }
603 static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar )
604 {
605  if ( iVar < 6 )
606  {
607  int i;
608  for ( i = 0; i < nWords; i++ )
609  if ( t[i] & s_Truths6[iVar] )
610  return 0;
611  return 1;
612  }
613  else
614  {
615  int i, Step = (1 << (iVar - 6));
616  word * tLimit = t + nWords;
617  for ( ; t < tLimit; t += 2*Step )
618  for ( i = 0; i < Step; i++ )
619  if ( t[i+Step] )
620  return 0;
621  return 1;
622  }
623 }
624 static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar )
625 {
626  if ( iVar < 6 )
627  {
628  int i;
629  for ( i = 0; i < nWords; i++ )
630  if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
631  return 0;
632  return 1;
633  }
634  else
635  {
636  int i, Step = (1 << (iVar - 6));
637  word * tLimit = t + nWords;
638  for ( ; t < tLimit; t += 2*Step )
639  for ( i = 0; i < Step; i++ )
640  if ( ~t[i+Step] )
641  return 0;
642  return 1;
643  }
644 }
645 static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
646 {
647  if ( iVar < 6 )
648  {
649  int i, Shift = (1 << iVar);
650  for ( i = 0; i < nWords; i++ )
651  if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
652  return 0;
653  return 1;
654  }
655  else
656  {
657  int i, Step = (1 << (iVar - 6));
658  word * tLimit = t + nWords;
659  for ( ; t < tLimit; t += 2*Step )
660  for ( i = 0; i < Step; i++ )
661  if ( t[i] != ~t[i+Step] )
662  return 0;
663  return 1;
664  }
665 }
666 
667 /**Function*************************************************************
668 
669  Synopsis [Stretch truthtable to have more input variables.]
670 
671  Description []
672 
673  SideEffects []
674 
675  SeeAlso []
676 
677 ***********************************************************************/
678 static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
679 {
680  int w, i, step, nWords;
681  if ( nVarS == nVarB )
682  return;
683  assert( nVarS < nVarB );
684  step = Abc_TruthWordNum(nVarS);
685  nWords = Abc_TruthWordNum(nVarB);
686  if ( step == nWords )
687  return;
688  assert( step < nWords );
689  for ( w = 0; w < nWords; w += step )
690  for ( i = 0; i < step; i++ )
691  pInOut[w + i] = pInOut[i];
692 }
693 static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
694 {
695  int w, i, step, nWords;
696  if ( nVarS == nVarB )
697  return;
698  assert( nVarS < nVarB );
699  step = Abc_Truth6WordNum(nVarS);
700  nWords = Abc_Truth6WordNum(nVarB);
701  if ( step == nWords )
702  return;
703  assert( step < nWords );
704  for ( w = 0; w < nWords; w += step )
705  for ( i = 0; i < step; i++ )
706  pInOut[w + i] = pInOut[i];
707 }
708 static inline word Abc_Tt6Stretch( word t, int nVars )
709 {
710  assert( nVars >= 0 );
711  if ( nVars == 0 )
712  nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
713  if ( nVars == 1 )
714  nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
715  if ( nVars == 2 )
716  nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
717  if ( nVars == 3 )
718  nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
719  if ( nVars == 4 )
720  nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
721  if ( nVars == 5 )
722  nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
723  assert( nVars == 6 );
724  return t;
725 }
726 
727 /**Function*************************************************************
728 
729  Synopsis []
730 
731  Description []
732 
733  SideEffects []
734 
735  SeeAlso []
736 
737 ***********************************************************************/
738 static inline int Abc_TtIsHexDigit( char HexChar )
739 {
740  return (HexChar >= '0' && HexChar <= '9') || (HexChar >= 'A' && HexChar <= 'F') || (HexChar >= 'a' && HexChar <= 'f');
741 }
742 static inline char Abc_TtPrintDigit( int Digit )
743 {
744  assert( Digit >= 0 && Digit < 16 );
745  if ( Digit < 10 )
746  return '0' + Digit;
747  return 'A' + Digit-10;
748 }
749 static inline char Abc_TtPrintDigitLower( int Digit )
750 {
751  assert( Digit >= 0 && Digit < 16 );
752  if ( Digit < 10 )
753  return '0' + Digit;
754  return 'a' + Digit-10;
755 }
756 static inline int Abc_TtReadHexDigit( char HexChar )
757 {
758  if ( HexChar >= '0' && HexChar <= '9' )
759  return HexChar - '0';
760  if ( HexChar >= 'A' && HexChar <= 'F' )
761  return HexChar - 'A' + 10;
762  if ( HexChar >= 'a' && HexChar <= 'f' )
763  return HexChar - 'a' + 10;
764  assert( 0 ); // not a hexadecimal symbol
765  return -1; // return value which makes no sense
766 }
767 
768 /**Function*************************************************************
769 
770  Synopsis []
771 
772  Description []
773 
774  SideEffects []
775 
776  SeeAlso []
777 
778 ***********************************************************************/
779 static inline void Abc_TtPrintHex( word * pTruth, int nVars )
780 {
781  word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
782  int k;
783  assert( nVars >= 2 );
784  for ( pThis = pTruth; pThis < pLimit; pThis++ )
785  for ( k = 0; k < 16; k++ )
786  printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
787  printf( "\n" );
788 }
789 static inline void Abc_TtPrintHexRev( FILE * pFile, word * pTruth, int nVars )
790 {
791  word * pThis;
792  int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
793  assert( nVars >= 2 );
794  for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
795  for ( k = StartK - 1; k >= 0; k-- )
796  fprintf( pFile, "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
797 // printf( "\n" );
798 }
799 static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
800 {
801  word * pThis;
802  int k;
803  assert( nVars >= 2 );
804  for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
805  for ( k = 0; k < 16; k++ )
806  printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
807  printf( "\n" );
808 }
809 static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
810 {
811  word * pThis;
812  char * pStrInit = pStr;
813  int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
814  assert( nVars >= 2 );
815  for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
816  for ( k = StartK - 1; k >= 0; k-- )
817  *pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
818  return pStr - pStrInit;
819 }
820 static inline void Abc_TtPrintHexArrayRev( FILE * pFile, word * pTruth, int nDigits )
821 {
822  int k;
823  for ( k = nDigits - 1; k >= 0; k-- )
824  fprintf( pFile, "%c", Abc_TtPrintDigitLower( Abc_TtGetHex(pTruth, k) ) );
825 }
826 
827 /**Function*************************************************************
828 
829  Synopsis [Reads hex truth table from a string.]
830 
831  Description []
832 
833  SideEffects []
834 
835  SeeAlso []
836 
837 ***********************************************************************/
838 static inline int Abc_TtReadHex( word * pTruth, char * pString )
839 {
840  int k, nVars, Digit, nDigits;
841  // skip the first 2 symbols if they are "0x"
842  if ( pString[0] == '0' && pString[1] == 'x' )
843  pString += 2;
844  // count the number of hex digits
845  nDigits = 0;
846  for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
847  nDigits++;
848  if ( nDigits == 1 )
849  {
850  if ( pString[0] == '0' || pString[0] == 'F' )
851  {
852  pTruth[0] = (pString[0] == '0') ? 0 : ~(word)0;
853  return 0;
854  }
855  if ( pString[0] == '5' || pString[0] == 'A' )
856  {
857  pTruth[0] = (pString[0] == '5') ? s_Truths6Neg[0] : s_Truths6[0];
858  return 1;
859  }
860  }
861  // determine the number of variables
862  nVars = 2 + Abc_Base2Log( nDigits );
863  // clean storage
864  for ( k = Abc_TtWordNum(nVars) - 1; k >= 0; k-- )
865  pTruth[k] = 0;
866  // read hexadecimal digits in the reverse order
867  // (the last symbol in the string is the least significant digit)
868  for ( k = 0; k < nDigits; k++ )
869  {
870  Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
871  assert( Digit >= 0 && Digit < 16 );
872  Abc_TtSetHex( pTruth, k, Digit );
873  }
874  if ( nVars < 6 )
875  pTruth[0] = Abc_Tt6Stretch( pTruth[0], nVars );
876  return nVars;
877 }
878 static inline int Abc_TtReadHexNumber( word * pTruth, char * pString )
879 {
880  // count the number of hex digits
881  int k, Digit, nDigits = 0;
882  for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
883  nDigits++;
884  // read hexadecimal digits in the reverse order
885  // (the last symbol in the string is the least significant digit)
886  for ( k = 0; k < nDigits; k++ )
887  {
888  Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
889  assert( Digit >= 0 && Digit < 16 );
890  Abc_TtSetHex( pTruth, k, Digit );
891  }
892  return nDigits;
893 }
894 
895 
896 /**Function*************************************************************
897 
898  Synopsis []
899 
900  Description []
901 
902  SideEffects []
903 
904  SeeAlso []
905 
906 ***********************************************************************/
907 static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
908 {
909  word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
910  int k, Limit = Abc_MinInt( 64, (1 << nVars) );
911  assert( nVars >= 2 );
912  for ( pThis = pTruth; pThis < pLimit; pThis++ )
913  for ( k = 0; k < Limit; k++ )
914  printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
915  printf( "\n" );
916 }
917 
918 /**Function*************************************************************
919 
920  Synopsis []
921 
922  Description []
923 
924  SideEffects []
925 
926  SeeAlso []
927 
928 ***********************************************************************/
929 static inline int Abc_TtSuppFindFirst( int Supp )
930 {
931  int i;
932  assert( Supp > 0 );
933  for ( i = 0; i < 32; i++ )
934  if ( Supp & (1 << i) )
935  return i;
936  return -1;
937 }
938 static inline int Abc_TtSuppOnlyOne( int Supp )
939 {
940  if ( Supp == 0 )
941  return 0;
942  return (Supp & (Supp-1)) == 0;
943 }
944 static inline int Abc_TtSuppIsMinBase( int Supp )
945 {
946  assert( Supp > 0 );
947  return (Supp & (Supp+1)) == 0;
948 }
949 static inline int Abc_Tt6HasVar( word t, int iVar )
950 {
951  return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]);
952 }
953 static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
954 {
955  assert( iVar < nVars );
956  if ( nVars <= 6 )
957  return Abc_Tt6HasVar( t[0], iVar );
958  if ( iVar < 6 )
959  {
960  int i, Shift = (1 << iVar);
961  int nWords = Abc_TtWordNum( nVars );
962  for ( i = 0; i < nWords; i++ )
963  if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
964  return 1;
965  return 0;
966  }
967  else
968  {
969  int i, Step = (1 << (iVar - 6));
970  word * tLimit = t + Abc_TtWordNum( nVars );
971  for ( ; t < tLimit; t += 2*Step )
972  for ( i = 0; i < Step; i++ )
973  if ( t[i] != t[Step+i] )
974  return 1;
975  return 0;
976  }
977 }
978 static inline int Abc_TtSupport( word * t, int nVars )
979 {
980  int v, Supp = 0;
981  for ( v = 0; v < nVars; v++ )
982  if ( Abc_TtHasVar( t, nVars, v ) )
983  Supp |= (1 << v);
984  return Supp;
985 }
986 static inline int Abc_TtSupportSize( word * t, int nVars )
987 {
988  int v, SuppSize = 0;
989  for ( v = 0; v < nVars; v++ )
990  if ( Abc_TtHasVar( t, nVars, v ) )
991  SuppSize++;
992  return SuppSize;
993 }
994 static inline int Abc_TtSupportAndSize( word * t, int nVars, int * pSuppSize )
995 {
996  int v, Supp = 0;
997  *pSuppSize = 0;
998  for ( v = 0; v < nVars; v++ )
999  if ( Abc_TtHasVar( t, nVars, v ) )
1000  Supp |= (1 << v), (*pSuppSize)++;
1001  return Supp;
1002 }
1003 static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
1004 {
1005  int v, Supp = 0;
1006  *pSuppSize = 0;
1007  assert( nVars <= 6 );
1008  for ( v = 0; v < nVars; v++ )
1009  if ( Abc_Tt6HasVar( t, v ) )
1010  Supp |= (1 << v), (*pSuppSize)++;
1011  return Supp;
1012 }
1013 
1014 /**Function*************************************************************
1015 
1016  Synopsis [Checks if there is a var whose both cofs have supp <= nSuppLim.]
1017 
1018  Description []
1019 
1020  SideEffects []
1021 
1022  SeeAlso []
1023 
1024 ***********************************************************************/
1025 static inline int Abc_TtCheckCondDep2( word * pTruth, int nVars, int nSuppLim )
1026 {
1027  int v, d, nWords = Abc_TtWordNum(nVars);
1028  if ( nVars <= nSuppLim + 1 )
1029  return 0;
1030  for ( v = 0; v < nVars; v++ )
1031  {
1032  int nDep0 = 0, nDep1 = 0;
1033  for ( d = 0; d < nVars; d++ )
1034  {
1035  if ( v == d )
1036  continue;
1037  if ( v < d )
1038  {
1039  nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 0, 2 );
1040  nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 1, 3 );
1041  }
1042  else // if ( v > d )
1043  {
1044  nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 0, 1 );
1045  nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 2, 3 );
1046  }
1047  if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
1048  break;
1049  }
1050  if ( d == nVars )
1051  return v;
1052  }
1053  return nVars;
1054 }
1055 static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim )
1056 {
1057  int nVarsMax = 13;
1058  word Cof0[128], Cof1[128]; // pow( 2, nVarsMax-6 )
1059  int v, d, nWords = Abc_TtWordNum(nVars);
1060  assert( nVars <= nVarsMax );
1061  if ( nVars <= nSuppLim + 1 )
1062  return 0;
1063  for ( v = 0; v < nVars; v++ )
1064  {
1065  int nDep0 = 0, nDep1 = 0;
1066  Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
1067  Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
1068  for ( d = 0; d < nVars; d++ )
1069  {
1070  if ( v == d )
1071  continue;
1072  nDep0 += Abc_TtHasVar( Cof0, nVars, d );
1073  nDep1 += Abc_TtHasVar( Cof1, nVars, d );
1074  if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
1075  break;
1076  }
1077  if ( d == nVars )
1078  return v;
1079  }
1080  return nVars;
1081 }
1082 
1083 
1084 /**Function*************************************************************
1085 
1086  Synopsis [Detecting elementary functions.]
1087 
1088  Description []
1089 
1090  SideEffects []
1091 
1092  SeeAlso []
1093 
1094 ***********************************************************************/
1095 static inline int Abc_TtOnlyOneOne( word t )
1096 {
1097  if ( t == 0 )
1098  return 0;
1099  return (t & (t-1)) == 0;
1100 }
1101 static inline int Gia_ManTtIsAndType( word t, int nVars )
1102 {
1103  return Abc_TtOnlyOneOne( t & Abc_Tt6Mask(1 << nVars) );
1104 }
1105 static inline int Gia_ManTtIsOrType( word t, int nVars )
1106 {
1107  return Abc_TtOnlyOneOne( ~t & Abc_Tt6Mask(1 << nVars) );
1108 }
1109 static inline int Gia_ManTtIsXorType( word t, int nVars )
1110 {
1111  return ((((t & 1) ? ~t : t) ^ s_TruthXors[nVars]) & Abc_Tt6Mask(1 << nVars)) == 0;
1112 }
1113 
1114 
1115 /**Function*************************************************************
1116 
1117  Synopsis []
1118 
1119  Description []
1120 
1121  SideEffects []
1122 
1123  SeeAlso []
1124 
1125 ***********************************************************************/
1126 static inline word Abc_Tt6Flip( word Truth, int iVar )
1127 {
1128  return Truth = ((Truth << (1 << iVar)) & s_Truths6[iVar]) | ((Truth & s_Truths6[iVar]) >> (1 << iVar));
1129 }
1130 static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
1131 {
1132  if ( nWords == 1 )
1133  pTruth[0] = ((pTruth[0] << (1 << iVar)) & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
1134  else if ( iVar <= 5 )
1135  {
1136  int w, shift = (1 << iVar);
1137  for ( w = 0; w < nWords; w++ )
1138  pTruth[w] = ((pTruth[w] << shift) & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
1139  }
1140  else // if ( iVar > 5 )
1141  {
1142  word * pLimit = pTruth + nWords;
1143  int i, iStep = Abc_TtWordNum(iVar);
1144  for ( ; pTruth < pLimit; pTruth += 2*iStep )
1145  for ( i = 0; i < iStep; i++ )
1146  ABC_SWAP( word, pTruth[i], pTruth[i + iStep] );
1147  }
1148 }
1149 
1150 /**Function*************************************************************
1151 
1152  Synopsis []
1153 
1154  Description []
1155 
1156  SideEffects []
1157 
1158  SeeAlso []
1159 
1160 ***********************************************************************/
1161 static inline word Abc_Tt6Permute_rec( word t, int * pPerm, int nVars )
1162 {
1163  word uRes0, uRes1; int Var;
1164  if ( t == 0 ) return 0;
1165  if ( ~t == 0 ) return ~(word)0;
1166  for ( Var = nVars-1; Var >= 0; Var-- )
1167  if ( Abc_Tt6HasVar( t, Var ) )
1168  break;
1169  assert( Var >= 0 );
1170  uRes0 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor0(t, Var), pPerm, Var );
1171  uRes1 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor1(t, Var), pPerm, Var );
1172  return (uRes0 & s_Truths6Neg[pPerm[Var]]) | (uRes1 & s_Truths6[pPerm[Var]]);
1173 }
1174 
1175 /**Function*************************************************************
1176 
1177  Synopsis []
1178 
1179  Description []
1180 
1181  SideEffects []
1182 
1183  SeeAlso []
1184 
1185 ***********************************************************************/
1186 static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar )
1187 {
1188  return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar));
1189 }
1190 static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
1191 {
1192  static word s_PMasks[5][3] = {
1193  { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
1194  { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
1195  { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
1196  { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
1197  { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
1198  };
1199  if ( iVar < 5 )
1200  {
1201  int i, Shift = (1 << iVar);
1202  for ( i = 0; i < nWords; i++ )
1203  pTruth[i] = (pTruth[i] & s_PMasks[iVar][0]) | ((pTruth[i] & s_PMasks[iVar][1]) << Shift) | ((pTruth[i] & s_PMasks[iVar][2]) >> Shift);
1204  }
1205  else if ( iVar == 5 )
1206  {
1207  unsigned * pTruthU = (unsigned *)pTruth;
1208  unsigned * pLimitU = (unsigned *)(pTruth + nWords);
1209  for ( ; pTruthU < pLimitU; pTruthU += 4 )
1210  ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] );
1211  }
1212  else // if ( iVar > 5 )
1213  {
1214  word * pLimit = pTruth + nWords;
1215  int i, iStep = Abc_TtWordNum(iVar);
1216  for ( ; pTruth < pLimit; pTruth += 4*iStep )
1217  for ( i = 0; i < iStep; i++ )
1218  ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] );
1219  }
1220 }
1221 static inline word Abc_Tt6SwapVars( word t, int iVar, int jVar )
1222 {
1223  word * s_PMasks = Ps_PMasks[iVar][jVar];
1224  int shift = (1 << jVar) - (1 << iVar);
1225  assert( iVar < jVar );
1226  return (t & s_PMasks[0]) | ((t & s_PMasks[1]) << shift) | ((t & s_PMasks[2]) >> shift);
1227 }
1228 static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
1229 {
1230  if ( iVar == jVar )
1231  return;
1232  if ( jVar < iVar )
1233  ABC_SWAP( int, iVar, jVar );
1234  assert( iVar < jVar && jVar < nVars );
1235  if ( nVars <= 6 )
1236  {
1237  pTruth[0] = Abc_Tt6SwapVars( pTruth[0], iVar, jVar );
1238  return;
1239  }
1240  if ( jVar <= 5 )
1241  {
1242  word * s_PMasks = Ps_PMasks[iVar][jVar];
1243  int nWords = Abc_TtWordNum(nVars);
1244  int w, shift = (1 << jVar) - (1 << iVar);
1245  for ( w = 0; w < nWords; w++ )
1246  pTruth[w] = (pTruth[w] & s_PMasks[0]) | ((pTruth[w] & s_PMasks[1]) << shift) | ((pTruth[w] & s_PMasks[2]) >> shift);
1247  return;
1248  }
1249  if ( iVar <= 5 && jVar > 5 )
1250  {
1251  word low2High, high2Low;
1252  word * pLimit = pTruth + Abc_TtWordNum(nVars);
1253  int j, jStep = Abc_TtWordNum(jVar);
1254  int shift = 1 << iVar;
1255  for ( ; pTruth < pLimit; pTruth += 2*jStep )
1256  for ( j = 0; j < jStep; j++ )
1257  {
1258  low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
1259  high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
1260  pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
1261  pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
1262  }
1263  return;
1264  }
1265  {
1266  word * pLimit = pTruth + Abc_TtWordNum(nVars);
1267  int i, iStep = Abc_TtWordNum(iVar);
1268  int j, jStep = Abc_TtWordNum(jVar);
1269  for ( ; pTruth < pLimit; pTruth += 2*jStep )
1270  for ( i = 0; i < jStep; i += 2*iStep )
1271  for ( j = 0; j < iStep; j++ )
1272  ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
1273  return;
1274  }
1275 }
1276 // moves one var (v) to the given position (p)
1277 static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p )
1278 {
1279  int iVar = V2P[v], jVar = p;
1280  if ( iVar == jVar )
1281  return;
1282  Abc_TtSwapVars( pF, nVars, iVar, jVar );
1283  V2P[P2V[iVar]] = jVar;
1284  V2P[P2V[jVar]] = iVar;
1285  P2V[iVar] ^= P2V[jVar];
1286  P2V[jVar] ^= P2V[iVar];
1287  P2V[iVar] ^= P2V[jVar];
1288 }
1289 
1290 /**Function*************************************************************
1291 
1292  Synopsis [Support minimization.]
1293 
1294  Description []
1295 
1296  SideEffects []
1297 
1298  SeeAlso []
1299 
1300 ***********************************************************************/
1301 static inline void Abc_TtShrink( word * pF, int nVars, int nVarsAll, unsigned Phase )
1302 {
1303  int i, k, Var = 0;
1304  assert( nVarsAll <= 16 );
1305  for ( i = 0; i < nVarsAll; i++ )
1306  if ( Phase & (1 << i) )
1307  {
1308  for ( k = i-1; k >= Var; k-- )
1309  Abc_TtSwapAdjacent( pF, Abc_TtWordNum(nVarsAll), k );
1310  Var++;
1311  }
1312  assert( Var == nVars );
1313 }
1314 static inline int Abc_TtMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars )
1315 {
1316  int v, iVar = 0, uSupp = 0;
1317  assert( nVarsAll <= 16 );
1318  for ( v = 0; v < nVarsAll; v++ )
1319  if ( Abc_TtHasVar( t, nVarsAll, v ) )
1320  {
1321  uSupp |= (1 << v);
1322  if ( pSupp )
1323  pSupp[iVar] = pSupp[v];
1324  iVar++;
1325  }
1326  if ( pnVars )
1327  *pnVars = iVar;
1328  if ( uSupp == 0 || Abc_TtSuppIsMinBase( uSupp ) )
1329  return 0;
1330  Abc_TtShrink( t, iVar, nVarsAll, uSupp );
1331  return 1;
1332 }
1333 
1334 /**Function*************************************************************
1335 
1336  Synopsis [Cut minimization.]
1337 
1338  Description []
1339 
1340  SideEffects []
1341 
1342  SeeAlso []
1343 
1344 ***********************************************************************/
1345 static inline word Abc_Tt6Expand( word t, int * pCut0, int nCutSize0, int * pCut, int nCutSize )
1346 {
1347  int i, k;
1348  for ( i = nCutSize - 1, k = nCutSize0 - 1; i >= 0 && k >= 0; i-- )
1349  {
1350  if ( pCut[i] > pCut0[k] )
1351  continue;
1352  assert( pCut[i] == pCut0[k] );
1353  if ( k < i )
1354  t = Abc_Tt6SwapVars( t, k, i );
1355  k--;
1356  }
1357  assert( k == -1 );
1358  return t;
1359 }
1360 static inline void Abc_TtExpand( word * pTruth0, int nVars, int * pCut0, int nCutSize0, int * pCut, int nCutSize )
1361 {
1362  int i, k;
1363  for ( i = nCutSize - 1, k = nCutSize0 - 1; i >= 0 && k >= 0; i-- )
1364  {
1365  if ( pCut[i] > pCut0[k] )
1366  continue;
1367  assert( pCut[i] == pCut0[k] );
1368  if ( k < i )
1369  Abc_TtSwapVars( pTruth0, nVars, k, i );
1370  k--;
1371  }
1372  assert( k == -1 );
1373 }
1374 static inline int Abc_Tt6MinBase( word * pTruth, int * pVars, int nVars )
1375 {
1376  word t = *pTruth;
1377  int i, k;
1378  for ( i = k = 0; i < nVars; i++ )
1379  {
1380  if ( !Abc_Tt6HasVar( t, i ) )
1381  continue;
1382  if ( k < i )
1383  {
1384  if ( pVars ) pVars[k] = pVars[i];
1385  t = Abc_Tt6SwapVars( t, k, i );
1386  }
1387  k++;
1388  }
1389  if ( k == nVars )
1390  return k;
1391  assert( k < nVars );
1392  *pTruth = t;
1393  return k;
1394 }
1395 static inline int Abc_TtMinBase( word * pTruth, int * pVars, int nVars, int nVarsAll )
1396 {
1397  int i, k;
1398  assert( nVars <= nVarsAll );
1399  for ( i = k = 0; i < nVars; i++ )
1400  {
1401  if ( !Abc_TtHasVar( pTruth, nVarsAll, i ) )
1402  continue;
1403  if ( k < i )
1404  {
1405  if ( pVars ) pVars[k] = pVars[i];
1406  Abc_TtSwapVars( pTruth, nVarsAll, k, i );
1407  }
1408  k++;
1409  }
1410  if ( k == nVars )
1411  return k;
1412  assert( k < nVars );
1413 // assert( k == Abc_TtSupportSize(pTruth, nVars) );
1414  return k;
1415 }
1416 
1417 /**Function*************************************************************
1418 
1419  Synopsis [Implemeting given NPN config.]
1420 
1421  Description []
1422 
1423  SideEffects []
1424 
1425  SeeAlso []
1426 
1427 ***********************************************************************/
1428 static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
1429 {
1430  int i, k, nWords = Abc_TtWordNum( nVars );
1431  if ( (uCanonPhase >> nVars) & 1 )
1432  Abc_TtNot( pTruth, nWords );
1433  for ( i = 0; i < nVars; i++ )
1434  if ( (uCanonPhase >> i) & 1 )
1435  Abc_TtFlip( pTruth, nWords, i );
1436  if ( pCanonPerm )
1437  for ( i = 0; i < nVars; i++ )
1438  {
1439  for ( k = i; k < nVars; k++ )
1440  if ( pCanonPerm[k] == i )
1441  break;
1442  assert( k < nVars );
1443  if ( i == k )
1444  continue;
1445  Abc_TtSwapVars( pTruth, nVars, i, k );
1446  ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
1447  }
1448 }
1449 
1450 /**Function*************************************************************
1451 
1452  Synopsis []
1453 
1454  Description []
1455 
1456  SideEffects []
1457 
1458  SeeAlso []
1459 
1460 ***********************************************************************/
1461 static inline int Abc_TtCountOnesSlow( word t )
1462 {
1463  t = (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
1464  t = (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
1465  t = (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
1466  t = (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
1467  t = (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
1468  return (t & ABC_CONST(0x00000000FFFFFFFF)) + (t>>32);
1469 }
1470 static inline int Abc_TtCountOnes( word x )
1471 {
1472  x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
1473  x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
1474  x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
1475  x = x + (x >> 8);
1476  x = x + (x >> 16);
1477  x = x + (x >> 32);
1478  return (int)(x & 0xFF);
1479 }
1480 
1481 /**Function*************************************************************
1482 
1483  Synopsis []
1484 
1485  Description []
1486 
1487  SideEffects []
1488 
1489  SeeAlso []
1490 
1491 ***********************************************************************/
1492 static inline int Abc_Tt6FirstBit( word t )
1493 {
1494  int n = 0;
1495  if ( t == 0 ) return -1;
1496  if ( (t & ABC_CONST(0x00000000FFFFFFFF)) == 0 ) { n += 32; t >>= 32; }
1497  if ( (t & ABC_CONST(0x000000000000FFFF)) == 0 ) { n += 16; t >>= 16; }
1498  if ( (t & ABC_CONST(0x00000000000000FF)) == 0 ) { n += 8; t >>= 8; }
1499  if ( (t & ABC_CONST(0x000000000000000F)) == 0 ) { n += 4; t >>= 4; }
1500  if ( (t & ABC_CONST(0x0000000000000003)) == 0 ) { n += 2; t >>= 2; }
1501  if ( (t & ABC_CONST(0x0000000000000001)) == 0 ) { n++; }
1502  return n;
1503 }
1504 static inline int Abc_Tt6LastBit( word t )
1505 {
1506  int n = 0;
1507  if ( t == 0 ) return -1;
1508  if ( (t & ABC_CONST(0xFFFFFFFF00000000)) == 0 ) { n += 32; t <<= 32; }
1509  if ( (t & ABC_CONST(0xFFFF000000000000)) == 0 ) { n += 16; t <<= 16; }
1510  if ( (t & ABC_CONST(0xFF00000000000000)) == 0 ) { n += 8; t <<= 8; }
1511  if ( (t & ABC_CONST(0xF000000000000000)) == 0 ) { n += 4; t <<= 4; }
1512  if ( (t & ABC_CONST(0xC000000000000000)) == 0 ) { n += 2; t <<= 2; }
1513  if ( (t & ABC_CONST(0x8000000000000000)) == 0 ) { n++; }
1514  return 63-n;
1515 }
1516 static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
1517 {
1518  int w, nWords = Abc_TtWordNum(nVars);
1519  for ( w = 0; w < nWords; w++ )
1520  if ( pIn[w] )
1521  return 64*w + Abc_Tt6FirstBit(pIn[w]);
1522  return -1;
1523 }
1524 static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
1525 {
1526  int w, nWords = Abc_TtWordNum(nVars);
1527  for ( w = 0; w < nWords; w++ )
1528  if ( ~pIn[w] )
1529  return 64*w + Abc_Tt6FirstBit(~pIn[w]);
1530  return -1;
1531 }
1532 static inline int Abc_TtFindLastBit( word * pIn, int nVars )
1533 {
1534  int w, nWords = Abc_TtWordNum(nVars);
1535  for ( w = nWords - 1; w >= 0; w-- )
1536  if ( pIn[w] )
1537  return 64*w + Abc_Tt6LastBit(pIn[w]);
1538  return -1;
1539 }
1540 static inline int Abc_TtFindLastZero( word * pIn, int nVars )
1541 {
1542  int w, nWords = Abc_TtWordNum(nVars);
1543  for ( w = nWords - 1; w >= 0; w-- )
1544  if ( ~pIn[w] )
1545  return 64*w + Abc_Tt6LastBit(~pIn[w]);
1546  return -1;
1547 }
1548 
1549 
1550 /**Function*************************************************************
1551 
1552  Synopsis []
1553 
1554  Description []
1555 
1556  SideEffects []
1557 
1558  SeeAlso []
1559 
1560 ***********************************************************************/
1561 static inline void Abc_TtReverseVars( word * pTruth, int nVars )
1562 {
1563  int k;
1564  for ( k = 0; k < nVars/2 ; k++ )
1565  Abc_TtSwapVars( pTruth, nVars, k, nVars - 1 - k );
1566 }
1567 static inline void Abc_TtReverseBits( word * pTruth, int nVars )
1568 {
1569  static unsigned char pMirror[256] = {
1570  0, 128, 64, 192, 32, 160, 96, 224, 16, 144, 80, 208, 48, 176, 112, 240,
1571  8, 136, 72, 200, 40, 168, 104, 232, 24, 152, 88, 216, 56, 184, 120, 248,
1572  4, 132, 68, 196, 36, 164, 100, 228, 20, 148, 84, 212, 52, 180, 116, 244,
1573  12, 140, 76, 204, 44, 172, 108, 236, 28, 156, 92, 220, 60, 188, 124, 252,
1574  2, 130, 66, 194, 34, 162, 98, 226, 18, 146, 82, 210, 50, 178, 114, 242,
1575  10, 138, 74, 202, 42, 170, 106, 234, 26, 154, 90, 218, 58, 186, 122, 250,
1576  6, 134, 70, 198, 38, 166, 102, 230, 22, 150, 86, 214, 54, 182, 118, 246,
1577  14, 142, 78, 206, 46, 174, 110, 238, 30, 158, 94, 222, 62, 190, 126, 254,
1578  1, 129, 65, 193, 33, 161, 97, 225, 17, 145, 81, 209, 49, 177, 113, 241,
1579  9, 137, 73, 201, 41, 169, 105, 233, 25, 153, 89, 217, 57, 185, 121, 249,
1580  5, 133, 69, 197, 37, 165, 101, 229, 21, 149, 85, 213, 53, 181, 117, 245,
1581  13, 141, 77, 205, 45, 173, 109, 237, 29, 157, 93, 221, 61, 189, 125, 253,
1582  3, 131, 67, 195, 35, 163, 99, 227, 19, 147, 83, 211, 51, 179, 115, 243,
1583  11, 139, 75, 203, 43, 171, 107, 235, 27, 155, 91, 219, 59, 187, 123, 251,
1584  7, 135, 71, 199, 39, 167, 103, 231, 23, 151, 87, 215, 55, 183, 119, 247,
1585  15, 143, 79, 207, 47, 175, 111, 239, 31, 159, 95, 223, 63, 191, 127, 255
1586  };
1587  unsigned char Temp, * pTruthC = (unsigned char *)pTruth;
1588  int i, nBytes = (nVars > 6) ? (1 << (nVars - 3)) : 8;
1589  for ( i = 0; i < nBytes/2; i++ )
1590  {
1591  Temp = pMirror[pTruthC[i]];
1592  pTruthC[i] = pMirror[pTruthC[nBytes-1-i]];
1593  pTruthC[nBytes-1-i] = Temp;
1594  }
1595 }
1596 
1597 
1598 /**Function*************************************************************
1599 
1600  Synopsis [Checks unateness of a function.]
1601 
1602  Description []
1603 
1604  SideEffects []
1605 
1606  SeeAlso []
1607 
1608 ***********************************************************************/
1609 static inline int Abc_Tt6PosVar( word t, int iVar )
1610 {
1611  return ((t >> (1<<iVar)) & t & s_Truths6Neg[iVar]) == (t & s_Truths6Neg[iVar]);
1612 }
1613 static inline int Abc_Tt6NegVar( word t, int iVar )
1614 {
1615  return ((t << (1<<iVar)) & t & s_Truths6[iVar]) == (t & s_Truths6[iVar]);
1616 }
1617 static inline int Abc_TtPosVar( word * t, int nVars, int iVar )
1618 {
1619  assert( iVar < nVars );
1620  if ( nVars <= 6 )
1621  return Abc_Tt6PosVar( t[0], iVar );
1622  if ( iVar < 6 )
1623  {
1624  int i, Shift = (1 << iVar);
1625  int nWords = Abc_TtWordNum( nVars );
1626  for ( i = 0; i < nWords; i++ )
1627  if ( ((t[i] >> Shift) & t[i] & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
1628  return 0;
1629  return 1;
1630  }
1631  else
1632  {
1633  int i, Step = (1 << (iVar - 6));
1634  word * tLimit = t + Abc_TtWordNum( nVars );
1635  for ( ; t < tLimit; t += 2*Step )
1636  for ( i = 0; i < Step; i++ )
1637  if ( t[i] != (t[i] & t[Step+i]) )
1638  return 0;
1639  return 1;
1640  }
1641 }
1642 static inline int Abc_TtNegVar( word * t, int nVars, int iVar )
1643 {
1644  assert( iVar < nVars );
1645  if ( nVars <= 6 )
1646  return Abc_Tt6NegVar( t[0], iVar );
1647  if ( iVar < 6 )
1648  {
1649  int i, Shift = (1 << iVar);
1650  int nWords = Abc_TtWordNum( nVars );
1651  for ( i = 0; i < nWords; i++ )
1652  if ( ((t[i] << Shift) & t[i] & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
1653  return 0;
1654  return 1;
1655  }
1656  else
1657  {
1658  int i, Step = (1 << (iVar - 6));
1659  word * tLimit = t + Abc_TtWordNum( nVars );
1660  for ( ; t < tLimit; t += 2*Step )
1661  for ( i = 0; i < Step; i++ )
1662  if ( (t[i] & t[Step+i]) != t[Step+i] )
1663  return 0;
1664  return 1;
1665  }
1666 }
1667 static inline int Abc_TtIsUnate( word * t, int nVars )
1668 {
1669  int i;
1670  for ( i = 0; i < nVars; i++ )
1671  if ( !Abc_TtNegVar(t, nVars, i) && !Abc_TtPosVar(t, nVars, i) )
1672  return 0;
1673  return 1;
1674 }
1675 static inline int Abc_TtIsPosUnate( word * t, int nVars )
1676 {
1677  int i;
1678  for ( i = 0; i < nVars; i++ )
1679  if ( !Abc_TtPosVar(t, nVars, i) )
1680  return 0;
1681  return 1;
1682 }
1683 static inline void Abc_TtMakePosUnate( word * t, int nVars )
1684 {
1685  int i, nWords = Abc_TtWordNum(nVars);
1686  for ( i = 0; i < nVars; i++ )
1687  if ( Abc_TtNegVar(t, nVars, i) )
1688  Abc_TtFlip( t, nWords, i );
1689  else assert( Abc_TtPosVar(t, nVars, i) );
1690 }
1691 
1692 
1693 /**Function*************************************************************
1694 
1695  Synopsis [Computes ISOP for 6 variables or less.]
1696 
1697  Description []
1698 
1699  SideEffects []
1700 
1701  SeeAlso []
1702 
1703 ***********************************************************************/
1704 static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars, int * pnCubes )
1705 {
1706  word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
1707  int Var;
1708  assert( nVars <= 6 );
1709  assert( (uOn & ~uOnDc) == 0 );
1710  if ( uOn == 0 )
1711  return 0;
1712  if ( uOnDc == ~(word)0 )
1713  {
1714  (*pnCubes)++;
1715  return ~(word)0;
1716  }
1717  assert( nVars > 0 );
1718  // find the topmost var
1719  for ( Var = nVars-1; Var >= 0; Var-- )
1720  if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
1721  break;
1722  assert( Var >= 0 );
1723  // cofactor
1724  uOn0 = Abc_Tt6Cofactor0( uOn, Var );
1725  uOn1 = Abc_Tt6Cofactor1( uOn , Var );
1726  uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
1727  uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
1728  // solve for cofactors
1729  uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var, pnCubes );
1730  uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var, pnCubes );
1731  uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pnCubes );
1732  // derive the final truth table
1733  uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
1734  assert( (uOn & ~uRes2) == 0 );
1735  assert( (uRes2 & ~uOnDc) == 0 );
1736  return uRes2;
1737 }
1738 static inline int Abc_Tt7Isop( word uOn[2], word uOnDc[2], int nVars, word uRes[2] )
1739 {
1740  int nCubes = 0;
1741  if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
1742  uRes[0] = uRes[1] = Abc_Tt6Isop( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), &nCubes );
1743  else
1744  {
1745  word uRes0, uRes1, uRes2;
1746  assert( nVars == 7 );
1747  // solve for cofactors
1748  uRes0 = Abc_Tt6Isop( uOn[0] & ~uOnDc[1], uOnDc[0], 6, &nCubes );
1749  uRes1 = Abc_Tt6Isop( uOn[1] & ~uOnDc[0], uOnDc[1], 6, &nCubes );
1750  uRes2 = Abc_Tt6Isop( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, &nCubes );
1751  // derive the final truth table
1752  uRes[0] = uRes2 | uRes0;
1753  uRes[1] = uRes2 | uRes1;
1754  assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
1755  assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
1756  }
1757  return nCubes;
1758 }
1759 static inline int Abc_Tt8Isop( word uOn[4], word uOnDc[4], int nVars, word uRes[4] )
1760 {
1761  int nCubes = 0;
1762  if ( nVars <= 6 )
1763  uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6Isop( uOn[0], uOnDc[0], nVars, &nCubes );
1764  else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
1765  {
1766  nCubes = Abc_Tt7Isop( uOn, uOnDc, 7, uRes );
1767  uRes[2] = uRes[0];
1768  uRes[3] = uRes[1];
1769  }
1770  else
1771  {
1772  word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
1773  assert( nVars == 8 );
1774  // cofactor
1775  uOn0[0] = uOn[0] & ~uOnDc[2];
1776  uOn0[1] = uOn[1] & ~uOnDc[3];
1777  uOn1[0] = uOn[2] & ~uOnDc[0];
1778  uOn1[1] = uOn[3] & ~uOnDc[1];
1779  uOnDc2[0] = uOnDc[0] & uOnDc[2];
1780  uOnDc2[1] = uOnDc[1] & uOnDc[3];
1781  // solve for cofactors
1782  nCubes += Abc_Tt7Isop( uOn0, uOnDc+0, 7, uRes0 );
1783  nCubes += Abc_Tt7Isop( uOn1, uOnDc+2, 7, uRes1 );
1784  uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
1785  uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
1786  nCubes += Abc_Tt7Isop( uOn2, uOnDc2, 7, uRes2 );
1787  // derive the final truth table
1788  uRes[0] = uRes2[0] | uRes0[0];
1789  uRes[1] = uRes2[1] | uRes0[1];
1790  uRes[2] = uRes2[0] | uRes1[0];
1791  uRes[3] = uRes2[1] | uRes1[1];
1792  assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
1793  assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
1794  }
1795  return nCubes;
1796 }
1797 
1798 /**Function*************************************************************
1799 
1800  Synopsis [Computes CNF size.]
1801 
1802  Description []
1803 
1804  SideEffects []
1805 
1806  SeeAlso []
1807 
1808 ***********************************************************************/
1809 static inline int Abc_Tt6CnfSize( word t, int nVars )
1810 {
1811  int nCubes = 0;
1812  Abc_Tt6Isop( t, t, nVars, &nCubes );
1813  Abc_Tt6Isop( ~t, ~t, nVars, &nCubes );
1814  assert( nCubes <= 64 );
1815  return nCubes;
1816 }
1817 static inline int Abc_Tt8CnfSize( word t[4], int nVars )
1818 {
1819  word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
1820  int nCubes = 0;
1821  nCubes += Abc_Tt8Isop( t, t, nVars, uRes );
1822  nCubes += Abc_Tt8Isop( tc, tc, nVars, uRes );
1823  assert( nCubes <= 256 );
1824  return nCubes;
1825 }
1826 
1827 /**Function*************************************************************
1828 
1829  Synopsis [Derives ISOP cover for the function.]
1830 
1831  Description []
1832 
1833  SideEffects []
1834 
1835  SeeAlso []
1836 
1837 ***********************************************************************/
1838 static inline word Abc_Tt6IsopCover( word uOn, word uOnDc, int nVars, int * pCover, int * pnCubes )
1839 {
1840  word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
1841  int c, Var, nBeg0, nEnd0, nEnd1;
1842  assert( nVars <= 6 );
1843  assert( (uOn & ~uOnDc) == 0 );
1844  if ( uOn == 0 )
1845  return 0;
1846  if ( uOnDc == ~(word)0 )
1847  {
1848  pCover[(*pnCubes)++] = 0;
1849  return ~(word)0;
1850  }
1851  assert( nVars > 0 );
1852  // find the topmost var
1853  for ( Var = nVars-1; Var >= 0; Var-- )
1854  if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
1855  break;
1856  assert( Var >= 0 );
1857  // cofactor
1858  uOn0 = Abc_Tt6Cofactor0( uOn, Var );
1859  uOn1 = Abc_Tt6Cofactor1( uOn , Var );
1860  uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
1861  uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
1862  // solve for cofactors
1863  nBeg0 = *pnCubes;
1864  uRes0 = Abc_Tt6IsopCover( uOn0 & ~uOnDc1, uOnDc0, Var, pCover, pnCubes );
1865  nEnd0 = *pnCubes;
1866  uRes1 = Abc_Tt6IsopCover( uOn1 & ~uOnDc0, uOnDc1, Var, pCover, pnCubes );
1867  nEnd1 = *pnCubes;
1868  uRes2 = Abc_Tt6IsopCover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pCover, pnCubes );
1869  // derive the final truth table
1870  uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
1871  for ( c = nBeg0; c < nEnd0; c++ )
1872  pCover[c] |= (1 << (2*Var+0));
1873  for ( c = nEnd0; c < nEnd1; c++ )
1874  pCover[c] |= (1 << (2*Var+1));
1875  assert( (uOn & ~uRes2) == 0 );
1876  assert( (uRes2 & ~uOnDc) == 0 );
1877  return uRes2;
1878 }
1879 static inline void Abc_Tt7IsopCover( word uOn[2], word uOnDc[2], int nVars, word uRes[2], int * pCover, int * pnCubes )
1880 {
1881  if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
1882  uRes[0] = uRes[1] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), pCover, pnCubes );
1883  else
1884  {
1885  word uRes0, uRes1, uRes2;
1886  int c, nBeg0, nEnd0, nEnd1;
1887  assert( nVars == 7 );
1888  // solve for cofactors
1889  nBeg0 = *pnCubes;
1890  uRes0 = Abc_Tt6IsopCover( uOn[0] & ~uOnDc[1], uOnDc[0], 6, pCover, pnCubes );
1891  nEnd0 = *pnCubes;
1892  uRes1 = Abc_Tt6IsopCover( uOn[1] & ~uOnDc[0], uOnDc[1], 6, pCover, pnCubes );
1893  nEnd1 = *pnCubes;
1894  uRes2 = Abc_Tt6IsopCover( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, pCover, pnCubes );
1895  // derive the final truth table
1896  uRes[0] = uRes2 | uRes0;
1897  uRes[1] = uRes2 | uRes1;
1898  for ( c = nBeg0; c < nEnd0; c++ )
1899  pCover[c] |= (1 << (2*6+0));
1900  for ( c = nEnd0; c < nEnd1; c++ )
1901  pCover[c] |= (1 << (2*6+1));
1902  assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
1903  assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
1904  }
1905 }
1906 static inline void Abc_Tt8IsopCover( word uOn[4], word uOnDc[4], int nVars, word uRes[4], int * pCover, int * pnCubes )
1907 {
1908  if ( nVars <= 6 )
1909  uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], nVars, pCover, pnCubes );
1910  else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
1911  {
1912  Abc_Tt7IsopCover( uOn, uOnDc, 7, uRes, pCover, pnCubes );
1913  uRes[2] = uRes[0];
1914  uRes[3] = uRes[1];
1915  }
1916  else
1917  {
1918  word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
1919  int c, nBeg0, nEnd0, nEnd1;
1920  assert( nVars == 8 );
1921  // cofactor
1922  uOn0[0] = uOn[0] & ~uOnDc[2];
1923  uOn0[1] = uOn[1] & ~uOnDc[3];
1924  uOn1[0] = uOn[2] & ~uOnDc[0];
1925  uOn1[1] = uOn[3] & ~uOnDc[1];
1926  uOnDc2[0] = uOnDc[0] & uOnDc[2];
1927  uOnDc2[1] = uOnDc[1] & uOnDc[3];
1928  // solve for cofactors
1929  nBeg0 = *pnCubes;
1930  Abc_Tt7IsopCover( uOn0, uOnDc+0, 7, uRes0, pCover, pnCubes );
1931  nEnd0 = *pnCubes;
1932  Abc_Tt7IsopCover( uOn1, uOnDc+2, 7, uRes1, pCover, pnCubes );
1933  nEnd1 = *pnCubes;
1934  uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
1935  uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
1936  Abc_Tt7IsopCover( uOn2, uOnDc2, 7, uRes2, pCover, pnCubes );
1937  // derive the final truth table
1938  uRes[0] = uRes2[0] | uRes0[0];
1939  uRes[1] = uRes2[1] | uRes0[1];
1940  uRes[2] = uRes2[0] | uRes1[0];
1941  uRes[3] = uRes2[1] | uRes1[1];
1942  for ( c = nBeg0; c < nEnd0; c++ )
1943  pCover[c] |= (1 << (2*7+0));
1944  for ( c = nEnd0; c < nEnd1; c++ )
1945  pCover[c] |= (1 << (2*7+1));
1946  assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
1947  assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
1948  }
1949 }
1950 
1951 /**Function*************************************************************
1952 
1953  Synopsis [Computes CNF for the function.]
1954 
1955  Description []
1956 
1957  SideEffects []
1958 
1959  SeeAlso []
1960 
1961 ***********************************************************************/
1962 static inline int Abc_Tt6Cnf( word t, int nVars, int * pCover )
1963 {
1964  int c, nCubes = 0;
1965  Abc_Tt6IsopCover( t, t, nVars, pCover, &nCubes );
1966  for ( c = 0; c < nCubes; c++ )
1967  pCover[c] |= (1 << (2*nVars+0));
1968  Abc_Tt6IsopCover( ~t, ~t, nVars, pCover, &nCubes );
1969  for ( ; c < nCubes; c++ )
1970  pCover[c] |= (1 << (2*nVars+1));
1971  assert( nCubes <= 64 );
1972  return nCubes;
1973 }
1974 static inline int Abc_Tt8Cnf( word t[4], int nVars, int * pCover )
1975 {
1976  word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
1977  int c, nCubes = 0;
1978  Abc_Tt8IsopCover( t, t, nVars, uRes, pCover, &nCubes );
1979  for ( c = 0; c < nCubes; c++ )
1980  pCover[c] |= (1 << (2*nVars+0));
1981  Abc_Tt8IsopCover( tc, tc, nVars, uRes, pCover, &nCubes );
1982  for ( ; c < nCubes; c++ )
1983  pCover[c] |= (1 << (2*nVars+1));
1984  assert( nCubes <= 256 );
1985  return nCubes;
1986 }
1987 
1988 
1989 /**Function*************************************************************
1990 
1991  Synopsis [Computes ISOP for 6 variables or less.]
1992 
1993  Description []
1994 
1995  SideEffects []
1996 
1997  SeeAlso []
1998 
1999 ***********************************************************************/
2000 static inline int Abc_Tt6Esop( word t, int nVars, int * pCover )
2001 {
2002  word c0, c1;
2003  int Var, r0, r1, r2, Max, i;
2004  assert( nVars <= 6 );
2005  if ( t == 0 )
2006  return 0;
2007  if ( t == ~(word)0 )
2008  {
2009  if ( pCover ) *pCover = 0;
2010  return 1;
2011  }
2012  assert( nVars > 0 );
2013  // find the topmost var
2014  for ( Var = nVars-1; Var >= 0; Var-- )
2015  if ( Abc_Tt6HasVar( t, Var ) )
2016  break;
2017  assert( Var >= 0 );
2018  // cofactor
2019  c0 = Abc_Tt6Cofactor0( t, Var );
2020  c1 = Abc_Tt6Cofactor1( t, Var );
2021  // call recursively
2022  r0 = Abc_Tt6Esop( c0, Var, pCover ? pCover : NULL );
2023  r1 = Abc_Tt6Esop( c1, Var, pCover ? pCover + r0 : NULL );
2024  r2 = Abc_Tt6Esop( c0 ^ c1, Var, pCover ? pCover + r0 + r1 : NULL );
2025  Max = Abc_MaxInt( r0, Abc_MaxInt(r1, r2) );
2026  // add literals
2027  if ( pCover )
2028  {
2029  if ( Max == r0 )
2030  {
2031  for ( i = 0; i < r1; i++ )
2032  pCover[i] = pCover[r0+i];
2033  for ( i = 0; i < r2; i++ )
2034  pCover[r1+i] = pCover[r0+r1+i] | (1 << (2*Var+0));
2035  }
2036  else if ( Max == r1 )
2037  {
2038  for ( i = 0; i < r2; i++ )
2039  pCover[r0+i] = pCover[r0+r1+i] | (1 << (2*Var+1));
2040  }
2041  else
2042  {
2043  for ( i = 0; i < r0; i++ )
2044  pCover[i] |= (1 << (2*Var+0));
2045  for ( i = 0; i < r1; i++ )
2046  pCover[r0+i] |= (1 << (2*Var+1));
2047  }
2048  }
2049  return r0 + r1 + r2 - Max;
2050 }
2051 static inline word Abc_Tt6EsopBuild( int nVars, int * pCover, int nCubes )
2052 {
2053  word p, t = 0; int c, v;
2054  for ( c = 0; c < nCubes; c++ )
2055  {
2056  p = ~(word)0;
2057  for ( v = 0; v < nVars; v++ )
2058  if ( ((pCover[c] >> (v << 1)) & 3) == 1 )
2059  p &= ~s_Truths6[v];
2060  else if ( ((pCover[c] >> (v << 1)) & 3) == 2 )
2061  p &= s_Truths6[v];
2062  t ^= p;
2063  }
2064  return t;
2065 }
2066 static inline int Abc_Tt6EsopVerify( word t, int nVars )
2067 {
2068  int pCover[64];
2069  int nCubes = Abc_Tt6Esop( t, nVars, pCover );
2070  word t2 = Abc_Tt6EsopBuild( nVars, pCover, nCubes );
2071  if ( t != t2 )
2072  printf( "Verification failed.\n" );
2073  return nCubes;
2074 }
2075 
2076 /**Function*************************************************************
2077 
2078  Synopsis [Check if the function is decomposable with the given pair.]
2079 
2080  Description []
2081 
2082  SideEffects []
2083 
2084  SeeAlso []
2085 
2086 ***********************************************************************/
2087 static inline int Abc_TtCheckDsdAnd( word t, int i, int j, word * pOut )
2088 {
2089  word c0 = Abc_Tt6Cofactor0( t, i );
2090  word c1 = Abc_Tt6Cofactor1( t, i );
2091  word c00 = Abc_Tt6Cofactor0( c0, j );
2092  word c01 = Abc_Tt6Cofactor1( c0, j );
2093  word c10 = Abc_Tt6Cofactor0( c1, j );
2094  word c11 = Abc_Tt6Cofactor1( c1, j );
2095  if ( c00 == c01 && c00 == c10 ) // i * j
2096  {
2097  if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
2098  return 0;
2099  }
2100  if ( c11 == c00 && c11 == c10 ) // i * !j
2101  {
2102  if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01);
2103  return 1;
2104  }
2105  if ( c11 == c00 && c11 == c01 ) // !i * j
2106  {
2107  if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
2108  return 2;
2109  }
2110  if ( c11 == c01 && c11 == c10 ) // !i * !j
2111  {
2112  if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00);
2113  return 3;
2114  }
2115  if ( c00 == c11 && c01 == c10 )
2116  {
2117  if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
2118  return 4;
2119  }
2120  return -1;
2121 }
2122 static inline int Abc_TtCheckDsdMux( word t, int i, word * pOut )
2123 {
2124  word c0 = Abc_Tt6Cofactor0( t, i );
2125  word c1 = Abc_Tt6Cofactor1( t, i );
2126  word c00, c01, c10, c11;
2127  int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1;
2128  for ( k = 0; k < 6; k++ )
2129  {
2130  if ( k == i ) continue;
2131  fPres0 = Abc_Tt6HasVar( c0, k );
2132  fPres1 = Abc_Tt6HasVar( c1, k );
2133  if ( fPres0 && !fPres1 )
2134  {
2135  if ( iVar0 >= 0 )
2136  return -1;
2137  iVar0 = k;
2138  }
2139  if ( !fPres0 && fPres1 )
2140  {
2141  if ( iVar1 >= 0 )
2142  return -1;
2143  iVar1 = k;
2144  }
2145  }
2146  if ( iVar0 == -1 || iVar1 == -1 )
2147  return -1;
2148  c00 = Abc_Tt6Cofactor0( c0, iVar0 );
2149  c01 = Abc_Tt6Cofactor1( c0, iVar0 );
2150  c10 = Abc_Tt6Cofactor0( c1, iVar1 );
2151  c11 = Abc_Tt6Cofactor1( c1, iVar1 );
2152  if ( c00 == c10 && c01 == c11 ) // ITE(i, iVar1, iVar0)
2153  {
2154  if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
2155  return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0);
2156  }
2157  if ( c00 == ~c10 && c01 == ~c11 ) // ITE(i, iVar1, !iVar0)
2158  {
2159  if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
2160  return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1);
2161  }
2162  return -1;
2163 }
2164 static inline void Unm_ManCheckTest2()
2165 {
2166  word t, t1, Out, Var0, Var1, Var0_, Var1_;
2167  int iVar0, iVar1, i, Res;
2168  for ( iVar0 = 0; iVar0 < 6; iVar0++ )
2169  for ( iVar1 = 0; iVar1 < 6; iVar1++ )
2170  {
2171  if ( iVar0 == iVar1 )
2172  continue;
2173  Var0 = s_Truths6[iVar0];
2174  Var1 = s_Truths6[iVar1];
2175  for ( i = 0; i < 5; i++ )
2176  {
2177  Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0;
2178  Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1;
2179 
2180  t = Var0_ & Var1_;
2181  if ( i == 4 )
2182  t = ~(Var0_ ^ Var1_);
2183 
2184 // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
2185 
2186  Res = Abc_TtCheckDsdAnd( t, iVar0, iVar1, &Out );
2187  if ( Res == -1 )
2188  {
2189  printf( "No decomposition\n" );
2190  continue;
2191  }
2192 
2193  Var0_ = s_Truths6[iVar0];
2194  Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_;
2195 
2196  Var1_ = s_Truths6[iVar1];
2197  Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_;
2198 
2199  t1 = Var0_ & Var1_;
2200  if ( Res == 4 )
2201  t1 = Var0_ ^ Var1_;
2202 
2203  t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0));
2204 
2205 // Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
2206 
2207  if ( t1 != t )
2208  printf( "Verification failed.\n" );
2209  else
2210  printf( "Verification succeeded.\n" );
2211  }
2212  }
2213 }
2214 static inline void Unm_ManCheckTest()
2215 {
2216  word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_;
2217  int iVar0, iVar1, iCtrl, i, Res;
2218  for ( iCtrl = 0; iCtrl < 6; iCtrl++ )
2219  for ( iVar0 = 0; iVar0 < 6; iVar0++ )
2220  for ( iVar1 = 0; iVar1 < 6; iVar1++ )
2221  {
2222  if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 )
2223  continue;
2224  Ctrl = s_Truths6[iCtrl];
2225  Var0 = s_Truths6[iVar0];
2226  Var1 = s_Truths6[iVar1];
2227  for ( i = 0; i < 8; i++ )
2228  {
2229  Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl;
2230  Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0;
2231  Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1;
2232 
2233  t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
2234 
2235 // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
2236 
2237  Res = Abc_TtCheckDsdMux( t, iCtrl, &Out );
2238  if ( Res == -1 )
2239  {
2240  printf( "No decomposition\n" );
2241  continue;
2242  }
2243 
2244 // Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
2245 
2246  Ctrl_ = s_Truths6[iCtrl];
2247  Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
2248  Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_;
2249 
2250  Res >>= 16;
2251  Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
2252  Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_;
2253 
2254  t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
2255 
2256 // Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
2257 // Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
2258 
2259  t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl));
2260 
2261 // Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
2262 
2263  if ( t1 != t )
2264  printf( "Verification failed.\n" );
2265  else
2266  printf( "Verification succeeded.\n" );
2267  }
2268  }
2269 }
2270 
2271 
2272 
2273 /**Function*************************************************************
2274 
2275  Synopsis [Checks existence of bi-decomposition.]
2276 
2277  Description []
2278 
2279  SideEffects []
2280 
2281  SeeAlso []
2282 
2283 ***********************************************************************/
2284 static inline void Abc_TtComputeGraph( word * pTruth, int v, int nVars, int * pGraph )
2285 {
2286  word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 )
2287  word Cof00[64], Cof01[64], Cof10[64], Cof11[64];
2288  word CofXor, CofAndTest;
2289  int i, w, nWords = Abc_TtWordNum(nVars);
2290  pGraph[v] |= (1 << v);
2291  if ( v == nVars - 1 )
2292  return;
2293  assert( v < nVars - 1 );
2294  Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
2295  Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
2296  for ( i = v + 1; i < nVars; i++ )
2297  {
2298  Abc_TtCofactor0p( Cof00, Cof0, nWords, i );
2299  Abc_TtCofactor1p( Cof01, Cof0, nWords, i );
2300  Abc_TtCofactor0p( Cof10, Cof1, nWords, i );
2301  Abc_TtCofactor1p( Cof11, Cof1, nWords, i );
2302  for ( w = 0; w < nWords; w++ )
2303  {
2304  CofXor = Cof00[w] ^ Cof01[w] ^ Cof10[w] ^ Cof11[w];
2305  CofAndTest = (Cof00[w] & Cof01[w]) | (Cof10[w] & Cof11[w]);
2306  if ( CofXor & CofAndTest )
2307  {
2308  pGraph[v] |= (1 << i);
2309  pGraph[i] |= (1 << v);
2310  }
2311  else if ( CofXor & ~CofAndTest )
2312  {
2313  pGraph[v] |= (1 << (16+i));
2314  pGraph[i] |= (1 << (16+v));
2315  }
2316  }
2317  }
2318 }
2319 static inline void Abc_TtPrintVarSet( int Mask, int nVars )
2320 {
2321  int i;
2322  for ( i = 0; i < nVars; i++ )
2323  if ( (Mask >> i) & 1 )
2324  printf( "1" );
2325  else
2326  printf( "." );
2327 }
2328 static inline void Abc_TtPrintBiDec( word * pTruth, int nVars )
2329 {
2330  int v, pGraph[12] = {0};
2331  assert( nVars <= 12 );
2332  for ( v = 0; v < nVars; v++ )
2333  {
2334  Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
2335  Abc_TtPrintVarSet( pGraph[v], nVars );
2336  printf( " " );
2337  Abc_TtPrintVarSet( pGraph[v] >> 16, nVars );
2338  printf( "\n" );
2339  }
2340 }
2341 static inline int Abc_TtVerifyBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word wThis, word wThat )
2342 {
2343  int pVarsThis[12], pVarsThat[12], pVarsAll[12];
2344  int nThis = Abc_TtBitCount16(This);
2345  int nThat = Abc_TtBitCount16(That);
2346  int i, k, nWords = Abc_TtWordNum(nVars);
2347  word pThis[64] = {wThis}, pThat[64] = {wThat};
2348  assert( nVars <= 12 );
2349  for ( i = 0; i < nVars; i++ )
2350  pVarsAll[i] = i;
2351  for ( i = k = 0; i < nVars; i++ )
2352  if ( (This >> i) & 1 )
2353  pVarsThis[k++] = i;
2354  assert( k == nThis );
2355  for ( i = k = 0; i < nVars; i++ )
2356  if ( (That >> i) & 1 )
2357  pVarsThat[k++] = i;
2358  assert( k == nThat );
2359  Abc_TtStretch6( pThis, nThis, nVars );
2360  Abc_TtStretch6( pThat, nThat, nVars );
2361  Abc_TtExpand( pThis, nVars, pVarsThis, nThis, pVarsAll, nVars );
2362  Abc_TtExpand( pThat, nVars, pVarsThat, nThat, pVarsAll, nVars );
2363  for ( k = 0; k < nWords; k++ )
2364  if ( pTruth[k] != (pThis[k] & pThat[k]) )
2365  return 0;
2366  return 1;
2367 }
2368 static inline void Abc_TtExist( word * pTruth, int iVar, int nWords )
2369 {
2370  word Cof0[64], Cof1[64];
2371  Abc_TtCofactor0p( Cof0, pTruth, nWords, iVar );
2372  Abc_TtCofactor1p( Cof1, pTruth, nWords, iVar );
2373  Abc_TtOr( pTruth, Cof0, Cof1, nWords );
2374 }
2375 static inline int Abc_TtCheckBiDec( word * pTruth, int nVars, int This, int That )
2376 {
2377  int VarMask[2] = {This & ~That, That & ~This};
2378  int v, c, nWords = Abc_TtWordNum(nVars);
2379  word pTempR[2][64];
2380  for ( c = 0; c < 2; c++ )
2381  {
2382  Abc_TtCopy( pTempR[c], pTruth, nWords, 0 );
2383  for ( v = 0; v < nVars; v++ )
2384  if ( ((VarMask[c] >> v) & 1) )
2385  Abc_TtExist( pTempR[c], v, nWords );
2386  }
2387  for ( v = 0; v < nWords; v++ )
2388  if ( ~pTruth[v] & pTempR[0][v] & pTempR[1][v] )
2389  return 0;
2390  return 1;
2391 }
2392 static inline word Abc_TtDeriveBiDecOne( word * pTruth, int nVars, int This )
2393 {
2394  word pTemp[64];
2395  int nThis = Abc_TtBitCount16(This);
2396  int v, nWords = Abc_TtWordNum(nVars);
2397  Abc_TtCopy( pTemp, pTruth, nWords, 0 );
2398  for ( v = 0; v < nVars; v++ )
2399  if ( !((This >> v) & 1) )
2400  Abc_TtExist( pTemp, v, nWords );
2401  Abc_TtShrink( pTemp, nThis, nVars, This );
2402  return Abc_Tt6Stretch( pTemp[0], nThis );
2403 }
2404 static inline void Abc_TtDeriveBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word * pThis, word * pThat )
2405 {
2406  assert( Abc_TtBitCount16(This) <= nSuppLim );
2407  assert( Abc_TtBitCount16(That) <= nSuppLim );
2408  pThis[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, This );
2409  pThat[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, That );
2410  if ( !Abc_TtVerifyBiDec(pTruth, nVars, This, That, nSuppLim, pThis[0], pThat[0] ) )
2411  printf( "Bi-decomposition verification failed.\n" );
2412 }
2413 // detect simple case of decomposition with topmost AND gate
2414 static inline int Abc_TtCheckBiDecSimple( word * pTruth, int nVars, int nSuppLim )
2415 {
2416  word Cof0[64], Cof1[64];
2417  int v, Res = 0, nDecVars = 0, nWords = Abc_TtWordNum(nVars);
2418  for ( v = 0; v < nVars; v++ )
2419  {
2420  Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
2421  Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
2422  if ( !Abc_TtIsConst0(Cof0, nWords) && !Abc_TtIsConst0(Cof1, nWords) )
2423  continue;
2424  nDecVars++;
2425  Res |= 1 << v;
2426  if ( nDecVars >= nVars - nSuppLim )
2427  return ((Res ^ (int)Abc_Tt6Mask(nVars)) << 16) | Res;
2428  }
2429  return 0;
2430 }
2431 static inline int Abc_TtProcessBiDec( word * pTruth, int nVars, int nSuppLim )
2432 {
2433  int i, v, Res, nSupp, CountShared = 0, pGraph[12] = {0};
2434  assert( nSuppLim < nVars && nVars <= 12 );
2435  assert( 2 <= nSuppLim && nSuppLim <= 6 );
2436  Res = Abc_TtCheckBiDecSimple( pTruth, nVars, nSuppLim );
2437  if ( Res )
2438  return Res;
2439  for ( v = 0; v < nVars; v++ )
2440  {
2441  Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
2442  nSupp = Abc_TtBitCount16(pGraph[v] & 0xFFFF);
2443  if ( nSupp > nSuppLim )
2444  {
2445  // this variable is shared - check if the limit is exceeded
2446  if ( ++CountShared > 2*nSuppLim - nVars )
2447  return 0;
2448  }
2449  else if ( nVars - nSupp <= nSuppLim )
2450  {
2451  int This = pGraph[v] & 0xFFFF;
2452  int That = This ^ (int)Abc_Tt6Mask(nVars);
2453  // find the other component
2454  int Graph = That;
2455  for ( i = 0; i < nVars; i++ )
2456  if ( (That >> i) & 1 )
2457  Graph |= pGraph[i] & 0xFFFF;
2458  // check if this can be done
2459  if ( Abc_TtBitCount16(Graph) > nSuppLim )
2460  continue;
2461  // try decomposition
2462  if ( Abc_TtCheckBiDec(pTruth, nVars, This, Graph) )
2463  return (Graph << 16) | This;
2464  }
2465  }
2466  return 0;
2467 }
2468 
2469 /**Function*************************************************************
2470 
2471  Synopsis [Tests decomposition procedures.]
2472 
2473  Description []
2474 
2475  SideEffects []
2476 
2477  SeeAlso []
2478 
2479 ***********************************************************************/
2480 static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLim )
2481 {
2482  word This, That, pTemp[64];
2483  int Res, resThis, resThat, nThis, nThat;
2484  int nWords = Abc_TtWordNum(nVars);
2485  Abc_TtCopy( pTemp, pTruth, nWords, 0 );
2486  Res = Abc_TtProcessBiDec( pTemp, nVars, nSuppLim );
2487  if ( Res == 0 )
2488  {
2489  //Dau_DsdPrintFromTruth( pTemp, nVars );
2490  //printf( "Non_dec\n\n" );
2491  return;
2492  }
2493 
2494  resThis = Res & 0xFFFF;
2495  resThat = Res >> 16;
2496 
2497  Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
2498  return;
2499 
2500  //if ( !(resThis & resThat) )
2501  // return;
2502 
2503 // Dau_DsdPrintFromTruth( pTemp, nVars );
2504 
2505  nThis = Abc_TtBitCount16(resThis);
2506  nThat = Abc_TtBitCount16(resThat);
2507 
2508  printf( "Variable sets: " );
2509  Abc_TtPrintVarSet( resThis, nVars );
2510  printf( " " );
2511  Abc_TtPrintVarSet( resThat, nVars );
2512  printf( "\n" );
2513  Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
2514 // Dau_DsdPrintFromTruth( &This, nThis );
2515 // Dau_DsdPrintFromTruth( &That, nThat );
2516  printf( "\n" );
2517 }
2518 static inline void Abc_TtProcessBiDecExperiment()
2519 {
2520  int nVars = 3;
2521  int nSuppLim = 2;
2522  int Res, resThis, resThat;
2523  word This, That;
2524 // word t = ABC_CONST(0x8000000000000000);
2525 // word t = (s_Truths6[0] | s_Truths6[1]) & (s_Truths6[2] | s_Truths6[3] | s_Truths6[4] | s_Truths6[5]);
2526 // word t = ((s_Truths6[0] & s_Truths6[1]) | (~s_Truths6[1] & s_Truths6[2]));
2527  word t = ((s_Truths6[0] | s_Truths6[1]) & (s_Truths6[1] | s_Truths6[2]));
2528  Abc_TtPrintBiDec( &t, nVars );
2529  Res = Abc_TtProcessBiDec( &t, nVars, nSuppLim );
2530  resThis = Res & 0xFFFF;
2531  resThat = Res >> 16;
2532  Abc_TtDeriveBiDec( &t, nVars, resThis, resThat, nSuppLim, &This, &That );
2533 // Dau_DsdPrintFromTruth( &This, Abc_TtBitCount16(resThis) );
2534 // Dau_DsdPrintFromTruth( &That, Abc_TtBitCount16(resThat) );
2535  nVars = nSuppLim;
2536 }
2537 
2538 /*=== utilTruth.c ===========================================================*/
2539 
2540 
2541 ABC_NAMESPACE_HEADER_END
2542 
2543 #endif
2544 
2545 ////////////////////////////////////////////////////////////////////////
2546 /// END OF FILE ///
2547 ////////////////////////////////////////////////////////////////////////
Abc_Tt6IsopCover
static word Abc_Tt6IsopCover(word uOn, word uOnDc, int nVars, int *pCover, int *pnCubes)
Definition: utilTruth.h:1838
Abc_Tt8Isop
static int Abc_Tt8Isop(word uOn[4], word uOnDc[4], int nVars, word uRes[4])
Definition: utilTruth.h:1759
Abc_TtSharp
static void Abc_TtSharp(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:241
Abc_TtReverseVars
static void Abc_TtReverseVars(word *pTruth, int nVars)
Definition: utilTruth.h:1561
Abc_TtPrintDigit
static char Abc_TtPrintDigit(int Digit)
Definition: utilTruth.h:742
Abc_TtCheckEqualCofs
static int Abc_TtCheckEqualCofs(word *pTruth, int nWords, int iVar, int jVar, int Num1, int Num2)
Definition: utilTruth.h:475
Abc_Tt6Expand
static word Abc_Tt6Expand(word t, int *pCut0, int nCutSize0, int *pCut, int nCutSize)
Definition: utilTruth.h:1345
Abc_TtStretch5
static void Abc_TtStretch5(unsigned *pInOut, int nVarS, int nVarB)
Definition: utilTruth.h:678
Abc_TtReadHexNumber
static int Abc_TtReadHexNumber(word *pTruth, char *pString)
Definition: utilTruth.h:878
Abc_Tt6Cof1IsConst0
static int Abc_Tt6Cof1IsConst0(word t, int iVar)
Definition: utilTruth.h:540
Abc_TtMinimumBase
static int Abc_TtMinimumBase(word *t, int *pSupp, int nVarsAll, int *pnVars)
Definition: utilTruth.h:1314
Abc_TtSuppFindFirst
static int Abc_TtSuppFindFirst(int Supp)
Definition: utilTruth.h:929
Abc_TtMinBase
static int Abc_TtMinBase(word *pTruth, int *pVars, int nVars, int nVarsAll)
Definition: utilTruth.h:1395
Abc_TtSupport
static int Abc_TtSupport(word *t, int nVars)
Definition: utilTruth.h:978
Abc_Tt6Permute_rec
static word Abc_Tt6Permute_rec(word t, int *pPerm, int nVars)
Definition: utilTruth.h:1161
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_TtCofactor1p
static void Abc_TtCofactor1p(word *pOut, word *pIn, int nWords, int iVar)
Definition: utilTruth.h:403
Abc_TtFindLastZero
static int Abc_TtFindLastZero(word *pIn, int nVars)
Definition: utilTruth.h:1540
Abc_Tt6CnfSize
static int Abc_Tt6CnfSize(word t, int nVars)
Definition: utilTruth.h:1809
Abc_TtTruthIsConst0
static int Abc_TtTruthIsConst0(word *p, int nWords)
Definition: utilTruth.h:558
Abc_TtBitCount8
static int Abc_TtBitCount8[256]
Definition: utilTruth.h:117
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Gia_ManTtIsOrType
static int Gia_ManTtIsOrType(word t, int nVars)
Definition: utilTruth.h:1105
Abc_Tt6HasVar
static int Abc_Tt6HasVar(word t, int iVar)
Definition: utilTruth.h:949
Abc_TtSuppIsMinBase
static int Abc_TtSuppIsMinBase(int Supp)
Definition: utilTruth.h:944
Abc_Truth6WordNum
static int Abc_Truth6WordNum(int nVars)
Definition: abc_global.h:257
Abc_TtPrintHexRev
static void Abc_TtPrintHexRev(FILE *pFile, word *pTruth, int nVars)
Definition: utilTruth.h:789
Abc_TtPrintHexArrayRev
static void Abc_TtPrintHexArrayRev(FILE *pFile, word *pTruth, int nDigits)
Definition: utilTruth.h:820
Abc_Tt6Cof0IsConst1
static int Abc_Tt6Cof0IsConst1(word t, int iVar)
Definition: utilTruth.h:539
Abc_TtClear
static void Abc_TtClear(word *pOut, int nWords)
Definition: utilTruth.h:197
Abc_TtCof0IsConst0
static int Abc_TtCof0IsConst0(word *t, int nWords, int iVar)
Definition: utilTruth.h:561
Abc_TtIsConst0
static int Abc_TtIsConst0(word *pIn1, int nWords)
Definition: utilTruth.h:293
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Abc_TtFindFirstBit
static int Abc_TtFindFirstBit(word *pIn, int nVars)
Definition: utilTruth.h:1516
Abc_TtUnit
static void Abc_TtUnit(word *pOut, int nWords)
Definition: utilTruth.h:209
Abc_Tt6EsopBuild
static word Abc_Tt6EsopBuild(int nVars, int *pCover, int nCubes)
Definition: utilTruth.h:2051
Abc_TtFindFirstZero
static int Abc_TtFindFirstZero(word *pIn, int nVars)
Definition: utilTruth.h:1524
Abc_Tt6PosVar
static int Abc_Tt6PosVar(word t, int iVar)
Definition: utilTruth.h:1609
Abc_TtReadHexDigit
static int Abc_TtReadHexDigit(char HexChar)
Definition: utilTruth.h:756
Abc_TtExist
static void Abc_TtExist(word *pTruth, int iVar, int nWords)
Definition: utilTruth.h:2368
Abc_Tt6FirstBit
static int Abc_Tt6FirstBit(word t)
Definition: utilTruth.h:1492
Abc_TtOr
static void Abc_TtOr(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:247
Abc_TtSetBit
static void Abc_TtSetBit(word *p, int i)
Definition: utilTruth.h:150
Abc_TtProcessBiDec
static int Abc_TtProcessBiDec(word *pTruth, int nVars, int nSuppLim)
Definition: utilTruth.h:2431
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
Unm_ManCheckTest2
static void Unm_ManCheckTest2()
Definition: utilTruth.h:2164
Abc_TtCountOnes
static int Abc_TtCountOnes(word x)
Definition: utilTruth.h:1470
Gia_ManTtIsAndType
static int Gia_ManTtIsAndType(word t, int nVars)
Definition: utilTruth.h:1101
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_TtCheckBiDec
static int Abc_TtCheckBiDec(word *pTruth, int nVars, int This, int That)
Definition: utilTruth.h:2375
Abc_TtGetBit
static int Abc_TtGetBit(word *p, int i)
MACRO DEFINITIONS ///.
Definition: utilTruth.h:149
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Abc_TtCheckDsdAnd
static int Abc_TtCheckDsdAnd(word t, int i, int j, word *pOut)
Definition: utilTruth.h:2087
Abc_TtGetHex
static int Abc_TtGetHex(word *p, int k)
Definition: utilTruth.h:154
nWords
int nWords
Definition: abcNpn.c:127
Abc_TtConst1
static void Abc_TtConst1(word *pIn1, int nWords)
Definition: utilTruth.h:315
Abc_TtCheckCondDep2
static int Abc_TtCheckCondDep2(word *pTruth, int nVars, int nSuppLim)
Definition: utilTruth.h:1025
Abc_TtIsConst1
static int Abc_TtIsConst1(word *pIn1, int nWords)
Definition: utilTruth.h:301
Abc_TtByteNum
static int Abc_TtByteNum(int nVars)
Definition: utilTruth.h:170
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Abc_Tt6MinBase
static int Abc_Tt6MinBase(word *pTruth, int *pVars, int nVars)
Definition: utilTruth.h:1374
Abc_TtReadHex
static int Abc_TtReadHex(word *pTruth, char *pString)
Definition: utilTruth.h:838
Unm_ManCheckTest
static void Unm_ManCheckTest()
Definition: utilTruth.h:2214
Abc_TtCof1IsConst1
static int Abc_TtCof1IsConst1(word *t, int nWords, int iVar)
Definition: utilTruth.h:624
Abc_TtBitCount16
static int Abc_TtBitCount16(int i)
Definition: utilTruth.h:127
Abc_TtWriteHexRev
static int Abc_TtWriteHexRev(char *pStr, word *pTruth, int nVars)
Definition: utilTruth.h:809
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Abc_Tt6SwapAdjacent
static word Abc_Tt6SwapAdjacent(word Truth, int iVar)
Definition: utilTruth.h:1186
Abc_TtXorBit
static void Abc_TtXorBit(word *p, int i)
Definition: utilTruth.h:151
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Abc_TtFill
static void Abc_TtFill(word *pOut, int nWords)
Definition: utilTruth.h:203
Abc_TtIsPosUnate
static int Abc_TtIsPosUnate(word *t, int nVars)
Definition: utilTruth.h:1675
Abc_TtHexDigitNum
static int Abc_TtHexDigitNum(int nVars)
Definition: utilTruth.h:171
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
Abc_TtCof0IsConst1
static int Abc_TtCof0IsConst1(word *t, int nWords, int iVar)
Definition: utilTruth.h:582
Abc_Tt6LastBit
static int Abc_Tt6LastBit(word t)
Definition: utilTruth.h:1504
Abc_TtCofactor0p
static void Abc_TtCofactor0p(word *pOut, word *pIn, int nWords, int iVar)
Definition: utilTruth.h:381
Abc_Tt6Cof0IsConst0
static int Abc_Tt6Cof0IsConst0(word t, int iVar)
Definition: utilTruth.h:538
Ps_PMasks
static word Ps_PMasks[5][6][3]
Definition: utilTruth.h:73
Abc_TtCountOnesSlow
static int Abc_TtCountOnesSlow(word t)
Definition: utilTruth.h:1461
Abc_TtDeriveBiDecOne
static word Abc_TtDeriveBiDecOne(word *pTruth, int nVars, int This)
Definition: utilTruth.h:2392
Abc_TtPrintBinary
static void Abc_TtPrintBinary(word *pTruth, int nVars)
Definition: utilTruth.h:907
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_TtMakePosUnate
static void Abc_TtMakePosUnate(word *t, int nVars)
Definition: utilTruth.h:1683
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
Abc_Tt6Cof1IsConst1
static int Abc_Tt6Cof1IsConst1(word t, int iVar)
Definition: utilTruth.h:541
Abc_TtDeriveBiDec
static void Abc_TtDeriveBiDec(word *pTruth, int nVars, int This, int That, int nSuppLim, word *pThis, word *pThat)
Definition: utilTruth.h:2404
Abc_Tt6EsopVerify
static int Abc_Tt6EsopVerify(word t, int nVars)
Definition: utilTruth.h:2066
Abc_TtStretch6
static void Abc_TtStretch6(word *pInOut, int nVarS, int nVarB)
Definition: utilTruth.h:693
Abc_TtVerifyBiDec
static int Abc_TtVerifyBiDec(word *pTruth, int nVars, int This, int That, int nSuppLim, word wThis, word wThat)
Definition: utilTruth.h:2341
Abc_TtCheckBiDecSimple
static int Abc_TtCheckBiDecSimple(word *pTruth, int nVars, int nSuppLim)
Definition: utilTruth.h:2414
Abc_TtPrintBiDec
static void Abc_TtPrintBiDec(word *pTruth, int nVars)
Definition: utilTruth.h:2328
Abc_Tt6Isop
static word Abc_Tt6Isop(word uOn, word uOnDc, int nVars, int *pnCubes)
Definition: utilTruth.h:1704
Abc_Tt7Isop
static int Abc_Tt7Isop(word uOn[2], word uOnDc[2], int nVars, word uRes[2])
Definition: utilTruth.h:1738
Abc_TtSupportAndSize
static int Abc_TtSupportAndSize(word *t, int nVars, int *pSuppSize)
Definition: utilTruth.h:994
Abc_Tt8CnfSize
static int Abc_Tt8CnfSize(word t[4], int nVars)
Definition: utilTruth.h:1817
Gia_ManTtIsXorType
static int Gia_ManTtIsXorType(word t, int nVars)
Definition: utilTruth.h:1109
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
Abc_TtXorHex
static void Abc_TtXorHex(word *p, int k, int d)
Definition: utilTruth.h:156
Abc_TtImplementNpnConfig
static void Abc_TtImplementNpnConfig(word *pTruth, int nVars, char *pCanonPerm, unsigned uCanonPhase)
Definition: utilTruth.h:1428
Abc_TtOnlyOneOne
static int Abc_TtOnlyOneOne(word t)
Definition: utilTruth.h:1095
Abc_TtHasVar
static int Abc_TtHasVar(word *t, int nVars, int iVar)
Definition: utilTruth.h:953
s_PMasks
static word s_PMasks[5][3]
Definition: utilTruth.h:65
s_Truths6Neg
static word s_Truths6Neg[6]
Definition: utilTruth.h:47
Abc_Tt6Flip
static word Abc_Tt6Flip(word Truth, int iVar)
Definition: utilTruth.h:1126
Abc_Tt8Cnf
static int Abc_Tt8Cnf(word t[4], int nVars, int *pCover)
Definition: utilTruth.h:1974
Abc_Tt7IsopCover
static void Abc_Tt7IsopCover(word uOn[2], word uOnDc[2], int nVars, word uRes[2], int *pCover, int *pnCubes)
Definition: utilTruth.h:1879
Abc_TtCofactor0
static void Abc_TtCofactor0(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:425
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Abc_Tt6SupportAndSize
static int Abc_Tt6SupportAndSize(word t, int nVars, int *pSuppSize)
Definition: utilTruth.h:1003
Abc_Tt6NegVar
static int Abc_Tt6NegVar(word t, int iVar)
Definition: utilTruth.h:1613
Abc_TtProcessBiDecTest
static void Abc_TtProcessBiDecTest(word *pTruth, int nVars, int nSuppLim)
Definition: utilTruth.h:2480
Abc_TtFlip
static void Abc_TtFlip(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:1130
Abc_Tt6Mask
static word Abc_Tt6Mask(int nBits)
Definition: utilTruth.h:184
Abc_TtPrintHex
static void Abc_TtPrintHex(word *pTruth, int nVars)
Definition: utilTruth.h:779
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
Abc_Tt6CofsOpposite
static int Abc_Tt6CofsOpposite(word t, int iVar)
Definition: utilTruth.h:542
Abc_TtShrink
static void Abc_TtShrink(word *pF, int nVars, int nVarsAll, unsigned Phase)
Definition: utilTruth.h:1301
Abc_TtPosVar
static int Abc_TtPosVar(word *t, int nVars, int iVar)
Definition: utilTruth.h:1617
Abc_TtExpand
static void Abc_TtExpand(word *pTruth0, int nVars, int *pCut0, int nCutSize0, int *pCut, int nCutSize)
Definition: utilTruth.h:1360
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Abc_TtSetHex
static void Abc_TtSetHex(word *p, int k, int d)
Definition: utilTruth.h:155
Abc_Tt6Cnf
static int Abc_Tt6Cnf(word t, int nVars, int *pCover)
Definition: utilTruth.h:1962
Abc_TtComputeGraph
static void Abc_TtComputeGraph(word *pTruth, int v, int nVars, int *pGraph)
Definition: utilTruth.h:2284
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
Abc_TtCheckDsdMux
static int Abc_TtCheckDsdMux(word t, int i, word *pOut)
Definition: utilTruth.h:2122
Abc_TtCheckCondDep
static int Abc_TtCheckCondDep(word *pTruth, int nVars, int nSuppLim)
Definition: utilTruth.h:1055
Abc_TtMux
static void Abc_TtMux(word *pOut, word *pCtrl, word *pIn1, word *pIn0, int nWords)
Definition: utilTruth.h:263
Abc_Base2Log
static int Abc_Base2Log(unsigned n)
Definition: abc_global.h:251
Abc_TtIsHexDigit
static int Abc_TtIsHexDigit(char HexChar)
Definition: utilTruth.h:738
Abc_TtCofactor1
static void Abc_TtCofactor1(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:444
Abc_TtCompare
static int Abc_TtCompare(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:277
s_TruthXors
static word s_TruthXors[6]
Definition: utilTruth.h:56
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
Abc_TtConst0
static void Abc_TtConst0(word *pIn1, int nWords)
Definition: utilTruth.h:309
Abc_TtCofsOpposite
static int Abc_TtCofsOpposite(word *t, int nWords, int iVar)
Definition: utilTruth.h:645
Abc_TtElemInit2
static void Abc_TtElemInit2(word *pTtElems, int nVars)
Definition: utilTruth.h:344
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Minisat::Var
int Var
Definition: SolverTypes.h:42
Abc_TtSupportSize
static int Abc_TtSupportSize(word *t, int nVars)
Definition: utilTruth.h:986
Abc_TtNegVar
static int Abc_TtNegVar(word *t, int nVars, int iVar)
Definition: utilTruth.h:1642
Abc_Tt6SwapVars
static word Abc_Tt6SwapVars(word t, int iVar, int jVar)
Definition: utilTruth.h:1221
Abc_TtSuppOnlyOne
static int Abc_TtSuppOnlyOne(int Supp)
Definition: utilTruth.h:938
Abc_TtPrintVarSet
static void Abc_TtPrintVarSet(int Mask, int nVars)
Definition: utilTruth.h:2319
Abc_Tt6Cof0EqualCof0
static int Abc_Tt6Cof0EqualCof0(word t1, word t2, int iVar)
Definition: utilTruth.h:544
Abc_Tt8IsopCover
static void Abc_Tt8IsopCover(word uOn[4], word uOnDc[4], int nVars, word uRes[4], int *pCover, int *pnCubes)
Definition: utilTruth.h:1906
Abc_TtIsUnate
static int Abc_TtIsUnate(word *t, int nVars)
Definition: utilTruth.h:1667
Abc_TtProcessBiDecExperiment
static void Abc_TtProcessBiDecExperiment()
Definition: utilTruth.h:2518
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtCof1IsConst0
static int Abc_TtCof1IsConst0(word *t, int nWords, int iVar)
Definition: utilTruth.h:603
Abc_TtFindLastBit
static int Abc_TtFindLastBit(word *pIn, int nVars)
Definition: utilTruth.h:1532
Abc_TtPrintHexSpecial
static void Abc_TtPrintHexSpecial(word *pTruth, int nVars)
Definition: utilTruth.h:799
Abc_Tt6Cof0EqualCof1
static int Abc_Tt6Cof0EqualCof1(word t1, word t2, int iVar)
Definition: utilTruth.h:543
Abc_TtSwapVars
static void Abc_TtSwapVars(word *pTruth, int nVars, int iVar, int jVar)
Definition: utilTruth.h:1228
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
s_Truths6
static ABC_NAMESPACE_HEADER_START word s_Truths6[6]
INCLUDES ///.
Definition: utilTruth.h:38
Abc_Tt6Cof1EqualCof1
static int Abc_Tt6Cof1EqualCof1(word t1, word t2, int iVar)
Definition: utilTruth.h:545
Abc_TtXor
static void Abc_TtXor(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:253
Abc_TtElemInit
static void Abc_TtElemInit(word **pTtElems, int nVars)
Definition: utilTruth.h:333
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
Abc_TtReverseBits
static void Abc_TtReverseBits(word *pTruth, int nVars)
Definition: utilTruth.h:1567
Abc_TtSwapAdjacent
static void Abc_TtSwapAdjacent(word *pTruth, int nWords, int iVar)
Definition: utilTruth.h:1190
Abc_TtMoveVar
static void Abc_TtMoveVar(word *pF, int nVars, int *V2P, int *P2V, int v, int p)
Definition: utilTruth.h:1277
Abc_TtTruthIsConst1
static int Abc_TtTruthIsConst1(word *p, int nWords)
Definition: utilTruth.h:559
Abc_TtPrintDigitLower
static char Abc_TtPrintDigitLower(int Digit)
Definition: utilTruth.h:749
Abc_TtCompareRev
static int Abc_TtCompareRev(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:285
Abc_Tt6Esop
static int Abc_Tt6Esop(word t, int nVars, int *pCover)
Definition: utilTruth.h:2000