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