1 /**CFile****************************************************************
2 
3   FileName    [exp.h]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Boolean expression.]
8 
9   Synopsis    [External declarations.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: exp.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__map__mio__exp_h
22 #define ABC__map__mio__exp_h
23 
24 ////////////////////////////////////////////////////////////////////////
25 ///                          INCLUDES                                ///
26 ////////////////////////////////////////////////////////////////////////
27 
28 ////////////////////////////////////////////////////////////////////////
29 ///                         PARAMETERS                               ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 
33 ABC_NAMESPACE_HEADER_START
34 
35 ////////////////////////////////////////////////////////////////////////
36 ///                         BASIC TYPES                              ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 ////////////////////////////////////////////////////////////////////////
40 ///                      MACRO DEFINITIONS                           ///
41 ////////////////////////////////////////////////////////////////////////
42 
43 #define EXP_CONST0 -1
44 #define EXP_CONST1 -2
45 
Exp_Const0()46 static inline Vec_Int_t * Exp_Const0()
47 {
48     Vec_Int_t * vExp;
49     vExp = Vec_IntAlloc( 1 );
50     Vec_IntPush( vExp, EXP_CONST0 );
51     return vExp;
52 }
Exp_Const1()53 static inline Vec_Int_t * Exp_Const1()
54 {
55     Vec_Int_t * vExp;
56     vExp = Vec_IntAlloc( 1 );
57     Vec_IntPush( vExp, EXP_CONST1 );
58     return vExp;
59 }
Exp_IsConst(Vec_Int_t * p)60 static inline int Exp_IsConst( Vec_Int_t * p )
61 {
62     return Vec_IntEntry(p,0) == EXP_CONST0 || Vec_IntEntry(p,0) == EXP_CONST1;
63 }
Exp_IsConst0(Vec_Int_t * p)64 static inline int Exp_IsConst0( Vec_Int_t * p )
65 {
66     return Vec_IntEntry(p,0) == EXP_CONST0;
67 }
Exp_IsConst1(Vec_Int_t * p)68 static inline int Exp_IsConst1( Vec_Int_t * p )
69 {
70     return Vec_IntEntry(p,0) == EXP_CONST1;
71 }
Exp_Var(int iVar)72 static inline Vec_Int_t * Exp_Var( int iVar )
73 {
74     Vec_Int_t * vExp;
75     vExp = Vec_IntAlloc( 1 );
76     Vec_IntPush( vExp, 2 * iVar );
77     return vExp;
78 }
Exp_LitShift(int nVars,int Lit,int Shift)79 static inline int Exp_LitShift( int nVars, int Lit, int Shift )
80 {
81     if ( Lit < 2 * nVars )
82         return Lit;
83     return Lit + 2 * Shift;
84 }
Exp_IsLit(Vec_Int_t * p)85 static inline int Exp_IsLit( Vec_Int_t * p )
86 {
87     return Vec_IntSize(p) == 1 && !Exp_IsConst(p);
88 }
Exp_NodeNum(Vec_Int_t * p)89 static inline int Exp_NodeNum( Vec_Int_t * p )
90 {
91     return Vec_IntSize(p)/2;
92 }
Exp_Not(Vec_Int_t * p)93 static inline Vec_Int_t * Exp_Not( Vec_Int_t * p )
94 {
95     Vec_IntWriteEntry( p, 0, Vec_IntEntry(p,0) ^ 1 );
96     return p;
97 }
Exp_PrintLit(int nVars,int Lit)98 static inline void Exp_PrintLit( int nVars, int Lit )
99 {
100     if ( Lit == EXP_CONST0 )
101         Abc_Print( 1, "Const0" );
102     else if ( Lit == EXP_CONST1 )
103         Abc_Print( 1, "Const1" );
104     else if ( Lit < 2 * nVars )
105         Abc_Print( 1, "%s%c", (Lit&1) ? "!" : " ", 'a' + Lit/2 );
106     else
107         Abc_Print( 1, "%s%d", (Lit&1) ? "!" : " ", Lit/2 );
108 }
Exp_Print(int nVars,Vec_Int_t * p)109 static inline void Exp_Print( int nVars, Vec_Int_t * p )
110 {
111     int i;
112     for ( i = 0; i < Exp_NodeNum(p); i++ )
113     {
114         Abc_Print( 1, "%2d = ", nVars + i );
115         Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+0) );
116         Abc_Print( 1, " & " );
117         Exp_PrintLit( nVars, Vec_IntEntry(p, 2*i+1) );
118         Abc_Print( 1, "\n" );
119     }
120     Abc_Print( 1, " F = " );
121     Exp_PrintLit( nVars, Vec_IntEntryLast(p) );
122     Abc_Print( 1, "\n" );
123 }
Exp_Reverse(Vec_Int_t * p)124 static inline Vec_Int_t * Exp_Reverse( Vec_Int_t * p )
125 {
126     Vec_IntReverseOrder( p );
127     return p;
128 }
Exp_PrintReverse(int nVars,Vec_Int_t * p)129 static inline void Exp_PrintReverse( int nVars, Vec_Int_t * p )
130 {
131     Exp_Reverse( p );
132     Exp_Print( nVars, p );
133     Exp_Reverse( p );
134 }
Exp_And(int * pMan,int nVars,Vec_Int_t * p0,Vec_Int_t * p1,int fCompl0,int fCompl1)135 static inline Vec_Int_t * Exp_And( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1, int fCompl0, int fCompl1 )
136 {
137     int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
138     Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 1 );
139     assert( (Len0 & 1) && (Len1 & 1) );
140     Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2) );
141     Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ fCompl0, Len1/2 ) );
142     Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ fCompl1 );
143     for ( i = 1; i < Len0; i++ )
144         Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
145     for ( i = 1; i < Len1; i++ )
146         Vec_IntPush( r, Vec_IntEntry(p1, i) );
147     assert( Vec_IntSize(r) == Len0 + Len1 + 1 );
148     return r;
149 }
Exp_Or(int * pMan,int nVars,Vec_Int_t * p0,Vec_Int_t * p1)150 static inline Vec_Int_t * Exp_Or( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
151 {
152     return Exp_Not( Exp_And(pMan, nVars, p0, p1, 1, 1) );
153 }
Exp_Xor(int * pMan,int nVars,Vec_Int_t * p0,Vec_Int_t * p1)154 static inline Vec_Int_t * Exp_Xor( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
155 {
156     int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
157     Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 5 );
158     assert( (Len0 & 1) && (Len1 & 1) );
159     Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 2)     );
160     Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 1) + 1 );
161     Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 0) + 1 );
162     Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0) ^ 1, Len1/2 ) );
163     Vec_IntPush( r, Vec_IntEntry(p1, 0) );
164     Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, 0), Len1/2 ) );
165     Vec_IntPush( r, Vec_IntEntry(p1, 0) ^ 1 );
166     for ( i = 1; i < Len0; i++ )
167         Vec_IntPush( r, Exp_LitShift( nVars, Vec_IntEntry(p0, i), Len1/2 ) );
168     for ( i = 1; i < Len1; i++ )
169         Vec_IntPush( r, Vec_IntEntry(p1, i) );
170     assert( Vec_IntSize(r) == Len0 + Len1 + 5 );
171     return Exp_Not( r );
172 }
Exp_Truth6Lit(int nVars,int Lit,word * puFanins,word * puNodes)173 static inline word Exp_Truth6Lit( int nVars, int Lit, word * puFanins, word * puNodes )
174 {
175     if ( Lit == EXP_CONST0 )
176         return 0;
177     if ( Lit == EXP_CONST1 )
178         return ~(word)0;
179     if ( Lit < 2 * nVars )
180         return  (Lit&1) ? ~puFanins[Lit/2] : puFanins[Lit/2];
181     return (Lit&1) ? ~puNodes[Lit/2-nVars] : puNodes[Lit/2-nVars];
182 }
Exp_Truth6(int nVars,Vec_Int_t * p,word * puFanins)183 static inline word Exp_Truth6( int nVars, Vec_Int_t * p, word * puFanins )
184 {
185     static word Truth6[6] = {
186         ABC_CONST(0xAAAAAAAAAAAAAAAA),
187         ABC_CONST(0xCCCCCCCCCCCCCCCC),
188         ABC_CONST(0xF0F0F0F0F0F0F0F0),
189         ABC_CONST(0xFF00FF00FF00FF00),
190         ABC_CONST(0xFFFF0000FFFF0000),
191         ABC_CONST(0xFFFFFFFF00000000)
192     };
193     word * puNodes, Res;
194     int i;
195     if ( puFanins == NULL )
196         puFanins = (word *)Truth6;
197     puNodes = ABC_CALLOC( word, Exp_NodeNum(p) );
198     for ( i = 0; i < Exp_NodeNum(p); i++ )
199         puNodes[i] = Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes ) &
200                      Exp_Truth6Lit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes );
201     Res = Exp_Truth6Lit( nVars, Vec_IntEntryLast(p), puFanins, puNodes );
202     ABC_FREE( puNodes );
203     return Res;
204 }
Exp_Truth8(int nVars,Vec_Int_t * p,word ** puFanins,word * puRes)205 static inline void Exp_Truth8( int nVars, Vec_Int_t * p, word ** puFanins, word * puRes )
206 {
207     word Truth8[8][4] = {
208         { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
209         { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
210         { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
211         { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
212         { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
213         { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
214         { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
215         { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
216     };
217     word * puFaninsInt[8], * pStore, * pThis = NULL;
218     int i, k, iRoot = Vec_IntEntryLast(p);
219     if ( puFanins == NULL )
220     {
221         puFanins = puFaninsInt;
222         for ( k = 0; k < 8; k++ )
223             puFanins[k] = Truth8[k];
224     }
225     if ( Exp_NodeNum(p) == 0 )
226     {
227         assert( iRoot < 2 * nVars );
228         if ( iRoot == EXP_CONST0 || iRoot == EXP_CONST1 )
229             for ( k = 0; k < 4; k++ )
230                 puRes[k] = iRoot == EXP_CONST0 ? 0 : ~(word)0;
231         else
232             for ( k = 0; k < 4; k++ )
233                 puRes[k] = Abc_LitIsCompl(iRoot) ? ~puFanins[Abc_Lit2Var(iRoot)][k] : puFanins[Abc_Lit2Var(iRoot)][k];
234         return;
235     }
236     pStore = ABC_CALLOC( word, 4 * Exp_NodeNum(p) );
237     for ( i = 0; i < Exp_NodeNum(p); i++ )
238     {
239         int iVar0 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+0) );
240         int iVar1 = Abc_Lit2Var( Vec_IntEntry(p, 2*i+1) );
241         int fCompl0 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+0) );
242         int fCompl1 = Abc_LitIsCompl( Vec_IntEntry(p, 2*i+1) );
243         word * pIn0 = iVar0 < nVars ? puFanins[iVar0] : pStore + 4 * (iVar0 - nVars);
244         word * pIn1 = iVar1 < nVars ? puFanins[iVar1] : pStore + 4 * (iVar1 - nVars);
245         pThis = pStore + 4 * i;
246         if ( fCompl0 && fCompl1 )
247             for ( k = 0; k < 4; k++ )
248                 pThis[k] = ~pIn0[k] & ~pIn1[k];
249         else if ( fCompl0 && !fCompl1 )
250             for ( k = 0; k < 4; k++ )
251                 pThis[k] = ~pIn0[k] &  pIn1[k];
252         else if ( !fCompl0 && fCompl1 )
253             for ( k = 0; k < 4; k++ )
254                 pThis[k] =  pIn0[k] & ~pIn1[k];
255         else //if ( !fCompl0 && !fCompl1 )
256             for ( k = 0; k < 4; k++ )
257                 pThis[k] =  pIn0[k] &  pIn1[k];
258     }
259     assert( Abc_Lit2Var(iRoot) - nVars == i - 1 );
260     for ( k = 0; k < 4; k++ )
261         puRes[k] = Abc_LitIsCompl(iRoot) ? ~pThis[k] : pThis[k];
262     ABC_FREE( pStore );
263 }
Exp_TruthLit(int nVars,int Lit,word ** puFanins,word ** puNodes,word * pRes,int nWords)264 static inline void Exp_TruthLit( int nVars, int Lit, word ** puFanins, word ** puNodes, word * pRes, int nWords )
265 {
266     int w;
267     if ( Lit == EXP_CONST0 )
268         for ( w = 0; w < nWords; w++ )
269             pRes[w] = 0;
270     else if ( Lit == EXP_CONST1 )
271         for ( w = 0; w < nWords; w++ )
272             pRes[w] = ~(word)0;
273     else if ( Lit < 2 * nVars )
274         for ( w = 0; w < nWords; w++ )
275             pRes[w] = (Lit&1) ? ~puFanins[Lit/2][w] : puFanins[Lit/2][w];
276     else
277         for ( w = 0; w < nWords; w++ )
278             pRes[w] = (Lit&1) ? ~puNodes[Lit/2-nVars][w] : puNodes[Lit/2-nVars][w];
279 }
Exp_Truth(int nVars,Vec_Int_t * p,word * pRes)280 static inline void Exp_Truth( int nVars, Vec_Int_t * p, word * pRes )
281 {
282     static word Truth6[6] = {
283         ABC_CONST(0xAAAAAAAAAAAAAAAA),
284         ABC_CONST(0xCCCCCCCCCCCCCCCC),
285         ABC_CONST(0xF0F0F0F0F0F0F0F0),
286         ABC_CONST(0xFF00FF00FF00FF00),
287         ABC_CONST(0xFFFF0000FFFF0000),
288         ABC_CONST(0xFFFFFFFF00000000)
289     };
290     word ** puFanins, ** puNodes, * pTemp0, * pTemp1;
291     int i, w, nWords = (nVars <= 6 ? 1 : 1 << (nVars-6));
292     // create elementary variables
293     puFanins = ABC_ALLOC( word *, nVars );
294     for ( i = 0; i < nVars; i++ )
295         puFanins[i] = ABC_ALLOC( word, nWords );
296     // assign elementary truth tables
297     for ( i = 0; i < nVars; i++ )
298         if ( i < 6 )
299             for ( w = 0; w < nWords; w++ )
300                 puFanins[i][w] = Truth6[i];
301         else
302             for ( w = 0; w < nWords; w++ )
303                 puFanins[i][w] = (w & (1 << (i-6))) ? ~(word)0 : 0;
304     // create intermediate nodes
305     puNodes = ABC_ALLOC( word *, Exp_NodeNum(p) );
306     for ( i = 0; i < Exp_NodeNum(p); i++ )
307         puNodes[i] = ABC_ALLOC( word, nWords );
308     // evaluate the expression
309     pTemp0 = ABC_ALLOC( word, nWords );
310     pTemp1 = ABC_ALLOC( word, nWords );
311     for ( i = 0; i < Exp_NodeNum(p); i++ )
312     {
313         Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+0), puFanins, puNodes, pTemp0, nWords );
314         Exp_TruthLit( nVars, Vec_IntEntry(p, 2*i+1), puFanins, puNodes, pTemp1, nWords );
315         for ( w = 0; w < nWords; w++ )
316             puNodes[i][w] = pTemp0[w] & pTemp1[w];
317     }
318     ABC_FREE( pTemp0 );
319     ABC_FREE( pTemp1 );
320     // copy the final result
321     Exp_TruthLit( nVars, Vec_IntEntryLast(p), puFanins, puNodes, pRes, nWords );
322     // cleanup
323     for ( i = 0; i < nVars; i++ )
324         ABC_FREE( puFanins[i] );
325     ABC_FREE( puFanins );
326     for ( i = 0; i < Exp_NodeNum(p); i++ )
327         ABC_FREE( puNodes[i] );
328     ABC_FREE( puNodes );
329 }
330 
331 ////////////////////////////////////////////////////////////////////////
332 ///                    FUNCTION DECLARATIONS                         ///
333 ////////////////////////////////////////////////////////////////////////
334 
335 ABC_NAMESPACE_HEADER_END
336 
337 
338 #endif
339 
340 ////////////////////////////////////////////////////////////////////////
341 ///                       END OF FILE                                ///
342 ////////////////////////////////////////////////////////////////////////
343 
344