abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
combination.c
Go to the documentation of this file.
1 #include <stdio.h>
2 #include "base/main/main.h"
3 #include "aig/aig/aig.h"
4 #include "aig/saig/saig.h"
5 #include <string.h>
6 #include "base/main/mainInt.h"
7 #include "proof/pdr/pdr.h"
8 #include <time.h>
9 
11 
12 long countCombination(long n, long k)
13 {
14  assert( n >= k );
15  if( n == k ) return 1;
16  if( k == 1 ) return n;
17  return countCombination( n-1, k-1 ) + countCombination( n-1, k );
18 }
19 
20 void listCombination(int n, int t)
21 {
22  Vec_Int_t *vC;
23  int i, j, combCounter = 0;
24 
25  //Initialization
26  vC = Vec_IntAlloc(t+3);
27  for(i=-1; i<t; i++)
28  Vec_IntPush( vC, i );
29  Vec_IntPush( vC, n );
30  Vec_IntPush( vC, 0 );
31 
32  while(1)
33  {
34  //visit combination
35  printf("Comb-%3d : ", ++combCounter);
36  for( i=t; i>0; i--)
37  printf("vC[%d] = %d ", i, Vec_IntEntry(vC, i));
38  printf("\n");
39 
40  j = 1;
41  while( Vec_IntEntry( vC, j ) + 1 == Vec_IntEntry( vC, j+1 ) )
42  {
43  //printf("\nGochon = %d, %d\n", Vec_IntEntry( vC, j ) + 1, Vec_IntEntry( vC, j+1 ));
44  Vec_IntWriteEntry( vC, j, j-1 );
45  j = j + 1;
46  }
47  if( j > t ) break;
48  Vec_IntWriteEntry( vC, j, Vec_IntEntry( vC, j ) + 1 );
49  }
50 
51  Vec_IntFree(vC);
52 }
53 
55  Vec_Int_t *vCandidateMonotoneSignals_,
56  Vec_Ptr_t *vDisj_nCk_,
57  int combN, int combK )
58 {
59  Aig_Obj_t *pObjMonoCand, *pObj;
60  int targetPoIndex;
61 
62  //Knuth's Data Strcuture
63  int totalCombination_KNUTH = 0;
64  Vec_Int_t *vC_KNUTH;
65  int i_KNUTH, j_KNUTH;
66 
67  //Knuth's Data Structure Initialization
68  vC_KNUTH = Vec_IntAlloc(combK+3);
69  for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++)
70  Vec_IntPush( vC_KNUTH, i_KNUTH );
71  Vec_IntPush( vC_KNUTH, combN );
72  Vec_IntPush( vC_KNUTH, 0 );
73 
74  while(1)
75  {
76  totalCombination_KNUTH++;
77  pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew));
78  for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--)
79  {
80  targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH));
81  pObj = Aig_ObjChild0Copy(Aig_ManCo( pAigOld, targetPoIndex ));
82  pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand );
83  }
84  Vec_PtrPush(vDisj_nCk_, pObjMonoCand );
85 
86  j_KNUTH = 1;
87  while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
88  {
89  Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
90  j_KNUTH = j_KNUTH + 1;
91  }
92  if( j_KNUTH > combK ) break;
93  Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
94  }
95 
96  Vec_IntFree(vC_KNUTH);
97 
98  return totalCombination_KNUTH;
99 }
100 
102  Vec_Ptr_t *vDisj_nCk_,
103  int combN, int combK )
104 {
105  Aig_Obj_t *pObjMonoCand, *pObj;
106  int targetPoIndex;
107 
108  //Knuth's Data Strcuture
109  int totalCombination_KNUTH = 0;
110  Vec_Int_t *vC_KNUTH;
111  int i_KNUTH, j_KNUTH;
112 
113  //Knuth's Data Structure Initialization
114  vC_KNUTH = Vec_IntAlloc(combK+3);
115  for(i_KNUTH=-1; i_KNUTH<combK; i_KNUTH++)
116  Vec_IntPush( vC_KNUTH, i_KNUTH );
117  Vec_IntPush( vC_KNUTH, combN );
118  Vec_IntPush( vC_KNUTH, 0 );
119 
120  while(1)
121  {
122  totalCombination_KNUTH++;
123  pObjMonoCand = Aig_Not(Aig_ManConst1(pAigNew));
124  for( i_KNUTH=combK; i_KNUTH>0; i_KNUTH--)
125  {
126  //targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals_, Vec_IntEntry(vC_KNUTH, i_KNUTH));
127  targetPoIndex = Vec_IntEntry(vC_KNUTH, i_KNUTH);
128  pObj = (Aig_Obj_t *)(Aig_ManLo( pAigOld, targetPoIndex )->pData);
129  pObjMonoCand = Aig_Or( pAigNew, pObj, pObjMonoCand );
130  }
131  Vec_PtrPush(vDisj_nCk_, pObjMonoCand );
132 
133  j_KNUTH = 1;
134  while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
135  {
136  Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
137  j_KNUTH = j_KNUTH + 1;
138  }
139  if( j_KNUTH > combK ) break;
140  Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
141  }
142 
143  Vec_IntFree(vC_KNUTH);
144 
145  return totalCombination_KNUTH;
146 }
147 
148 Aig_Man_t *generateDisjunctiveTester( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK )
149 {
150  //AIG creation related data structure
151  Aig_Man_t *pNewAig;
152  int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
153  //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
154  int i, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
155  int combN_internal, combK_internal; //, targetPoIndex;
156  long longI, lCombinationCount;
157  //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
158  Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
159  Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
160  Vec_Int_t *vCandidateMonotoneSignals;
161 
162  extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
163 
164  //Knuth's Data Strcuture
165  //Vec_Int_t *vC_KNUTH;
166  //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
167 
168  //Collecting target HINT signals
169  vCandidateMonotoneSignals = findHintOutputs(pNtk);
170  if( vCandidateMonotoneSignals == NULL )
171  {
172  printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
173  combN_internal = 0;
174  }
175  else
176  {
177  //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
178  // printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
179  hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
180  hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
181  combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
182  }
183 
184  //combK_internal = combK;
185 
186  //Knuth's Data Structure Initialization
187  //vC_KNUTH = Vec_IntAlloc(combK_internal+3);
188  //for(i_KNUTH=-1; i_KNUTH<combK_internal; i_KNUTH++)
189  // Vec_IntPush( vC_KNUTH, i_KNUTH );
190  //Vec_IntPush( vC_KNUTH, combN_internal );
191  //Vec_IntPush( vC_KNUTH, 0 );
192 
193  //Standard AIG duplication begins
194  //Standard AIG Manager Creation
195  pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
196  pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
197  sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
198  pNewAig->pSpec = NULL;
199 
200  //Standard Mapping of Constant Nodes
201  pObj = Aig_ManConst1( pAig );
202  pObj->pData = Aig_ManConst1( pNewAig );
203 
204  //Standard AIG PI duplication
205  Saig_ManForEachPi( pAig, pObj, i )
206  {
207  piCopied++;
208  pObj->pData = Aig_ObjCreateCi(pNewAig);
209  }
210 
211  //Standard AIG LO duplication
212  Saig_ManForEachLo( pAig, pObj, i )
213  {
214  loCopied++;
215  pObj->pData = Aig_ObjCreateCi(pNewAig);
216  }
217 
218  //nCk LO creation
219  lCombinationCount = 0;
220  for(combK_internal=1; combK_internal<=combK; combK_internal++)
221  lCombinationCount += countCombination( combN_internal, combK_internal );
222  assert( lCombinationCount > 0 );
223  vLO_nCk = Vec_PtrAlloc(lCombinationCount);
224  for( longI = 0; longI < lCombinationCount; longI++ )
225  {
226  loCreated++;
227  pObj = Aig_ObjCreateCi(pNewAig);
228  Vec_PtrPush( vLO_nCk, pObj );
229  }
230 
231  //Standard Node duplication
232  Aig_ManForEachNode( pAig, pObj, i )
233  {
234  pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
235  }
236 
237  //nCk specific logic creation (i.e. nCk number of OR gates)
238  vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
239 
240 
241 
242  //while(1)
243  //{
244  // //visit combination
245  // //printf("Comb-%3d : ", ++combCounter_KNUTH);
246  // pObjMonoCand = Aig_Not(Aig_ManConst1(pNewAig));
247  // for( i_KNUTH=combK_internal; i_KNUTH>0; i_KNUTH--)
248  // {
249  // //printf("vC[%d] = %d ", i_KNUTH, Vec_IntEntry(vC_KNUTH, i_KNUTH));
250  // targetPoIndex = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntEntry(vC_KNUTH, i_KNUTH));
251  // pObj = Aig_ObjChild0Copy(Aig_ManCo( pAig, targetPoIndex ));
252  // pObjMonoCand = Aig_Or( pNewAig, pObj, pObjMonoCand );
253  // }
254  // Vec_PtrPush(vDisj_nCk, pObjMonoCand );
255  // //printf("\n");
256 
257  // j_KNUTH = 1;
258  // while( Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 == Vec_IntEntry( vC_KNUTH, j_KNUTH+1 ) )
259  // {
260  // Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, j_KNUTH-1 );
261  // j_KNUTH = j_KNUTH + 1;
262  // }
263  // if( j_KNUTH > combK_internal ) break;
264  // Vec_IntWriteEntry( vC_KNUTH, j_KNUTH, Vec_IntEntry( vC_KNUTH, j_KNUTH ) + 1 );
265  //}
266  for( combK_internal=1; combK_internal<=combK; combK_internal++ )
267  generateCombinatorialStabil( pNewAig, pAig, vCandidateMonotoneSignals,
268  vDisj_nCk, combN_internal, combK_internal );
269 
270 
271  //creation of implication logic
272  vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
273  for( longI = 0; longI < lCombinationCount; longI++ )
274  {
275  pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
276  pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
277 
278  pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
279  Vec_PtrPush(vPODriver_nCk, pObj);
280  }
281 
282  //Standard PO duplication
283  Saig_ManForEachPo( pAig, pObj, i )
284  {
285  poCopied++;
286  pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
287  }
288 
289  //nCk specific PO creation
290  for( longI = 0; longI < lCombinationCount; longI++ )
291  {
292  Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
293  }
294 
295  //Standard LI duplication
296  Saig_ManForEachLi( pAig, pObj, i )
297  {
298  liCopied++;
299  Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
300  }
301 
302  //nCk specific LI creation
303  for( longI = 0; longI < lCombinationCount; longI++ )
304  {
305  liCreated++;
306  Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
307  }
308 
309  //clean-up, book-keeping
310  assert( liCopied + liCreated == loCopied + loCreated );
311  nRegCount = loCopied + loCreated;
312 
313  Aig_ManSetRegNum( pNewAig, nRegCount );
314  Aig_ManCleanup( pNewAig );
315  assert( Aig_ManCheck( pNewAig ) );
316 
317  //Vec_IntFree(vC_KNUTH);
318  return pNewAig;
319 }
320 
322 {
323  //AIG creation related data structure
324  Aig_Man_t *pNewAig;
325  int piCopied = 0, loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0, poCopied = 0;
326  //int i, iElem, nRegCount, hintSingalBeginningMarker, hintSingalEndMarker;
327  int i, nRegCount;
328  int combN_internal, combK_internal; //, targetPoIndex;
329  long longI, lCombinationCount;
330  //Aig_Obj_t *pObj, *pObjMonoCand, *pObjLO_nCk, *pObjDisj_nCk;
331  Aig_Obj_t *pObj, *pObjLO_nCk, *pObjDisj_nCk;
332  Vec_Ptr_t *vLO_nCk, *vPODriver_nCk, *vDisj_nCk;
333 
334  extern Vec_Int_t *findHintOutputs(Abc_Ntk_t *pNtk);
335 
336  //Knuth's Data Strcuture
337  //Vec_Int_t *vC_KNUTH;
338  //int i_KNUTH, j_KNUTH, combCounter_KNUTH = 0;
339 
340  //Collecting target HINT signals
341  //vCandidateMonotoneSignals = findHintOutputs(pNtk);
342  //if( vCandidateMonotoneSignals == NULL )
343  //{
344  // printf("\nTraget Signal Set is Empty: Duplicating given AIG\n");
345  // combN_internal = 0;
346  //}
347  //else
348  //{
349  //Vec_IntForEachEntry( vCandidateMonotoneSignals, iElem, i )
350  // printf("Po[%d] = %s\n", iElem, Abc_ObjName( Abc_NtkPo(pNtk, iElem) ) );
351  // hintSingalBeginningMarker = Vec_IntEntry( vCandidateMonotoneSignals, 0 );
352  // hintSingalEndMarker = Vec_IntEntry( vCandidateMonotoneSignals, Vec_IntSize(vCandidateMonotoneSignals) - 1 );
353  // combN_internal = hintSingalEndMarker - hintSingalBeginningMarker + 1;
354  //}
355 
356  combN_internal = Aig_ManRegNum(pAig);
357 
358  pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
359  pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_nCk") + 1 );
360  sprintf(pNewAig->pName, "%s_%s", pAig->pName, "nCk");
361  pNewAig->pSpec = NULL;
362 
363  //Standard Mapping of Constant Nodes
364  pObj = Aig_ManConst1( pAig );
365  pObj->pData = Aig_ManConst1( pNewAig );
366 
367  //Standard AIG PI duplication
368  Saig_ManForEachPi( pAig, pObj, i )
369  {
370  piCopied++;
371  pObj->pData = Aig_ObjCreateCi(pNewAig);
372  }
373 
374  //Standard AIG LO duplication
375  Saig_ManForEachLo( pAig, pObj, i )
376  {
377  loCopied++;
378  pObj->pData = Aig_ObjCreateCi(pNewAig);
379  }
380 
381  //nCk LO creation
382  lCombinationCount = 0;
383  for(combK_internal=1; combK_internal<=combK; combK_internal++)
384  lCombinationCount += countCombination( combN_internal, combK_internal );
385  assert( lCombinationCount > 0 );
386  vLO_nCk = Vec_PtrAlloc(lCombinationCount);
387  for( longI = 0; longI < lCombinationCount; longI++ )
388  {
389  loCreated++;
390  pObj = Aig_ObjCreateCi(pNewAig);
391  Vec_PtrPush( vLO_nCk, pObj );
392  }
393 
394  //Standard Node duplication
395  Aig_ManForEachNode( pAig, pObj, i )
396  {
397  pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
398  }
399 
400  //nCk specific logic creation (i.e. nCk number of OR gates)
401  vDisj_nCk = Vec_PtrAlloc(lCombinationCount);
402 
403  for( combK_internal=1; combK_internal<=combK; combK_internal++ )
404  {
405  generateCombinatorialStabilExhaust( pNewAig, pAig,
406  vDisj_nCk, combN_internal, combK_internal );
407  }
408 
409 
410  //creation of implication logic
411  vPODriver_nCk = Vec_PtrAlloc(lCombinationCount);
412  for( longI = 0; longI < lCombinationCount; longI++ )
413  {
414  pObjLO_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vLO_nCk, longI ));
415  pObjDisj_nCk = (Aig_Obj_t *)(Vec_PtrEntry( vDisj_nCk, longI ));
416 
417  pObj = Aig_Or( pNewAig, Aig_Not(pObjDisj_nCk), pObjLO_nCk);
418  Vec_PtrPush(vPODriver_nCk, pObj);
419  }
420 
421  //Standard PO duplication
422  Saig_ManForEachPo( pAig, pObj, i )
423  {
424  poCopied++;
425  pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
426  }
427 
428  //nCk specific PO creation
429  for( longI = 0; longI < lCombinationCount; longI++ )
430  {
431  Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
432  }
433 
434  //Standard LI duplication
435  Saig_ManForEachLi( pAig, pObj, i )
436  {
437  liCopied++;
438  Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
439  }
440 
441  //nCk specific LI creation
442  for( longI = 0; longI < lCombinationCount; longI++ )
443  {
444  liCreated++;
445  Aig_ObjCreateCo( pNewAig, (Aig_Obj_t *)(Vec_PtrEntry( vPODriver_nCk, longI )) );
446  }
447 
448  //clean-up, book-keeping
449  assert( liCopied + liCreated == loCopied + loCreated );
450  nRegCount = loCopied + loCreated;
451 
452  Aig_ManSetRegNum( pNewAig, nRegCount );
453  Aig_ManCleanup( pNewAig );
454  assert( Aig_ManCheck( pNewAig ) );
455 
456  Vec_PtrFree(vLO_nCk);
457  Vec_PtrFree(vPODriver_nCk);
458  Vec_PtrFree(vDisj_nCk);
459  //Vec_IntFree(vC_KNUTH);
460  return pNewAig;
461 }
462 
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
char * malloc()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
ABC_DLL int Aig_ManCheck(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: aigCheck.c:45
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void * pData
Definition: aig.h:87
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
Aig_Man_t * generateGeneralDisjunctiveTester(Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combK)
Definition: combination.c:321
void listCombination(int n, int t)
Definition: combination.c:20
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
ABC_NAMESPACE_IMPL_START long countCombination(long n, long k)
Definition: combination.c:12
static Aig_Obj_t * Aig_ManLo(Aig_Man_t *p, int i)
Definition: aig.h:268
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
char * sprintf()
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
int generateCombinatorialStabil(Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, Vec_Int_t *vCandidateMonotoneSignals_, Vec_Ptr_t *vDisj_nCk_, int combN, int combK)
Definition: combination.c:54
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
int strlen()
Vec_Int_t * findHintOutputs(Abc_Ntk_t *pNtk)
Definition: monotone.c:90
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_Man_t * generateDisjunctiveTester(Abc_Ntk_t *pNtk, Aig_Man_t *pAig, int combN, int combK)
Definition: combination.c:148
int generateCombinatorialStabilExhaust(Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, Vec_Ptr_t *vDisj_nCk_, int combN, int combK)
Definition: combination.c:101
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91