abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaHcd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaHcd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [New choice computation package.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaHcd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "giaAig.h"
23 #include "aig/aig/aig.h"
24 #include "opt/dar/dar.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 // choicing parameters
34 typedef struct Hcd_Pars_t_ Hcd_Pars_t;
35 struct Hcd_Pars_t_
36 {
37  int nWords; // the number of simulation words
38  int nBTLimit; // conflict limit at a node
39  int nSatVarMax; // the max number of SAT variables
40  int fSynthesis; // set to 1 to perform synthesis
41  int fPolarFlip; // uses polarity adjustment
42  int fSimulateTfo; // uses simulation of TFO classes
43  int fPower; // uses power-aware rewriting
44  int fUseGia; // uses GIA package
45  int fUseCSat; // uses circuit-based solver
46  int fVerbose; // verbose stats
47  clock_t timeSynth; // synthesis runtime
48  int nNodesAhead; // the lookahead in terms of nodes
49  int nCallsRecycle; // calls to perform before recycling SAT solver
50 };
51 
52 extern void Gia_ComputeEquivalences( Gia_Man_t * pMiter, int nBTLimit, int fUseMiniSat, int fVerbose );
53 
54 ////////////////////////////////////////////////////////////////////////
55 /// FUNCTION DEFINITIONS ///
56 ////////////////////////////////////////////////////////////////////////
57 
58 /**Function*************************************************************
59 
60  Synopsis [This procedure sets default parameters.]
61 
62  Description []
63 
64  SideEffects []
65 
66  SeeAlso []
67 
68 ***********************************************************************/
69 void Hcd_ManSetDefaultParams( Hcd_Pars_t * p )
70 {
71  memset( p, 0, sizeof(Hcd_Pars_t) );
72  p->nWords = 8; // the number of simulation words
73  p->nBTLimit = 1000; // conflict limit at a node
74  p->nSatVarMax = 5000; // the max number of SAT variables
75  p->fSynthesis = 1; // derives three snapshots
76  p->fPolarFlip = 1; // uses polarity adjustment
77  p->fSimulateTfo = 1; // simulate TFO
78  p->fPower = 0; // power-aware rewriting
79  p->fVerbose = 0; // verbose stats
80  p->nNodesAhead = 1000; // the lookahead in terms of nodes
81  p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
82 }
83 
84 
85 /**Function*************************************************************
86 
87  Synopsis [Reproduces script "compress".]
88 
89  Description []
90 
91  SideEffects []
92 
93  SeeAlso []
94 
95 ***********************************************************************/
96 Aig_Man_t * Hcd_Compress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
97 //alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
98 {
99  Aig_Man_t * pTemp;
100 
101  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
102  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
103 
104  Dar_ManDefaultRwrParams( pParsRwr );
105  Dar_ManDefaultRefParams( pParsRef );
106 
107  pParsRwr->fUpdateLevel = fUpdateLevel;
108  pParsRef->fUpdateLevel = fUpdateLevel;
109 
110  pParsRwr->fPower = fPower;
111 
112  pParsRwr->fVerbose = 0;//fVerbose;
113  pParsRef->fVerbose = 0;//fVerbose;
114 
115 // pAig = Aig_ManDupDfs( pAig );
116  if ( fVerbose ) Aig_ManPrintStats( pAig );
117 
118  // rewrite
119  Dar_ManRewrite( pAig, pParsRwr );
120  pAig = Aig_ManDupDfs( pTemp = pAig );
121  Aig_ManStop( pTemp );
122  if ( fVerbose ) Aig_ManPrintStats( pAig );
123 
124  // refactor
125  Dar_ManRefactor( pAig, pParsRef );
126  pAig = Aig_ManDupDfs( pTemp = pAig );
127  Aig_ManStop( pTemp );
128  if ( fVerbose ) Aig_ManPrintStats( pAig );
129 
130  // balance
131  if ( fBalance )
132  {
133  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
134  Aig_ManStop( pTemp );
135  if ( fVerbose ) Aig_ManPrintStats( pAig );
136  }
137 
138  pParsRwr->fUseZeros = 1;
139  pParsRef->fUseZeros = 1;
140 
141  // rewrite
142  Dar_ManRewrite( pAig, pParsRwr );
143  pAig = Aig_ManDupDfs( pTemp = pAig );
144  Aig_ManStop( pTemp );
145  if ( fVerbose ) Aig_ManPrintStats( pAig );
146 
147  return pAig;
148 }
149 
150 /**Function*************************************************************
151 
152  Synopsis [Reproduces script "compress2".]
153 
154  Description []
155 
156  SideEffects []
157 
158  SeeAlso []
159 
160 ***********************************************************************/
161 Aig_Man_t * Hcd_Compress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
162 //alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
163 {
164  Aig_Man_t * pTemp;
165 
166  Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
167  Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
168 
169  Dar_ManDefaultRwrParams( pParsRwr );
170  Dar_ManDefaultRefParams( pParsRef );
171 
172  pParsRwr->fUpdateLevel = fUpdateLevel;
173  pParsRef->fUpdateLevel = fUpdateLevel;
174  pParsRwr->fFanout = fFanout;
175  pParsRwr->fPower = fPower;
176 
177  pParsRwr->fVerbose = 0;//fVerbose;
178  pParsRef->fVerbose = 0;//fVerbose;
179 
180 // pAig = Aig_ManDupDfs( pAig );
181  if ( fVerbose ) Aig_ManPrintStats( pAig );
182 
183  // rewrite
184  Dar_ManRewrite( pAig, pParsRwr );
185  pAig = Aig_ManDupDfs( pTemp = pAig );
186  Aig_ManStop( pTemp );
187  if ( fVerbose ) Aig_ManPrintStats( pAig );
188 
189  // refactor
190  Dar_ManRefactor( pAig, pParsRef );
191  pAig = Aig_ManDupDfs( pTemp = pAig );
192  Aig_ManStop( pTemp );
193  if ( fVerbose ) Aig_ManPrintStats( pAig );
194 
195  // balance
196 // if ( fBalance )
197  {
198  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
199  Aig_ManStop( pTemp );
200  if ( fVerbose ) Aig_ManPrintStats( pAig );
201  }
202 
203  // rewrite
204  Dar_ManRewrite( pAig, pParsRwr );
205  pAig = Aig_ManDupDfs( pTemp = pAig );
206  Aig_ManStop( pTemp );
207  if ( fVerbose ) Aig_ManPrintStats( pAig );
208 
209  pParsRwr->fUseZeros = 1;
210  pParsRef->fUseZeros = 1;
211 
212  // rewrite
213  Dar_ManRewrite( pAig, pParsRwr );
214  pAig = Aig_ManDupDfs( pTemp = pAig );
215  Aig_ManStop( pTemp );
216  if ( fVerbose ) Aig_ManPrintStats( pAig );
217 
218  // balance
219  if ( fBalance )
220  {
221  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
222  Aig_ManStop( pTemp );
223  if ( fVerbose ) Aig_ManPrintStats( pAig );
224  }
225 
226  // refactor
227  Dar_ManRefactor( pAig, pParsRef );
228  pAig = Aig_ManDupDfs( pTemp = pAig );
229  Aig_ManStop( pTemp );
230  if ( fVerbose ) Aig_ManPrintStats( pAig );
231 
232  // rewrite
233  Dar_ManRewrite( pAig, pParsRwr );
234  pAig = Aig_ManDupDfs( pTemp = pAig );
235  Aig_ManStop( pTemp );
236  if ( fVerbose ) Aig_ManPrintStats( pAig );
237 
238  // balance
239  if ( fBalance )
240  {
241  pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
242  Aig_ManStop( pTemp );
243  if ( fVerbose ) Aig_ManPrintStats( pAig );
244  }
245  return pAig;
246 }
247 
248 /**Function*************************************************************
249 
250  Synopsis [Reproduces script "compress2".]
251 
252  Description []
253 
254  SideEffects []
255 
256  SeeAlso []
257 
258 ***********************************************************************/
259 Vec_Ptr_t * Hcd_ChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
260 //alias resyn "b; rw; rwz; b; rwz; b"
261 //alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
262 {
263  Vec_Ptr_t * vGias;
264  Gia_Man_t * pGia;
265 
266  vGias = Vec_PtrAlloc( 3 );
267  pGia = Gia_ManFromAig(pAig);
268  Vec_PtrPush( vGias, pGia );
269 
270  pAig = Hcd_Compress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
271  pGia = Gia_ManFromAig(pAig);
272  Vec_PtrPush( vGias, pGia );
273 //Aig_ManPrintStats( pAig );
274 
275  pAig = Hcd_Compress2( pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose );
276  pGia = Gia_ManFromAig(pAig);
277  Vec_PtrPush( vGias, pGia );
278 //Aig_ManPrintStats( pAig );
279 
280  Aig_ManStop( pAig );
281  return vGias;
282 }
283 
284 
285 /**Function*************************************************************
286 
287  Synopsis [Duplicates the AIG in the DFS order.]
288 
289  Description []
290 
291  SideEffects []
292 
293  SeeAlso []
294 
295 ***********************************************************************/
296 int Hcd_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
297 {
298  if ( ~pObj->Value )
299  return pObj->Value;
300  Hcd_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
301  if ( Gia_ObjIsCo(pObj) )
302  return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
303  Hcd_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
304  return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
305 }
306 
307 /**Function*************************************************************
308 
309  Synopsis [Derives the miter of several AIGs for choice computation.]
310 
311  Description []
312 
313  SideEffects []
314 
315  SeeAlso []
316 
317 ***********************************************************************/
318 Gia_Man_t * Hcd_ManChoiceMiter( Vec_Ptr_t * vGias )
319 {
320  Gia_Man_t * pNew, * pGia, * pGia0;
321  int i, k, iNode, nNodes;
322  // make sure they have equal parameters
323  assert( Vec_PtrSize(vGias) > 0 );
324  pGia0 = (Gia_Man_t *)Vec_PtrEntry( vGias, 0 );
325  Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
326  {
327  assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) );
328  assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) );
329  assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
330  Gia_ManFillValue( pGia );
331  Gia_ManConst0(pGia)->Value = 0;
332  }
333  // start the new manager
334  pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
335  pNew->pName = Abc_UtilStrsav( pGia0->pName );
336  pNew->pSpec = Abc_UtilStrsav( pGia0->pSpec );
337  // create new CIs and assign them to the old manager CIs
338  for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
339  {
340  iNode = Gia_ManAppendCi(pNew);
341  Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
342  Gia_ManCi( pGia, k )->Value = iNode;
343  }
344  // create internal nodes
345  Gia_ManHashAlloc( pNew );
346  for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
347  {
348  Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
349  Hcd_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
350  }
351  Gia_ManHashStop( pNew );
352  // check the presence of dangling nodes
353  nNodes = Gia_ManHasDangling( pNew );
354  assert( nNodes == 0 );
355  return pNew;
356 }
357 
358 /**Function*************************************************************
359 
360  Synopsis [Returns 1 if pOld is in the TFI of pNode.]
361 
362  Description []
363 
364  SideEffects []
365 
366  SeeAlso []
367 
368 ***********************************************************************/
369 int Hcd_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
370 {
371  // check the trivial cases
372  if ( pNode == NULL )
373  return 0;
374  if ( Gia_ObjIsCi(pNode) )
375  return 0;
376 // if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
377 // return 0;
378  if ( pNode == pOld )
379  return 1;
380  // skip the visited node
381  if ( pNode->fMark0 )
382  return 0;
383  pNode->fMark0 = 1;
384  Vec_PtrPush( vVisited, pNode );
385  // check the children
386  if ( Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
387  return 1;
388  if ( Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
389  return 1;
390  // check equivalent nodes
391  return Hcd_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
392 }
393 
394 /**Function*************************************************************
395 
396  Synopsis [Returns 1 if pOld is in the TFI of pNode.]
397 
398  Description []
399 
400  SideEffects []
401 
402  SeeAlso []
403 
404 ***********************************************************************/
405 int Hcd_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
406 {
407  Vec_Ptr_t * vVisited;
408  Gia_Obj_t * pObj;
409  int RetValue, i;
410  assert( !Gia_IsComplement(pOld) );
411  assert( !Gia_IsComplement(pNode) );
412  vVisited = Vec_PtrAlloc( 100 );
413  RetValue = Hcd_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
414  Vec_PtrForEachEntry( Gia_Obj_t *, vVisited, pObj, i )
415  pObj->fMark0 = 0;
416  Vec_PtrFree( vVisited );
417  return RetValue;
418 }
419 
420 /**Function*************************************************************
421 
422  Synopsis [Adds the next entry while making choices.]
423 
424  Description []
425 
426  SideEffects []
427 
428  SeeAlso []
429 
430 ***********************************************************************/
431 void Hcd_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
432 {
433  if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
434  {
435  Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
436  return;
437  }
438  Hcd_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
439 }
440 
441 /**Function*************************************************************
442 
443  Synopsis [Duplicates the AIG in the DFS order.]
444 
445  Description []
446 
447  SideEffects []
448 
449  SeeAlso []
450 
451 ***********************************************************************/
452 void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
453 {
454  Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
455  if ( ~pObj->Value )
456  return;
457  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
458  {
459  if ( Gia_ObjIsConst0(pRepr) )
460  {
461  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
462  return;
463  }
464  Hcd_ManEquivToChoices_rec( pNew, p, pRepr );
465  assert( Gia_ObjIsAnd(pObj) );
466  Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
467  Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
468  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
469  if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
470  {
471  assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
472  return;
473  }
474  if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
475  return;
476  assert( pRepr->Value < pObj->Value );
477  pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
478  pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
479  if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
480  {
481  assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
482  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
483  return;
484  }
485  if ( !Hcd_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
486  {
487  assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
488  Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
489  Hcd_ManAddNextEntry_rec( pNew, pReprNew, pObjNew );
490  }
491  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
492  return;
493  }
494  assert( Gia_ObjIsAnd(pObj) );
495  Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
496  Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
497  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
498 }
499 
500 /**Function*************************************************************
501 
502  Synopsis [Removes choices, which contain fanouts.]
503 
504  Description []
505 
506  SideEffects []
507 
508  SeeAlso []
509 
510 ***********************************************************************/
511 void Hcd_ManRemoveBadChoices( Gia_Man_t * p )
512 {
513  Gia_Obj_t * pObj;
514  int i, iObj, iPrev, Counter = 0;
515  // mark nodes with fanout
516  Gia_ManForEachObj( p, pObj, i )
517  {
518  pObj->fMark0 = 0;
519  if ( Gia_ObjIsAnd(pObj) )
520  {
521  Gia_ObjFanin0(pObj)->fMark0 = 1;
522  Gia_ObjFanin1(pObj)->fMark0 = 1;
523  }
524  else if ( Gia_ObjIsCo(pObj) )
525  Gia_ObjFanin0(pObj)->fMark0 = 1;
526  }
527  // go through the classes and remove
528  Gia_ManForEachClass( p, i )
529  {
530  for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
531  {
532  if ( !Gia_ManObj(p, iObj)->fMark0 )
533  {
534  iPrev = iObj;
535  continue;
536  }
537  Gia_ObjSetRepr( p, iObj, GIA_VOID );
538  Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
539  Gia_ObjSetNext( p, iObj, 0 );
540  Counter++;
541  }
542  }
543  // remove the marks
544  Gia_ManCleanMark0( p );
545 // printf( "Removed %d bad choices.\n", Counter );
546 }
547 
548 /**Function*************************************************************
549 
550  Synopsis [Reduces AIG using equivalence classes.]
551 
552  Description []
553 
554  SideEffects []
555 
556  SeeAlso []
557 
558 ***********************************************************************/
559 Gia_Man_t * Hcd_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
560 {
561  Gia_Man_t * pNew, * pTemp;
562  Gia_Obj_t * pObj, * pRepr;
563  int i;
564  assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
565  Gia_ManSetPhase( p );
566  pNew = Gia_ManStart( Gia_ManObjNum(p) );
567  pNew->pName = Abc_UtilStrsav( p->pName );
568  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
569  pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
570  pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
571  for ( i = 0; i < Gia_ManObjNum(p); i++ )
572  Gia_ObjSetRepr( pNew, i, GIA_VOID );
573  Gia_ManFillValue( p );
574  Gia_ManConst0(p)->Value = 0;
575  Gia_ManForEachCi( p, pObj, i )
576  pObj->Value = Gia_ManAppendCi(pNew);
577  Gia_ManForEachRo( p, pObj, i )
578  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
579  {
580  assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
581  pObj->Value = pRepr->Value;
582  }
583  Gia_ManHashAlloc( pNew );
584  Gia_ManForEachCo( p, pObj, i )
585  Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
586  Gia_ManForEachCo( p, pObj, i )
587  if ( i % nSnapshots == 0 )
588  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
589  Gia_ManHashStop( pNew );
590  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
591  Hcd_ManRemoveBadChoices( pNew );
592 // Gia_ManEquivPrintClasses( pNew, 0, 0 );
593  pNew = Gia_ManCleanup( pTemp = pNew );
594  Gia_ManStop( pTemp );
595 // Gia_ManEquivPrintClasses( pNew, 0, 0 );
596  return pNew;
597 }
598 
599 /**Function*************************************************************
600 
601  Synopsis [Performs computation of AIGs with choices.]
602 
603  Description []
604 
605  SideEffects []
606 
607  SeeAlso []
608 
609 ***********************************************************************/
610 Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose )
611 {
612  Vec_Ptr_t * vGias;
613  Gia_Man_t * pGia, * pMiter;
614  Aig_Man_t * pAigNew;
615  int i;
616  clock_t clk = clock();
617  // perform synthesis
618  if ( fSynthesis )
619  {
620  vGias = Hcd_ChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, 0, 0 );
621  if ( fVerbose )
622  ABC_PRT( "Synthesis time", clock() - clk );
623  // create choices
624  clk = clock();
625  pMiter = Hcd_ManChoiceMiter( vGias );
626  Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
627  Gia_ManStop( pGia );
628 
629  Gia_AigerWrite( pMiter, "m3.aig", 0, 0 );
630  }
631  else
632  {
633  vGias = Vec_PtrStart( 3 );
634  pMiter = Gia_ManFromAig(pAig);
635  }
636  // perform choicing
637  Gia_ComputeEquivalences( pMiter, nBTLimit, fUseMiniSat, fVerbose );
638  // derive AIG with choices
639  pGia = Hcd_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
640  Gia_ManSetRegNum( pGia, Aig_ManRegNum(pAig) );
641  Gia_ManStop( pMiter );
642  Vec_PtrFree( vGias );
643  if ( fVerbose )
644  ABC_PRT( "Choicing time", clock() - clk );
645 // Gia_ManHasChoices_very_old( pGia );
646  // transform back
647  pAigNew = Gia_ManToAig( pGia, 1 );
648  Gia_ManStop( pGia );
649 
650  if ( fVerbose )
651  {
652  extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
653  extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
654  printf( "Choices : Reprs = %5d. Equivs = %5d. Choices = %5d.\n",
655  Dch_DeriveChoiceCountReprs( pAigNew ),
656  Dch_DeriveChoiceCountEquivs( pAigNew ),
657  Aig_ManChoiceNum( pAigNew ) );
658  }
659 
660  return pAigNew;
661 }
662 
663 /**Function*************************************************************
664 
665  Synopsis [Performs computation of AIGs with choices.]
666 
667  Description []
668 
669  SideEffects []
670 
671  SeeAlso []
672 
673 ***********************************************************************/
674 void Hcd_ComputeChoicesTest( Gia_Man_t * pGia, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose )
675 {
676  Aig_Man_t * pAig, * pAigNew;
677  pAig = Gia_ManToAig( pGia, 0 );
678  pAigNew = Hcd_ComputeChoices( pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose );
679  Aig_ManStop( pAigNew );
680  Aig_ManStop( pAig );
681 }
682 
683 ////////////////////////////////////////////////////////////////////////
684 /// END OF FILE ///
685 ////////////////////////////////////////////////////////////////////////
686 
687 
688 ABC_NAMESPACE_IMPL_END
689 
memset
char * memset()
Hcd_ManSetDefaultParams
void Hcd_ManSetDefaultParams(Hcd_Pars_t *p)
FUNCTION DEFINITIONS ///.
Definition: giaHcd.c:69
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Gia_ObjPhaseReal
static int Gia_ObjPhaseReal(Gia_Obj_t *pObj)
Definition: gia.h:416
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManCi
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Dar_RefPar_t_::fUpdateLevel
int fUpdateLevel
Definition: dar.h:64
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Aig_ManDupDfs
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
Hcd_Pars_t_::fSynthesis
int fSynthesis
Definition: giaHcd.c:40
Dar_ManRewrite
int Dar_ManRewrite(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
Definition: darCore.c:78
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Gia_ComputeEquivalences
void Gia_ComputeEquivalences(Gia_Man_t *pMiter, int nBTLimit, int fUseMiniSat, int fVerbose)
Definition: giaGiarf.c:1030
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Hcd_Pars_t_::fVerbose
int fVerbose
Definition: giaHcd.c:46
Hcd_Pars_t_::fSimulateTfo
int fSimulateTfo
Definition: giaHcd.c:42
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Hcd_Pars_t_
Definition: giaHcd.c:35
Gia_Obj_t_
Definition: gia.h:75
Hcd_ObjCheckTfi
int Hcd_ObjCheckTfi(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
Definition: giaHcd.c:405
Gia_ManHasDangling
int Gia_ManHasDangling(Gia_Man_t *p)
Definition: giaUtil.c:1155
Gia_ManFromAig
Gia_Man_t * Gia_ManFromAig(Aig_Man_t *p)
INCLUDES ///.
Definition: giaAig.c:73
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Hcd_Pars_t_::fUseCSat
int fUseCSat
Definition: giaHcd.c:45
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Dar_RefPar_t_::fVerbose
int fVerbose
Definition: dar.h:66
Hcd_Pars_t_::nWords
int nWords
Definition: giaHcd.c:37
Hcd_ComputeChoicesTest
void Hcd_ComputeChoicesTest(Gia_Man_t *pGia, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose)
Definition: giaHcd.c:674
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Hcd_Pars_t
typedefABC_NAMESPACE_IMPL_START struct Hcd_Pars_t_ Hcd_Pars_t
DECLARATIONS ///.
Definition: giaHcd.c:34
Hcd_Pars_t_::nNodesAhead
int nNodesAhead
Definition: giaHcd.c:48
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Hcd_ComputeChoices
Aig_Man_t * Hcd_ComputeChoices(Aig_Man_t *pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose)
Definition: giaHcd.c:610
Hcd_Pars_t_::fUseGia
int fUseGia
Definition: giaHcd.c:44
Dar_ManRefactor
int Dar_ManRefactor(Aig_Man_t *pAig, Dar_RefPar_t *pPars)
Definition: darRefact.c:496
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
Hcd_Compress
Aig_Man_t * Hcd_Compress(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition: giaHcd.c:96
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Hcd_ChoiceSynthesis
Vec_Ptr_t * Hcd_ChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition: giaHcd.c:259
Hcd_Pars_t_::nSatVarMax
int nSatVarMax
Definition: giaHcd.c:39
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManToAig
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition: giaAig.c:277
Dar_ManDefaultRefParams
void Dar_ManDefaultRefParams(Dar_RefPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: darRefact.c:85
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Hcd_ManRemoveBadChoices
void Hcd_ManRemoveBadChoices(Gia_Man_t *p)
Definition: giaHcd.c:511
Hcd_Compress2
Aig_Man_t * Hcd_Compress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Definition: giaHcd.c:161
Gia_ObjNextObj
static Gia_Obj_t * Gia_ObjNextObj(Gia_Man_t *p, int Id)
Definition: gia.h:911
Dch_DeriveChoiceCountEquivs
int Dch_DeriveChoiceCountEquivs(Aig_Man_t *pAig)
Definition: dchChoice.c:89
Hcd_ManChoiceMiter_rec
int Hcd_ManChoiceMiter_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaHcd.c:296
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Dar_RefPar_t_::fUseZeros
int fUseZeros
Definition: dar.h:65
Aig_ManChoiceNum
int Aig_ManChoiceNum(Aig_Man_t *p)
Definition: aigUtil.c:1007
Hcd_ManAddNextEntry_rec
void Hcd_ManAddNextEntry_rec(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode)
Definition: giaHcd.c:431
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_ObjNext
static int Gia_ObjNext(Gia_Man_t *p, int Id)
Definition: gia.h:912
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ObjSetNext
static void Gia_ObjSetNext(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:913
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Gia_ManCo
static Gia_Obj_t * Gia_ManCo(Gia_Man_t *p, int v)
Definition: gia.h:404
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Hcd_ManEquivToChoices
Gia_Man_t * Hcd_ManEquivToChoices(Gia_Man_t *p, int nSnapshots)
Definition: giaHcd.c:559
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Dar_RwrPar_t
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
Definition: dar.h:42
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Dar_RefPar_t_
Definition: dar.h:58
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Hcd_Pars_t_::nCallsRecycle
int nCallsRecycle
Definition: giaHcd.c:49
Hcd_ManChoiceMiter
Gia_Man_t * Hcd_ManChoiceMiter(Vec_Ptr_t *vGias)
Definition: giaHcd.c:318
Gia_ManForEachClass
#define Gia_ManForEachClass(p, i)
Definition: gia.h:927
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Hcd_Pars_t_::timeSynth
clock_t timeSynth
Definition: giaHcd.c:47
Dch_DeriveChoiceCountReprs
int Dch_DeriveChoiceCountReprs(Aig_Man_t *pAig)
FUNCTION DECLARATIONS ///.
Definition: dchChoice.c:75
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Hcd_Pars_t_::fPower
int fPower
Definition: giaHcd.c:43
Hcd_ManEquivToChoices_rec
void Hcd_ManEquivToChoices_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaHcd.c:452
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Dar_ManBalance
Aig_Man_t * Dar_ManBalance(Aig_Man_t *p, int fUpdateLevel)
Definition: darBalance.c:554
Gia_Rpr_t_
Definition: gia.h:56
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Hcd_ObjCheckTfi_rec
int Hcd_ObjCheckTfi_rec(Gia_Man_t *p, Gia_Obj_t *pOld, Gia_Obj_t *pNode, Vec_Ptr_t *vVisited)
Definition: giaHcd.c:369
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Dar_ManDefaultRwrParams
void Dar_ManDefaultRwrParams(Dar_RwrPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: darCore.c:51
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Hcd_Pars_t_::nBTLimit
int nBTLimit
Definition: giaHcd.c:38
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Hcd_Pars_t_::fPolarFlip
int fPolarFlip
Definition: giaHcd.c:41
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387