abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
utilIsop.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [utilIsop.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [ISOP computation.]
8 
9  Synopsis [ISOP computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - October 4, 2014.]
16 
17  Revision [$Id: utilIsop.c,v 1.00 2014/10/04 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 
26 #include "misc/vec/vec.h"
27 #include "misc/util/utilTruth.h"
28 
29 ABC_NAMESPACE_IMPL_START
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 #define ABC_ISOP_MAX_VAR 16
36 #define ABC_ISOP_MAX_WORD (ABC_ISOP_MAX_VAR > 6 ? (1 << (ABC_ISOP_MAX_VAR-6)) : 1)
37 #define ABC_ISOP_MAX_CUBE 0xFFFF
38 
39 typedef word FUNC_ISOP( word *, word *, word *, word, int * );
40 
41 static FUNC_ISOP Abc_Isop7Cover;
42 static FUNC_ISOP Abc_Isop8Cover;
43 static FUNC_ISOP Abc_Isop9Cover;
44 static FUNC_ISOP Abc_Isop10Cover;
45 static FUNC_ISOP Abc_Isop11Cover;
46 static FUNC_ISOP Abc_Isop12Cover;
47 static FUNC_ISOP Abc_Isop13Cover;
48 static FUNC_ISOP Abc_Isop14Cover;
49 static FUNC_ISOP Abc_Isop15Cover;
50 static FUNC_ISOP Abc_Isop16Cover;
51 
52 static FUNC_ISOP * s_pFuncIsopCover[17] =
53 {
54  NULL, // 0
55  NULL, // 1
56  NULL, // 2
57  NULL, // 3
58  NULL, // 4
59  NULL, // 5
60  NULL, // 6
61  Abc_Isop7Cover, // 7
62  Abc_Isop8Cover, // 8
63  Abc_Isop9Cover, // 9
64  Abc_Isop10Cover, // 10
65  Abc_Isop11Cover, // 11
66  Abc_Isop12Cover, // 12
67  Abc_Isop13Cover, // 13
68  Abc_Isop14Cover, // 14
69  Abc_Isop15Cover, // 15
70  Abc_Isop16Cover // 16
71 };
72 
73 extern word Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, word CostLim, int * pCover );
74 extern word Abc_EsopCheck( word * pOn, int nVars, word CostLim, int * pCover );
75 
76 static inline word Abc_Cube2Cost( int nCubes ) { return (word)nCubes << 32; }
77 static inline int Abc_CostCubes( word Cost ) { return (int)(Cost >> 32); }
78 static inline int Abc_CostLits( word Cost ) { return (int)(Cost & 0xFFFFFFFF); }
79 
80 ////////////////////////////////////////////////////////////////////////
81 /// FUNCTION DEFINITIONS ///
82 ////////////////////////////////////////////////////////////////////////
83 
84 /**Function*************************************************************
85 
86  Synopsis [These procedures assume that function has exact support.]
87 
88  Description []
89 
90  SideEffects []
91 
92  SeeAlso []
93 
94 ***********************************************************************/
95 static inline void Abc_IsopAddLits( int * pCover, word Cost0, word Cost1, int Var )
96 {
97  if ( pCover )
98  {
99  int c, nCubes0, nCubes1;
100  nCubes0 = Abc_CostCubes( Cost0 );
101  nCubes1 = Abc_CostCubes( Cost1 );
102  for ( c = 0; c < nCubes0; c++ )
103  pCover[c] |= (1 << Abc_Var2Lit(Var,0));
104  for ( c = 0; c < nCubes1; c++ )
105  pCover[nCubes0+c] |= (1 << Abc_Var2Lit(Var,1));
106  }
107 }
108 word Abc_Isop6Cover( word uOn, word uOnDc, word * pRes, int nVars, word CostLim, int * pCover )
109 {
110  word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
111  word Cost0, Cost1, Cost2; int Var;
112  assert( nVars <= 6 );
113  assert( (uOn & ~uOnDc) == 0 );
114  if ( uOn == 0 )
115  {
116  pRes[0] = 0;
117  return 0;
118  }
119  if ( uOnDc == ~(word)0 )
120  {
121  pRes[0] = ~(word)0;
122  if ( pCover ) pCover[0] = 0;
123  return Abc_Cube2Cost(1);
124  }
125  assert( nVars > 0 );
126  // find the topmost var
127  for ( Var = nVars-1; Var >= 0; Var-- )
128  if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
129  break;
130  assert( Var >= 0 );
131  // cofactor
132  uOn0 = Abc_Tt6Cofactor0( uOn, Var );
133  uOn1 = Abc_Tt6Cofactor1( uOn , Var );
134  uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
135  uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
136  // solve for cofactors
137  Cost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, CostLim, pCover );
138  if ( Cost0 >= CostLim ) return CostLim;
139  Cost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
140  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
141  Cost2 = Abc_Isop6Cover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
142  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
143  // derive the final truth table
144  *pRes = uRes2 | (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
145  assert( (uOn & ~*pRes) == 0 && (*pRes & ~uOnDc) == 0 );
146  Abc_IsopAddLits( pCover, Cost0, Cost1, Var );
147  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
148 }
149 word Abc_Isop7Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
150 {
151  word uOn0, uOn1, uOn2, uOnDc2, uRes0, uRes1, uRes2;
152  word Cost0, Cost1, Cost2; int nVars = 6;
153  assert( (pOn[0] & ~pOnDc[0]) == 0 );
154  assert( (pOn[1] & ~pOnDc[1]) == 0 );
155  // cofactor
156  uOn0 = pOn[0] & ~pOnDc[1];
157  uOn1 = pOn[1] & ~pOnDc[0];
158  // solve for cofactors
159  Cost0 = Abc_IsopCheck( &uOn0, pOnDc, &uRes0, nVars, CostLim, pCover );
160  if ( Cost0 >= CostLim ) return CostLim;
161  Cost1 = Abc_IsopCheck( &uOn1, pOnDc+1, &uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
162  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
163  uOn2 = (pOn[0] & ~uRes0) | (pOn[1] & ~uRes1);
164  uOnDc2 = pOnDc[0] & pOnDc[1];
165  Cost2 = Abc_IsopCheck( &uOn2, &uOnDc2, &uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
166  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
167  // derive the final truth table
168  pRes[0] = uRes2 | uRes0;
169  pRes[1] = uRes2 | uRes1;
170  assert( (pOn[0] & ~pRes[0]) == 0 && (pRes[0] & ~pOnDc[0]) == 0 );
171  assert( (pOn[1] & ~pRes[1]) == 0 && (pRes[1] & ~pOnDc[1]) == 0 );
172  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
173  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
174 }
175 word Abc_Isop8Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
176 {
177  word uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
178  word Cost0, Cost1, Cost2; int nVars = 7;
179  // negative cofactor
180  uOn2[0] = pOn[0] & ~pOnDc[2];
181  uOn2[1] = pOn[1] & ~pOnDc[3];
182  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
183  if ( Cost0 >= CostLim ) return CostLim;
184  // positive cofactor
185  uOn2[0] = pOn[2] & ~pOnDc[0];
186  uOn2[1] = pOn[3] & ~pOnDc[1];
187  Cost1 = Abc_IsopCheck( uOn2, pOnDc+2, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
188  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
189  // middle cofactor
190  uOn2[0] = (pOn[0] & ~uRes0[0]) | (pOn[2] & ~uRes1[0]); uOnDc2[0] = pOnDc[0] & pOnDc[2];
191  uOn2[1] = (pOn[1] & ~uRes0[1]) | (pOn[3] & ~uRes1[1]); uOnDc2[1] = pOnDc[1] & pOnDc[3];
192  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
193  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
194  // derive the final truth table
195  pRes[0] = uRes2[0] | uRes0[0];
196  pRes[1] = uRes2[1] | uRes0[1];
197  pRes[2] = uRes2[0] | uRes1[0];
198  pRes[3] = uRes2[1] | uRes1[1];
199  assert( (pOn[0] & ~pRes[0]) == 0 && (pOn[1] & ~pRes[1]) == 0 && (pOn[2] & ~pRes[2]) == 0 && (pOn[3] & ~pRes[3]) == 0 );
200  assert( (pRes[0] & ~pOnDc[0])==0 && (pRes[1] & ~pOnDc[1])==0 && (pRes[2] & ~pOnDc[2])==0 && (pRes[3] & ~pOnDc[3])==0 );
201  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
202  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
203 }
204 word Abc_Isop9Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
205 {
206  word uOn2[4], uOnDc2[4], uRes0[4], uRes1[4], uRes2[4];
207  word Cost0, Cost1, Cost2; int c, nVars = 8, nWords = 4;
208  // negative cofactor
209  for ( c = 0; c < nWords; c++ )
210  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
211  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
212  if ( Cost0 >= CostLim ) return CostLim;
213  // positive cofactor
214  for ( c = 0; c < nWords; c++ )
215  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
216  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
217  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
218  // middle cofactor
219  for ( c = 0; c < nWords; c++ )
220  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
221  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
222  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
223  // derive the final truth table
224  for ( c = 0; c < nWords; c++ )
225  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
226  // verify
227  for ( c = 0; c < (nWords<<1); c++ )
228  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
229  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
230  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
231 }
232 word Abc_Isop10Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
233 {
234  word uOn2[8], uOnDc2[8], uRes0[8], uRes1[8], uRes2[8];
235  word Cost0, Cost1, Cost2; int c, nVars = 9, nWords = 8;
236  // negative cofactor
237  for ( c = 0; c < nWords; c++ )
238  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
239  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
240  if ( Cost0 >= CostLim ) return CostLim;
241  // positive cofactor
242  for ( c = 0; c < nWords; c++ )
243  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
244  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
245  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
246  // middle cofactor
247  for ( c = 0; c < nWords; c++ )
248  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
249  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
250  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
251  // derive the final truth table
252  for ( c = 0; c < nWords; c++ )
253  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
254  // verify
255  for ( c = 0; c < (nWords<<1); c++ )
256  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
257  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
258  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
259 }
260 word Abc_Isop11Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
261 {
262  word uOn2[16], uOnDc2[16], uRes0[16], uRes1[16], uRes2[16];
263  word Cost0, Cost1, Cost2; int c, nVars = 10, nWords = 16;
264  // negative cofactor
265  for ( c = 0; c < nWords; c++ )
266  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
267  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
268  if ( Cost0 >= CostLim ) return CostLim;
269  // positive cofactor
270  for ( c = 0; c < nWords; c++ )
271  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
272  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
273  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
274  // middle cofactor
275  for ( c = 0; c < nWords; c++ )
276  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
277  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
278  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
279  // derive the final truth table
280  for ( c = 0; c < nWords; c++ )
281  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
282  // verify
283  for ( c = 0; c < (nWords<<1); c++ )
284  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
285  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
286  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
287 }
288 word Abc_Isop12Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
289 {
290  word uOn2[32], uOnDc2[32], uRes0[32], uRes1[32], uRes2[32];
291  word Cost0, Cost1, Cost2; int c, nVars = 11, nWords = 32;
292  // negative cofactor
293  for ( c = 0; c < nWords; c++ )
294  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
295  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
296  if ( Cost0 >= CostLim ) return CostLim;
297  // positive cofactor
298  for ( c = 0; c < nWords; c++ )
299  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
300  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
301  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
302  // middle cofactor
303  for ( c = 0; c < nWords; c++ )
304  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
305  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
306  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
307  // derive the final truth table
308  for ( c = 0; c < nWords; c++ )
309  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
310  // verify
311  for ( c = 0; c < (nWords<<1); c++ )
312  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
313  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
314  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
315 }
316 word Abc_Isop13Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
317 {
318  word uOn2[64], uOnDc2[64], uRes0[64], uRes1[64], uRes2[64];
319  word Cost0, Cost1, Cost2; int c, nVars = 12, nWords = 64;
320  // negative cofactor
321  for ( c = 0; c < nWords; c++ )
322  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
323  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
324  if ( Cost0 >= CostLim ) return CostLim;
325  // positive cofactor
326  for ( c = 0; c < nWords; c++ )
327  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
328  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
329  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
330  // middle cofactor
331  for ( c = 0; c < nWords; c++ )
332  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
333  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
334  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
335  // derive the final truth table
336  for ( c = 0; c < nWords; c++ )
337  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
338  // verify
339  for ( c = 0; c < (nWords<<1); c++ )
340  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
341  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
342  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
343 }
344 word Abc_Isop14Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
345 {
346  word uOn2[128], uOnDc2[128], uRes0[128], uRes1[128], uRes2[128];
347  word Cost0, Cost1, Cost2; int c, nVars = 13, nWords = 128;
348  // negative cofactor
349  for ( c = 0; c < nWords; c++ )
350  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
351  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
352  if ( Cost0 >= CostLim ) return CostLim;
353  // positive cofactor
354  for ( c = 0; c < nWords; c++ )
355  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
356  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
357  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
358  // middle cofactor
359  for ( c = 0; c < nWords; c++ )
360  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
361  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
362  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
363  // derive the final truth table
364  for ( c = 0; c < nWords; c++ )
365  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
366  // verify
367  for ( c = 0; c < (nWords<<1); c++ )
368  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
369  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
370  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
371 }
372 word Abc_Isop15Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
373 {
374  word uOn2[256], uOnDc2[256], uRes0[256], uRes1[256], uRes2[256];
375  word Cost0, Cost1, Cost2; int c, nVars = 14, nWords = 256;
376  // negative cofactor
377  for ( c = 0; c < nWords; c++ )
378  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
379  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
380  if ( Cost0 >= CostLim ) return CostLim;
381  // positive cofactor
382  for ( c = 0; c < nWords; c++ )
383  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
384  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
385  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
386  // middle cofactor
387  for ( c = 0; c < nWords; c++ )
388  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
389  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
390  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
391  // derive the final truth table
392  for ( c = 0; c < nWords; c++ )
393  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
394  // verify
395  for ( c = 0; c < (nWords<<1); c++ )
396  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
397  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
398  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
399 }
400 word Abc_Isop16Cover( word * pOn, word * pOnDc, word * pRes, word CostLim, int * pCover )
401 {
402  word uOn2[512], uOnDc2[512], uRes0[512], uRes1[512], uRes2[512];
403  word Cost0, Cost1, Cost2; int c, nVars = 15, nWords = 512;
404  // negative cofactor
405  for ( c = 0; c < nWords; c++ )
406  uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
407  Cost0 = Abc_IsopCheck( uOn2, pOnDc, uRes0, nVars, CostLim, pCover );
408  if ( Cost0 >= CostLim ) return CostLim;
409  // positive cofactor
410  for ( c = 0; c < nWords; c++ )
411  uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
412  Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
413  if ( Cost0 + Cost1 >= CostLim ) return CostLim;
414  // middle cofactor
415  for ( c = 0; c < nWords; c++ )
416  uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
417  Cost2 = Abc_IsopCheck( uOn2, uOnDc2, uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
418  if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
419  // derive the final truth table
420  for ( c = 0; c < nWords; c++ )
421  pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
422  // verify
423  for ( c = 0; c < (nWords<<1); c++ )
424  assert( (pOn[c] & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
425  Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
426  return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
427 }
428 word Abc_IsopCheck( word * pOn, word * pOnDc, word * pRes, int nVars, word CostLim, int * pCover )
429 {
430  int nVarsNew; word Cost;
431  if ( nVars <= 6 )
432  return Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVars, CostLim, pCover );
433  for ( nVarsNew = nVars; nVarsNew > 6; nVarsNew-- )
434  if ( Abc_TtHasVar( pOn, nVars, nVarsNew-1 ) || Abc_TtHasVar( pOnDc, nVars, nVarsNew-1 ) )
435  break;
436  if ( nVarsNew == 6 )
437  Cost = Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVarsNew, CostLim, pCover );
438  else
439  Cost = s_pFuncIsopCover[nVarsNew]( pOn, pOnDc, pRes, CostLim, pCover );
440  Abc_TtStretch6( pRes, nVarsNew, nVars );
441  return Cost;
442 }
443 
444 /**Function*************************************************************
445 
446  Synopsis [Create truth table for the given cover.]
447 
448  Description []
449 
450  SideEffects []
451 
452  SeeAlso []
453 
454 ***********************************************************************/
455 static inline word ** Abc_IsopTtElems()
456 {
457  static word TtElems[ABC_ISOP_MAX_VAR+1][ABC_ISOP_MAX_WORD], * pTtElems[ABC_ISOP_MAX_VAR+1] = {NULL};
458  if ( pTtElems[0] == NULL )
459  {
460  int v;
461  for ( v = 0; v <= ABC_ISOP_MAX_VAR; v++ )
462  pTtElems[v] = TtElems[v];
463  Abc_TtElemInit( pTtElems, ABC_ISOP_MAX_VAR );
464  }
465  return pTtElems;
466 }
467 void Abc_IsopBuildTruth( Vec_Int_t * vCover, int nVars, word * pRes, int fXor, int fCompl )
468 {
469  word ** pTtElems = Abc_IsopTtElems();
470  word pCube[ABC_ISOP_MAX_WORD];
471  int nWords = Abc_TtWordNum( nVars );
472  int c, v, Cube;
473  assert( nVars <= ABC_ISOP_MAX_VAR );
474  Abc_TtClear( pRes, nWords );
475  Vec_IntForEachEntry( vCover, Cube, c )
476  {
477  Abc_TtFill( pCube, nWords );
478  for ( v = 0; v < nVars; v++ )
479  if ( ((Cube >> (v << 1)) & 3) == 1 )
480  Abc_TtSharp( pCube, pCube, pTtElems[v], nWords );
481  else if ( ((Cube >> (v << 1)) & 3) == 2 )
482  Abc_TtAnd( pCube, pCube, pTtElems[v], nWords, 0 );
483  if ( fXor )
484  Abc_TtXor( pRes, pRes, pCube, nWords, 0 );
485  else
486  Abc_TtOr( pRes, pRes, pCube, nWords );
487  }
488  if ( fCompl )
489  Abc_TtNot( pRes, nWords );
490 }
491 static inline void Abc_IsopVerify( word * pFunc, int nVars, word * pRes, Vec_Int_t * vCover, int fXor, int fCompl )
492 {
493  Abc_IsopBuildTruth( vCover, nVars, pRes, fXor, fCompl );
494  if ( !Abc_TtEqual( pFunc, pRes, Abc_TtWordNum(nVars) ) )
495  printf( "Verification failed.\n" );
496 // else
497 // printf( "Verification succeeded.\n" );
498 }
499 
500 /**Function*************************************************************
501 
502  Synopsis [This procedure assumes that function has exact support.]
503 
504  Description []
505 
506  SideEffects []
507 
508  SeeAlso []
509 
510 ***********************************************************************/
511 int Abc_Isop( word * pFunc, int nVars, int nCubeLim, Vec_Int_t * vCover, int fTryBoth )
512 {
513  word pRes[ABC_ISOP_MAX_WORD];
514  word Cost0, Cost1, Cost, CostInit = Abc_Cube2Cost(nCubeLim);
515  assert( nVars <= ABC_ISOP_MAX_VAR );
516  Vec_IntGrow( vCover, 1 << (nVars-1) );
517  if ( fTryBoth )
518  {
519  Cost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, NULL );
520  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
521  Cost1 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Cost0, NULL );
522  Cost = Abc_MinWord( Cost0, Cost1 );
523  if ( Cost == CostInit )
524  {
525  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
526  return -1;
527  }
528  if ( Cost == Cost0 )
529  {
530  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
531  Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
532  }
533  else // if ( Cost == Cost1 )
534  {
535  Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
536  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
537  }
538  }
539  else
540  {
541  Cost = Cost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
542  if ( Cost == CostInit )
543  return -1;
544  }
545  vCover->nSize = Abc_CostCubes(Cost);
546  assert( vCover->nSize <= vCover->nCap );
547 // Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, Cost != Cost0 );
548  return Cost != Cost0;
549 }
550 
551 /**Function*************************************************************
552 
553  Synopsis [Compute CNF assuming it does not exceed the limit.]
554 
555  Description [Please note that pCover should have at least 32 extra entries!]
556 
557  SideEffects []
558 
559  SeeAlso []
560 
561 ***********************************************************************/
562 int Abc_IsopCnf( word * pFunc, int nVars, int nCubeLim, int * pCover )
563 {
564  word pRes[ABC_ISOP_MAX_WORD];
565  word Cost0, Cost1, CostInit = Abc_Cube2Cost(nCubeLim);
566  int c, nCubes0, nCubes1;
567  assert( nVars <= ABC_ISOP_MAX_VAR );
568  assert( Abc_TtHasVar( pFunc, nVars, nVars - 1 ) );
569  if ( nVars > 6 )
570  Cost0 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, CostInit, pCover );
571  else
572  Cost0 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostInit, pCover );
573  if ( Cost0 >= CostInit )
574  return CostInit;
575  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
576  if ( nVars > 6 )
577  Cost1 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, CostInit, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
578  else
579  Cost1 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostInit, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
580  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
581  if ( Cost0 + Cost1 >= CostInit )
582  return CostInit;
583  nCubes0 = Abc_CostCubes(Cost0);
584  nCubes1 = Abc_CostCubes(Cost1);
585  if ( pCover )
586  {
587  for ( c = 0; c < nCubes0; c++ )
588  pCover[c] |= (1 << Abc_Var2Lit(nVars, 0));
589  for ( c = 0; c < nCubes1; c++ )
590  pCover[c+nCubes0] |= (1 << Abc_Var2Lit(nVars, 1));
591  }
592  return nCubes0 + nCubes1;
593 }
594 
595 
596 /**Function*************************************************************
597 
598  Synopsis []
599 
600  Description []
601 
602  SideEffects []
603 
604  SeeAlso []
605 
606 ***********************************************************************/
607 int Abc_IsopCountLits( Vec_Int_t * vCover, int nVars )
608 {
609  int i, k, Entry, Literal, nLits = 0;
610  if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
611  return 0;
612  Vec_IntForEachEntry( vCover, Entry, i )
613  {
614  for ( k = 0; k < nVars; k++ )
615  {
616  Literal = 3 & (Entry >> (k << 1));
617  if ( Literal == 1 ) // neg literal
618  nLits++;
619  else if ( Literal == 2 ) // pos literal
620  nLits++;
621  else if ( Literal != 0 )
622  assert( 0 );
623  }
624  }
625  return nLits;
626 }
627 void Abc_IsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl )
628 {
629  int i, k, Entry, Literal;
630  if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
631  {
632  printf( "Constant %d\n", Vec_IntSize(vCover) );
633  return;
634  }
635  Vec_IntForEachEntry( vCover, Entry, i )
636  {
637  for ( k = 0; k < nVars; k++ )
638  {
639  Literal = 3 & (Entry >> (k << 1));
640  if ( Literal == 1 ) // neg literal
641  printf( "0" );
642  else if ( Literal == 2 ) // pos literal
643  printf( "1" );
644  else if ( Literal == 0 )
645  printf( "-" );
646  else assert( 0 );
647  }
648  printf( " %d\n", !fCompl );
649  }
650 }
651 void Abc_IsopPrint( word * t, int nVars, Vec_Int_t * vCover, int fTryBoth )
652 {
653  int fCompl = Abc_Isop( t, nVars, ABC_ISOP_MAX_CUBE, vCover, fTryBoth );
654  Abc_IsopPrintCover( vCover, nVars, fCompl );
655 }
656 
657 
658 /**Function*************************************************************
659 
660  Synopsis [These procedures assume that function has exact support.]
661 
662  Description []
663 
664  SideEffects []
665 
666  SeeAlso []
667 
668 ***********************************************************************/
669 static inline int Abc_EsopAddLits( int * pCover, word r0, word r1, word r2, word Max, int Var )
670 {
671  int i, c0, c1, c2;
672  if ( Max == r0 )
673  {
674  c2 = Abc_CostCubes(r2);
675  if ( pCover )
676  {
677  c0 = Abc_CostCubes(r0);
678  c1 = Abc_CostCubes(r1);
679  for ( i = 0; i < c1; i++ )
680  pCover[i] = pCover[c0+i];
681  for ( i = 0; i < c2; i++ )
682  pCover[c1+i] = pCover[c0+c1+i] | (1 << Abc_Var2Lit(Var,0));
683  }
684  return c2;
685  }
686  else if ( Max == r1 )
687  {
688  c2 = Abc_CostCubes(r2);
689  if ( pCover )
690  {
691  c0 = Abc_CostCubes(r0);
692  c1 = Abc_CostCubes(r1);
693  for ( i = 0; i < c2; i++ )
694  pCover[c0+i] = pCover[c0+c1+i] | (1 << Abc_Var2Lit(Var,1));
695  }
696  return c2;
697  }
698  else
699  {
700  c0 = Abc_CostCubes(r0);
701  c1 = Abc_CostCubes(r1);
702  if ( pCover )
703  {
704  c2 = Abc_CostCubes(r2);
705  for ( i = 0; i < c0; i++ )
706  pCover[i] |= (1 << Abc_Var2Lit(Var,0));
707  for ( i = 0; i < c1; i++ )
708  pCover[c0+i] |= (1 << Abc_Var2Lit(Var,1));
709  }
710  return c0 + c1;
711  }
712 }
713 word Abc_Esop6Cover( word t, int nVars, word CostLim, int * pCover )
714 {
715  word c0, c1;
716  word r0, r1, r2, Max;
717  int Var;
718  assert( nVars <= 6 );
719  if ( t == 0 )
720  return 0;
721  if ( t == ~(word)0 )
722  {
723  if ( pCover ) *pCover = 0;
724  return Abc_Cube2Cost(1);
725  }
726  assert( nVars > 0 );
727  // find the topmost var
728  for ( Var = nVars-1; Var >= 0; Var-- )
729  if ( Abc_Tt6HasVar( t, Var ) )
730  break;
731  assert( Var >= 0 );
732  // cofactor
733  c0 = Abc_Tt6Cofactor0( t, Var );
734  c1 = Abc_Tt6Cofactor1( t, Var );
735  // call recursively
736  r0 = Abc_Esop6Cover( c0, Var, CostLim, pCover ? pCover : NULL );
737  if ( r0 >= CostLim ) return CostLim;
738  r1 = Abc_Esop6Cover( c1, Var, CostLim, pCover ? pCover + Abc_CostCubes(r0) : NULL );
739  if ( r1 >= CostLim ) return CostLim;
740  r2 = Abc_Esop6Cover( c0 ^ c1, Var, CostLim, pCover ? pCover + Abc_CostCubes(r0) + Abc_CostCubes(r1) : NULL );
741  if ( r2 >= CostLim ) return CostLim;
742  Max = Abc_MaxWord( r0, Abc_MaxWord(r1, r2) );
743  if ( r0 + r1 + r2 - Max >= CostLim ) return CostLim;
744  return r0 + r1 + r2 - Max + Abc_EsopAddLits( pCover, r0, r1, r2, Max, Var );
745 }
746 word Abc_EsopCover( word * pOn, int nVars, word CostLim, int * pCover )
747 {
748  word r0, r1, r2, Max;
749  int c, nWords = (1 << (nVars - 7));
750  assert( nVars > 6 );
751  assert( Abc_TtHasVar( pOn, nVars, nVars - 1 ) );
752  r0 = Abc_EsopCheck( pOn, nVars-1, CostLim, pCover );
753  if ( r0 >= CostLim ) return CostLim;
754  r1 = Abc_EsopCheck( pOn+nWords, nVars-1, CostLim, pCover ? pCover + Abc_CostCubes(r0) : NULL );
755  if ( r1 >= CostLim ) return CostLim;
756  for ( c = 0; c < nWords; c++ )
757  pOn[c] ^= pOn[nWords+c];
758  r2 = Abc_EsopCheck( pOn, nVars-1, CostLim, pCover ? pCover + Abc_CostCubes(r0) + Abc_CostCubes(r1) : NULL );
759  for ( c = 0; c < nWords; c++ )
760  pOn[c] ^= pOn[nWords+c];
761  if ( r2 >= CostLim ) return CostLim;
762  Max = Abc_MaxWord( r0, Abc_MaxWord(r1, r2) );
763  if ( r0 + r1 + r2 - Max >= CostLim ) return CostLim;
764  return r0 + r1 + r2 - Max + Abc_EsopAddLits( pCover, r0, r1, r2, Max, nVars-1 );
765 }
766 word Abc_EsopCheck( word * pOn, int nVars, word CostLim, int * pCover )
767 {
768  int nVarsNew; word Cost;
769  if ( nVars <= 6 )
770  return Abc_Esop6Cover( *pOn, nVars, CostLim, pCover );
771  for ( nVarsNew = nVars; nVarsNew > 6; nVarsNew-- )
772  if ( Abc_TtHasVar( pOn, nVars, nVarsNew-1 ) )
773  break;
774  if ( nVarsNew == 6 )
775  Cost = Abc_Esop6Cover( *pOn, nVarsNew, CostLim, pCover );
776  else
777  Cost = Abc_EsopCover( pOn, nVarsNew, CostLim, pCover );
778  return Cost;
779 }
780 
781 
782 /**Function*************************************************************
783 
784  Synopsis [Perform ISOP computation by subtracting cubes.]
785 
786  Description []
787 
788  SideEffects []
789 
790  SeeAlso []
791 
792 ***********************************************************************/
793 static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords )
794 {
795  int w;
796  for ( w = 0; w < nWords; w++ )
797  if ( pIn1[w] & pIn2[w] )
798  return 1;
799  return 0;
800 }
801 static inline int Abc_TtCheckWithCubePos2Neg( word * t, word * c, int nWords, int iVar )
802 {
803  if ( iVar < 6 )
804  {
805  int i, Shift = (1 << iVar);
806  for ( i = 0; i < nWords; i++ )
807  if ( t[i] & (c[i] >> Shift) )
808  return 0;
809  return 1;
810  }
811  else
812  {
813  int i, Step = (1 << (iVar - 6));
814  word * tLimit = t + nWords;
815  for ( ; t < tLimit; t += 2*Step )
816  for ( i = 0; i < Step; i++ )
817  if ( t[Step+i] & c[i] )
818  return 0;
819  return 1;
820  }
821 }
822 static inline int Abc_TtCheckWithCubeNeg2Pos( word * t, word * c, int nWords, int iVar )
823 {
824  if ( iVar < 6 )
825  {
826  int i, Shift = (1 << iVar);
827  for ( i = 0; i < nWords; i++ )
828  if ( t[i] & (c[i] << Shift) )
829  return 0;
830  return 1;
831  }
832  else
833  {
834  int i, Step = (1 << (iVar - 6));
835  word * tLimit = t + nWords;
836  for ( ; t < tLimit; t += 2*Step )
837  for ( i = 0; i < Step; i++ )
838  if ( t[i] & c[Step+i] )
839  return 0;
840  return 1;
841  }
842 }
843 static inline void Abc_TtExpandCubePos2Neg( word * t, int nWords, int iVar )
844 {
845  if ( iVar < 6 )
846  {
847  int i, Shift = (1 << iVar);
848  for ( i = 0; i < nWords; i++ )
849  t[i] |= (t[i] >> Shift);
850  }
851  else
852  {
853  int i, Step = (1 << (iVar - 6));
854  word * tLimit = t + nWords;
855  for ( ; t < tLimit; t += 2*Step )
856  for ( i = 0; i < Step; i++ )
857  t[i] = t[Step+i];
858  }
859 }
860 static inline void Abc_TtExpandCubeNeg2Pos( word * t, int nWords, int iVar )
861 {
862  if ( iVar < 6 )
863  {
864  int i, Shift = (1 << iVar);
865  for ( i = 0; i < nWords; i++ )
866  t[i] |= (t[i] << Shift);
867  }
868  else
869  {
870  int i, Step = (1 << (iVar - 6));
871  word * tLimit = t + nWords;
872  for ( ; t < tLimit; t += 2*Step )
873  for ( i = 0; i < Step; i++ )
874  t[Step+i] = t[i];
875  }
876 }
877 word Abc_IsopNew( word * pOn, word * pOnDc, word * pRes, int nVars, word CostLim, int * pCover )
878 {
879  word pCube[ABC_ISOP_MAX_WORD];
880  word pOnset[ABC_ISOP_MAX_WORD];
881  word pOffset[ABC_ISOP_MAX_WORD];
882  int pBlocks[16], nBlocks, vTwo, uTwo;
883  int nWords = Abc_TtWordNum(nVars);
884  int c, v, u, iMint, Cube, nLits = 0;
885  assert( nVars <= ABC_ISOP_MAX_VAR );
886  Abc_TtClear( pRes, nWords );
887  Abc_TtCopy( pOnset, pOn, nWords, 0 );
888  Abc_TtCopy( pOffset, pOnDc, nWords, 1 );
889  if ( nVars < 6 )
890  pOnset[0] >>= (64 - (1 << nVars));
891  for ( c = 0; !Abc_TtIsConst0(pOnset, nWords); c++ )
892  {
893  // pick one minterm
894  iMint = Abc_TtFindFirstBit(pOnset, nVars);
895  for ( Cube = v = 0; v < nVars; v++ )
896  Cube |= (1 << Abc_Var2Lit(v, (iMint >> v) & 1));
897  // check expansion for the minterm
898  nBlocks = 0;
899  for ( v = 0; v < nVars; v++ )
900  if ( (pBlocks[v] = Abc_TtGetBit(pOffset, iMint ^ (1 << v))) )
901  nBlocks++;
902  // check second step
903  if ( nBlocks == nVars ) // cannot expand
904  {
905  Abc_TtSetBit( pRes, iMint );
906  Abc_TtXorBit( pOnset, iMint );
907  pCover[c] = Cube;
908  nLits += nVars;
909  continue;
910  }
911  // check dual expansion
912  vTwo = uTwo = -1;
913  if ( nBlocks < nVars - 1 )
914  {
915  for ( v = 0; v < nVars && vTwo == -1; v++ )
916  if ( !pBlocks[v] )
917  for ( u = v + 1; u < nVars; u++ )
918  if ( !pBlocks[u] )
919  {
920  if ( Abc_TtGetBit( pOffset, iMint ^ (1 << v) ^ (1 << u) ) )
921  continue;
922  // can expand both directions
923  vTwo = v;
924  uTwo = u;
925  break;
926  }
927  }
928  if ( vTwo == -1 ) // can expand only one
929  {
930  for ( v = 0; v < nVars; v++ )
931  if ( !pBlocks[v] )
932  break;
933  Abc_TtSetBit( pRes, iMint );
934  Abc_TtSetBit( pRes, iMint ^ (1 << v) );
935  Abc_TtXorBit( pOnset, iMint );
936  if ( Abc_TtGetBit(pOnset, iMint ^ (1 << v)) )
937  Abc_TtXorBit( pOnset, iMint ^ (1 << v) );
938  pCover[c] = Cube & ~(3 << Abc_Var2Lit(v, 0));
939  nLits += nVars - 1;
940  continue;
941  }
942  if ( nBlocks == nVars - 2 && vTwo >= 0 ) // can expand only these two
943  {
944  Abc_TtSetBit( pRes, iMint );
945  Abc_TtSetBit( pRes, iMint ^ (1 << vTwo) );
946  Abc_TtSetBit( pRes, iMint ^ (1 << uTwo) );
947  Abc_TtSetBit( pRes, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
948  Abc_TtXorBit( pOnset, iMint );
949  if ( Abc_TtGetBit(pOnset, iMint ^ (1 << vTwo)) )
950  Abc_TtXorBit( pOnset, iMint ^ (1 << vTwo) );
951  if ( Abc_TtGetBit(pOnset, iMint ^ (1 << uTwo)) )
952  Abc_TtXorBit( pOnset, iMint ^ (1 << uTwo) );
953  if ( Abc_TtGetBit(pOnset, iMint ^ (1 << vTwo) ^ (1 << uTwo)) )
954  Abc_TtXorBit( pOnset, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
955  pCover[c] = Cube & ~(3 << Abc_Var2Lit(vTwo, 0)) & ~(3 << Abc_Var2Lit(uTwo, 0));
956  nLits += nVars - 2;
957  continue;
958  }
959  // can expand others as well
960  Abc_TtClear( pCube, nWords );
961  Abc_TtSetBit( pCube, iMint );
962  Abc_TtSetBit( pCube, iMint ^ (1 << vTwo) );
963  Abc_TtSetBit( pCube, iMint ^ (1 << uTwo) );
964  Abc_TtSetBit( pCube, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
965  Cube &= ~(3 << Abc_Var2Lit(vTwo, 0)) & ~(3 << Abc_Var2Lit(uTwo, 0));
966  assert( !Abc_TtIntersect(pCube, pOffset, nWords) );
967  // expand against offset
968  for ( v = 0; v < nVars; v++ )
969  if ( v != vTwo && v != uTwo )
970  {
971  int Shift = Abc_Var2Lit( v, 0 );
972  if ( (Cube >> Shift) == 2 && Abc_TtCheckWithCubePos2Neg(pOffset, pCube, nWords, v) ) // pos literal
973  {
974  Abc_TtExpandCubePos2Neg( pCube, nWords, v );
975  Cube &= ~(3 << Shift);
976  }
977  else if ( (Cube >> Shift) == 1 && Abc_TtCheckWithCubeNeg2Pos(pOffset, pCube, nWords, v) ) // neg literal
978  {
979  Abc_TtExpandCubeNeg2Pos( pCube, nWords, v );
980  Cube &= ~(3 << Shift);
981  }
982  else
983  nLits++;
984  }
985  // add cube to solution
986  Abc_TtOr( pRes, pRes, pCube, nWords );
987  Abc_TtSharp( pOnset, pOnset, pCube, nWords );
988  pCover[c] = Cube;
989  }
990  pRes[0] = Abc_Tt6Stretch( pRes[0], nVars );
991  return Abc_Cube2Cost(c) | nLits;
992 }
993 void Abc_IsopTestNew()
994 {
995  int nVars = 4;
996  Vec_Int_t * vCover = Vec_IntAlloc( 1000 );
997  word r, t = (s_Truths6[0] & s_Truths6[1]) ^ (s_Truths6[2] & s_Truths6[3]), copy = t;
998 // word r, t = ~s_Truths6[0] | (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]), copy = t;
999 // word r, t = 0xABCDABCDABCDABCD, copy = t;
1000 // word r, t = 0x6996000000006996, copy = t;
1001 // word Cost = Abc_IsopNew( &t, &t, &r, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1002  word Cost = Abc_EsopCheck( &t, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1003  vCover->nSize = Abc_CostCubes(Cost);
1004  assert( vCover->nSize <= vCover->nCap );
1005  printf( "Cubes = %d. Lits = %d.\n", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
1006  Abc_IsopPrintCover( vCover, nVars, 0 );
1007  Abc_IsopVerify( &copy, nVars, &r, vCover, 1, 0 );
1008  Vec_IntFree( vCover );
1009 }
1010 
1011 /**Function*************************************************************
1012 
1013  Synopsis [Compute CNF assuming it does not exceed the limit.]
1014 
1015  Description [Please note that pCover should have at least 32 extra entries!]
1016 
1017  SideEffects []
1018 
1019  SeeAlso []
1020 
1021 ***********************************************************************/
1022 int Abc_IsopTest( word * pFunc, int nVars, Vec_Int_t * vCover )
1023 {
1024  int fVerbose = 0;
1025  static word TotalCost[6] = {0};
1026  static abctime TotalTime[6] = {0};
1027  static int Counter;
1028  word pRes[ABC_ISOP_MAX_WORD];
1029  word Cost;
1030  abctime clk;
1031  Counter++;
1032  if ( Counter == 9999 )
1033  {
1034  Abc_PrintTime( 1, "0", TotalTime[0] );
1035  Abc_PrintTime( 1, "1", TotalTime[1] );
1036  Abc_PrintTime( 1, "2", TotalTime[2] );
1037  Abc_PrintTime( 1, "3", TotalTime[3] );
1038  Abc_PrintTime( 1, "4", TotalTime[4] );
1039  Abc_PrintTime( 1, "5", TotalTime[5] );
1040  }
1041  assert( nVars <= ABC_ISOP_MAX_VAR );
1042 // if ( fVerbose )
1043 // Dau_DsdPrintFromTruth( pFunc, nVars ), printf( " " );
1044 
1045  clk = Abc_Clock();
1046  Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1047  vCover->nSize = Abc_CostCubes(Cost);
1048  assert( vCover->nSize <= vCover->nCap );
1049  if ( fVerbose )
1050  printf( "%5d %7d ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
1051 // Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
1052  TotalCost[0] += Abc_CostCubes(Cost);
1053  TotalTime[0] += Abc_Clock() - clk;
1054 
1055 
1056  clk = Abc_Clock();
1057  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
1058  Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1059  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
1060  vCover->nSize = Abc_CostCubes(Cost);
1061  assert( vCover->nSize <= vCover->nCap );
1062  if ( fVerbose )
1063  printf( "%5d %7d ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
1064 // Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
1065  TotalCost[1] += Abc_CostCubes(Cost);
1066  TotalTime[1] += Abc_Clock() - clk;
1067 
1068 /*
1069  clk = Abc_Clock();
1070  Cost = Abc_EsopCheck( pFunc, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1071  vCover->nSize = Abc_CostCubes(Cost);
1072  assert( vCover->nSize <= vCover->nCap );
1073  if ( fVerbose )
1074  printf( "%5d %7d ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
1075 // Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 0 );
1076  TotalCost[2] += Abc_CostCubes(Cost);
1077  TotalTime[2] += Abc_Clock() - clk;
1078 
1079 
1080  clk = Abc_Clock();
1081  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
1082  Cost = Abc_EsopCheck( pFunc, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1083  Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
1084  vCover->nSize = Abc_CostCubes(Cost);
1085  assert( vCover->nSize <= vCover->nCap );
1086  if ( fVerbose )
1087  printf( "%5d %7d ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
1088 // Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 1 );
1089  TotalCost[3] += Abc_CostCubes(Cost);
1090  TotalTime[3] += Abc_Clock() - clk;
1091 */
1092 
1093 /*
1094  // try new computation
1095  clk = Abc_Clock();
1096  Cost = Abc_IsopNew( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
1097  vCover->nSize = Abc_CostCubes(Cost);
1098  assert( vCover->nSize <= vCover->nCap );
1099  if ( fVerbose )
1100  printf( "%5d %7d ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
1101  Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
1102  TotalCost[4] += Abc_CostCubes(Cost);
1103  TotalTime[4] += Abc_Clock() - clk;
1104 */
1105 /*
1106  // try old computation
1107  clk = Abc_Clock();
1108  Cost = Kit_TruthIsop( (unsigned *)pFunc, nVars, vCover, 1 );
1109  vCover->nSize = Vec_IntSize(vCover);
1110  assert( vCover->nSize <= vCover->nCap );
1111  if ( fVerbose )
1112  printf( "%5d %7d ", Vec_IntSize(vCover), Abc_IsopCountLits(vCover, nVars) );
1113  TotalCost[4] += Vec_IntSize(vCover);
1114  TotalTime[4] += Abc_Clock() - clk;
1115 */
1116 
1117  clk = Abc_Clock();
1118  Cost = Abc_Isop( pFunc, nVars, ABC_ISOP_MAX_CUBE, vCover, 1 );
1119  if ( fVerbose )
1120  printf( "%5d %7d ", Vec_IntSize(vCover), Abc_IsopCountLits(vCover, nVars) );
1121  TotalCost[5] += Vec_IntSize(vCover);
1122  TotalTime[5] += Abc_Clock() - clk;
1123 
1124  if ( fVerbose )
1125  printf( " | %8d %8d %8d %8d %8d %8d", (int)TotalCost[0], (int)TotalCost[1], (int)TotalCost[2], (int)TotalCost[3], (int)TotalCost[4], (int)TotalCost[5] );
1126  if ( fVerbose )
1127  printf( "\n" );
1128 //Abc_IsopPrintCover( vCover, nVars, 0 );
1129  return 1;
1130 }
1131 
1132 
1133 ////////////////////////////////////////////////////////////////////////
1134 /// END OF FILE ///
1135 ////////////////////////////////////////////////////////////////////////
1136 
1137 
1138 ABC_NAMESPACE_IMPL_END
1139 
Abc_Isop9Cover
static FUNC_ISOP Abc_Isop9Cover
Definition: utilIsop.c:43
Abc_TtSharp
static void Abc_TtSharp(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:241
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Abc_Isop11Cover
static FUNC_ISOP Abc_Isop11Cover
Definition: utilIsop.c:45
Abc_Isop15Cover
static FUNC_ISOP Abc_Isop15Cover
Definition: utilIsop.c:49
Minisat::copy
static void copy(const T &from, T &to)
Definition: Alg.h:61
Abc_Isop14Cover
static FUNC_ISOP Abc_Isop14Cover
Definition: utilIsop.c:48
Abc_IsopPrint
void Abc_IsopPrint(word *t, int nVars, Vec_Int_t *vCover, int fTryBoth)
Definition: utilIsop.c:651
Abc_MinWord
static word Abc_MinWord(word a, word b)
Definition: abc_global.h:241
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_Tt6HasVar
static int Abc_Tt6HasVar(word t, int iVar)
Definition: utilTruth.h:949
Abc_TtCheckWithCubeNeg2Pos
static int Abc_TtCheckWithCubeNeg2Pos(word *t, word *c, int nWords, int iVar)
Definition: utilIsop.c:822
Abc_IsopTtElems
static word ** Abc_IsopTtElems()
Definition: utilIsop.c:455
Abc_TtClear
static void Abc_TtClear(word *pOut, int nWords)
Definition: utilTruth.h:197
Abc_TtIsConst0
static int Abc_TtIsConst0(word *pIn1, int nWords)
Definition: utilTruth.h:293
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Abc_TtFindFirstBit
static int Abc_TtFindFirstBit(word *pIn, int nVars)
Definition: utilTruth.h:1516
Abc_EsopCover
word Abc_EsopCover(word *pOn, int nVars, word CostLim, int *pCover)
Definition: utilIsop.c:746
Abc_Isop7Cover
static FUNC_ISOP Abc_Isop7Cover
Definition: utilIsop.c:41
Abc_Isop6Cover
word Abc_Isop6Cover(word uOn, word uOnDc, word *pRes, int nVars, word CostLim, int *pCover)
Definition: utilIsop.c:108
Abc_TtOr
static void Abc_TtOr(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:247
Abc_TtSetBit
static void Abc_TtSetBit(word *p, int i)
Definition: utilTruth.h:150
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_EsopAddLits
static int Abc_EsopAddLits(int *pCover, word r0, word r1, word r2, word Max, int Var)
Definition: utilIsop.c:669
Abc_TtGetBit
static int Abc_TtGetBit(word *p, int i)
MACRO DEFINITIONS ///.
Definition: utilTruth.h:149
Abc_IsopVerify
static void Abc_IsopVerify(word *pFunc, int nVars, word *pRes, Vec_Int_t *vCover, int fXor, int fCompl)
Definition: utilIsop.c:491
nWords
int nWords
Definition: abcNpn.c:127
s_pFuncIsopCover
static FUNC_ISOP * s_pFuncIsopCover[17]
Definition: utilIsop.c:52
Abc_Isop8Cover
static FUNC_ISOP Abc_Isop8Cover
Definition: utilIsop.c:42
Abc_Isop13Cover
static FUNC_ISOP Abc_Isop13Cover
Definition: utilIsop.c:47
Vec_IntGrow
static void Vec_IntGrow(Vec_Int_t *p, int nCapMin)
Definition: bblif.c:336
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Abc_TtXorBit
static void Abc_TtXorBit(word *p, int i)
Definition: utilTruth.h:151
Abc_TtFill
static void Abc_TtFill(word *pOut, int nWords)
Definition: utilTruth.h:203
Abc_EsopCheck
word Abc_EsopCheck(word *pOn, int nVars, word CostLim, int *pCover)
Definition: utilIsop.c:766
Abc_TtCopy
static void Abc_TtCopy(word *pOut, word *pIn, int nWords, int fCompl)
Definition: utilTruth.h:221
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Abc_Isop12Cover
static FUNC_ISOP Abc_Isop12Cover
Definition: utilIsop.c:46
ABC_ISOP_MAX_WORD
#define ABC_ISOP_MAX_WORD
Definition: utilIsop.c:36
Abc_IsopAddLits
static void Abc_IsopAddLits(int *pCover, word Cost0, word Cost1, int Var)
FUNCTION DEFINITIONS ///.
Definition: utilIsop.c:95
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_IsopPrintCover
void Abc_IsopPrintCover(Vec_Int_t *vCover, int nVars, int fCompl)
Definition: utilIsop.c:627
Abc_CostCubes
static int Abc_CostCubes(word Cost)
Definition: utilIsop.c:77
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
Abc_TtStretch6
static void Abc_TtStretch6(word *pInOut, int nVarS, int nVarB)
Definition: utilTruth.h:693
Abc_CostLits
static int Abc_CostLits(word Cost)
Definition: utilIsop.c:78
Abc_IsopTestNew
void Abc_IsopTestNew()
Definition: utilIsop.c:993
Abc_IsopCnf
int Abc_IsopCnf(word *pFunc, int nVars, int nCubeLim, int *pCover)
Definition: utilIsop.c:562
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_TtHasVar
static int Abc_TtHasVar(word *t, int nVars, int iVar)
Definition: utilTruth.h:953
s_Truths6Neg
static word s_Truths6Neg[6]
Definition: utilTruth.h:47
Abc_TtIntersect
static int Abc_TtIntersect(word *pIn1, word *pIn2, int nWords)
Definition: utilIsop.c:793
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_Esop6Cover
word Abc_Esop6Cover(word t, int nVars, word CostLim, int *pCover)
Definition: utilIsop.c:713
Abc_Isop16Cover
static FUNC_ISOP Abc_Isop16Cover
Definition: utilIsop.c:50
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Abc_IsopCountLits
int Abc_IsopCountLits(Vec_Int_t *vCover, int nVars)
Definition: utilIsop.c:607
FUNC_ISOP
word FUNC_ISOP(word *, word *, word *, word, int *)
Definition: utilIsop.c:39
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
Abc_Cube2Cost
static word Abc_Cube2Cost(int nCubes)
Definition: utilIsop.c:76
Abc_IsopNew
word Abc_IsopNew(word *pOn, word *pOnDc, word *pRes, int nVars, word CostLim, int *pCover)
Definition: utilIsop.c:877
Minisat::Var
int Var
Definition: SolverTypes.h:42
Abc_TtExpandCubePos2Neg
static void Abc_TtExpandCubePos2Neg(word *t, int nWords, int iVar)
Definition: utilIsop.c:843
Abc_TtExpandCubeNeg2Pos
static void Abc_TtExpandCubeNeg2Pos(word *t, int nWords, int iVar)
Definition: utilIsop.c:860
Abc_IsopBuildTruth
void Abc_IsopBuildTruth(Vec_Int_t *vCover, int nVars, word *pRes, int fXor, int fCompl)
Definition: utilIsop.c:467
ABC_ISOP_MAX_VAR
#define ABC_ISOP_MAX_VAR
DECLARATIONS ///.
Definition: utilIsop.c:35
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Isop10Cover
static FUNC_ISOP Abc_Isop10Cover
Definition: utilIsop.c:44
Abc_IsopCheck
word Abc_IsopCheck(word *pOn, word *pOnDc, word *pRes, int nVars, word CostLim, int *pCover)
Definition: utilIsop.c:428
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Abc_IsopTest
int Abc_IsopTest(word *pFunc, int nVars, Vec_Int_t *vCover)
Definition: utilIsop.c:1022
Abc_TtXor
static void Abc_TtXor(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:253
Abc_TtElemInit
static void Abc_TtElemInit(word **pTtElems, int nVars)
Definition: utilTruth.h:333
Abc_TtNot
static void Abc_TtNot(word *pOut, int nWords)
Definition: utilTruth.h:215
ABC_ISOP_MAX_CUBE
#define ABC_ISOP_MAX_CUBE
Definition: utilIsop.c:37
Abc_TtCheckWithCubePos2Neg
static int Abc_TtCheckWithCubePos2Neg(word *t, word *c, int nWords, int iVar)
Definition: utilIsop.c:801
Abc_Isop
int Abc_Isop(word *pFunc, int nVars, int nCubeLim, Vec_Int_t *vCover, int fTryBoth)
Definition: utilIsop.c:511
Abc_MaxWord
static word Abc_MaxWord(word a, word b)
Definition: abc_global.h:240