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 s_PPMasks[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 };
Abc_TtBitCount16(int i)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:
Abc_TtGetBit(word * p,int i)149 static inline int     Abc_TtGetBit( word * p, int i )         { return (int)(p[i>>6] >> (word)(i & 63)) & 1;        }
Abc_TtSetBit(word * p,int i)150 static inline void    Abc_TtSetBit( word * p, int i )         { p[i>>6] |= (word)(((word)1)<<(i & 63));             }
Abc_TtXorBit(word * p,int i)151 static inline void    Abc_TtXorBit( word * p, int i )         { p[i>>6] ^= (word)(((word)1)<<(i & 63));             }
152 
153 // read/write k-th digit d of a quaternary number:
Abc_TtGetQua(word * p,int k)154 static inline int     Abc_TtGetQua( word * p, int k )         { return (int)(p[k>>5] >> (word)((k<<1) & 63)) & 3;   }
Abc_TtSetQua(word * p,int k,int d)155 static inline void    Abc_TtSetQua( word * p, int k, int d )  { p[k>>5] |= (word)(((word)d)<<((k<<1) & 63));        }
Abc_TtXorQua(word * p,int k,int d)156 static inline void    Abc_TtXorQua( word * p, int k, int d )  { p[k>>5] ^= (word)(((word)d)<<((k<<1) & 63));        }
157 
158 // read/write k-th digit d of a hexadecimal number:
Abc_TtGetHex(word * p,int k)159 static inline int     Abc_TtGetHex( word * p, int k )         { return (int)(p[k>>4] >> (word)((k<<2) & 63)) & 15;  }
Abc_TtSetHex(word * p,int k,int d)160 static inline void    Abc_TtSetHex( word * p, int k, int d )  { p[k>>4] |= (word)(((word)d)<<((k<<2) & 63));        }
Abc_TtXorHex(word * p,int k,int d)161 static inline void    Abc_TtXorHex( word * p, int k, int d )  { p[k>>4] ^= (word)(((word)d)<<((k<<2) & 63));        }
162 
163 // read/write k-th digit d of a 256-base number:
Abc_TtGet256(word * p,int k)164 static inline int     Abc_TtGet256( word * p, int k )         { return (int)(p[k>>3] >> (word)((k<<3) & 63)) & 255; }
Abc_TtSet256(word * p,int k,int d)165 static inline void    Abc_TtSet256( word * p, int k, int d )  { p[k>>3] |= (word)(((word)d)<<((k<<3) & 63));        }
Abc_TtXor256(word * p,int k,int d)166 static inline void    Abc_TtXor256( word * p, int k, int d )  { p[k>>3] ^= (word)(((word)d)<<((k<<3) & 63));        }
167 
168 /**Function*************************************************************
169 
170   Synopsis    []
171 
172   Description []
173 
174   SideEffects []
175 
176   SeeAlso     []
177 
178 ***********************************************************************/
Abc_TtWordNum(int nVars)179 static inline int  Abc_TtWordNum( int nVars )     { return nVars <= 6 ? 1 : 1 << (nVars-6); }
Abc_TtByteNum(int nVars)180 static inline int  Abc_TtByteNum( int nVars )     { return nVars <= 3 ? 1 : 1 << (nVars-3); }
Abc_TtHexDigitNum(int nVars)181 static inline int  Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 << (nVars-2); }
182 
183 /**Function*************************************************************
184 
185   Synopsis    [Bit mask.]
186 
187   Description []
188 
189   SideEffects []
190 
191   SeeAlso     []
192 
193 ***********************************************************************/
Abc_Tt6Mask(int nBits)194 static inline word Abc_Tt6Mask( int nBits )       { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits);        }
Abc_TtMask(word * pTruth,int nWords,int nBits)195 static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
196 {
197     int w;
198     assert( nBits >= 0 && nBits <= nWords * 64 );
199     for ( w = 0; w < nWords; w++ )
200         if ( nBits >= (w + 1) * 64 )
201             pTruth[w] = ~(word)0;
202         else if ( nBits > w * 64 )
203             pTruth[w] = Abc_Tt6Mask( nBits - w * 64 );
204         else
205             pTruth[w] = 0;
206 }
207 
208 /**Function*************************************************************
209 
210   Synopsis    []
211 
212   Description []
213 
214   SideEffects []
215 
216   SeeAlso     []
217 
218 ***********************************************************************/
Abc_TtConst(word * pOut,int nWords,int fConst1)219 static inline void Abc_TtConst( word * pOut, int nWords, int fConst1 )
220 {
221     int w;
222     for ( w = 0; w < nWords; w++ )
223         pOut[w] = fConst1 ? ~(word)0 : 0;
224 }
Abc_TtClear(word * pOut,int nWords)225 static inline void Abc_TtClear( word * pOut, int nWords )
226 {
227     int w;
228     for ( w = 0; w < nWords; w++ )
229         pOut[w] = 0;
230 }
Abc_TtFill(word * pOut,int nWords)231 static inline void Abc_TtFill( word * pOut, int nWords )
232 {
233     int w;
234     for ( w = 0; w < nWords; w++ )
235         pOut[w] = ~(word)0;
236 }
Abc_TtUnit(word * pOut,int nWords,int fCompl)237 static inline void Abc_TtUnit( word * pOut, int nWords, int fCompl )
238 {
239     int w;
240     for ( w = 0; w < nWords; w++ )
241         pOut[w] = fCompl ? ~s_Truths6[0] : s_Truths6[0];
242 }
Abc_TtNot(word * pOut,int nWords)243 static inline void Abc_TtNot( word * pOut, int nWords )
244 {
245     int w;
246     for ( w = 0; w < nWords; w++ )
247         pOut[w] = ~pOut[w];
248 }
Abc_TtCopy(word * pOut,word * pIn,int nWords,int fCompl)249 static inline void Abc_TtCopy( word * pOut, word * pIn, int nWords, int fCompl )
250 {
251     int w;
252     if ( fCompl )
253         for ( w = 0; w < nWords; w++ )
254             pOut[w] = ~pIn[w];
255     else
256         for ( w = 0; w < nWords; w++ )
257             pOut[w] = pIn[w];
258 }
Abc_TtAnd(word * pOut,word * pIn1,word * pIn2,int nWords,int fCompl)259 static inline void Abc_TtAnd( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
260 {
261     int w;
262     if ( fCompl )
263         for ( w = 0; w < nWords; w++ )
264             pOut[w] = ~(pIn1[w] & pIn2[w]);
265     else
266         for ( w = 0; w < nWords; w++ )
267             pOut[w] = pIn1[w] & pIn2[w];
268 }
Abc_TtAndCompl(word * pOut,word * pIn1,int fCompl1,word * pIn2,int fCompl2,int nWords)269 static inline void Abc_TtAndCompl( word * pOut, word * pIn1, int fCompl1, word * pIn2, int fCompl2, int nWords )
270 {
271     int w;
272     if ( fCompl1 )
273     {
274         if ( fCompl2 )
275             for ( w = 0; w < nWords; w++ )
276                 pOut[w] = ~pIn1[w] & ~pIn2[w];
277         else
278             for ( w = 0; w < nWords; w++ )
279                 pOut[w] = ~pIn1[w] & pIn2[w];
280     }
281     else
282     {
283         if ( fCompl2 )
284             for ( w = 0; w < nWords; w++ )
285                 pOut[w] = pIn1[w] & ~pIn2[w];
286         else
287             for ( w = 0; w < nWords; w++ )
288                 pOut[w] = pIn1[w] & pIn2[w];
289     }
290 }
Abc_TtAndSharp(word * pOut,word * pIn1,word * pIn2,int nWords,int fCompl)291 static inline void Abc_TtAndSharp( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
292 {
293     int w;
294     if ( fCompl )
295         for ( w = 0; w < nWords; w++ )
296             pOut[w] = pIn1[w] & ~pIn2[w];
297     else
298         for ( w = 0; w < nWords; w++ )
299             pOut[w] = pIn1[w] & pIn2[w];
300 }
Abc_TtSharp(word * pOut,word * pIn1,word * pIn2,int nWords)301 static inline void Abc_TtSharp( word * pOut, word * pIn1, word * pIn2, int nWords )
302 {
303     int w;
304     for ( w = 0; w < nWords; w++ )
305         pOut[w] = pIn1[w] & ~pIn2[w];
306 }
Abc_TtOr(word * pOut,word * pIn1,word * pIn2,int nWords)307 static inline void Abc_TtOr( word * pOut, word * pIn1, word * pIn2, int nWords )
308 {
309     int w;
310     for ( w = 0; w < nWords; w++ )
311         pOut[w] = pIn1[w] | pIn2[w];
312 }
Abc_TtOrXor(word * pOut,word * pIn1,word * pIn2,int nWords)313 static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWords )
314 {
315     int w;
316     for ( w = 0; w < nWords; w++ )
317         pOut[w] |= pIn1[w] ^ pIn2[w];
318 }
Abc_TtXor(word * pOut,word * pIn1,word * pIn2,int nWords,int fCompl)319 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
320 {
321     int w;
322     if ( fCompl )
323         for ( w = 0; w < nWords; w++ )
324             pOut[w] = pIn1[w] ^ ~pIn2[w];
325     else
326         for ( w = 0; w < nWords; w++ )
327             pOut[w] = pIn1[w] ^ pIn2[w];
328 }
Abc_TtMux(word * pOut,word * pCtrl,word * pIn1,word * pIn0,int nWords)329 static inline void Abc_TtMux( word * pOut, word * pCtrl, word * pIn1, word * pIn0, int nWords )
330 {
331     int w;
332     for ( w = 0; w < nWords; w++ )
333         pOut[w] = (pCtrl[w] & pIn1[w]) | (~pCtrl[w] & pIn0[w]);
334 }
Abc_TtMaj(word * pOut,word * pIn0,word * pIn1,word * pIn2,int nWords)335 static inline void Abc_TtMaj( word * pOut, word * pIn0, word * pIn1, word * pIn2, int nWords )
336 {
337     int w;
338     for ( w = 0; w < nWords; w++ )
339         pOut[w] = (pIn0[w] & pIn1[w]) | (pIn0[w] & pIn2[w]) | (pIn1[w] & pIn2[w]);
340 }
Abc_TtIntersect(word * pIn1,word * pIn2,int nWords,int fCompl)341 static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCompl )
342 {
343     int w;
344     if ( fCompl )
345     {
346         for ( w = 0; w < nWords; w++ )
347             if ( ~pIn1[w] & pIn2[w] )
348                 return 1;
349     }
350     else
351     {
352         for ( w = 0; w < nWords; w++ )
353             if ( pIn1[w] & pIn2[w] )
354                 return 1;
355     }
356     return 0;
357 }
Abc_TtEqual(word * pIn1,word * pIn2,int nWords)358 static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
359 {
360     int w;
361     for ( w = 0; w < nWords; w++ )
362         if ( pIn1[w] != pIn2[w] )
363             return 0;
364     return 1;
365 }
Abc_TtOpposite(word * pIn1,word * pIn2,int nWords)366 static inline int Abc_TtOpposite( word * pIn1, word * pIn2, int nWords )
367 {
368     int w;
369     for ( w = 0; w < nWords; w++ )
370         if ( pIn1[w] != ~pIn2[w] )
371             return 0;
372     return 1;
373 }
Abc_TtImply(word * pIn1,word * pIn2,int nWords)374 static inline int Abc_TtImply( word * pIn1, word * pIn2, int nWords )
375 {
376     int w;
377     for ( w = 0; w < nWords; w++ )
378         if ( (pIn1[w] & pIn2[w]) != pIn1[w] )
379             return 0;
380     return 1;
381 }
Abc_TtCompare(word * pIn1,word * pIn2,int nWords)382 static inline int Abc_TtCompare( word * pIn1, word * pIn2, int nWords )
383 {
384     int w;
385     for ( w = 0; w < nWords; w++ )
386         if ( pIn1[w] != pIn2[w] )
387             return (pIn1[w] < pIn2[w]) ? -1 : 1;
388     return 0;
389 }
Abc_TtCompareRev(word * pIn1,word * pIn2,int nWords)390 static inline int Abc_TtCompareRev( word * pIn1, word * pIn2, int nWords )
391 {
392     int w;
393     for ( w = nWords - 1; w >= 0; w-- )
394         if ( pIn1[w] != pIn2[w] )
395             return (pIn1[w] < pIn2[w]) ? -1 : 1;
396     return 0;
397 }
Abc_TtIsConst0(word * pIn1,int nWords)398 static inline int Abc_TtIsConst0( word * pIn1, int nWords )
399 {
400     int w;
401     for ( w = 0; w < nWords; w++ )
402         if ( pIn1[w] )
403             return 0;
404     return 1;
405 }
Abc_TtIsConst1(word * pIn1,int nWords)406 static inline int Abc_TtIsConst1( word * pIn1, int nWords )
407 {
408     int w;
409     for ( w = 0; w < nWords; w++ )
410         if ( ~pIn1[w] )
411             return 0;
412     return 1;
413 }
Abc_TtConst0(word * pIn1,int nWords)414 static inline void Abc_TtConst0( word * pIn1, int nWords )
415 {
416     int w;
417     for ( w = 0; w < nWords; w++ )
418         pIn1[w] = 0;
419 }
Abc_TtConst1(word * pIn1,int nWords)420 static inline void Abc_TtConst1( word * pIn1, int nWords )
421 {
422     int w;
423     for ( w = 0; w < nWords; w++ )
424         pIn1[w] = ~(word)0;
425 }
Abc_TtIthVar(word * pOut,int iVar,int nVars)426 static inline void Abc_TtIthVar( word * pOut, int iVar, int nVars )
427 {
428     int k, nWords = Abc_TtWordNum( nVars );
429     if ( iVar < 6 )
430     {
431         for ( k = 0; k < nWords; k++ )
432             pOut[k] = s_Truths6[iVar];
433     }
434     else
435     {
436         for ( k = 0; k < nWords; k++ )
437             if ( k & (1 << (iVar-6)) )
438                 pOut[k] = ~(word)0;
439             else
440                 pOut[k] = 0;
441     }
442 }
443 
444 /**Function*************************************************************
445 
446   Synopsis    []
447 
448   Description []
449 
450   SideEffects []
451 
452   SeeAlso     []
453 
454 ***********************************************************************/
Abc_TtIsAndCompl(word * pOut,int fCompl,word * pIn1,int fCompl1,word * pIn2,int fCompl2,word * pCare,int nWords)455 static inline int Abc_TtIsAndCompl( word * pOut, int fCompl, word * pIn1, int fCompl1, word * pIn2, int fCompl2, word * pCare, int nWords )
456 {
457     int w;
458     if ( fCompl )
459     {
460         if ( fCompl1 )
461         {
462             if ( fCompl2 )
463             {
464                 for ( w = 0; w < nWords; w++ )
465                     if ( (~pOut[w] & pCare[w]) != (~pIn1[w] & ~pIn2[w] & pCare[w]) )
466                         return 0;
467             }
468             else
469             {
470                 for ( w = 0; w < nWords; w++ )
471                     if ( (~pOut[w] & pCare[w]) != (~pIn1[w] & pIn2[w] & pCare[w]) )
472                         return 0;
473             }
474         }
475         else
476         {
477             if ( fCompl2 )
478             {
479                 for ( w = 0; w < nWords; w++ )
480                     if ( (~pOut[w] & pCare[w]) != (pIn1[w] & ~pIn2[w] & pCare[w]) )
481                         return 0;
482             }
483             else
484             {
485                 for ( w = 0; w < nWords; w++ )
486                     if ( (~pOut[w] & pCare[w]) != (pIn1[w] & pIn2[w] & pCare[w]) )
487                         return 0;
488             }
489         }
490     }
491     else
492     {
493         if ( fCompl1 )
494         {
495             if ( fCompl2 )
496             {
497                 for ( w = 0; w < nWords; w++ )
498                     if ( (pOut[w] & pCare[w]) != (~pIn1[w] & ~pIn2[w] & pCare[w]) )
499                         return 0;
500             }
501             else
502             {
503                 for ( w = 0; w < nWords; w++ )
504                     if ( (pOut[w] & pCare[w]) != (~pIn1[w] & pIn2[w] & pCare[w]) )
505                         return 0;
506             }
507         }
508         else
509         {
510             if ( fCompl2 )
511             {
512                 for ( w = 0; w < nWords; w++ )
513                     if ( (pOut[w] & pCare[w]) != (pIn1[w] & ~pIn2[w] & pCare[w]) )
514                         return 0;
515             }
516             else
517             {
518                 for ( w = 0; w < nWords; w++ )
519                     if ( (pOut[w] & pCare[w]) != (pIn1[w] & pIn2[w] & pCare[w]) )
520                         return 0;
521             }
522         }
523     }
524     return 1;
525 }
526 
Abc_TtIsXorCompl(word * pOut,int fCompl,word * pIn1,word * pIn2,word * pCare,int nWords)527 static inline int Abc_TtIsXorCompl( word * pOut, int fCompl, word * pIn1, word * pIn2, word * pCare, int nWords )
528 {
529     int w;
530     if ( fCompl )
531     {
532         for ( w = 0; w < nWords; w++ )
533             if ( (~pOut[w] & pCare[w]) != ((pIn1[w] ^ pIn2[w]) & pCare[w]) )
534                 return 0;
535     }
536     else
537     {
538         for ( w = 0; w < nWords; w++ )
539             if ( ( pOut[w] & pCare[w]) != ((pIn1[w] ^ pIn2[w]) & pCare[w]) )
540                 return 0;
541     }
542     return 1;
543 }
544 
545 
546 /**Function*************************************************************
547 
548   Synopsis    [Compares Cof0 and Cof1.]
549 
550   Description []
551 
552   SideEffects []
553 
554   SeeAlso     []
555 
556 ***********************************************************************/
Abc_TtCompare1VarCofs(word * pTruth,int nWords,int iVar)557 static inline int Abc_TtCompare1VarCofs( word * pTruth, int nWords, int iVar )
558 {
559     if ( nWords == 1 )
560     {
561         word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
562         word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
563         if ( Cof0 != Cof1 )
564             return Cof0 < Cof1 ? -1 : 1;
565         return 0;
566     }
567     if ( iVar <= 5 )
568     {
569         word Cof0, Cof1;
570         int w, shift = (1 << iVar);
571         for ( w = 0; w < nWords; w++ )
572         {
573             Cof0 = pTruth[w] & s_Truths6Neg[iVar];
574             Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
575             if ( Cof0 != Cof1 )
576                 return Cof0 < Cof1 ? -1 : 1;
577         }
578         return 0;
579     }
580     // if ( iVar > 5 )
581     {
582         word * pLimit = pTruth + nWords;
583         int i, iStep = Abc_TtWordNum(iVar);
584         assert( nWords >= 2 );
585         for ( ; pTruth < pLimit; pTruth += 2*iStep )
586             for ( i = 0; i < iStep; i++ )
587                 if ( pTruth[i] != pTruth[i + iStep] )
588                     return pTruth[i] < pTruth[i + iStep] ? -1 : 1;
589         return 0;
590     }
591 }
Abc_TtCompare1VarCofsRev(word * pTruth,int nWords,int iVar)592 static inline int Abc_TtCompare1VarCofsRev( word * pTruth, int nWords, int iVar )
593 {
594     if ( nWords == 1 )
595     {
596         word Cof0 = pTruth[0] & s_Truths6Neg[iVar];
597         word Cof1 = (pTruth[0] >> (1 << iVar)) & s_Truths6Neg[iVar];
598         if ( Cof0 != Cof1 )
599             return Cof0 < Cof1 ? -1 : 1;
600         return 0;
601     }
602     if ( iVar <= 5 )
603     {
604         word Cof0, Cof1;
605         int w, shift = (1 << iVar);
606         for ( w = nWords - 1; w >= 0; w-- )
607         {
608             Cof0 = pTruth[w] & s_Truths6Neg[iVar];
609             Cof1 = (pTruth[w] >> shift) & s_Truths6Neg[iVar];
610             if ( Cof0 != Cof1 )
611                 return Cof0 < Cof1 ? -1 : 1;
612         }
613         return 0;
614     }
615     // if ( iVar > 5 )
616     {
617         word * pLimit = pTruth + nWords;
618         int i, iStep = Abc_TtWordNum(iVar);
619         assert( nWords >= 2 );
620         for ( pLimit -= 2*iStep; pLimit >= pTruth; pLimit -= 2*iStep )
621             for ( i = iStep - 1; i >= 0; i-- )
622                 if ( pLimit[i] != pLimit[i + iStep] )
623                     return pLimit[i] < pLimit[i + iStep] ? -1 : 1;
624         return 0;
625     }
626 }
627 
628 /**Function*************************************************************
629 
630   Synopsis    [Compute elementary truth tables.]
631 
632   Description []
633 
634   SideEffects []
635 
636   SeeAlso     []
637 
638 ***********************************************************************/
Abc_TtElemInit(word ** pTtElems,int nVars)639 static inline void Abc_TtElemInit( word ** pTtElems, int nVars )
640 {
641     int i, k, nWords = Abc_TtWordNum( nVars );
642     for ( i = 0; i < nVars; i++ )
643         if ( i < 6 )
644             for ( k = 0; k < nWords; k++ )
645                 pTtElems[i][k] = s_Truths6[i];
646         else
647             for ( k = 0; k < nWords; k++ )
648                 pTtElems[i][k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
649 }
Abc_TtElemInit2(word * pTtElems,int nVars)650 static inline void Abc_TtElemInit2( word * pTtElems, int nVars )
651 {
652     int i, k, nWords = Abc_TtWordNum( nVars );
653     for ( i = 0; i < nVars; i++ )
654     {
655         word * pTruth = pTtElems + i * nWords;
656         if ( i < 6 )
657             for ( k = 0; k < nWords; k++ )
658                 pTruth[k] = s_Truths6[i];
659         else
660             for ( k = 0; k < nWords; k++ )
661                 pTruth[k] = (k & (1 << (i-6))) ? ~(word)0 : 0;
662     }
663 }
664 
665 /**Function*************************************************************
666 
667   Synopsis    []
668 
669   Description []
670 
671   SideEffects []
672 
673   SeeAlso     []
674 
675 ***********************************************************************/
Abc_Tt6Cofactor0(word t,int iVar)676 static inline word Abc_Tt6Cofactor0( word t, int iVar )
677 {
678     assert( iVar >= 0 && iVar < 6 );
679     return (t &s_Truths6Neg[iVar]) | ((t &s_Truths6Neg[iVar]) << (1<<iVar));
680 }
Abc_Tt6Cofactor1(word t,int iVar)681 static inline word Abc_Tt6Cofactor1( word t, int iVar )
682 {
683     assert( iVar >= 0 && iVar < 6 );
684     return (t & s_Truths6[iVar]) | ((t & s_Truths6[iVar]) >> (1<<iVar));
685 }
686 
Abc_TtCofactor0p(word * pOut,word * pIn,int nWords,int iVar)687 static inline void Abc_TtCofactor0p( word * pOut, word * pIn, int nWords, int iVar )
688 {
689     if ( nWords == 1 )
690         pOut[0] = ((pIn[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pIn[0] & s_Truths6Neg[iVar]);
691     else if ( iVar <= 5 )
692     {
693         int w, shift = (1 << iVar);
694         for ( w = 0; w < nWords; w++ )
695             pOut[w] = ((pIn[w] & s_Truths6Neg[iVar]) << shift) | (pIn[w] & s_Truths6Neg[iVar]);
696     }
697     else // if ( iVar > 5 )
698     {
699         word * pLimit = pIn + nWords;
700         int i, iStep = Abc_TtWordNum(iVar);
701         for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
702             for ( i = 0; i < iStep; i++ )
703             {
704                 pOut[i]         = pIn[i];
705                 pOut[i + iStep] = pIn[i];
706             }
707     }
708 }
Abc_TtCofactor1p(word * pOut,word * pIn,int nWords,int iVar)709 static inline void Abc_TtCofactor1p( word * pOut, word * pIn, int nWords, int iVar )
710 {
711     if ( nWords == 1 )
712         pOut[0] = (pIn[0] & s_Truths6[iVar]) | ((pIn[0] & s_Truths6[iVar]) >> (1 << iVar));
713     else if ( iVar <= 5 )
714     {
715         int w, shift = (1 << iVar);
716         for ( w = 0; w < nWords; w++ )
717             pOut[w] = (pIn[w] & s_Truths6[iVar]) | ((pIn[w] & s_Truths6[iVar]) >> shift);
718     }
719     else // if ( iVar > 5 )
720     {
721         word * pLimit = pIn + nWords;
722         int i, iStep = Abc_TtWordNum(iVar);
723         for ( ; pIn < pLimit; pIn += 2*iStep, pOut += 2*iStep )
724             for ( i = 0; i < iStep; i++ )
725             {
726                 pOut[i]         = pIn[i + iStep];
727                 pOut[i + iStep] = pIn[i + iStep];
728             }
729     }
730 }
Abc_TtCofactor0(word * pTruth,int nWords,int iVar)731 static inline void Abc_TtCofactor0( word * pTruth, int nWords, int iVar )
732 {
733     if ( nWords == 1 )
734         pTruth[0] = ((pTruth[0] & s_Truths6Neg[iVar]) << (1 << iVar)) | (pTruth[0] & s_Truths6Neg[iVar]);
735     else if ( iVar <= 5 )
736     {
737         int w, shift = (1 << iVar);
738         for ( w = 0; w < nWords; w++ )
739             pTruth[w] = ((pTruth[w] & s_Truths6Neg[iVar]) << shift) | (pTruth[w] & s_Truths6Neg[iVar]);
740     }
741     else // if ( iVar > 5 )
742     {
743         word * pLimit = pTruth + nWords;
744         int i, iStep = Abc_TtWordNum(iVar);
745         for ( ; pTruth < pLimit; pTruth += 2*iStep )
746             for ( i = 0; i < iStep; i++ )
747                 pTruth[i + iStep] = pTruth[i];
748     }
749 }
Abc_TtCofactor1(word * pTruth,int nWords,int iVar)750 static inline void Abc_TtCofactor1( word * pTruth, int nWords, int iVar )
751 {
752     if ( nWords == 1 )
753         pTruth[0] = (pTruth[0] & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
754     else if ( iVar <= 5 )
755     {
756         int w, shift = (1 << iVar);
757         for ( w = 0; w < nWords; w++ )
758             pTruth[w] = (pTruth[w] & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
759     }
760     else // if ( iVar > 5 )
761     {
762         word * pLimit = pTruth + nWords;
763         int i, iStep = Abc_TtWordNum(iVar);
764         for ( ; pTruth < pLimit; pTruth += 2*iStep )
765             for ( i = 0; i < iStep; i++ )
766                 pTruth[i] = pTruth[i + iStep];
767     }
768 }
769 
770 /**Function*************************************************************
771 
772   Synopsis    [Checks pairs of cofactors w.r.t. two variables.]
773 
774   Description []
775 
776   SideEffects []
777 
778   SeeAlso     []
779 
780 ***********************************************************************/
Abc_TtCheckEqualCofs(word * pTruth,int nWords,int iVar,int jVar,int Num1,int Num2)781 static inline int Abc_TtCheckEqualCofs( word * pTruth, int nWords, int iVar, int jVar, int Num1, int Num2 )
782 {
783     assert( Num1 < Num2 && Num2 < 4 );
784     assert( iVar < jVar );
785     if ( nWords == 1 )
786     {
787         word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
788         int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
789         int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
790         return ((pTruth[0] >> shift1) & Mask) == ((pTruth[0] >> shift2) & Mask);
791     }
792     if ( jVar <= 5 )
793     {
794         word Mask = s_Truths6Neg[jVar] & s_Truths6Neg[iVar];
795         int shift1 = (Num1 >> 1) * (1 << jVar) + (Num1 & 1) * (1 << iVar);
796         int shift2 = (Num2 >> 1) * (1 << jVar) + (Num2 & 1) * (1 << iVar);
797         int w;
798         for ( w = 0; w < nWords; w++ )
799             if ( ((pTruth[w] >> shift1) & Mask) != ((pTruth[w] >> shift2) & Mask) )
800                 return 0;
801         return 1;
802     }
803     if ( iVar <= 5 && jVar > 5 )
804     {
805         word * pLimit = pTruth + nWords;
806         int j, jStep = Abc_TtWordNum(jVar);
807         int shift1 = (Num1 & 1) * (1 << iVar);
808         int shift2 = (Num2 & 1) * (1 << iVar);
809         int Offset1 = (Num1 >> 1) * jStep;
810         int Offset2 = (Num2 >> 1) * jStep;
811         for ( ; pTruth < pLimit; pTruth += 2*jStep )
812             for ( j = 0; j < jStep; j++ )
813                 if ( ((pTruth[j + Offset1] >> shift1) & s_Truths6Neg[iVar]) != ((pTruth[j + Offset2] >> shift2) & s_Truths6Neg[iVar]) )
814                     return 0;
815         return 1;
816     }
817     {
818         word * pLimit = pTruth + nWords;
819         int j, jStep = Abc_TtWordNum(jVar);
820         int i, iStep = Abc_TtWordNum(iVar);
821         int Offset1 = (Num1 >> 1) * jStep + (Num1 & 1) * iStep;
822         int Offset2 = (Num2 >> 1) * jStep + (Num2 & 1) * iStep;
823         for ( ; pTruth < pLimit; pTruth += 2*jStep )
824             for ( i = 0; i < jStep; i += 2*iStep )
825                 for ( j = 0; j < iStep; j++ )
826                     if ( pTruth[Offset1 + i + j] != pTruth[Offset2 + i + j] )
827                         return 0;
828         return 1;
829     }
830 }
831 
832 
833 /**Function*************************************************************
834 
835   Synopsis    []
836 
837   Description []
838 
839   SideEffects []
840 
841   SeeAlso     []
842 
843 ***********************************************************************/
Abc_Tt6Cof0IsConst0(word t,int iVar)844 static inline int Abc_Tt6Cof0IsConst0( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == 0;                                          }
Abc_Tt6Cof0IsConst1(word t,int iVar)845 static inline int Abc_Tt6Cof0IsConst1( word t, int iVar ) { return (t & s_Truths6Neg[iVar]) == s_Truths6Neg[iVar];                         }
Abc_Tt6Cof1IsConst0(word t,int iVar)846 static inline int Abc_Tt6Cof1IsConst0( word t, int iVar ) { return (t & s_Truths6[iVar]) == 0;                                             }
Abc_Tt6Cof1IsConst1(word t,int iVar)847 static inline int Abc_Tt6Cof1IsConst1( word t, int iVar ) { return (t & s_Truths6[iVar]) == s_Truths6[iVar];                               }
Abc_Tt6CofsOpposite(word t,int iVar)848 static inline int Abc_Tt6CofsOpposite( word t, int iVar ) { return (~t & s_Truths6Neg[iVar]) == ((t >> (1 << iVar)) & s_Truths6Neg[iVar]); }
Abc_Tt6Cof0EqualCof1(word t1,word t2,int iVar)849 static inline int Abc_Tt6Cof0EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == ((t2 >> (1 << iVar)) & s_Truths6Neg[iVar]); }
Abc_Tt6Cof0EqualCof0(word t1,word t2,int iVar)850 static inline int Abc_Tt6Cof0EqualCof0( word t1, word t2, int iVar ) { return (t1 & s_Truths6Neg[iVar]) == (t2 & s_Truths6Neg[iVar]); }
Abc_Tt6Cof1EqualCof1(word t1,word t2,int iVar)851 static inline int Abc_Tt6Cof1EqualCof1( word t1, word t2, int iVar ) { return (t1 & s_Truths6[iVar])    == (t2 & s_Truths6[iVar]); }
852 
853 /**Function*************************************************************
854 
855   Synopsis    []
856 
857   Description []
858 
859   SideEffects []
860 
861   SeeAlso     []
862 
863 ***********************************************************************/
Abc_TtTruthIsConst0(word * p,int nWords)864 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; }
Abc_TtTruthIsConst1(word * p,int nWords)865 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; }
866 
Abc_TtCof0IsConst0(word * t,int nWords,int iVar)867 static inline int Abc_TtCof0IsConst0( word * t, int nWords, int iVar )
868 {
869     if ( iVar < 6 )
870     {
871         int i;
872         for ( i = 0; i < nWords; i++ )
873             if ( t[i] & s_Truths6Neg[iVar] )
874                 return 0;
875         return 1;
876     }
877     else
878     {
879         int i, Step = (1 << (iVar - 6));
880         word * tLimit = t + nWords;
881         for ( ; t < tLimit; t += 2*Step )
882             for ( i = 0; i < Step; i++ )
883                 if ( t[i] )
884                     return 0;
885         return 1;
886     }
887 }
Abc_TtCof0IsConst1(word * t,int nWords,int iVar)888 static inline int Abc_TtCof0IsConst1( word * t, int nWords, int iVar )
889 {
890     if ( iVar < 6 )
891     {
892         int i;
893         for ( i = 0; i < nWords; i++ )
894             if ( (t[i] & s_Truths6Neg[iVar]) != s_Truths6Neg[iVar] )
895                 return 0;
896         return 1;
897     }
898     else
899     {
900         int i, Step = (1 << (iVar - 6));
901         word * tLimit = t + nWords;
902         for ( ; t < tLimit; t += 2*Step )
903             for ( i = 0; i < Step; i++ )
904                 if ( ~t[i] )
905                     return 0;
906         return 1;
907     }
908 }
Abc_TtCof1IsConst0(word * t,int nWords,int iVar)909 static inline int Abc_TtCof1IsConst0( word * t, int nWords, int iVar )
910 {
911     if ( iVar < 6 )
912     {
913         int i;
914         for ( i = 0; i < nWords; i++ )
915             if ( t[i] & s_Truths6[iVar] )
916                 return 0;
917         return 1;
918     }
919     else
920     {
921         int i, Step = (1 << (iVar - 6));
922         word * tLimit = t + nWords;
923         for ( ; t < tLimit; t += 2*Step )
924             for ( i = 0; i < Step; i++ )
925                 if ( t[i+Step] )
926                     return 0;
927         return 1;
928     }
929 }
Abc_TtCof1IsConst1(word * t,int nWords,int iVar)930 static inline int Abc_TtCof1IsConst1( word * t, int nWords, int iVar )
931 {
932     if ( iVar < 6 )
933     {
934         int i;
935         for ( i = 0; i < nWords; i++ )
936             if ( (t[i] & s_Truths6[iVar]) != s_Truths6[iVar] )
937                 return 0;
938         return 1;
939     }
940     else
941     {
942         int i, Step = (1 << (iVar - 6));
943         word * tLimit = t + nWords;
944         for ( ; t < tLimit; t += 2*Step )
945             for ( i = 0; i < Step; i++ )
946                 if ( ~t[i+Step] )
947                     return 0;
948         return 1;
949     }
950 }
Abc_TtCofsOpposite(word * t,int nWords,int iVar)951 static inline int Abc_TtCofsOpposite( word * t, int nWords, int iVar )
952 {
953     if ( iVar < 6 )
954     {
955         int i, Shift = (1 << iVar);
956         for ( i = 0; i < nWords; i++ )
957             if ( ((t[i] << Shift) & s_Truths6[iVar]) != (~t[i] & s_Truths6[iVar]) )
958                 return 0;
959         return 1;
960     }
961     else
962     {
963         int i, Step = (1 << (iVar - 6));
964         word * tLimit = t + nWords;
965         for ( ; t < tLimit; t += 2*Step )
966             for ( i = 0; i < Step; i++ )
967                 if ( t[i] != ~t[i+Step] )
968                     return 0;
969         return 1;
970     }
971 }
972 
973 /**Function*************************************************************
974 
975   Synopsis    [Stretch truthtable to have more input variables.]
976 
977   Description []
978 
979   SideEffects []
980 
981   SeeAlso     []
982 
983 ***********************************************************************/
Abc_TtStretch5(unsigned * pInOut,int nVarS,int nVarB)984 static inline void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
985 {
986     int w, i, step, nWords;
987     if ( nVarS == nVarB )
988         return;
989     assert( nVarS < nVarB );
990     step = Abc_TruthWordNum(nVarS);
991     nWords = Abc_TruthWordNum(nVarB);
992     if ( step == nWords )
993         return;
994     assert( step < nWords );
995     for ( w = 0; w < nWords; w += step )
996         for ( i = 0; i < step; i++ )
997             pInOut[w + i] = pInOut[i];
998 }
Abc_TtStretch6(word * pInOut,int nVarS,int nVarB)999 static inline void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
1000 {
1001     int w, i, step, nWords;
1002     if ( nVarS == nVarB )
1003         return;
1004     assert( nVarS < nVarB );
1005     step = Abc_Truth6WordNum(nVarS);
1006     nWords = Abc_Truth6WordNum(nVarB);
1007     if ( step == nWords )
1008         return;
1009     assert( step < nWords );
1010     for ( w = 0; w < nWords; w += step )
1011         for ( i = 0; i < step; i++ )
1012             pInOut[w + i] = pInOut[i];
1013 }
Abc_Tt6Stretch(word t,int nVars)1014 static inline word Abc_Tt6Stretch( word t, int nVars )
1015 {
1016     assert( nVars >= 0 );
1017     if ( nVars == 0 )
1018         nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
1019     if ( nVars == 1 )
1020         nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
1021     if ( nVars == 2 )
1022         nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
1023     if ( nVars == 3 )
1024         nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
1025     if ( nVars == 4 )
1026         nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
1027     if ( nVars == 5 )
1028         nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
1029     assert( nVars == 6 );
1030     return t;
1031 }
1032 
1033 /**Function*************************************************************
1034 
1035   Synopsis    []
1036 
1037   Description []
1038 
1039   SideEffects []
1040 
1041   SeeAlso     []
1042 
1043 ***********************************************************************/
Abc_TtIsHexDigit(char HexChar)1044 static inline int Abc_TtIsHexDigit( char HexChar )
1045 {
1046     return (HexChar >= '0' && HexChar <= '9') || (HexChar >= 'A' && HexChar <= 'F') || (HexChar >= 'a' && HexChar <= 'f');
1047 }
Abc_TtPrintDigit(int Digit)1048 static inline char Abc_TtPrintDigit( int Digit )
1049 {
1050     assert( Digit >= 0 && Digit < 16 );
1051     if ( Digit < 10 )
1052         return '0' + Digit;
1053     return 'A' + Digit-10;
1054 }
Abc_TtPrintDigitLower(int Digit)1055 static inline char Abc_TtPrintDigitLower( int Digit )
1056 {
1057     assert( Digit >= 0 && Digit < 16 );
1058     if ( Digit < 10 )
1059         return '0' + Digit;
1060     return 'a' + Digit-10;
1061 }
Abc_TtReadHexDigit(char HexChar)1062 static inline int Abc_TtReadHexDigit( char HexChar )
1063 {
1064     if ( HexChar >= '0' && HexChar <= '9' )
1065         return HexChar - '0';
1066     if ( HexChar >= 'A' && HexChar <= 'F' )
1067         return HexChar - 'A' + 10;
1068     if ( HexChar >= 'a' && HexChar <= 'f' )
1069         return HexChar - 'a' + 10;
1070     assert( 0 ); // not a hexadecimal symbol
1071     return -1; // return value which makes no sense
1072 }
1073 
1074 /**Function*************************************************************
1075 
1076   Synopsis    []
1077 
1078   Description []
1079 
1080   SideEffects []
1081 
1082   SeeAlso     []
1083 
1084 ***********************************************************************/
Abc_TtPrintHex(word * pTruth,int nVars)1085 static inline void Abc_TtPrintHex( word * pTruth, int nVars )
1086 {
1087     word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
1088     int k;
1089     assert( nVars >= 2 );
1090     for ( pThis = pTruth; pThis < pLimit; pThis++ )
1091         for ( k = 0; k < 16; k++ )
1092             printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
1093     printf( "\n" );
1094 }
Abc_TtPrintHexRev(FILE * pFile,word * pTruth,int nVars)1095 static inline void Abc_TtPrintHexRev( FILE * pFile, word * pTruth, int nVars )
1096 {
1097     word * pThis;
1098     int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
1099     assert( nVars >= 2 );
1100     for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1101         for ( k = StartK - 1; k >= 0; k-- )
1102             fprintf( pFile, "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
1103 //    printf( "\n" );
1104 }
Abc_TtPrintHexSpecial(word * pTruth,int nVars)1105 static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
1106 {
1107     word * pThis;
1108     int k;
1109     assert( nVars >= 2 );
1110     for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1111         for ( k = 0; k < 16; k++ )
1112             printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
1113     printf( "\n" );
1114 }
Abc_TtWriteHexRev(char * pStr,word * pTruth,int nVars)1115 static inline int Abc_TtWriteHexRev( char * pStr, word * pTruth, int nVars )
1116 {
1117     word * pThis;
1118     char * pStrInit = pStr;
1119     int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
1120     assert( nVars >= 2 );
1121     for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
1122         for ( k = StartK - 1; k >= 0; k-- )
1123             *pStr++ = Abc_TtPrintDigit( (int)(pThis[0] >> (k << 2)) & 15 );
1124     return pStr - pStrInit;
1125 }
Abc_TtPrintHexArrayRev(FILE * pFile,word * pTruth,int nDigits)1126 static inline void Abc_TtPrintHexArrayRev( FILE * pFile, word * pTruth, int nDigits )
1127 {
1128     int k;
1129     for ( k = nDigits - 1; k >= 0; k-- )
1130         fprintf( pFile, "%c", Abc_TtPrintDigitLower( Abc_TtGetHex(pTruth, k) ) );
1131 }
1132 
1133 /**Function*************************************************************
1134 
1135   Synopsis    [Reads hex truth table from a string.]
1136 
1137   Description []
1138 
1139   SideEffects []
1140 
1141   SeeAlso     []
1142 
1143 ***********************************************************************/
Abc_TtReadHex(word * pTruth,char * pString)1144 static inline int Abc_TtReadHex( word * pTruth, char * pString )
1145 {
1146     int k, nVars, Digit, nDigits;
1147     // skip the first 2 symbols if they are "0x"
1148     if ( pString[0] == '0' && pString[1] == 'x' )
1149         pString += 2;
1150     // count the number of hex digits
1151     nDigits = 0;
1152     for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
1153         nDigits++;
1154     if ( nDigits == 1 )
1155     {
1156         if ( pString[0] == '0' || pString[0] == 'F' )
1157         {
1158             pTruth[0] = (pString[0] == '0') ? 0 : ~(word)0;
1159             return 0;
1160         }
1161         if ( pString[0] == '5' || pString[0] == 'A' )
1162         {
1163             pTruth[0] = (pString[0] == '5') ? s_Truths6Neg[0] : s_Truths6[0];
1164             return 1;
1165         }
1166     }
1167     // determine the number of variables
1168     nVars = 2 + (nDigits == 1 ? 0 : Abc_Base2Log(nDigits));
1169     // clean storage
1170     for ( k = Abc_TtWordNum(nVars) - 1; k >= 0; k-- )
1171         pTruth[k] = 0;
1172     // read hexadecimal digits in the reverse order
1173     // (the last symbol in the string is the least significant digit)
1174     for ( k = 0; k < nDigits; k++ )
1175     {
1176         Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
1177         assert( Digit >= 0 && Digit < 16 );
1178         Abc_TtSetHex( pTruth, k, Digit );
1179     }
1180     if ( nVars < 6 )
1181         pTruth[0] = Abc_Tt6Stretch( pTruth[0], nVars );
1182     return nVars;
1183 }
Abc_TtReadHexNumber(word * pTruth,char * pString)1184 static inline int Abc_TtReadHexNumber( word * pTruth, char * pString )
1185 {
1186     // count the number of hex digits
1187     int k, Digit, nDigits = 0;
1188     for ( k = 0; Abc_TtIsHexDigit(pString[k]); k++ )
1189         nDigits++;
1190     // read hexadecimal digits in the reverse order
1191     // (the last symbol in the string is the least significant digit)
1192     for ( k = 0; k < nDigits; k++ )
1193     {
1194         Digit = Abc_TtReadHexDigit( pString[nDigits - 1 - k] );
1195         assert( Digit >= 0 && Digit < 16 );
1196         Abc_TtSetHex( pTruth, k, Digit );
1197     }
1198     return nDigits;
1199 }
1200 
1201 
1202 /**Function*************************************************************
1203 
1204   Synopsis    []
1205 
1206   Description []
1207 
1208   SideEffects []
1209 
1210   SeeAlso     []
1211 
1212 ***********************************************************************/
Abc_TtPrintBinary(word * pTruth,int nVars)1213 static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
1214 {
1215     word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
1216     int k, Limit = Abc_MinInt( 64, (1 << nVars) );
1217     assert( nVars >= 2 );
1218     for ( pThis = pTruth; pThis < pLimit; pThis++ )
1219         for ( k = 0; k < Limit; k++ )
1220             printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
1221     printf( "\n" );
1222 }
1223 
1224 /**Function*************************************************************
1225 
1226   Synopsis    []
1227 
1228   Description []
1229 
1230   SideEffects []
1231 
1232   SeeAlso     []
1233 
1234 ***********************************************************************/
Abc_TtSuppFindFirst(int Supp)1235 static inline int Abc_TtSuppFindFirst( int Supp )
1236 {
1237     int i;
1238     assert( Supp > 0 );
1239     for ( i = 0; i < 32; i++ )
1240         if ( Supp & (1 << i) )
1241             return i;
1242     return -1;
1243 }
Abc_TtSuppOnlyOne(int Supp)1244 static inline int Abc_TtSuppOnlyOne( int Supp )
1245 {
1246     if ( Supp == 0 )
1247         return 0;
1248     return (Supp & (Supp-1)) == 0;
1249 }
Abc_TtSuppIsMinBase(int Supp)1250 static inline int Abc_TtSuppIsMinBase( int Supp )
1251 {
1252     assert( Supp > 0 );
1253     return (Supp & (Supp+1)) == 0;
1254 }
Abc_Tt6HasVar(word t,int iVar)1255 static inline int Abc_Tt6HasVar( word t, int iVar )
1256 {
1257     return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]);
1258 }
Abc_Tt6XorVar(word t,int iVar)1259 static inline int Abc_Tt6XorVar( word t, int iVar )
1260 {
1261     return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) == ~(t & s_Truths6Neg[iVar]);
1262 }
Abc_TtHasVar(word * t,int nVars,int iVar)1263 static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
1264 {
1265     assert( iVar < nVars );
1266     if ( nVars <= 6 )
1267         return Abc_Tt6HasVar( t[0], iVar );
1268     if ( iVar < 6 )
1269     {
1270         int i, Shift = (1 << iVar);
1271         int nWords = Abc_TtWordNum( nVars );
1272         for ( i = 0; i < nWords; i++ )
1273             if ( ((t[i] >> Shift) & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
1274                 return 1;
1275         return 0;
1276     }
1277     else
1278     {
1279         int i, Step = (1 << (iVar - 6));
1280         word * tLimit = t + Abc_TtWordNum( nVars );
1281         for ( ; t < tLimit; t += 2*Step )
1282             for ( i = 0; i < Step; i++ )
1283                 if ( t[i] != t[Step+i] )
1284                     return 1;
1285         return 0;
1286     }
1287 }
Abc_TtSupport(word * t,int nVars)1288 static inline int Abc_TtSupport( word * t, int nVars )
1289 {
1290     int v, Supp = 0;
1291     for ( v = 0; v < nVars; v++ )
1292         if ( Abc_TtHasVar( t, nVars, v ) )
1293             Supp |= (1 << v);
1294     return Supp;
1295 }
Abc_TtSupportSize(word * t,int nVars)1296 static inline int Abc_TtSupportSize( word * t, int nVars )
1297 {
1298     int v, SuppSize = 0;
1299     for ( v = 0; v < nVars; v++ )
1300         if ( Abc_TtHasVar( t, nVars, v ) )
1301             SuppSize++;
1302     return SuppSize;
1303 }
Abc_TtSupportAndSize(word * t,int nVars,int * pSuppSize)1304 static inline int Abc_TtSupportAndSize( word * t, int nVars, int * pSuppSize )
1305 {
1306     int v, Supp = 0;
1307     *pSuppSize = 0;
1308     for ( v = 0; v < nVars; v++ )
1309         if ( Abc_TtHasVar( t, nVars, v ) )
1310             Supp |= (1 << v), (*pSuppSize)++;
1311     return Supp;
1312 }
Abc_Tt6SupportAndSize(word t,int nVars,int * pSuppSize)1313 static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize )
1314 {
1315     int v, Supp = 0;
1316     *pSuppSize = 0;
1317     assert( nVars <= 6 );
1318     for ( v = 0; v < nVars; v++ )
1319         if ( Abc_Tt6HasVar( t, v ) )
1320             Supp |= (1 << v), (*pSuppSize)++;
1321     return Supp;
1322 }
1323 
1324 /**Function*************************************************************
1325 
1326   Synopsis    [Checks if there is a var whose both cofs have supp <= nSuppLim.]
1327 
1328   Description []
1329 
1330   SideEffects []
1331 
1332   SeeAlso     []
1333 
1334 ***********************************************************************/
Abc_TtCheckCondDep2(word * pTruth,int nVars,int nSuppLim)1335 static inline int Abc_TtCheckCondDep2( word * pTruth, int nVars, int nSuppLim )
1336 {
1337     int v, d, nWords = Abc_TtWordNum(nVars);
1338     if ( nVars <= nSuppLim + 1 )
1339         return 0;
1340     for ( v = 0; v < nVars; v++ )
1341     {
1342         int nDep0 = 0, nDep1 = 0;
1343         for ( d = 0; d < nVars; d++ )
1344         {
1345             if ( v == d )
1346                 continue;
1347             if ( v < d )
1348             {
1349                 nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 0, 2 );
1350                 nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 1, 3 );
1351             }
1352             else // if ( v > d )
1353             {
1354                 nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 0, 1 );
1355                 nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 2, 3 );
1356             }
1357             if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
1358                 break;
1359         }
1360         if ( d == nVars )
1361             return v;
1362     }
1363     return nVars;
1364 }
Abc_TtCheckCondDep(word * pTruth,int nVars,int nSuppLim)1365 static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim )
1366 {
1367     int nVarsMax = 13;
1368     word Cof0[128], Cof1[128]; // pow( 2, nVarsMax-6 )
1369     int v, d, nWords = Abc_TtWordNum(nVars);
1370     assert( nVars <= nVarsMax );
1371     if ( nVars <= nSuppLim + 1 )
1372         return 0;
1373     for ( v = 0; v < nVars; v++ )
1374     {
1375         int nDep0 = 0, nDep1 = 0;
1376         Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
1377         Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
1378         for ( d = 0; d < nVars; d++ )
1379         {
1380             if ( v == d )
1381                 continue;
1382             nDep0 += Abc_TtHasVar( Cof0, nVars, d );
1383             nDep1 += Abc_TtHasVar( Cof1, nVars, d );
1384             if ( nDep0 > nSuppLim || nDep1 > nSuppLim )
1385                 break;
1386         }
1387         if ( d == nVars )
1388             return v;
1389     }
1390     return nVars;
1391 }
1392 
1393 
1394 /**Function*************************************************************
1395 
1396   Synopsis    [Detecting elementary functions.]
1397 
1398   Description []
1399 
1400   SideEffects []
1401 
1402   SeeAlso     []
1403 
1404 ***********************************************************************/
Abc_TtOnlyOneOne(word t)1405 static inline int Abc_TtOnlyOneOne( word t )
1406 {
1407     if ( t == 0 )
1408         return 0;
1409     return (t & (t-1)) == 0;
1410 }
Abc_Tt6IsAndType(word t,int nVars)1411 static inline int Abc_Tt6IsAndType( word t, int nVars )
1412 {
1413     return Abc_TtOnlyOneOne( t & Abc_Tt6Mask(1 << nVars) );
1414 }
Abc_Tt6IsOrType(word t,int nVars)1415 static inline int Abc_Tt6IsOrType( word t, int nVars )
1416 {
1417     return Abc_TtOnlyOneOne( ~t & Abc_Tt6Mask(1 << nVars) );
1418 }
Abc_Tt6IsXorType(word t,int nVars)1419 static inline int Abc_Tt6IsXorType( word t, int nVars )
1420 {
1421     return ((((t & 1) ? ~t : t) ^ s_TruthXors[nVars]) & Abc_Tt6Mask(1 << nVars)) == 0;
1422 }
1423 
1424 
1425 /**Function*************************************************************
1426 
1427   Synopsis    []
1428 
1429   Description []
1430 
1431   SideEffects []
1432 
1433   SeeAlso     []
1434 
1435 ***********************************************************************/
Abc_Tt6Flip(word Truth,int iVar)1436 static inline word Abc_Tt6Flip( word Truth, int iVar )
1437 {
1438     return Truth = ((Truth << (1 << iVar)) & s_Truths6[iVar]) | ((Truth & s_Truths6[iVar]) >> (1 << iVar));
1439 }
Abc_TtFlip(word * pTruth,int nWords,int iVar)1440 static inline void Abc_TtFlip( word * pTruth, int nWords, int iVar )
1441 {
1442     if ( nWords == 1 )
1443         pTruth[0] = ((pTruth[0] << (1 << iVar)) & s_Truths6[iVar]) | ((pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
1444     else if ( iVar <= 5 )
1445     {
1446         int w, shift = (1 << iVar);
1447         for ( w = 0; w < nWords; w++ )
1448             pTruth[w] = ((pTruth[w] << shift) & s_Truths6[iVar]) | ((pTruth[w] & s_Truths6[iVar]) >> shift);
1449     }
1450     else // if ( iVar > 5 )
1451     {
1452         word * pLimit = pTruth + nWords;
1453         int i, iStep = Abc_TtWordNum(iVar);
1454         for ( ; pTruth < pLimit; pTruth += 2*iStep )
1455             for ( i = 0; i < iStep; i++ )
1456                 ABC_SWAP( word, pTruth[i], pTruth[i + iStep] );
1457     }
1458 }
1459 
1460 /**Function*************************************************************
1461 
1462   Synopsis    []
1463 
1464   Description []
1465 
1466   SideEffects []
1467 
1468   SeeAlso     []
1469 
1470 ***********************************************************************/
Abc_Tt6Permute_rec(word t,int * pPerm,int nVars)1471 static inline word Abc_Tt6Permute_rec( word t, int * pPerm, int nVars )
1472 {
1473     word uRes0, uRes1; int Var;
1474     if (  t == 0 ) return 0;
1475     if ( ~t == 0 ) return ~(word)0;
1476     for ( Var = nVars-1; Var >= 0; Var-- )
1477         if ( Abc_Tt6HasVar( t, Var ) )
1478              break;
1479     assert( Var >= 0 );
1480     uRes0 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor0(t, Var), pPerm, Var );
1481     uRes1 = Abc_Tt6Permute_rec( Abc_Tt6Cofactor1(t, Var), pPerm, Var );
1482     return (uRes0 & s_Truths6Neg[pPerm[Var]]) | (uRes1 & s_Truths6[pPerm[Var]]);
1483 }
1484 
1485 /**Function*************************************************************
1486 
1487   Synopsis    []
1488 
1489   Description []
1490 
1491   SideEffects []
1492 
1493   SeeAlso     []
1494 
1495 ***********************************************************************/
Abc_Tt6SwapAdjacent(word Truth,int iVar)1496 static inline word Abc_Tt6SwapAdjacent( word Truth, int iVar )
1497 {
1498     return (Truth & s_PMasks[iVar][0]) | ((Truth & s_PMasks[iVar][1]) << (1 << iVar)) | ((Truth & s_PMasks[iVar][2]) >> (1 << iVar));
1499 }
Abc_TtSwapAdjacent(word * pTruth,int nWords,int iVar)1500 static inline void Abc_TtSwapAdjacent( word * pTruth, int nWords, int iVar )
1501 {
1502     if ( iVar < 5 )
1503     {
1504         int i, Shift = (1 << iVar);
1505         for ( i = 0; i < nWords; i++ )
1506             pTruth[i] = (pTruth[i] & s_PMasks[iVar][0]) | ((pTruth[i] & s_PMasks[iVar][1]) << Shift) | ((pTruth[i] & s_PMasks[iVar][2]) >> Shift);
1507     }
1508     else if ( iVar == 5 )
1509     {
1510         unsigned * pTruthU = (unsigned *)pTruth;
1511         unsigned * pLimitU = (unsigned *)(pTruth + nWords);
1512         for ( ; pTruthU < pLimitU; pTruthU += 4 )
1513             ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] );
1514     }
1515     else // if ( iVar > 5 )
1516     {
1517         word * pLimit = pTruth + nWords;
1518         int i, iStep = Abc_TtWordNum(iVar);
1519         for ( ; pTruth < pLimit; pTruth += 4*iStep )
1520             for ( i = 0; i < iStep; i++ )
1521                 ABC_SWAP( word, pTruth[i + iStep], pTruth[i + 2*iStep] );
1522     }
1523 }
Abc_Tt6SwapVars(word t,int iVar,int jVar)1524 static inline word Abc_Tt6SwapVars( word t, int iVar, int jVar )
1525 {
1526     word * s_PMasks = s_PPMasks[iVar][jVar];
1527     int shift = (1 << jVar) - (1 << iVar);
1528     assert( iVar < jVar );
1529     return (t & s_PMasks[0]) | ((t & s_PMasks[1]) << shift) | ((t & s_PMasks[2]) >> shift);
1530 }
Abc_TtSwapVars(word * pTruth,int nVars,int iVar,int jVar)1531 static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar )
1532 {
1533     if ( iVar == jVar )
1534         return;
1535     if ( jVar < iVar )
1536         ABC_SWAP( int, iVar, jVar );
1537     assert( iVar < jVar && jVar < nVars );
1538     if ( nVars <= 6 )
1539     {
1540         pTruth[0] = Abc_Tt6SwapVars( pTruth[0], iVar, jVar );
1541         return;
1542     }
1543     if ( jVar <= 5 )
1544     {
1545         word * s_PMasks = s_PPMasks[iVar][jVar];
1546         int nWords = Abc_TtWordNum(nVars);
1547         int w, shift = (1 << jVar) - (1 << iVar);
1548         for ( w = 0; w < nWords; w++ )
1549             pTruth[w] = (pTruth[w] & s_PMasks[0]) | ((pTruth[w] & s_PMasks[1]) << shift) | ((pTruth[w] & s_PMasks[2]) >> shift);
1550         return;
1551     }
1552     if ( iVar <= 5 && jVar > 5 )
1553     {
1554         word low2High, high2Low;
1555         word * pLimit = pTruth + Abc_TtWordNum(nVars);
1556         int j, jStep = Abc_TtWordNum(jVar);
1557         int shift = 1 << iVar;
1558         for ( ; pTruth < pLimit; pTruth += 2*jStep )
1559             for ( j = 0; j < jStep; j++ )
1560             {
1561                 low2High = (pTruth[j] & s_Truths6[iVar]) >> shift;
1562                 high2Low = (pTruth[j+jStep] << shift) & s_Truths6[iVar];
1563                 pTruth[j] = (pTruth[j] & ~s_Truths6[iVar]) | high2Low;
1564                 pTruth[j+jStep] = (pTruth[j+jStep] & s_Truths6[iVar]) | low2High;
1565             }
1566         return;
1567     }
1568     {
1569         word * pLimit = pTruth + Abc_TtWordNum(nVars);
1570         int i, iStep = Abc_TtWordNum(iVar);
1571         int j, jStep = Abc_TtWordNum(jVar);
1572         for ( ; pTruth < pLimit; pTruth += 2*jStep )
1573             for ( i = 0; i < jStep; i += 2*iStep )
1574                 for ( j = 0; j < iStep; j++ )
1575                     ABC_SWAP( word, pTruth[iStep + i + j], pTruth[jStep + i + j] );
1576         return;
1577     }
1578 }
1579 // moves one var (v) to the given position (p)
Abc_TtMoveVar(word * pF,int nVars,int * V2P,int * P2V,int v,int p)1580 static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p )
1581 {
1582     int iVar = V2P[v], jVar = p;
1583     if ( iVar == jVar )
1584         return;
1585     Abc_TtSwapVars( pF, nVars, iVar, jVar );
1586     V2P[P2V[iVar]] = jVar;
1587     V2P[P2V[jVar]] = iVar;
1588     P2V[iVar] ^= P2V[jVar];
1589     P2V[jVar] ^= P2V[iVar];
1590     P2V[iVar] ^= P2V[jVar];
1591 }
Abc_Tt6RemoveVar(word t,int iVar)1592 static inline word Abc_Tt6RemoveVar( word t, int iVar )
1593 {
1594     assert( !Abc_Tt6HasVar(t, iVar) );
1595     while ( iVar < 5 )
1596         t = Abc_Tt6SwapAdjacent( t, iVar++ );
1597     return t;
1598 }
1599 
1600 /**Function*************************************************************
1601 
1602   Synopsis    [Support minimization.]
1603 
1604   Description []
1605 
1606   SideEffects []
1607 
1608   SeeAlso     []
1609 
1610 ***********************************************************************/
Abc_TtShrink(word * pF,int nVars,int nVarsAll,unsigned Phase)1611 static inline void Abc_TtShrink( word * pF, int nVars, int nVarsAll, unsigned Phase )
1612 {
1613     int i, k, Var = 0;
1614     assert( nVarsAll <= 16 );
1615     for ( i = 0; i < nVarsAll; i++ )
1616         if ( Phase & (1 << i) )
1617         {
1618             for ( k = i-1; k >= Var; k-- )
1619                 Abc_TtSwapAdjacent( pF, Abc_TtWordNum(nVarsAll), k );
1620             Var++;
1621         }
1622     assert( Var == nVars );
1623 }
Abc_TtMinimumBase(word * t,int * pSupp,int nVarsAll,int * pnVars)1624 static inline int Abc_TtMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars )
1625 {
1626     int v, iVar = 0, uSupp = 0;
1627     assert( nVarsAll <= 16 );
1628     for ( v = 0; v < nVarsAll; v++ )
1629         if ( Abc_TtHasVar( t, nVarsAll, v ) )
1630         {
1631             uSupp |= (1 << v);
1632             if ( pSupp )
1633                 pSupp[iVar] = pSupp[v];
1634             iVar++;
1635         }
1636     if ( pnVars )
1637         *pnVars = iVar;
1638     if ( uSupp == 0 || Abc_TtSuppIsMinBase( uSupp ) )
1639         return 0;
1640     Abc_TtShrink( t, iVar, nVarsAll, uSupp );
1641     return 1;
1642 }
Abc_TtSimplify(word * t,int * pLits,int nVarsAll,int * pnVars)1643 static inline int Abc_TtSimplify( word * t, int * pLits, int nVarsAll, int * pnVars )
1644 {
1645     int v, u;
1646     for ( v = 0; v < nVarsAll; v++ )
1647     {
1648         if ( pLits[v] == 0 )
1649             Abc_TtCofactor0( t, Abc_TtWordNum(nVarsAll), v );
1650         else if ( pLits[v] == 1 )
1651             Abc_TtCofactor1( t, Abc_TtWordNum(nVarsAll), v );
1652     }
1653     for ( v = 0;   v < nVarsAll; v++ )
1654     for ( u = v+1; u < nVarsAll; u++ )
1655         if ( Abc_Lit2Var(pLits[v]) == Abc_Lit2Var(pLits[u]) )
1656         {
1657             assert( nVarsAll <= 6 );
1658             if ( pLits[v] == pLits[u] )
1659             {
1660                 word t0 = Abc_Tt6Cofactor0(Abc_Tt6Cofactor0(*t, v), u);
1661                 word t1 = Abc_Tt6Cofactor1(Abc_Tt6Cofactor1(*t, v), u);
1662                 *t = (t0 & s_Truths6Neg[v]) | (t1 & s_Truths6[v]);
1663             }
1664             else // if ( pLits[v] == Abc_LitNot(pLits[u]) )
1665             {
1666                 word t0 = Abc_Tt6Cofactor1(Abc_Tt6Cofactor0(*t, v), u);
1667                 word t1 = Abc_Tt6Cofactor0(Abc_Tt6Cofactor1(*t, v), u);
1668                 *t = (t0 & s_Truths6Neg[v]) | (t1 & s_Truths6[v]);
1669             }
1670         }
1671     return Abc_TtMinimumBase( t, pLits, nVarsAll, pnVars );
1672 }
1673 
1674 /**Function*************************************************************
1675 
1676   Synopsis    [Cut minimization.]
1677 
1678   Description []
1679 
1680   SideEffects []
1681 
1682   SeeAlso     []
1683 
1684 ***********************************************************************/
Abc_Tt6Expand(word t,int * pCut0,int nCutSize0,int * pCut,int nCutSize)1685 static inline word Abc_Tt6Expand( word t, int * pCut0, int nCutSize0, int * pCut, int nCutSize )
1686 {
1687     int i, k;
1688     for ( i = nCutSize - 1, k = nCutSize0 - 1; i >= 0 && k >= 0; i-- )
1689     {
1690         if ( pCut[i] > pCut0[k] )
1691             continue;
1692         assert( pCut[i] == pCut0[k] );
1693         if ( k < i )
1694             t = Abc_Tt6SwapVars( t, k, i );
1695         k--;
1696     }
1697     assert( k == -1 );
1698     return t;
1699 }
Abc_TtExpand(word * pTruth0,int nVars,int * pCut0,int nCutSize0,int * pCut,int nCutSize)1700 static inline void Abc_TtExpand( word * pTruth0, int nVars, int * pCut0, int nCutSize0, int * pCut, int nCutSize )
1701 {
1702     int i, k;
1703     for ( i = nCutSize - 1, k = nCutSize0 - 1; i >= 0 && k >= 0; i-- )
1704     {
1705         if ( pCut[i] > pCut0[k] )
1706             continue;
1707         assert( pCut[i] == pCut0[k] );
1708         if ( k < i )
1709             Abc_TtSwapVars( pTruth0, nVars, k, i );
1710         k--;
1711     }
1712     assert( k == -1 );
1713 }
Abc_Tt6MinBase(word * pTruth,int * pVars,int nVars)1714 static inline int Abc_Tt6MinBase( word * pTruth, int * pVars, int nVars )
1715 {
1716     word t = *pTruth;
1717     int i, k;
1718     for ( i = k = 0; i < nVars; i++ )
1719     {
1720         if ( !Abc_Tt6HasVar( t, i ) )
1721             continue;
1722         if ( k < i )
1723         {
1724             if ( pVars ) pVars[k] = pVars[i];
1725             t = Abc_Tt6SwapVars( t, k, i );
1726         }
1727         k++;
1728     }
1729     if ( k == nVars )
1730         return k;
1731     assert( k < nVars );
1732     *pTruth = t;
1733     return k;
1734 }
Abc_TtMinBase(word * pTruth,int * pVars,int nVars,int nVarsAll)1735 static inline int Abc_TtMinBase( word * pTruth, int * pVars, int nVars, int nVarsAll )
1736 {
1737     int i, k;
1738     assert( nVars <= nVarsAll );
1739     for ( i = k = 0; i < nVars; i++ )
1740     {
1741         if ( !Abc_TtHasVar( pTruth, nVarsAll, i ) )
1742             continue;
1743         if ( k < i )
1744         {
1745             if ( pVars ) pVars[k] = pVars[i];
1746             Abc_TtSwapVars( pTruth, nVarsAll, k, i );
1747         }
1748         k++;
1749     }
1750     if ( k == nVars )
1751         return k;
1752     assert( k < nVars );
1753 //    assert( k == Abc_TtSupportSize(pTruth, nVars) );
1754     return k;
1755 }
1756 
1757 /**Function*************************************************************
1758 
1759   Synopsis    [Implemeting given NPN config.]
1760 
1761   Description []
1762 
1763   SideEffects []
1764 
1765   SeeAlso     []
1766 
1767 ***********************************************************************/
Abc_TtImplementNpnConfig(word * pTruth,int nVars,char * pCanonPerm,unsigned uCanonPhase)1768 static inline void Abc_TtImplementNpnConfig( word * pTruth, int nVars, char * pCanonPerm, unsigned uCanonPhase )
1769 {
1770     int i, k, nWords = Abc_TtWordNum( nVars );
1771     if ( (uCanonPhase >> nVars) & 1 )
1772         Abc_TtNot( pTruth, nWords );
1773     for ( i = 0; i < nVars; i++ )
1774         if ( (uCanonPhase >> i) & 1 )
1775             Abc_TtFlip( pTruth, nWords, i );
1776     if ( pCanonPerm )
1777     for ( i = 0; i < nVars; i++ )
1778     {
1779         for ( k = i; k < nVars; k++ )
1780             if ( pCanonPerm[k] == i )
1781                 break;
1782         assert( k < nVars );
1783         if ( i == k )
1784             continue;
1785         Abc_TtSwapVars( pTruth, nVars, i, k );
1786         ABC_SWAP( int, pCanonPerm[i], pCanonPerm[k] );
1787     }
1788 }
1789 
1790 /**Function*************************************************************
1791 
1792   Synopsis    []
1793 
1794   Description []
1795 
1796   SideEffects []
1797 
1798   SeeAlso     []
1799 
1800 ***********************************************************************/
Abc_TtCountOnesSlow(word t)1801 static inline int Abc_TtCountOnesSlow( word t )
1802 {
1803     t =    (t & ABC_CONST(0x5555555555555555)) + ((t>> 1) & ABC_CONST(0x5555555555555555));
1804     t =    (t & ABC_CONST(0x3333333333333333)) + ((t>> 2) & ABC_CONST(0x3333333333333333));
1805     t =    (t & ABC_CONST(0x0F0F0F0F0F0F0F0F)) + ((t>> 4) & ABC_CONST(0x0F0F0F0F0F0F0F0F));
1806     t =    (t & ABC_CONST(0x00FF00FF00FF00FF)) + ((t>> 8) & ABC_CONST(0x00FF00FF00FF00FF));
1807     t =    (t & ABC_CONST(0x0000FFFF0000FFFF)) + ((t>>16) & ABC_CONST(0x0000FFFF0000FFFF));
1808     return (t & ABC_CONST(0x00000000FFFFFFFF)) +  (t>>32);
1809 }
Abc_TtCountOnes(word x)1810 static inline int Abc_TtCountOnes( word x )
1811 {
1812     x = x - ((x >> 1) & ABC_CONST(0x5555555555555555));
1813     x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333));
1814     x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F);
1815     x = x + (x >> 8);
1816     x = x + (x >> 16);
1817     x = x + (x >> 32);
1818     return (int)(x & 0xFF);
1819 }
Abc_TtCountOnesVec(word * x,int nWords)1820 static inline int Abc_TtCountOnesVec( word * x, int nWords )
1821 {
1822     int w, Count = 0;
1823     for ( w = 0; w < nWords; w++ )
1824         Count += Abc_TtCountOnes( x[w] );
1825     return Count;
1826 }
Abc_TtCountOnesVecMask(word * x,word * pMask,int nWords,int fCompl)1827 static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl )
1828 {
1829     int w, Count = 0;
1830     if ( fCompl )
1831         for ( w = 0; w < nWords; w++ )
1832             Count += Abc_TtCountOnes( pMask[w] & ~x[w] );
1833     else
1834         for ( w = 0; w < nWords; w++ )
1835             Count += Abc_TtCountOnes( pMask[w] & x[w] );
1836     return Count;
1837 }
Abc_TtCountOnesVecXor(word * x,word * y,int nWords)1838 static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
1839 {
1840     int w, Count = 0;
1841     for ( w = 0; w < nWords; w++ )
1842         Count += Abc_TtCountOnes( x[w] ^ y[w] );
1843     return Count;
1844 }
1845 
1846 /**Function*************************************************************
1847 
1848   Synopsis    []
1849 
1850   Description []
1851 
1852   SideEffects []
1853 
1854   SeeAlso     []
1855 
1856 ***********************************************************************/
Abc_Tt6FirstBit(word t)1857 static inline int Abc_Tt6FirstBit( word t )
1858 {
1859     int n = 0;
1860     if ( t == 0 ) return -1;
1861     if ( (t & ABC_CONST(0x00000000FFFFFFFF)) == 0 ) { n += 32; t >>= 32; }
1862     if ( (t & ABC_CONST(0x000000000000FFFF)) == 0 ) { n += 16; t >>= 16; }
1863     if ( (t & ABC_CONST(0x00000000000000FF)) == 0 ) { n +=  8; t >>=  8; }
1864     if ( (t & ABC_CONST(0x000000000000000F)) == 0 ) { n +=  4; t >>=  4; }
1865     if ( (t & ABC_CONST(0x0000000000000003)) == 0 ) { n +=  2; t >>=  2; }
1866     if ( (t & ABC_CONST(0x0000000000000001)) == 0 ) { n++; }
1867     return n;
1868 }
Abc_Tt6LastBit(word t)1869 static inline int Abc_Tt6LastBit( word t )
1870 {
1871     int n = 0;
1872     if ( t == 0 ) return -1;
1873     if ( (t & ABC_CONST(0xFFFFFFFF00000000)) == 0 ) { n += 32; t <<= 32; }
1874     if ( (t & ABC_CONST(0xFFFF000000000000)) == 0 ) { n += 16; t <<= 16; }
1875     if ( (t & ABC_CONST(0xFF00000000000000)) == 0 ) { n +=  8; t <<=  8; }
1876     if ( (t & ABC_CONST(0xF000000000000000)) == 0 ) { n +=  4; t <<=  4; }
1877     if ( (t & ABC_CONST(0xC000000000000000)) == 0 ) { n +=  2; t <<=  2; }
1878     if ( (t & ABC_CONST(0x8000000000000000)) == 0 ) { n++; }
1879     return 63-n;
1880 }
Abc_TtFindFirstBit(word * pIn,int nVars)1881 static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
1882 {
1883     int w, nWords = Abc_TtWordNum(nVars);
1884     for ( w = 0; w < nWords; w++ )
1885         if ( pIn[w] )
1886             return 64*w + Abc_Tt6FirstBit(pIn[w]);
1887     return -1;
1888 }
Abc_TtFindFirstBit2(word * pIn,int nWords)1889 static inline int Abc_TtFindFirstBit2( word * pIn, int nWords )
1890 {
1891     int w;
1892     for ( w = 0; w < nWords; w++ )
1893         if ( pIn[w] )
1894             return 64*w + Abc_Tt6FirstBit(pIn[w]);
1895     return -1;
1896 }
Abc_TtFindLastBit(word * pIn,int nVars)1897 static inline int Abc_TtFindLastBit( word * pIn, int nVars )
1898 {
1899     int w, nWords = Abc_TtWordNum(nVars);
1900     for ( w = nWords - 1; w >= 0; w-- )
1901         if ( pIn[w] )
1902             return 64*w + Abc_Tt6LastBit(pIn[w]);
1903     return -1;
1904 }
Abc_TtFindLastBit2(word * pIn,int nWords)1905 static inline int Abc_TtFindLastBit2( word * pIn, int nWords )
1906 {
1907     int w;
1908     for ( w = nWords - 1; w >= 0; w-- )
1909         if ( pIn[w] )
1910             return 64*w + Abc_Tt6LastBit(pIn[w]);
1911     return -1;
1912 }
Abc_TtFindFirstDiffBit(word * pIn1,word * pIn2,int nVars)1913 static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
1914 {
1915     int w, nWords = Abc_TtWordNum(nVars);
1916     for ( w = 0; w < nWords; w++ )
1917         if ( pIn1[w] ^ pIn2[w] )
1918             return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
1919     return -1;
1920 }
Abc_TtFindFirstDiffBit2(word * pIn1,word * pIn2,int nWords)1921 static inline int Abc_TtFindFirstDiffBit2( word * pIn1, word * pIn2, int nWords )
1922 {
1923     int w;
1924     for ( w = 0; w < nWords; w++ )
1925         if ( pIn1[w] ^ pIn2[w] )
1926             return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
1927     return -1;
1928 }
Abc_TtFindLastDiffBit(word * pIn1,word * pIn2,int nVars)1929 static inline int Abc_TtFindLastDiffBit( word * pIn1, word * pIn2, int nVars )
1930 {
1931     int w, nWords = Abc_TtWordNum(nVars);
1932     for ( w = nWords - 1; w >= 0; w-- )
1933         if ( pIn1[w] ^ pIn2[w] )
1934             return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
1935     return -1;
1936 }
Abc_TtFindLastDiffBit2(word * pIn1,word * pIn2,int nWords)1937 static inline int Abc_TtFindLastDiffBit2( word * pIn1, word * pIn2, int nWords )
1938 {
1939     int w;
1940     for ( w = nWords - 1; w >= 0; w-- )
1941         if ( pIn1[w] ^ pIn2[w] )
1942             return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
1943     return -1;
1944 }
Abc_TtFindFirstZero(word * pIn,int nVars)1945 static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
1946 {
1947     int w, nWords = Abc_TtWordNum(nVars);
1948     for ( w = 0; w < nWords; w++ )
1949         if ( ~pIn[w] )
1950             return 64*w + Abc_Tt6FirstBit(~pIn[w]);
1951     return -1;
1952 }
Abc_TtFindLastZero(word * pIn,int nVars)1953 static inline int Abc_TtFindLastZero( word * pIn, int nVars )
1954 {
1955     int w, nWords = Abc_TtWordNum(nVars);
1956     for ( w = nWords - 1; w >= 0; w-- )
1957         if ( ~pIn[w] )
1958             return 64*w + Abc_Tt6LastBit(~pIn[w]);
1959     return -1;
1960 }
1961 
1962 
1963 /**Function*************************************************************
1964 
1965   Synopsis    []
1966 
1967   Description []
1968 
1969   SideEffects []
1970 
1971   SeeAlso     []
1972 
1973 ***********************************************************************/
Abc_TtReverseVars(word * pTruth,int nVars)1974 static inline void Abc_TtReverseVars( word * pTruth, int nVars )
1975 {
1976     int k;
1977     for ( k = 0; k < nVars/2 ; k++ )
1978         Abc_TtSwapVars( pTruth, nVars, k, nVars - 1 - k );
1979 }
Abc_TtReverseBits(word * pTruth,int nVars)1980 static inline void Abc_TtReverseBits( word * pTruth, int nVars )
1981 {
1982     static unsigned char pMirror[256] = {
1983           0, 128,  64, 192,  32, 160,  96, 224,  16, 144,  80, 208,  48, 176, 112, 240,
1984           8, 136,  72, 200,  40, 168, 104, 232,  24, 152,  88, 216,  56, 184, 120, 248,
1985           4, 132,  68, 196,  36, 164, 100, 228,  20, 148,  84, 212,  52, 180, 116, 244,
1986          12, 140,  76, 204,  44, 172, 108, 236,  28, 156,  92, 220,  60, 188, 124, 252,
1987           2, 130,  66, 194,  34, 162,  98, 226,  18, 146,  82, 210,  50, 178, 114, 242,
1988          10, 138,  74, 202,  42, 170, 106, 234,  26, 154,  90, 218,  58, 186, 122, 250,
1989           6, 134,  70, 198,  38, 166, 102, 230,  22, 150,  86, 214,  54, 182, 118, 246,
1990          14, 142,  78, 206,  46, 174, 110, 238,  30, 158,  94, 222,  62, 190, 126, 254,
1991           1, 129,  65, 193,  33, 161,  97, 225,  17, 145,  81, 209,  49, 177, 113, 241,
1992           9, 137,  73, 201,  41, 169, 105, 233,  25, 153,  89, 217,  57, 185, 121, 249,
1993           5, 133,  69, 197,  37, 165, 101, 229,  21, 149,  85, 213,  53, 181, 117, 245,
1994          13, 141,  77, 205,  45, 173, 109, 237,  29, 157,  93, 221,  61, 189, 125, 253,
1995           3, 131,  67, 195,  35, 163,  99, 227,  19, 147,  83, 211,  51, 179, 115, 243,
1996          11, 139,  75, 203,  43, 171, 107, 235,  27, 155,  91, 219,  59, 187, 123, 251,
1997           7, 135,  71, 199,  39, 167, 103, 231,  23, 151,  87, 215,  55, 183, 119, 247,
1998          15, 143,  79, 207,  47, 175, 111, 239,  31, 159,  95, 223,  63, 191, 127, 255
1999     };
2000     unsigned char Temp, * pTruthC = (unsigned char *)pTruth;
2001     int i, nBytes = (nVars > 6) ? (1 << (nVars - 3)) : 8;
2002     for ( i = 0; i < nBytes/2; i++ )
2003     {
2004         Temp = pMirror[pTruthC[i]];
2005         pTruthC[i] = pMirror[pTruthC[nBytes-1-i]];
2006         pTruthC[nBytes-1-i] = Temp;
2007     }
2008 }
2009 
2010 
2011 /**Function*************************************************************
2012 
2013   Synopsis    [Checks unateness of a function.]
2014 
2015   Description []
2016 
2017   SideEffects []
2018 
2019   SeeAlso     []
2020 
2021 ***********************************************************************/
Abc_Tt6PosVar(word t,int iVar)2022 static inline int Abc_Tt6PosVar( word t, int iVar )
2023 {
2024     return ((t >> (1<<iVar)) & t & s_Truths6Neg[iVar]) == (t & s_Truths6Neg[iVar]);
2025 }
Abc_Tt6NegVar(word t,int iVar)2026 static inline int Abc_Tt6NegVar( word t, int iVar )
2027 {
2028     return ((t << (1<<iVar)) & t & s_Truths6[iVar]) == (t & s_Truths6[iVar]);
2029 }
Abc_TtPosVar(word * t,int nVars,int iVar)2030 static inline int Abc_TtPosVar( word * t, int nVars, int iVar )
2031 {
2032     assert( iVar < nVars );
2033     if ( nVars <= 6 )
2034         return Abc_Tt6PosVar( t[0], iVar );
2035     if ( iVar < 6 )
2036     {
2037         int i, Shift = (1 << iVar);
2038         int nWords = Abc_TtWordNum( nVars );
2039         for ( i = 0; i < nWords; i++ )
2040             if ( ((t[i] >> Shift) & t[i] & s_Truths6Neg[iVar]) != (t[i] & s_Truths6Neg[iVar]) )
2041                 return 0;
2042         return 1;
2043     }
2044     else
2045     {
2046         int i, Step = (1 << (iVar - 6));
2047         word * tLimit = t + Abc_TtWordNum( nVars );
2048         for ( ; t < tLimit; t += 2*Step )
2049             for ( i = 0; i < Step; i++ )
2050                 if ( t[i] != (t[i] & t[Step+i]) )
2051                     return 0;
2052         return 1;
2053     }
2054 }
Abc_TtNegVar(word * t,int nVars,int iVar)2055 static inline int Abc_TtNegVar( word * t, int nVars, int iVar )
2056 {
2057     assert( iVar < nVars );
2058     if ( nVars <= 6 )
2059         return Abc_Tt6NegVar( t[0], iVar );
2060     if ( iVar < 6 )
2061     {
2062         int i, Shift = (1 << iVar);
2063         int nWords = Abc_TtWordNum( nVars );
2064         for ( i = 0; i < nWords; i++ )
2065             if ( ((t[i] << Shift) & t[i] & s_Truths6[iVar]) != (t[i] & s_Truths6[iVar]) )
2066                 return 0;
2067         return 1;
2068     }
2069     else
2070     {
2071         int i, Step = (1 << (iVar - 6));
2072         word * tLimit = t + Abc_TtWordNum( nVars );
2073         for ( ; t < tLimit; t += 2*Step )
2074             for ( i = 0; i < Step; i++ )
2075                 if ( (t[i] & t[Step+i]) != t[Step+i] )
2076                     return 0;
2077         return 1;
2078     }
2079 }
Abc_TtIsUnate(word * t,int nVars)2080 static inline int Abc_TtIsUnate( word * t, int nVars )
2081 {
2082     int i;
2083     for ( i = 0; i < nVars; i++ )
2084         if ( !Abc_TtNegVar(t, nVars, i) && !Abc_TtPosVar(t, nVars, i) )
2085             return 0;
2086     return 1;
2087 }
Abc_TtIsPosUnate(word * t,int nVars)2088 static inline int Abc_TtIsPosUnate( word * t, int nVars )
2089 {
2090     int i;
2091     for ( i = 0; i < nVars; i++ )
2092         if ( !Abc_TtPosVar(t, nVars, i) )
2093             return 0;
2094     return 1;
2095 }
Abc_TtMakePosUnate(word * t,int nVars)2096 static inline void Abc_TtMakePosUnate( word * t, int nVars )
2097 {
2098     int i, nWords = Abc_TtWordNum(nVars);
2099     for ( i = 0; i < nVars; i++ )
2100         if ( Abc_TtNegVar(t, nVars, i) )
2101             Abc_TtFlip( t, nWords, i );
2102         else assert( Abc_TtPosVar(t, nVars, i) );
2103 }
2104 
2105 
2106 /**Function*************************************************************
2107 
2108   Synopsis    [Computes ISOP for 6 variables or less.]
2109 
2110   Description []
2111 
2112   SideEffects []
2113 
2114   SeeAlso     []
2115 
2116 ***********************************************************************/
Abc_Tt6Isop(word uOn,word uOnDc,int nVars,int * pnCubes)2117 static inline word Abc_Tt6Isop( word uOn, word uOnDc, int nVars, int * pnCubes )
2118 {
2119     word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
2120     int Var;
2121     assert( nVars <= 6 );
2122     assert( (uOn & ~uOnDc) == 0 );
2123     if ( uOn == 0 )
2124         return 0;
2125     if ( uOnDc == ~(word)0 )
2126     {
2127         (*pnCubes)++;
2128         return ~(word)0;
2129     }
2130     assert( nVars > 0 );
2131     // find the topmost var
2132     for ( Var = nVars-1; Var >= 0; Var-- )
2133         if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
2134              break;
2135     assert( Var >= 0 );
2136     // cofactor
2137     uOn0   = Abc_Tt6Cofactor0( uOn,   Var );
2138     uOn1   = Abc_Tt6Cofactor1( uOn  , Var );
2139     uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
2140     uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
2141     // solve for cofactors
2142     uRes0 = Abc_Tt6Isop( uOn0 & ~uOnDc1, uOnDc0, Var, pnCubes );
2143     uRes1 = Abc_Tt6Isop( uOn1 & ~uOnDc0, uOnDc1, Var, pnCubes );
2144     uRes2 = Abc_Tt6Isop( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pnCubes );
2145     // derive the final truth table
2146     uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
2147     assert( (uOn & ~uRes2) == 0 );
2148     assert( (uRes2 & ~uOnDc) == 0 );
2149     return uRes2;
2150 }
Abc_Tt7Isop(word uOn[2],word uOnDc[2],int nVars,word uRes[2])2151 static inline int Abc_Tt7Isop( word uOn[2], word uOnDc[2], int nVars, word uRes[2] )
2152 {
2153     int nCubes = 0;
2154     if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
2155         uRes[0] = uRes[1] = Abc_Tt6Isop( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), &nCubes );
2156     else
2157     {
2158         word uRes0, uRes1, uRes2;
2159         assert( nVars == 7 );
2160         // solve for cofactors
2161         uRes0 = Abc_Tt6Isop( uOn[0] & ~uOnDc[1], uOnDc[0], 6, &nCubes );
2162         uRes1 = Abc_Tt6Isop( uOn[1] & ~uOnDc[0], uOnDc[1], 6, &nCubes );
2163         uRes2 = Abc_Tt6Isop( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, &nCubes );
2164         // derive the final truth table
2165         uRes[0] = uRes2 | uRes0;
2166         uRes[1] = uRes2 | uRes1;
2167         assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
2168         assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
2169     }
2170     return nCubes;
2171 }
Abc_Tt8Isop(word uOn[4],word uOnDc[4],int nVars,word uRes[4])2172 static inline int Abc_Tt8Isop( word uOn[4], word uOnDc[4], int nVars, word uRes[4] )
2173 {
2174     int nCubes = 0;
2175     if ( nVars <= 6 )
2176         uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6Isop( uOn[0], uOnDc[0], nVars, &nCubes );
2177     else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
2178     {
2179         nCubes = Abc_Tt7Isop( uOn, uOnDc, 7, uRes );
2180         uRes[2] = uRes[0];
2181         uRes[3] = uRes[1];
2182     }
2183     else
2184     {
2185         word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
2186         assert( nVars == 8 );
2187         // cofactor
2188         uOn0[0] = uOn[0] & ~uOnDc[2];
2189         uOn0[1] = uOn[1] & ~uOnDc[3];
2190         uOn1[0] = uOn[2] & ~uOnDc[0];
2191         uOn1[1] = uOn[3] & ~uOnDc[1];
2192         uOnDc2[0] = uOnDc[0] & uOnDc[2];
2193         uOnDc2[1] = uOnDc[1] & uOnDc[3];
2194         // solve for cofactors
2195         nCubes += Abc_Tt7Isop( uOn0, uOnDc+0, 7, uRes0 );
2196         nCubes += Abc_Tt7Isop( uOn1, uOnDc+2, 7, uRes1 );
2197         uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
2198         uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
2199         nCubes += Abc_Tt7Isop( uOn2, uOnDc2, 7, uRes2 );
2200         // derive the final truth table
2201         uRes[0] = uRes2[0] | uRes0[0];
2202         uRes[1] = uRes2[1] | uRes0[1];
2203         uRes[2] = uRes2[0] | uRes1[0];
2204         uRes[3] = uRes2[1] | uRes1[1];
2205         assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
2206         assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
2207     }
2208     return nCubes;
2209 }
2210 
2211 /**Function*************************************************************
2212 
2213   Synopsis    [Computes CNF size.]
2214 
2215   Description []
2216 
2217   SideEffects []
2218 
2219   SeeAlso     []
2220 
2221 ***********************************************************************/
Abc_Tt6CnfSize(word t,int nVars)2222 static inline int Abc_Tt6CnfSize( word t, int nVars )
2223 {
2224     int nCubes = 0;
2225     Abc_Tt6Isop(  t,  t, nVars, &nCubes );
2226     Abc_Tt6Isop( ~t, ~t, nVars, &nCubes );
2227     assert( nCubes <= 64 );
2228     return nCubes;
2229 }
Abc_Tt8CnfSize(word t[4],int nVars)2230 static inline int Abc_Tt8CnfSize( word t[4], int nVars )
2231 {
2232     word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
2233     int nCubes = 0;
2234     nCubes += Abc_Tt8Isop( t,  t,  nVars, uRes );
2235     nCubes += Abc_Tt8Isop( tc, tc, nVars, uRes );
2236     assert( nCubes <= 256 );
2237     return nCubes;
2238 }
2239 
2240 /**Function*************************************************************
2241 
2242   Synopsis    [Derives ISOP cover for the function.]
2243 
2244   Description []
2245 
2246   SideEffects []
2247 
2248   SeeAlso     []
2249 
2250 ***********************************************************************/
Abc_Tt6IsopCover(word uOn,word uOnDc,int nVars,int * pCover,int * pnCubes)2251 static inline word Abc_Tt6IsopCover( word uOn, word uOnDc, int nVars, int * pCover, int * pnCubes )
2252 {
2253     word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
2254     int c, Var, nBeg0, nEnd0, nEnd1;
2255     assert( nVars <= 6 );
2256     assert( (uOn & ~uOnDc) == 0 );
2257     if ( uOn == 0 )
2258         return 0;
2259     if ( uOnDc == ~(word)0 )
2260     {
2261         pCover[(*pnCubes)++] = 0;
2262         return ~(word)0;
2263     }
2264     assert( nVars > 0 );
2265     // find the topmost var
2266     for ( Var = nVars-1; Var >= 0; Var-- )
2267         if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
2268              break;
2269     assert( Var >= 0 );
2270     // cofactor
2271     uOn0   = Abc_Tt6Cofactor0( uOn,   Var );
2272     uOn1   = Abc_Tt6Cofactor1( uOn  , Var );
2273     uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
2274     uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
2275     // solve for cofactors
2276     nBeg0 = *pnCubes;
2277     uRes0 = Abc_Tt6IsopCover( uOn0 & ~uOnDc1, uOnDc0, Var, pCover, pnCubes );
2278     nEnd0 = *pnCubes;
2279     uRes1 = Abc_Tt6IsopCover( uOn1 & ~uOnDc0, uOnDc1, Var, pCover, pnCubes );
2280     nEnd1 = *pnCubes;
2281     uRes2 = Abc_Tt6IsopCover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pCover, pnCubes );
2282     // derive the final truth table
2283     uRes2 |= (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
2284     for ( c = nBeg0; c < nEnd0; c++ )
2285         pCover[c] |= (1 << (2*Var+0));
2286     for ( c = nEnd0; c < nEnd1; c++ )
2287         pCover[c] |= (1 << (2*Var+1));
2288     assert( (uOn & ~uRes2) == 0 );
2289     assert( (uRes2 & ~uOnDc) == 0 );
2290     return uRes2;
2291 }
Abc_Tt7IsopCover(word uOn[2],word uOnDc[2],int nVars,word uRes[2],int * pCover,int * pnCubes)2292 static inline void Abc_Tt7IsopCover( word uOn[2], word uOnDc[2], int nVars, word uRes[2], int * pCover, int * pnCubes )
2293 {
2294     if ( nVars <= 6 || (uOn[0] == uOn[1] && uOnDc[0] == uOnDc[1]) )
2295         uRes[0] = uRes[1] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], Abc_MinInt(nVars, 6), pCover, pnCubes );
2296     else
2297     {
2298         word uRes0, uRes1, uRes2;
2299         int c, nBeg0, nEnd0, nEnd1;
2300         assert( nVars == 7 );
2301         // solve for cofactors
2302         nBeg0 = *pnCubes;
2303         uRes0 = Abc_Tt6IsopCover( uOn[0] & ~uOnDc[1], uOnDc[0], 6, pCover, pnCubes );
2304         nEnd0 = *pnCubes;
2305         uRes1 = Abc_Tt6IsopCover( uOn[1] & ~uOnDc[0], uOnDc[1], 6, pCover, pnCubes );
2306         nEnd1 = *pnCubes;
2307         uRes2 = Abc_Tt6IsopCover( (uOn[0] & ~uRes0) | (uOn[1] & ~uRes1), uOnDc[0] & uOnDc[1], 6, pCover, pnCubes );
2308         // derive the final truth table
2309         uRes[0] = uRes2 | uRes0;
2310         uRes[1] = uRes2 | uRes1;
2311         for ( c = nBeg0; c < nEnd0; c++ )
2312             pCover[c] |= (1 << (2*6+0));
2313         for ( c = nEnd0; c < nEnd1; c++ )
2314             pCover[c] |= (1 << (2*6+1));
2315         assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 );
2316         assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 );
2317     }
2318 }
Abc_Tt8IsopCover(word uOn[4],word uOnDc[4],int nVars,word uRes[4],int * pCover,int * pnCubes)2319 static inline void Abc_Tt8IsopCover( word uOn[4], word uOnDc[4], int nVars, word uRes[4], int * pCover, int * pnCubes )
2320 {
2321     if ( nVars <= 6 )
2322         uRes[0] = uRes[1] = uRes[2] = uRes[3] = Abc_Tt6IsopCover( uOn[0], uOnDc[0], nVars, pCover, pnCubes );
2323     else if ( nVars == 7 || (uOn[0] == uOn[2] && uOn[1] == uOn[3] && uOnDc[0] == uOnDc[2] && uOnDc[1] == uOnDc[3]) )
2324     {
2325         Abc_Tt7IsopCover( uOn, uOnDc, 7, uRes, pCover, pnCubes );
2326         uRes[2] = uRes[0];
2327         uRes[3] = uRes[1];
2328     }
2329     else
2330     {
2331         word uOn0[2], uOn1[2], uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
2332         int c, nBeg0, nEnd0, nEnd1;
2333         assert( nVars == 8 );
2334         // cofactor
2335         uOn0[0] = uOn[0] & ~uOnDc[2];
2336         uOn0[1] = uOn[1] & ~uOnDc[3];
2337         uOn1[0] = uOn[2] & ~uOnDc[0];
2338         uOn1[1] = uOn[3] & ~uOnDc[1];
2339         uOnDc2[0] = uOnDc[0] & uOnDc[2];
2340         uOnDc2[1] = uOnDc[1] & uOnDc[3];
2341         // solve for cofactors
2342         nBeg0 = *pnCubes;
2343         Abc_Tt7IsopCover( uOn0, uOnDc+0, 7, uRes0, pCover, pnCubes );
2344         nEnd0 = *pnCubes;
2345         Abc_Tt7IsopCover( uOn1, uOnDc+2, 7, uRes1, pCover, pnCubes );
2346         nEnd1 = *pnCubes;
2347         uOn2[0] = (uOn[0] & ~uRes0[0]) | (uOn[2] & ~uRes1[0]);
2348         uOn2[1] = (uOn[1] & ~uRes0[1]) | (uOn[3] & ~uRes1[1]);
2349         Abc_Tt7IsopCover( uOn2, uOnDc2, 7, uRes2, pCover, pnCubes );
2350         // derive the final truth table
2351         uRes[0] = uRes2[0] | uRes0[0];
2352         uRes[1] = uRes2[1] | uRes0[1];
2353         uRes[2] = uRes2[0] | uRes1[0];
2354         uRes[3] = uRes2[1] | uRes1[1];
2355         for ( c = nBeg0; c < nEnd0; c++ )
2356             pCover[c] |= (1 << (2*7+0));
2357         for ( c = nEnd0; c < nEnd1; c++ )
2358             pCover[c] |= (1 << (2*7+1));
2359         assert( (uOn[0] & ~uRes[0]) == 0 && (uOn[1] & ~uRes[1]) == 0 && (uOn[2] & ~uRes[2]) == 0 && (uOn[3] & ~uRes[3]) == 0 );
2360         assert( (uRes[0] & ~uOnDc[0])==0 && (uRes[1] & ~uOnDc[1])==0 && (uRes[2] & ~uOnDc[2])==0 && (uRes[3] & ~uOnDc[3])==0 );
2361     }
2362 }
2363 
2364 /**Function*************************************************************
2365 
2366   Synopsis    [Computes CNF for the function.]
2367 
2368   Description []
2369 
2370   SideEffects []
2371 
2372   SeeAlso     []
2373 
2374 ***********************************************************************/
Abc_Tt6Cnf(word t,int nVars,int * pCover)2375 static inline int Abc_Tt6Cnf( word t, int nVars, int * pCover )
2376 {
2377     int c, nCubes = 0;
2378     Abc_Tt6IsopCover( t, t, nVars, pCover, &nCubes );
2379     for ( c = 0; c < nCubes; c++ )
2380         pCover[c] |= (1 << (2*nVars+0));
2381     Abc_Tt6IsopCover( ~t, ~t, nVars, pCover, &nCubes );
2382     for ( ; c < nCubes; c++ )
2383         pCover[c] |= (1 << (2*nVars+1));
2384     assert( nCubes <= 64 );
2385     return nCubes;
2386 }
Abc_Tt8Cnf(word t[4],int nVars,int * pCover)2387 static inline int Abc_Tt8Cnf( word t[4], int nVars, int * pCover )
2388 {
2389     word uRes[4], tc[4] = {~t[0], ~t[1], ~t[2], ~t[3]};
2390     int c, nCubes = 0;
2391     Abc_Tt8IsopCover( t,  t,  nVars, uRes, pCover, &nCubes );
2392     for ( c = 0; c < nCubes; c++ )
2393         pCover[c] |= (1 << (2*nVars+0));
2394     Abc_Tt8IsopCover( tc, tc, nVars, uRes, pCover, &nCubes );
2395     for ( ; c < nCubes; c++ )
2396         pCover[c] |= (1 << (2*nVars+1));
2397     assert( nCubes <= 256 );
2398     return nCubes;
2399 }
2400 
2401 
2402 /**Function*************************************************************
2403 
2404   Synopsis    [Computes ISOP for 6 variables or less.]
2405 
2406   Description []
2407 
2408   SideEffects []
2409 
2410   SeeAlso     []
2411 
2412 ***********************************************************************/
Abc_Tt6Esop(word t,int nVars,int * pCover)2413 static inline int Abc_Tt6Esop( word t, int nVars, int * pCover )
2414 {
2415     word c0, c1;
2416     int Var, r0, r1, r2, Max, i;
2417     assert( nVars <= 6 );
2418     if ( t == 0 )
2419         return 0;
2420     if ( t == ~(word)0 )
2421     {
2422         if ( pCover ) *pCover = 0;
2423         return 1;
2424     }
2425     assert( nVars > 0 );
2426     // find the topmost var
2427     for ( Var = nVars-1; Var >= 0; Var-- )
2428         if ( Abc_Tt6HasVar( t, Var ) )
2429              break;
2430     assert( Var >= 0 );
2431     // cofactor
2432     c0 = Abc_Tt6Cofactor0( t, Var );
2433     c1 = Abc_Tt6Cofactor1( t, Var );
2434     // call recursively
2435     r0 = Abc_Tt6Esop( c0,      Var, pCover ? pCover : NULL );
2436     r1 = Abc_Tt6Esop( c1,      Var, pCover ? pCover + r0 : NULL );
2437     r2 = Abc_Tt6Esop( c0 ^ c1, Var, pCover ? pCover + r0 + r1 : NULL );
2438     Max = Abc_MaxInt( r0, Abc_MaxInt(r1, r2) );
2439     // add literals
2440     if ( pCover )
2441     {
2442         if ( Max == r0 )
2443         {
2444             for ( i = 0; i < r1; i++ )
2445                 pCover[i] = pCover[r0+i];
2446             for ( i = 0; i < r2; i++ )
2447                 pCover[r1+i] = pCover[r0+r1+i] | (1 << (2*Var+0));
2448         }
2449         else if ( Max == r1 )
2450         {
2451             for ( i = 0; i < r2; i++ )
2452                 pCover[r0+i] = pCover[r0+r1+i] | (1 << (2*Var+1));
2453         }
2454         else
2455         {
2456             for ( i = 0; i < r0; i++ )
2457                 pCover[i] |= (1 << (2*Var+0));
2458             for ( i = 0; i < r1; i++ )
2459                 pCover[r0+i] |= (1 << (2*Var+1));
2460         }
2461     }
2462     return r0 + r1 + r2 - Max;
2463 }
Abc_Tt6EsopBuild(int nVars,int * pCover,int nCubes)2464 static inline word Abc_Tt6EsopBuild( int nVars, int * pCover, int nCubes )
2465 {
2466     word p, t = 0; int c, v;
2467     for ( c = 0; c < nCubes; c++ )
2468     {
2469         p = ~(word)0;
2470         for ( v = 0; v < nVars; v++ )
2471             if ( ((pCover[c] >> (v << 1)) & 3) == 1 )
2472                 p &= ~s_Truths6[v];
2473             else if ( ((pCover[c] >> (v << 1)) & 3) == 2 )
2474                 p &= s_Truths6[v];
2475         t ^= p;
2476     }
2477     return t;
2478 }
Abc_Tt6EsopVerify(word t,int nVars)2479 static inline int Abc_Tt6EsopVerify( word t, int nVars )
2480 {
2481     int pCover[64];
2482     int nCubes = Abc_Tt6Esop( t, nVars, pCover );
2483     word t2 = Abc_Tt6EsopBuild( nVars, pCover, nCubes );
2484     if ( t != t2 )
2485         printf( "Verification failed.\n" );
2486     return nCubes;
2487 }
2488 
2489 /**Function*************************************************************
2490 
2491   Synopsis    [Check if the function is output-decomposable with the given var.]
2492 
2493   Description []
2494 
2495   SideEffects []
2496 
2497   SeeAlso     []
2498 
2499 ***********************************************************************/
Abc_Tt6CheckOutDec(word t,int i,word * pOut)2500 static inline int Abc_Tt6CheckOutDec( word t, int i, word * pOut )
2501 {
2502     word c0 = Abc_Tt6Cofactor0( t, i );
2503     word c1 = Abc_Tt6Cofactor1( t, i );
2504     assert( c0 != c1 );
2505     if ( c0 == 0 ) //  F = i * G
2506     {
2507         if ( pOut ) *pOut = c1;
2508         return 0;
2509     }
2510     if ( c1 == 0 ) //  F = ~i * G
2511     {
2512         if ( pOut ) *pOut = c0;
2513         return 1;
2514     }
2515     if ( ~c0 == 0 ) //  F = ~i + G
2516     {
2517         if ( pOut ) *pOut = c1;
2518         return 2;
2519     }
2520     if ( ~c1 == 0 ) //  F = i + G
2521     {
2522         if ( pOut ) *pOut = c0;
2523         return 3;
2524     }
2525     if ( c0 == ~c1 ) //  F = i # G
2526     {
2527         if ( pOut ) *pOut = c0;
2528         return 4;
2529     }
2530     return -1;
2531 }
Abc_TtCheckOutDec(word * pTruth,int nVars,int v,word * pOut)2532 static inline int Abc_TtCheckOutDec( word * pTruth, int nVars, int v, word * pOut )
2533 {
2534     word Cof0[4], Cof1[4];
2535     int nWords = Abc_TtWordNum(nVars);
2536     assert( nVars <= 8 );
2537     Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
2538     Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
2539     assert( !Abc_TtEqual(Cof0, Cof1, nWords) );
2540     if ( Abc_TtIsConst0(Cof0, nWords) ) //if ( c0 == 0 ) //  F = i * G
2541     {
2542         if ( pOut ) Abc_TtCopy( pOut, Cof1, nWords, 0 ); //*pOut = c1;
2543         return 0;
2544     }
2545     if ( Abc_TtIsConst0(Cof1, nWords) ) //if ( c1 == 0 ) //  F = ~i * G
2546     {
2547         if ( pOut ) Abc_TtCopy( pOut, Cof0, nWords, 0 ); //*pOut = c0;
2548         return 1;
2549     }
2550     if ( Abc_TtIsConst1(Cof0, nWords) ) //if ( ~c0 == 0 ) //  F = ~i + G
2551     {
2552         if ( pOut ) Abc_TtCopy( pOut, Cof1, nWords, 0 ); //*pOut = c1;
2553         return 2;
2554     }
2555     if ( Abc_TtIsConst1(Cof1, nWords) ) //if ( ~c1 == 0 ) //  F = i + G
2556     {
2557         if ( pOut ) Abc_TtCopy( pOut, Cof0, nWords, 0 ); //*pOut = c0;
2558         return 3;
2559     }
2560     if ( Abc_TtOpposite(Cof0, Cof1, nWords) ) //if ( c0 == ~c1 )  //  F = i # G
2561     {
2562         if ( pOut ) Abc_TtCopy( pOut, Cof0, nWords, 0 ); //*pOut = c0;
2563         return 4;
2564     }
2565     return -1;
2566 }
Abc_TtCheckDecOutOne7(word * t,int * piVar,int * pType)2567 static inline word Abc_TtCheckDecOutOne7( word * t, int * piVar, int * pType )
2568 {
2569     int v, Type, Type2; word Out[2];
2570     for ( v = 6; v >= 0; v-- )
2571         if ( (Type = Abc_TtCheckOutDec(t, 7, v, NULL)) != -1 )
2572         {
2573             Abc_TtSwapVars( t, 7, 6, v );
2574             Type2 = Abc_TtCheckOutDec( t, 7, 6, Out );
2575             assert( Type == Type2 );
2576             *piVar = v;
2577             *pType = Type;
2578             return Out[0];
2579         }
2580     return 0;
2581 }
Abc_TtCheckDecOutOne8(word * t,int * piVar1,int * piVar2,int * pType1,int * pType2)2582 static inline word Abc_TtCheckDecOutOne8( word * t, int * piVar1, int * piVar2, int * pType1, int * pType2 )
2583 {
2584     int v, Type1, Type12, Type2, Type22; word Out[4], Out2[2];
2585     for ( v = 7; v >= 0; v-- )
2586         if ( (Type1 = Abc_TtCheckOutDec(t, 8, v, NULL)) != -1 )
2587         {
2588             Abc_TtSwapVars( t, 8, 7, v );
2589             Type12 = Abc_TtCheckOutDec( t, 8, 7, Out );
2590             assert( Type1 == Type12 );
2591             *piVar1 = v;
2592             *pType1 = Type1;
2593             break;
2594         }
2595     if ( v == -1 )
2596         return 0;
2597     for ( v = 6; v >= 0; v-- )
2598         if ( (Type2 = Abc_TtCheckOutDec(Out, 7, v, NULL)) != -1 && Abc_Lit2Var(Type2) == Abc_Lit2Var(Type1) )
2599         {
2600             Abc_TtSwapVars( Out, 7, 6, v );
2601             Type22 = Abc_TtCheckOutDec(Out, 7, 6, Out2);
2602             assert( Type2 == Type22 );
2603             *piVar2 = v;
2604             *pType2 = Type2;
2605             assert( *piVar2 < *piVar1 );
2606             return Out2[0];
2607         }
2608     return 0;
2609 }
2610 
2611 /**Function*************************************************************
2612 
2613   Synopsis    [Check if the function is input-decomposable with the given pair.]
2614 
2615   Description []
2616 
2617   SideEffects []
2618 
2619   SeeAlso     []
2620 
2621 ***********************************************************************/
Abc_TtCheckDsdAnd(word t,int i,int j,word * pOut)2622 static inline int Abc_TtCheckDsdAnd( word t, int i, int j, word * pOut )
2623 {
2624     word c0 = Abc_Tt6Cofactor0( t, i );
2625     word c1 = Abc_Tt6Cofactor1( t, i );
2626     word c00 = Abc_Tt6Cofactor0( c0, j );
2627     word c01 = Abc_Tt6Cofactor1( c0, j );
2628     word c10 = Abc_Tt6Cofactor0( c1, j );
2629     word c11 = Abc_Tt6Cofactor1( c1, j );
2630     if ( c00 == c01 && c00 == c10 ) //  i *  j
2631     {
2632         if ( pOut ) *pOut = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11);
2633         return 0;
2634     }
2635     if ( c11 == c00 && c11 == c10 ) //  i * !j
2636     {
2637         if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c01);
2638         return 1;
2639     }
2640     if ( c11 == c00 && c11 == c01 ) // !i *  j
2641     {
2642         if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
2643         return 2;
2644     }
2645     if ( c11 == c01 && c11 == c10 ) // !i * !j
2646     {
2647         if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c00);
2648         return 3;
2649     }
2650     if ( c00 == c11 && c01 == c10 )
2651     {
2652         if ( pOut ) *pOut = (~s_Truths6[i] & c11) | (s_Truths6[i] & c10);
2653         return 4;
2654     }
2655     return -1;
2656 }
Abc_TtCheckDsdMux(word t,int i,word * pOut)2657 static inline int Abc_TtCheckDsdMux( word t, int i, word * pOut )
2658 {
2659     word c0 = Abc_Tt6Cofactor0( t, i );
2660     word c1 = Abc_Tt6Cofactor1( t, i );
2661     word c00, c01, c10, c11;
2662     int k, fPres0, fPres1, iVar0 = -1, iVar1 = -1;
2663     for ( k = 0; k < 6; k++ )
2664     {
2665         if ( k == i ) continue;
2666         fPres0 = Abc_Tt6HasVar( c0, k );
2667         fPres1 = Abc_Tt6HasVar( c1, k );
2668         if ( fPres0 && !fPres1 )
2669         {
2670             if ( iVar0 >= 0 )
2671                 return -1;
2672             iVar0 = k;
2673         }
2674         if ( !fPres0 && fPres1 )
2675         {
2676             if ( iVar1 >= 0 )
2677                 return -1;
2678             iVar1 = k;
2679         }
2680     }
2681     if ( iVar0 == -1 || iVar1 == -1 )
2682         return -1;
2683     c00 = Abc_Tt6Cofactor0( c0, iVar0 );
2684     c01 = Abc_Tt6Cofactor1( c0, iVar0 );
2685     c10 = Abc_Tt6Cofactor0( c1, iVar1 );
2686     c11 = Abc_Tt6Cofactor1( c1, iVar1 );
2687     if ( c00 ==  c10 && c01 ==  c11 ) //  ITE(i,  iVar1,  iVar0)
2688     {
2689         if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
2690         return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 0);
2691     }
2692     if ( c00 == ~c10 && c01 == ~c11 ) //  ITE(i,  iVar1, !iVar0)
2693     {
2694         if ( pOut ) *pOut = (~s_Truths6[i] & c10) | (s_Truths6[i] & c11);
2695         return (Abc_Var2Lit(iVar1, 0) << 16) | Abc_Var2Lit(iVar0, 1);
2696     }
2697     return -1;
2698 }
Unm_ManCheckTest2()2699 static inline void Unm_ManCheckTest2()
2700 {
2701     word t, t1, Out, Var0, Var1, Var0_, Var1_;
2702     int iVar0, iVar1, i, Res;
2703     for ( iVar0 = 0; iVar0 < 6; iVar0++ )
2704     for ( iVar1 = 0; iVar1 < 6; iVar1++ )
2705     {
2706         if ( iVar0 == iVar1 )
2707             continue;
2708         Var0 = s_Truths6[iVar0];
2709         Var1 = s_Truths6[iVar1];
2710         for ( i = 0; i < 5; i++ )
2711         {
2712             Var0_ = ((i >> 0) & 1) ? ~Var0 : Var0;
2713             Var1_ = ((i >> 1) & 1) ? ~Var1 : Var1;
2714 
2715             t = Var0_ & Var1_;
2716             if ( i == 4 )
2717                 t = ~(Var0_ ^ Var1_);
2718 
2719 //            Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
2720 
2721             Res = Abc_TtCheckDsdAnd( t, iVar0, iVar1, &Out );
2722             if ( Res == -1 )
2723             {
2724                 printf( "No decomposition\n" );
2725                 continue;
2726             }
2727 
2728             Var0_ = s_Truths6[iVar0];
2729             Var0_ = ((Res >> 0) & 1) ? ~Var0_ : Var0_;
2730 
2731             Var1_ = s_Truths6[iVar1];
2732             Var1_ = ((Res >> 1) & 1) ? ~Var1_ : Var1_;
2733 
2734             t1 = Var0_ & Var1_;
2735             if ( Res == 4 )
2736                 t1 = Var0_ ^ Var1_;
2737 
2738             t1 = (~t1 & Abc_Tt6Cofactor0(Out, iVar0)) | (t1 & Abc_Tt6Cofactor1(Out, iVar0));
2739 
2740 //            Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
2741 
2742             if ( t1 != t )
2743                 printf( "Verification failed.\n" );
2744             else
2745                 printf( "Verification succeeded.\n" );
2746         }
2747     }
2748 }
Unm_ManCheckTest()2749 static inline void Unm_ManCheckTest()
2750 {
2751     word t, t1, Out, Ctrl, Var0, Var1, Ctrl_, Var0_, Var1_;
2752     int iVar0, iVar1, iCtrl, i, Res;
2753     for ( iCtrl = 0; iCtrl < 6; iCtrl++ )
2754     for ( iVar0 = 0; iVar0 < 6; iVar0++ )
2755     for ( iVar1 = 0; iVar1 < 6; iVar1++ )
2756     {
2757         if ( iCtrl == iVar0 || iCtrl == iVar1 || iVar0 == iVar1 )
2758             continue;
2759         Ctrl = s_Truths6[iCtrl];
2760         Var0 = s_Truths6[iVar0];
2761         Var1 = s_Truths6[iVar1];
2762         for ( i = 0; i < 8; i++ )
2763         {
2764             Ctrl_ = ((i >> 0) & 1) ? ~Ctrl : Ctrl;
2765             Var0_ = ((i >> 1) & 1) ? ~Var0 : Var0;
2766             Var1_ = ((i >> 2) & 1) ? ~Var1 : Var1;
2767 
2768             t = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
2769 
2770 //            Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ), printf( "\n" );
2771 
2772             Res = Abc_TtCheckDsdMux( t, iCtrl, &Out );
2773             if ( Res == -1 )
2774             {
2775                 printf( "No decomposition\n" );
2776                 continue;
2777             }
2778 
2779 //            Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
2780 
2781             Ctrl_ = s_Truths6[iCtrl];
2782             Var0_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
2783             Var0_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var0_ : Var0_;
2784 
2785             Res >>= 16;
2786             Var1_ = s_Truths6[Abc_Lit2Var(Res & 0xFFFF)];
2787             Var1_ = Abc_LitIsCompl(Res & 0xFFFF) ? ~Var1_ : Var1_;
2788 
2789             t1 = (~Ctrl_ & Var0_) | (Ctrl_ & Var1_);
2790 
2791 //            Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
2792 //            Kit_DsdPrintFromTruth( (unsigned *)&Out, 6 ), printf( "\n" );
2793 
2794             t1 = (~t1 & Abc_Tt6Cofactor0(Out, iCtrl)) | (t1 & Abc_Tt6Cofactor1(Out, iCtrl));
2795 
2796 //            Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ), printf( "\n" );
2797 
2798             if ( t1 != t )
2799                 printf( "Verification failed.\n" );
2800             else
2801                 printf( "Verification succeeded.\n" );
2802         }
2803     }
2804 }
2805 
2806 
2807 /**Function*************************************************************
2808 
2809   Synopsis    [Truth table evaluation.]
2810 
2811   Description []
2812 
2813   SideEffects []
2814 
2815   SeeAlso     []
2816 
2817 ***********************************************************************/
Abc_TtEvalLut6(word Ins[6],word Lut,int nVars)2818 static inline word Abc_TtEvalLut6( word Ins[6], word Lut, int nVars )
2819 {
2820     word Cube, Res = 0; int k, i;
2821     for ( k = 0; k < (1<<nVars); k++ )
2822     {
2823         if ( ((Lut >> k) & 1) == 0 )
2824             continue;
2825         Cube = ~(word)0;
2826         for ( i = 0; i < nVars; i++ )
2827             Cube &= ((k >> i) & 1) ? Ins[i] : ~Ins[i];
2828         Res |= Cube;
2829     }
2830     return Res;
2831 }
Abc_TtEvalLut5(unsigned Ins[5],int Lut,int nVars)2832 static inline unsigned Abc_TtEvalLut5( unsigned Ins[5], int Lut, int nVars )
2833 {
2834     unsigned Cube, Res = 0; int k, i;
2835     for ( k = 0; k < (1<<nVars); k++ )
2836     {
2837         if ( ((Lut >> k) & 1) == 0 )
2838             continue;
2839         Cube = ~(unsigned)0;
2840         for ( i = 0; i < nVars; i++ )
2841             Cube &= ((k >> i) & 1) ? Ins[i] : ~Ins[i];
2842         Res |= Cube;
2843     }
2844     return Res;
2845 }
Abc_TtEvalLut4(int Ins[4],int Lut,int nVars)2846 static inline int Abc_TtEvalLut4( int Ins[4], int Lut, int nVars )
2847 {
2848     int Cube, Res = 0; int k, i;
2849     for ( k = 0; k < (1<<nVars); k++ )
2850     {
2851         if ( ((Lut >> k) & 1) == 0 )
2852             continue;
2853         Cube = ~(int)0;
2854         for ( i = 0; i < nVars; i++ )
2855             Cube &= ((k >> i) & 1) ? Ins[i] : ~Ins[i];
2856         Res |= Cube;
2857     }
2858     return Res & ~(~0 << (1<<nVars));
2859 }
2860 
2861 
2862 /**Function*************************************************************
2863 
2864   Synopsis    [Checks existence of bi-decomposition.]
2865 
2866   Description []
2867 
2868   SideEffects []
2869 
2870   SeeAlso     []
2871 
2872 ***********************************************************************/
Abc_TtComputeGraph(word * pTruth,int v,int nVars,int * pGraph)2873 static inline void Abc_TtComputeGraph( word * pTruth, int v, int nVars, int * pGraph )
2874 {
2875     word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 )
2876     word Cof00[64], Cof01[64], Cof10[64], Cof11[64];
2877     word CofXor, CofAndTest;
2878     int i, w, nWords = Abc_TtWordNum(nVars);
2879     pGraph[v] |= (1 << v);
2880     if ( v == nVars - 1 )
2881         return;
2882     assert( v < nVars - 1 );
2883     Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
2884     Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
2885     for ( i = v + 1; i < nVars; i++ )
2886     {
2887         Abc_TtCofactor0p( Cof00, Cof0, nWords, i );
2888         Abc_TtCofactor1p( Cof01, Cof0, nWords, i );
2889         Abc_TtCofactor0p( Cof10, Cof1, nWords, i );
2890         Abc_TtCofactor1p( Cof11, Cof1, nWords, i );
2891         for ( w = 0; w < nWords; w++ )
2892         {
2893             CofXor     =  Cof00[w] ^ Cof01[w]  ^  Cof10[w] ^ Cof11[w];
2894             CofAndTest = (Cof00[w] & Cof01[w]) | (Cof10[w] & Cof11[w]);
2895             if ( CofXor & CofAndTest )
2896             {
2897                 pGraph[v] |= (1 << i);
2898                 pGraph[i] |= (1 << v);
2899             }
2900             else if ( CofXor & ~CofAndTest )
2901             {
2902                 pGraph[v] |= (1 << (16+i));
2903                 pGraph[i] |= (1 << (16+v));
2904             }
2905         }
2906     }
2907 }
Abc_TtPrintVarSet(int Mask,int nVars)2908 static inline void Abc_TtPrintVarSet( int Mask, int nVars )
2909 {
2910     int i;
2911     for ( i = 0; i < nVars; i++ )
2912         if ( (Mask >> i) & 1 )
2913             printf( "1" );
2914         else
2915             printf( "." );
2916 }
Abc_TtPrintBiDec(word * pTruth,int nVars)2917 static inline void Abc_TtPrintBiDec( word * pTruth, int nVars )
2918 {
2919     int v, pGraph[12] = {0};
2920     assert( nVars <= 12 );
2921     for ( v = 0; v < nVars; v++ )
2922     {
2923         Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
2924         Abc_TtPrintVarSet( pGraph[v], nVars );
2925         printf( "    " );
2926         Abc_TtPrintVarSet( pGraph[v] >> 16, nVars );
2927         printf( "\n" );
2928     }
2929 }
Abc_TtVerifyBiDec(word * pTruth,int nVars,int This,int That,int nSuppLim,word wThis,word wThat)2930 static inline int Abc_TtVerifyBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word wThis, word wThat )
2931 {
2932     int pVarsThis[12], pVarsThat[12], pVarsAll[12];
2933     int nThis = Abc_TtBitCount16(This);
2934     int nThat = Abc_TtBitCount16(That);
2935     int i, k, nWords = Abc_TtWordNum(nVars);
2936     word pThis[64] = {wThis}, pThat[64] = {wThat};
2937     assert( nVars <= 12 );
2938     for ( i = 0; i < nVars; i++ )
2939         pVarsAll[i] = i;
2940     for ( i = k = 0; i < nVars; i++ )
2941         if ( (This >> i) & 1 )
2942             pVarsThis[k++] = i;
2943     assert( k == nThis );
2944     for ( i = k = 0; i < nVars; i++ )
2945         if ( (That >> i) & 1 )
2946             pVarsThat[k++] = i;
2947     assert( k == nThat );
2948     Abc_TtStretch6( pThis, nThis, nVars );
2949     Abc_TtStretch6( pThat, nThat, nVars );
2950     Abc_TtExpand( pThis, nVars, pVarsThis, nThis, pVarsAll, nVars );
2951     Abc_TtExpand( pThat, nVars, pVarsThat, nThat, pVarsAll, nVars );
2952     for ( k = 0; k < nWords; k++ )
2953         if ( pTruth[k] != (pThis[k] & pThat[k]) )
2954             return 0;
2955     return 1;
2956 }
Abc_TtExist(word * pTruth,int iVar,int nWords)2957 static inline void Abc_TtExist( word * pTruth, int iVar, int nWords )
2958 {
2959     word Cof0[64], Cof1[64];
2960     Abc_TtCofactor0p( Cof0, pTruth, nWords, iVar );
2961     Abc_TtCofactor1p( Cof1, pTruth, nWords, iVar );
2962     Abc_TtOr( pTruth, Cof0, Cof1, nWords );
2963 }
Abc_TtCheckBiDec(word * pTruth,int nVars,int This,int That)2964 static inline int Abc_TtCheckBiDec( word * pTruth, int nVars, int This, int That )
2965 {
2966     int VarMask[2] = {This & ~That, That & ~This};
2967     int v, c, nWords = Abc_TtWordNum(nVars);
2968     word pTempR[2][64];
2969     for ( c = 0; c < 2; c++ )
2970     {
2971         Abc_TtCopy( pTempR[c], pTruth, nWords, 0 );
2972         for ( v = 0; v < nVars; v++ )
2973             if ( ((VarMask[c] >> v) & 1) )
2974                 Abc_TtExist( pTempR[c], v, nWords );
2975     }
2976     for ( v = 0; v < nWords; v++ )
2977         if ( ~pTruth[v] & pTempR[0][v] & pTempR[1][v] )
2978             return 0;
2979     return 1;
2980 }
Abc_TtDeriveBiDecOne(word * pTruth,int nVars,int This)2981 static inline word Abc_TtDeriveBiDecOne( word * pTruth, int nVars, int This )
2982 {
2983     word pTemp[64];
2984     int nThis = Abc_TtBitCount16(This);
2985     int v, nWords = Abc_TtWordNum(nVars);
2986     Abc_TtCopy( pTemp, pTruth, nWords, 0 );
2987     for ( v = 0; v < nVars; v++ )
2988         if ( !((This >> v) & 1) )
2989             Abc_TtExist( pTemp, v, nWords );
2990     Abc_TtShrink( pTemp, nThis, nVars, This );
2991     return Abc_Tt6Stretch( pTemp[0], nThis );
2992 }
Abc_TtDeriveBiDec(word * pTruth,int nVars,int This,int That,int nSuppLim,word * pThis,word * pThat)2993 static inline void Abc_TtDeriveBiDec( word * pTruth, int nVars, int This, int That, int nSuppLim, word * pThis, word * pThat )
2994 {
2995     assert( Abc_TtBitCount16(This) <= nSuppLim );
2996     assert( Abc_TtBitCount16(That) <= nSuppLim );
2997     pThis[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, This );
2998     pThat[0] = Abc_TtDeriveBiDecOne( pTruth, nVars, That );
2999     if ( !Abc_TtVerifyBiDec(pTruth, nVars, This, That, nSuppLim, pThis[0], pThat[0] ) )
3000         printf( "Bi-decomposition verification failed.\n" );
3001 }
3002 // detect simple case of decomposition with topmost AND gate
Abc_TtCheckBiDecSimple(word * pTruth,int nVars,int nSuppLim)3003 static inline int Abc_TtCheckBiDecSimple( word * pTruth, int nVars, int nSuppLim )
3004 {
3005     word Cof0[64], Cof1[64];
3006     int v, Res = 0, nDecVars = 0, nWords = Abc_TtWordNum(nVars);
3007     for ( v = 0; v < nVars; v++ )
3008     {
3009         Abc_TtCofactor0p( Cof0, pTruth, nWords, v );
3010         Abc_TtCofactor1p( Cof1, pTruth, nWords, v );
3011         if ( !Abc_TtIsConst0(Cof0, nWords) && !Abc_TtIsConst0(Cof1, nWords) )
3012             continue;
3013         nDecVars++;
3014         Res |= 1 << v;
3015         if ( nDecVars >= nVars - nSuppLim )
3016             return ((Res ^ (int)Abc_Tt6Mask(nVars)) << 16) | Res;
3017     }
3018     return 0;
3019 }
Abc_TtProcessBiDecInt(word * pTruth,int nVars,int nSuppLim)3020 static inline int Abc_TtProcessBiDecInt( word * pTruth, int nVars, int nSuppLim )
3021 {
3022     int i, v, Res, nSupp, CountShared = 0, pGraph[12] = {0};
3023     assert( nSuppLim < nVars && nVars <= 2 * nSuppLim && nVars <= 12 );
3024     assert( 2 <= nSuppLim && nSuppLim <= 6 );
3025     Res = Abc_TtCheckBiDecSimple( pTruth, nVars, nSuppLim );
3026     if ( Res )
3027         return Res;
3028     for ( v = 0; v < nVars; v++ )
3029     {
3030         Abc_TtComputeGraph( pTruth, v, nVars, pGraph );
3031         nSupp = Abc_TtBitCount16(pGraph[v] & 0xFFFF);
3032         if ( nSupp > nSuppLim )
3033         {
3034             // this variable is shared - check if the limit is exceeded
3035             if ( ++CountShared > 2*nSuppLim - nVars )
3036                 return 0;
3037         }
3038         else if ( nVars - nSupp <= nSuppLim )
3039         {
3040             int This = pGraph[v] & 0xFFFF;
3041             int That = This ^ (int)Abc_Tt6Mask(nVars);
3042             // find the other component
3043             int Graph = That;
3044             for ( i = 0; i < nVars; i++ )
3045                 if ( (That >> i) & 1 )
3046                     Graph |= pGraph[i] & 0xFFFF;
3047             // check if this can be done
3048             if ( Abc_TtBitCount16(Graph) > nSuppLim )
3049                 continue;
3050             // try decomposition
3051             if ( Abc_TtCheckBiDec(pTruth, nVars, This, Graph) )
3052                 return (Graph << 16) | This;
3053         }
3054     }
3055     return 0;
3056 }
Abc_TtProcessBiDec(word * pTruth,int nVars,int nSuppLim)3057 static inline int Abc_TtProcessBiDec( word * pTruth, int nVars, int nSuppLim )
3058 {
3059     word pFunc[64];
3060     int Res, nWords = Abc_TtWordNum(nVars);
3061     Abc_TtCopy( pFunc, pTruth, nWords, 0 );
3062     Res = Abc_TtProcessBiDecInt( pFunc, nVars, nSuppLim );
3063     if ( Res )
3064         return Res;
3065     Abc_TtCopy( pFunc, pTruth, nWords, 1 );
3066     Res = Abc_TtProcessBiDecInt( pFunc, nVars, nSuppLim );
3067     if ( Res )
3068         return Res | (1 << 30);
3069     return 0;
3070 }
3071 
3072 /**Function*************************************************************
3073 
3074   Synopsis    [Tests decomposition procedures.]
3075 
3076   Description []
3077 
3078   SideEffects []
3079 
3080   SeeAlso     []
3081 
3082 ***********************************************************************/
Abc_TtProcessBiDecTest(word * pTruth,int nVars,int nSuppLim)3083 static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLim )
3084 {
3085     word This, That, pTemp[64];
3086     int Res, resThis, resThat;//, nThis, nThat;
3087     int nWords = Abc_TtWordNum(nVars);
3088     Abc_TtCopy( pTemp, pTruth, nWords, 0 );
3089     Res = Abc_TtProcessBiDec( pTemp, nVars, nSuppLim );
3090     if ( Res == 0 )
3091     {
3092         //Dau_DsdPrintFromTruth( pTemp, nVars );
3093         //printf( "Non_dec\n\n" );
3094         return;
3095     }
3096 
3097     resThis = Res & 0xFFFF;
3098     resThat = Res >> 16;
3099 
3100     Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
3101     return;
3102 
3103     //if ( !(resThis & resThat) )
3104     //    return;
3105 
3106 //    Dau_DsdPrintFromTruth( pTemp, nVars );
3107 
3108     //nThis = Abc_TtBitCount16(resThis);
3109     //nThat = Abc_TtBitCount16(resThat);
3110 
3111     printf( "Variable sets:    " );
3112     Abc_TtPrintVarSet( resThis, nVars );
3113     printf( "    " );
3114     Abc_TtPrintVarSet( resThat, nVars );
3115     printf( "\n" );
3116     Abc_TtDeriveBiDec( pTemp, nVars, resThis, resThat, nSuppLim, &This, &That );
3117 //    Dau_DsdPrintFromTruth( &This, nThis );
3118 //    Dau_DsdPrintFromTruth( &That, nThat );
3119     printf( "\n" );
3120 }
Abc_TtProcessBiDecExperiment()3121 static inline void Abc_TtProcessBiDecExperiment()
3122 {
3123     int nVars = 3;
3124     int nSuppLim = 2;
3125     int Res, resThis, resThat;
3126     word This, That;
3127 //    word t = ABC_CONST(0x8000000000000000);
3128 //    word t = (s_Truths6[0] | s_Truths6[1]) & (s_Truths6[2] | s_Truths6[3] | s_Truths6[4] | s_Truths6[5]);
3129 //    word t = ((s_Truths6[0] & s_Truths6[1]) | (~s_Truths6[1] & s_Truths6[2]));
3130     word t = ((s_Truths6[0] | s_Truths6[1]) & (s_Truths6[1] | s_Truths6[2]));
3131     Abc_TtPrintBiDec( &t, nVars );
3132     Res = Abc_TtProcessBiDec( &t, nVars, nSuppLim );
3133     resThis = Res & 0xFFFF;
3134     resThat = Res >> 16;
3135     Abc_TtDeriveBiDec( &t, nVars, resThis, resThat, nSuppLim, &This, &That );
3136 //    Dau_DsdPrintFromTruth( &This, Abc_TtBitCount16(resThis) );
3137 //    Dau_DsdPrintFromTruth( &That, Abc_TtBitCount16(resThat) );
3138     nVars = nSuppLim;
3139 }
3140 
3141 /**Function*************************************************************
3142 
3143   Synopsis    [Truth table checking procedure.]
3144 
3145   Description []
3146 
3147   SideEffects []
3148 
3149   SeeAlso     []
3150 
3151 ***********************************************************************/
Abc_Tt4Equal3(int c0,int c1,int c2,int c3)3152 static inline int Abc_Tt4Equal3( int c0, int c1, int c2, int c3 )
3153 {
3154     if ( c0 == c1 && c0 == c2 ) return 3;
3155     if ( c0 == c1 && c0 == c3 ) return 2;
3156     if ( c0 == c3 && c0 == c2 ) return 1;
3157     if ( c3 == c1 && c3 == c2 ) return 0;
3158     return -1;
3159 }
Abc_Tt4Check2(int t,int i,int j,int * f,int * r)3160 static inline int Abc_Tt4Check2( int t, int i, int j, int * f, int * r )
3161 {
3162     int c0  =  t & r[j];
3163     int c1  = (t & f[j]) >> (1 << j);
3164     int c00 =  c0 & r[i];
3165     int c01 = (c0 & f[i]) >> (1 << i);
3166     int c10 =  c1 & r[i];
3167     int c11 = (c1 & f[i]) >> (1 << i);
3168     return Abc_Tt4Equal3( c00, c01, c10, c11 );
3169 }
Abc_Tt4CheckTwoLevel(int t)3170 static inline int Abc_Tt4CheckTwoLevel( int t )
3171 {
3172     int pair1, pair2;
3173     int f[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
3174     int r[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF };
3175     if ( (pair1 = Abc_Tt4Check2(t, 0, 1, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 2, 3, f, r)) >= 0 ) return (1 << 4) | (pair2 << 2) | pair1;
3176     if ( (pair1 = Abc_Tt4Check2(t, 0, 2, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 1, 3, f, r)) >= 0 ) return (2 << 4) | (pair2 << 2) | pair1;
3177     if ( (pair1 = Abc_Tt4Check2(t, 0, 3, f, r)) >= 0 && (pair2 = Abc_Tt4Check2(t, 1, 2, f, r)) >= 0 ) return (3 << 4) | (pair2 << 2) | pair1;
3178     return -1;
3179 }
Abc_Tt4CountOnes(int t)3180 static inline int Abc_Tt4CountOnes( int t )
3181 {
3182     t = (t & (0x5555)) + ((t >> 1) & (0x5555));
3183     t = (t & (0x3333)) + ((t >> 2) & (0x3333));
3184     t = (t & (0x0f0f)) + ((t >> 4) & (0x0f0f));
3185     t = (t & (0x00ff)) + ((t >> 8) & (0x00ff));
3186     return t;
3187 }
Abc_Tt4FirstBit(int t)3188 static inline int Abc_Tt4FirstBit( int t )
3189 {
3190     int n = 0;
3191     if ( t == 0 ) return -1;
3192     if ( (t & 0x00FF) == 0 ) { n +=  8; t >>=  8; }
3193     if ( (t & 0x000F) == 0 ) { n +=  4; t >>=  4; }
3194     if ( (t & 0x0003) == 0 ) { n +=  2; t >>=  2; }
3195     if ( (t & 0x0001) == 0 ) { n++; }
3196     return n;
3197 }
Abc_Tt4Check(int t)3198 static inline int Abc_Tt4Check( int t )
3199 {
3200     int Count, tn = 0xFFFF & ~t;
3201     if ( t == 0x6996 || tn == 0x6996 ) return 1;
3202     if ( (t & (t-1)) == 0 )            return 1;
3203     if ( (tn & (tn-1)) == 0 )          return 1;
3204     Count = Abc_Tt4CountOnes( t );
3205     if ( Count == 7 && Abc_Tt4CheckTwoLevel(t)  > 0 ) return 1;
3206     if ( Count == 9 && Abc_Tt4CheckTwoLevel(tn) > 0 ) return 1;
3207     return 0;
3208 }
3209 
3210 
3211 /**Function*************************************************************
3212 
3213   Synopsis    [Returns symmetry profile of the function.]
3214 
3215   Description []
3216 
3217   SideEffects []
3218 
3219   SeeAlso     []
3220 
3221 ***********************************************************************/
Abc_Tt6VarsAreSymmetric(word t,int iVar,int jVar)3222 static inline int Abc_Tt6VarsAreSymmetric( word t, int iVar, int jVar )
3223 {
3224     word * s_PMasks = s_PPMasks[iVar][jVar];
3225     int shift = (1 << jVar) - (1 << iVar);
3226     assert( iVar < jVar );
3227     return ((t & s_PMasks[1]) << shift) == (t & s_PMasks[2]);
3228 }
Abc_Tt6VarsAreAntiSymmetric(word t,int iVar,int jVar)3229 static inline int Abc_Tt6VarsAreAntiSymmetric( word t, int iVar, int jVar )
3230 {
3231     word * s_PMasks = s_PPMasks[iVar][jVar];
3232     int shift = (1 << jVar) + (1 << iVar);
3233     assert( iVar < jVar );
3234     return ((t & (s_PMasks[1] >> (1 << iVar))) << shift) == (t & (s_PMasks[2] << (1 << iVar)));
3235 }
Abc_TtVarsAreSymmetric(word * pTruth,int nVars,int i,int j,word * pCof0,word * pCof1)3236 static inline int Abc_TtVarsAreSymmetric( word * pTruth, int nVars, int i, int j, word * pCof0, word * pCof1 )
3237 {
3238     int nWords = Abc_TtWordNum( nVars );
3239     assert( i < nVars && j < nVars );
3240     Abc_TtCofactor0p( pCof0, pTruth, nWords, i );
3241     Abc_TtCofactor1p( pCof1, pTruth, nWords, i );
3242     Abc_TtCofactor1( pCof0, nWords, j );
3243     Abc_TtCofactor0( pCof1, nWords, j );
3244     return Abc_TtEqual( pCof0, pCof1, nWords );
3245 }
Abc_TtVarsAreAntiSymmetric(word * pTruth,int nVars,int i,int j,word * pCof0,word * pCof1)3246 static inline int Abc_TtVarsAreAntiSymmetric( word * pTruth, int nVars, int i, int j, word * pCof0, word * pCof1 )
3247 {
3248     int nWords = Abc_TtWordNum( nVars );
3249     assert( i < nVars && j < nVars );
3250     Abc_TtCofactor0p( pCof0, pTruth, nWords, i );
3251     Abc_TtCofactor1p( pCof1, pTruth, nWords, i );
3252     Abc_TtCofactor0( pCof0, nWords, j );
3253     Abc_TtCofactor1( pCof1, nWords, j );
3254     return Abc_TtEqual( pCof0, pCof1, nWords );
3255 }
Abc_TtIsFullySymmetric(word * pTruth,int nVars)3256 static inline int Abc_TtIsFullySymmetric( word * pTruth, int nVars )
3257 {
3258     int m, v, Polar = 0, Seen = 0;
3259     for ( m = 0; m < (1<<nVars); m++ )
3260     {
3261         int Count = 0;
3262         int Value = Abc_TtGetBit( pTruth, m );
3263         for ( v = 0; v < nVars; v++ )
3264             Count += ((m >> v) & 1);
3265         if ( (Seen >> Count) & 1 ) // seen this count
3266         {
3267             if ( Value != ((Polar >> Count) & 1) )
3268                 return -1;
3269         }
3270         else // new count
3271         {
3272             Seen  |= 1 << Count;
3273             if ( Value )
3274                 Polar |= 1 << Count;
3275         }
3276     }
3277     return Polar;
3278 }
Abc_TtGenFullySymmetric(word * pTruth,int nVars,int Polar)3279 static inline void Abc_TtGenFullySymmetric( word * pTruth, int nVars, int Polar )
3280 {
3281     int m, v, nWords = Abc_TtWordNum( nVars );
3282     Abc_TtClear( pTruth, nWords );
3283     for ( m = 0; m < (1<<nVars); m++ )
3284     {
3285         int Count = 0;
3286         for ( v = 0; v < nVars; v++ )
3287             Count += ((m >> v) & 1);
3288         if ( (Polar >> Count) & 1 )
3289             Abc_TtSetBit( pTruth, m );
3290     }
3291 }
Abc_TtTestFullySymmetric()3292 static inline void Abc_TtTestFullySymmetric()
3293 {
3294     word pTruth[4]; // 8-var function
3295     int PolarOut, PolarIn = 271;
3296     Abc_TtGenFullySymmetric( pTruth, 8, PolarIn );
3297     //Abc_TtXorBit( pTruth, 171 );
3298     PolarOut = Abc_TtIsFullySymmetric( pTruth, 8 );
3299     assert( PolarIn == PolarOut );
3300 }
3301 
3302 
3303 /**Function*************************************************************
3304 
3305   Synopsis    [Generates truth table of a symmetric function.]
3306 
3307   Description []
3308 
3309   SideEffects []
3310 
3311   SeeAlso     []
3312 
3313 ***********************************************************************/
Abc_TtSymFunGenerate(char * pOnes,int nVars)3314 static inline word * Abc_TtSymFunGenerate( char * pOnes, int nVars )
3315 {
3316     int m, k, Count;
3317     word * pTruth = ABC_CALLOC( word, Abc_TtWordNum(nVars) );
3318     assert( (int)strlen(pOnes) == nVars + 1 );
3319     for ( m = 0; m < (1 << nVars); m++ )
3320     {
3321         Count = 0;
3322         for ( k = 0; k < nVars; k++ )
3323             Count += (m >> k) & 1;
3324         if ( pOnes[Count] == '1' )
3325             Abc_TtXorBit( pTruth, m );
3326     }
3327     return pTruth;
3328 }
3329 
3330 
3331 ABC_NAMESPACE_HEADER_END
3332 
3333 #endif
3334 
3335 ////////////////////////////////////////////////////////////////////////
3336 ///                       END OF FILE                                ///
3337 ////////////////////////////////////////////////////////////////////////
3338