abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ifSelect.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ifSelect.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [FPGA mapping based on priority cuts.]
8 
9  Synopsis [Cut selection procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - November 21, 2006.]
16 
17  Revision [$Id: ifSelect.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "if.h"
22 #include "sat/bsat/satSolver.h"
23 
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Prints the logic cone with choices.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void If_ObjConePrint_rec( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
47 {
48  If_Cut_t * pCut;
49  pCut = If_ObjCutBest(pIfObj);
50  if ( If_CutDataInt(pCut) )
51  return;
52  Vec_PtrPush( vVisited, pCut );
53  // insert the worst case
54  If_CutSetDataInt( pCut, ~0 );
55  // skip in case of primary input
56  if ( If_ObjIsCi(pIfObj) )
57  return;
58  // compute the functions of the children
59  if ( pIfObj->pEquiv )
60  If_ObjConePrint_rec( pIfMan, pIfObj->pEquiv, vVisited );
61  If_ObjConePrint_rec( pIfMan, pIfObj->pFanin0, vVisited );
62  If_ObjConePrint_rec( pIfMan, pIfObj->pFanin1, vVisited );
63  printf( "%5d = %5d & %5d | %5d\n", pIfObj->Id, pIfObj->pFanin0->Id, pIfObj->pFanin1->Id, pIfObj->pEquiv ? pIfObj->pEquiv->Id : 0 );
64 }
65 void If_ObjConePrint( If_Man_t * pIfMan, If_Obj_t * pIfObj )
66 {
67  If_Cut_t * pCut;
68  If_Obj_t * pLeaf;
69  int i;
70  Vec_PtrClear( pIfMan->vTemp );
71  If_ObjConePrint_rec( pIfMan, pIfObj, pIfMan->vTemp );
72  Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
73  If_CutSetDataInt( pCut, 0 );
74  // print the leaf variables
75  printf( "Cut " );
76  pCut = If_ObjCutBest(pIfObj);
77  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
78  printf( "%d ", pLeaf->Id );
79  printf( "\n" );
80 }
81 
82 
83 /**Function*************************************************************
84 
85  Synopsis [Recursively derives local AIG for the cut.]
86 
87  Description []
88 
89  SideEffects []
90 
91  SeeAlso []
92 
93 ***********************************************************************/
94 int If_ManNodeShapeMap_rec( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, Vec_Int_t * vShape )
95 {
96  If_Cut_t * pCut;
97  If_Obj_t * pTemp;
98  int i, iFunc0, iFunc1;
99  // get the best cut
100  pCut = If_ObjCutBest(pIfObj);
101  // if the cut is visited, return the result
102  if ( If_CutDataInt(pCut) )
103  return If_CutDataInt(pCut);
104  // mark the node as visited
105  Vec_PtrPush( vVisited, pCut );
106  // insert the worst case
107  If_CutSetDataInt( pCut, ~0 );
108  // skip in case of primary input
109  if ( If_ObjIsCi(pIfObj) )
110  return If_CutDataInt(pCut);
111  // compute the functions of the children
112  for ( i = 0, pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv, i++ )
113  {
114  iFunc0 = If_ManNodeShapeMap_rec( pIfMan, pTemp->pFanin0, vVisited, vShape );
115  if ( iFunc0 == ~0 )
116  continue;
117  iFunc1 = If_ManNodeShapeMap_rec( pIfMan, pTemp->pFanin1, vVisited, vShape );
118  if ( iFunc1 == ~0 )
119  continue;
120  // both branches are solved
121  Vec_IntPush( vShape, pIfObj->Id );
122  Vec_IntPush( vShape, pTemp->Id );
123  If_CutSetDataInt( pCut, 1 );
124  break;
125  }
126  return If_CutDataInt(pCut);
127 }
128 int If_ManNodeShapeMap( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape )
129 {
130  If_Cut_t * pCut;
131  If_Obj_t * pLeaf;
132  int i, iRes;
133  // get the best cut
134  pCut = If_ObjCutBest(pIfObj);
135  assert( pCut->nLeaves > 1 );
136  // set the leaf variables
137  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
138  {
139  assert( If_CutDataInt( If_ObjCutBest(pLeaf) ) == 0 );
140  If_CutSetDataInt( If_ObjCutBest(pLeaf), 1 );
141  }
142  // recursively compute the function while collecting visited cuts
143  Vec_IntClear( vShape );
144  Vec_PtrClear( pIfMan->vTemp );
145  iRes = If_ManNodeShapeMap_rec( pIfMan, pIfObj, pIfMan->vTemp, vShape );
146  if ( iRes == ~0 )
147  {
148  Abc_Print( -1, "If_ManNodeShapeMap(): Computing local AIG has failed.\n" );
149  return 0;
150  }
151  // clean the cuts
152  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
153  If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
154  Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
155  If_CutSetDataInt( pCut, 0 );
156  return 1;
157 }
158 
159 
160 /**Function*************************************************************
161 
162  Synopsis [Recursively derives the local AIG for the cut.]
163 
164  Description []
165 
166  SideEffects []
167 
168  SeeAlso []
169 
170 ***********************************************************************/
171 static inline int If_WordCountOnes( unsigned uWord )
172 {
173  uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
174  uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
175  uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
176  uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
177  return (uWord & 0x0000FFFF) + (uWord>>16);
178 }
179 int If_ManNodeShapeMap2_rec( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, Vec_Int_t * vShape )
180 {
181  If_Cut_t * pCut;
182  If_Obj_t * pTemp, * pTempBest = NULL;
183  int i, iFunc, iFunc0, iFunc1, iBest = 0;
184  // get the best cut
185  pCut = If_ObjCutBest(pIfObj);
186  // if the cut is visited, return the result
187  if ( If_CutDataInt(pCut) )
188  return If_CutDataInt(pCut);
189  // mark the node as visited
190  Vec_PtrPush( vVisited, pCut );
191  // insert the worst case
192  If_CutSetDataInt( pCut, ~0 );
193  // skip in case of primary input
194  if ( If_ObjIsCi(pIfObj) )
195  return If_CutDataInt(pCut);
196  // compute the functions of the children
197  for ( i = 0, pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv, i++ )
198  {
199  iFunc0 = If_ManNodeShapeMap2_rec( pIfMan, pTemp->pFanin0, vVisited, vShape );
200  if ( iFunc0 == ~0 )
201  continue;
202  iFunc1 = If_ManNodeShapeMap2_rec( pIfMan, pTemp->pFanin1, vVisited, vShape );
203  if ( iFunc1 == ~0 )
204  continue;
205  iFunc = iFunc0 | iFunc1;
206 // if ( If_WordCountOnes(iBest) <= If_WordCountOnes(iFunc) )
207  if ( iBest < iFunc )
208  {
209  iBest = iFunc;
210  pTempBest = pTemp;
211  }
212  }
213  if ( pTempBest )
214  {
215  Vec_IntPush( vShape, pIfObj->Id );
216  Vec_IntPush( vShape, pTempBest->Id );
217  If_CutSetDataInt( pCut, iBest );
218  }
219  return If_CutDataInt(pCut);
220 }
221 int If_ManNodeShapeMap2( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape )
222 {
223  If_Cut_t * pCut;
224  If_Obj_t * pLeaf;
225  int i, iRes;
226  // get the best cut
227  pCut = If_ObjCutBest(pIfObj);
228  assert( pCut->nLeaves > 1 );
229  // set the leaf variables
230  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
231  If_CutSetDataInt( If_ObjCutBest(pLeaf), (1 << i) );
232  // recursively compute the function while collecting visited cuts
233  Vec_IntClear( vShape );
234  Vec_PtrClear( pIfMan->vTemp );
235  iRes = If_ManNodeShapeMap2_rec( pIfMan, pIfObj, pIfMan->vTemp, vShape );
236  if ( iRes == ~0 )
237  {
238  Abc_Print( -1, "If_ManNodeShapeMap2(): Computing local AIG has failed.\n" );
239  return 0;
240  }
241  // clean the cuts
242  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
243  If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
244  Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
245  If_CutSetDataInt( pCut, 0 );
246  return 1;
247 }
248 
249 
250 
251 /**Function*************************************************************
252 
253  Synopsis [Collects logic cone with choices]
254 
255  Description []
256 
257  SideEffects []
258 
259  SeeAlso []
260 
261 ***********************************************************************/
262 int If_ManConeCollect_rec( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, Vec_Ptr_t * vCone )
263 {
264  If_Cut_t * pCut;
265  If_Obj_t * pTemp;
266  int iFunc0, iFunc1;
267  int fRootAdded = 0;
268  int fNodeAdded = 0;
269  // get the best cut
270  pCut = If_ObjCutBest(pIfObj);
271  // if the cut is visited, return the result
272  if ( If_CutDataInt(pCut) )
273  return If_CutDataInt(pCut);
274  // mark the node as visited
275  Vec_PtrPush( vVisited, pCut );
276  // insert the worst case
277  If_CutSetDataInt( pCut, ~0 );
278  // skip in case of primary input
279  if ( If_ObjIsCi(pIfObj) )
280  return If_CutDataInt(pCut);
281  // compute the functions of the children
282  for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
283  {
284  iFunc0 = If_ManConeCollect_rec( pIfMan, pTemp->pFanin0, vVisited, vCone );
285  if ( iFunc0 == ~0 )
286  continue;
287  iFunc1 = If_ManConeCollect_rec( pIfMan, pTemp->pFanin1, vVisited, vCone );
288  if ( iFunc1 == ~0 )
289  continue;
290  fNodeAdded = 1;
291  If_CutSetDataInt( pCut, 1 );
292  Vec_PtrPush( vCone, pTemp );
293  if ( fRootAdded == 0 && pTemp == pIfObj )
294  fRootAdded = 1;
295  }
296  if ( fNodeAdded && !fRootAdded )
297  Vec_PtrPush( vCone, pIfObj );
298  return If_CutDataInt(pCut);
299 }
300 Vec_Ptr_t * If_ManConeCollect( If_Man_t * pIfMan, If_Obj_t * pIfObj, If_Cut_t * pCut )
301 {
302  Vec_Ptr_t * vCone;
303  If_Obj_t * pLeaf;
304  int i, RetValue;
305  // set the leaf variables
306  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
307  {
308  assert( If_CutDataInt( If_ObjCutBest(pLeaf) ) == 0 );
309  If_CutSetDataInt( If_ObjCutBest(pLeaf), 1 );
310  }
311  // recursively compute the function while collecting visited cuts
312  vCone = Vec_PtrAlloc( 100 );
313  Vec_PtrClear( pIfMan->vTemp );
314  RetValue = If_ManConeCollect_rec( pIfMan, pIfObj, pIfMan->vTemp, vCone );
315  assert( RetValue );
316  // clean the cuts
317  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
318  If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
319  Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
320  If_CutSetDataInt( pCut, 0 );
321  return vCone;
322 }
323 
324 /**Function*************************************************************
325 
326  Synopsis [Adding clauses.]
327 
328  Description []
329 
330  SideEffects []
331 
332  SeeAlso []
333 
334 ***********************************************************************/
335 static inline void sat_solver_add_choice( sat_solver * pSat, int iVar, Vec_Int_t * vVars )
336 {
337  int * pVars = Vec_IntArray(vVars);
338  int nVars = Vec_IntSize(vVars);
339  int i, k, Lits[2], Value;
340  assert( Vec_IntSize(vVars) < Vec_IntCap(vVars) );
341  // create literals
342  for ( i = 0; i < nVars; i++ )
343  pVars[i] = Abc_Var2Lit( pVars[i], 0 );
344  pVars[i] = Abc_Var2Lit( iVar, 1 );
345  // add clause
346  Value = sat_solver_addclause( pSat, pVars, pVars + nVars + 1 );
347  assert( Value );
348  // undo literals
349  for ( i = 0; i < nVars; i++ )
350  pVars[i] = Abc_Lit2Var( pVars[i] );
351  // add !out => !in
352  Lits[0] = Abc_Var2Lit( iVar, 0 );
353  for ( i = 0; i < nVars; i++ )
354  {
355  Lits[1] = Abc_Var2Lit( pVars[i], 1 );
356  Value = sat_solver_addclause( pSat, Lits, Lits + 2 );
357  assert( Value );
358  }
359  // add excluvisity
360  for ( i = 0; i < nVars; i++ )
361  for ( k = i+1; k < nVars; k++ )
362  {
363  Lits[0] = Abc_Var2Lit( pVars[i], 1 );
364  Lits[1] = Abc_Var2Lit( pVars[k], 1 );
365  Value = sat_solver_addclause( pSat, Lits, Lits + 2 );
366  assert( Value );
367  }
368 }
369 static inline int If_ObjSatVar( If_Obj_t * pIfObj ) { return If_CutDataInt(If_ObjCutBest(pIfObj)); }
370 static inline void If_ObjSetSatVar( If_Obj_t * pIfObj, int v ) { If_CutSetDataInt( If_ObjCutBest(pIfObj), v ); }
371 
372 
373 /**Function*************************************************************
374 
375  Synopsis [Recursively derives the local AIG for the cut.]
376 
377  Description []
378 
379  SideEffects []
380 
381  SeeAlso []
382 
383 ***********************************************************************/
384 void If_ManNodeShape2_rec( sat_solver * pSat, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape )
385 {
386  If_Obj_t * pTemp;
387  assert( sat_solver_var_value(pSat, If_ObjSatVar(pIfObj)) == 1 );
388  if ( pIfObj->fMark )
389  return;
390  pIfObj->fMark = 1;
391  for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
392  if ( sat_solver_var_value(pSat, If_ObjSatVar(pTemp)+1) == 1 )
393  break;
394  assert( pTemp != NULL );
395  If_ManNodeShape2_rec( pSat, pIfMan, pTemp->pFanin0, vShape );
396  If_ManNodeShape2_rec( pSat, pIfMan, pTemp->pFanin1, vShape );
397  Vec_IntPush( vShape, pIfObj->Id );
398  Vec_IntPush( vShape, pTemp->Id );
399 }
400 
401 /**Function*************************************************************
402 
403  Synopsis [Solve the problem of selecting choices for the given cut.]
404 
405  Description []
406 
407  SideEffects []
408 
409  SeeAlso []
410 
411 ***********************************************************************/
412 int If_ManNodeShapeSat( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape )
413 {
414  sat_solver * pSat;
415  If_Cut_t * pCut;
416  Vec_Ptr_t * vCone;
417  Vec_Int_t * vFanins;
418  If_Obj_t * pObj, * pTemp;
419  int i, Lit, Status;
420 
421  // get best cut
422  pCut = If_ObjCutBest(pIfObj);
423  assert( pCut->nLeaves > 1 );
424 
425  // collect the cone
426  vCone = If_ManConeCollect( pIfMan, pIfObj, pCut );
427 
428  // assign SAT variables
429  // EXTERNAL variable is even numbered
430  // INTERNAL variable is odd numbered
431  If_CutForEachLeaf( pIfMan, pCut, pObj, i )
432  {
433  assert( If_ObjSatVar(pObj) == 0 );
434  If_ObjSetSatVar( pObj, 2*(i+1) );
435  }
436  Vec_PtrForEachEntry( If_Obj_t *, vCone, pObj, i )
437  {
438  assert( If_ObjSatVar(pObj) == 0 );
439  If_ObjSetSatVar( pObj, 2*(i+1+pCut->nLeaves) );
440  }
441 
442  // start SAT solver
443  pSat = sat_solver_new();
444  sat_solver_setnvars( pSat, 2 * (pCut->nLeaves + Vec_PtrSize(vCone) + 1) );
445 
446  // add constraints
447  vFanins = Vec_IntAlloc( 100 );
448  Vec_PtrForEachEntry( If_Obj_t *, vCone, pObj, i )
449  {
450  assert( If_ObjIsAnd(pObj) );
451  Vec_IntClear( vFanins );
452  for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
453  if ( If_ObjSatVar(pTemp) )
454  Vec_IntPush( vFanins, If_ObjSatVar(pTemp)+1 ); // internal
455  assert( Vec_IntSize(vFanins) > 0 );
456  sat_solver_add_choice( pSat, If_ObjSatVar(pObj), vFanins ); // external
457  assert( If_ObjSatVar(pObj) > 0 );
458 // sat_solver_add_and( pSat, If_ObjSatVar(pObj)+1, If_ObjSatVar(pObj->pFanin0), If_ObjSatVar(pObj->pFanin1), 0, 0, 0 );
459  if ( If_ObjSatVar(pObj->pFanin0) > 0 && If_ObjSatVar(pObj->pFanin1) > 0 )
460  {
461  int Lits[2];
462  Lits[0] = Abc_Var2Lit( If_ObjSatVar(pObj)+1, 1 );
463  Lits[1] = Abc_Var2Lit( If_ObjSatVar(pObj->pFanin0), 0 );
464  Status = sat_solver_addclause( pSat, Lits, Lits + 2 );
465  assert( Status );
466 
467  Lits[0] = Abc_Var2Lit( If_ObjSatVar(pObj)+1, 1 );
468  Lits[1] = Abc_Var2Lit( If_ObjSatVar(pObj->pFanin1), 0 );
469  Status = sat_solver_addclause( pSat, Lits, Lits + 2 );
470  assert( Status );
471  }
472  }
473  Vec_IntFree( vFanins );
474 
475  // set cut variables to 1
476  pCut = If_ObjCutBest(pIfObj);
477  If_CutForEachLeaf( pIfMan, pCut, pObj, i )
478  {
479  Lit = Abc_Var2Lit( If_ObjSatVar(pObj), 0 ); // external
480  Status = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
481  assert( Status );
482  }
483  // set output variable to 1
484  Lit = Abc_Var2Lit( If_ObjSatVar(pIfObj), 0 ); // external
485  Status = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
486  assert( Status );
487 
488  // solve the problem
489  Status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
490  assert( Status == l_True );
491 
492  // mark cut nodes
493  If_CutForEachLeaf( pIfMan, pCut, pObj, i )
494  {
495  assert( pObj->fMark == 0 );
496  pObj->fMark = 1;
497  }
498 
499  // select the node's shape
500  Vec_IntClear( vShape );
501  assert( pIfObj->fMark == 0 );
502  If_ManNodeShape2_rec( pSat, pIfMan, pIfObj, vShape );
503 
504  // cleanup
505  sat_solver_delete( pSat );
506  If_CutForEachLeaf( pIfMan, pCut, pObj, i )
507  {
508  If_ObjSetSatVar( pObj, 0 );
509  pObj->fMark = 0;
510  }
511  Vec_PtrForEachEntry( If_Obj_t *, vCone, pObj, i )
512  {
513  If_ObjSetSatVar( pObj, 0 );
514  pObj->fMark = 0;
515  }
516  Vec_PtrFree( vCone );
517  return 1;
518 }
519 
520 
521 /**Function*************************************************************
522 
523  Synopsis [Verify that the shape is correct.]
524 
525  Description []
526 
527  SideEffects []
528 
529  SeeAlso []
530 
531 ***********************************************************************/
532 int If_ManCheckShape( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape )
533 {
534  If_Cut_t * pCut;
535  If_Obj_t * pLeaf;
536  int i, Entry1, Entry2, RetValue = 1;
537  // check that the marks are not set
538  pCut = If_ObjCutBest(pIfObj);
539  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
540  assert( pLeaf->fMark == 0 );
541  // set the marks of the shape
542  Vec_IntForEachEntryDouble( vShape, Entry1, Entry2, i )
543  {
544  pLeaf = If_ManObj(pIfMan, Entry2);
545  pLeaf->pFanin0->fMark = 1;
546  pLeaf->pFanin1->fMark = 1;
547  }
548  // check that the leaves are marked
549  If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
550  if ( pLeaf->fMark == 0 )
551  RetValue = 0;
552  else
553  pLeaf->fMark = 0;
554  // clean the inner marks
555  Vec_IntForEachEntryDouble( vShape, Entry1, Entry2, i )
556  {
557  pLeaf = If_ManObj(pIfMan, Entry2);
558  pLeaf->pFanin0->fMark = 0;
559  pLeaf->pFanin1->fMark = 0;
560  }
561  return RetValue;
562 }
563 
564 /**Function*************************************************************
565 
566  Synopsis [Recursively compute the set of nodes supported by the cut.]
567 
568  Description []
569 
570  SideEffects []
571 
572  SeeAlso []
573 
574 ***********************************************************************/
575 int If_ManNodeShape( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape, int fExact )
576 {
577  int RetValue;
578 // if ( pIfMan->nChoices == 0 )
579  {
580  RetValue = If_ManNodeShapeMap( pIfMan, pIfObj, vShape );
581  assert( RetValue );
582  if ( !fExact || If_ManCheckShape(pIfMan, pIfObj, vShape) )
583  return 1;
584  }
585 // if ( pIfObj->Id == 1254 && If_ObjCutBest(pIfObj)->nLeaves == 7 )
586 // If_ObjConePrint( pIfMan, pIfObj );
587  RetValue = If_ManNodeShapeMap2( pIfMan, pIfObj, vShape );
588  assert( RetValue );
589  RetValue = If_ManCheckShape(pIfMan, pIfObj, vShape);
590 // assert( RetValue );
591 // printf( "%d", RetValue );
592  return 1;
593 }
594 
595 ////////////////////////////////////////////////////////////////////////
596 /// END OF FILE ///
597 ////////////////////////////////////////////////////////////////////////
598 
599 
601 
If_Obj_t * pFanin0
Definition: if.h:321
int If_ManNodeShapeMap2(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Int_t *vShape)
Definition: ifSelect.c:221
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
unsigned nLeaves
Definition: if.h:289
int Id
Definition: if.h:316
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static If_Obj_t * If_ManObj(If_Man_t *p, int i)
Definition: if.h:370
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Ptr_t * vTemp
Definition: if.h:191
Definition: if.h:303
static int If_ObjIsAnd(If_Obj_t *pObj)
Definition: if.h:377
Definition: if.h:275
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
#define If_CutForEachLeaf(p, pCut, pLeaf, i)
Definition: if.h:474
int If_ManNodeShapeMap(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Int_t *vShape)
Definition: ifSelect.c:128
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static void If_ObjSetSatVar(If_Obj_t *pIfObj, int v)
Definition: ifSelect.c:370
void If_ObjConePrint(If_Man_t *pIfMan, If_Obj_t *pIfObj)
Definition: ifSelect.c:65
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define l_True
Definition: SolverTypes.h:84
static int If_ObjIsCi(If_Obj_t *pObj)
Definition: if.h:373
static If_Cut_t * If_ObjCutBest(If_Obj_t *pObj)
Definition: if.h:401
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
int If_ManNodeShape(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Int_t *vShape, int fExact)
Definition: ifSelect.c:575
void If_ManNodeShape2_rec(sat_solver *pSat, If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Int_t *vShape)
Definition: ifSelect.c:384
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
int If_ManNodeShapeSat(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Int_t *vShape)
Definition: ifSelect.c:412
static void If_CutSetDataInt(If_Cut_t *pCut, int Data)
Definition: if.h:415
Definition: if.h:180
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_Ptr_t * If_ManConeCollect(If_Man_t *pIfMan, If_Obj_t *pIfObj, If_Cut_t *pCut)
Definition: ifSelect.c:300
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static void sat_solver_add_choice(sat_solver *pSat, int iVar, Vec_Int_t *vVars)
Definition: ifSelect.c:335
static int If_CutDataInt(If_Cut_t *pCut)
Definition: if.h:414
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
If_Obj_t * pFanin1
Definition: if.h:322
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
int If_ManNodeShapeMap_rec(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Ptr_t *vVisited, Vec_Int_t *vShape)
Definition: ifSelect.c:94
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
If_Obj_t * pEquiv
Definition: if.h:323
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition: vecInt.h:66
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static int If_ObjSatVar(If_Obj_t *pIfObj)
Definition: ifSelect.c:369
static int If_WordCountOnes(unsigned uWord)
Definition: ifSelect.c:171
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
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
int If_ManCheckShape(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Int_t *vShape)
Definition: ifSelect.c:532
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
int If_ManConeCollect_rec(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Ptr_t *vVisited, Vec_Ptr_t *vCone)
Definition: ifSelect.c:262
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int If_ManNodeShapeMap2_rec(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Ptr_t *vVisited, Vec_Int_t *vShape)
Definition: ifSelect.c:179
unsigned fMark
Definition: if.h:310
ABC_NAMESPACE_IMPL_START void If_ObjConePrint_rec(If_Man_t *pIfMan, If_Obj_t *pIfObj, Vec_Ptr_t *vVisited)
DECLARATIONS ///.
Definition: ifSelect.c:46
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223