abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaAig.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaAig.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Transformation between AIG manager.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "giaAig.h"
22 #include "proof/fra/fra.h"
23 #include "proof/dch/dch.h"
24 #include "opt/dar/dar.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
34 static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
35 
36 static inline Aig_Obj_t * Gia_ObjChild0Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
37 static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
38 
39 ////////////////////////////////////////////////////////////////////////
40 /// FUNCTION DEFINITIONS ///
41 ////////////////////////////////////////////////////////////////////////
42 
43 /**Function*************************************************************
44 
45  Synopsis [Duplicates AIG in the DFS order.]
46 
47  Description []
48 
49  SideEffects []
50 
51  SeeAlso []
52 
53 ***********************************************************************/
54 void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
55 {
56  Aig_Obj_t * pNext;
57  if ( pObj->iData )
58  return;
59  assert( Aig_ObjIsNode(pObj) );
60  Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
61  Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
62  pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
63  if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
64  {
65  int iObjNew, iNextNew;
66  Gia_ManFromAig_rec( pNew, p, pNext );
67  iObjNew = Abc_Lit2Var(pObj->iData);
68  iNextNew = Abc_Lit2Var(pNext->iData);
69  if ( pNew->pNexts )
70  pNew->pNexts[iObjNew] = iNextNew;
71  }
72 }
73 Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
74 {
75  Gia_Man_t * pNew;
76  Aig_Obj_t * pObj;
77  int i;
78  // create the new manager
79  pNew = Gia_ManStart( Aig_ManObjNum(p) );
80  pNew->pName = Abc_UtilStrsav( p->pName );
81  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
82  pNew->nConstrs = p->nConstrs;
83  // create room to store equivalences
84  if ( p->pEquivs )
85  pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
86  // create the PIs
87  Aig_ManCleanData( p );
88  Aig_ManConst1(p)->iData = 1;
89  Aig_ManForEachCi( p, pObj, i )
90  pObj->iData = Gia_ManAppendCi( pNew );
91  // add logic for the POs
92  Aig_ManForEachCo( p, pObj, i )
93  Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
94  Aig_ManForEachCo( p, pObj, i )
95  Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
96  Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
97  if ( pNew->pNexts )
98  Gia_ManDeriveReprs( pNew );
99  return pNew;
100 }
101 
102 /**Function*************************************************************
103 
104  Synopsis [Duplicates AIG in the DFS order.]
105 
106  Description []
107 
108  SideEffects []
109 
110  SeeAlso []
111 
112 ***********************************************************************/
113 void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
114 {
115  if ( pObj == NULL || pObj->iData )
116  return;
117  assert( Aig_ObjIsNode(pObj) );
118  Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
119  Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
120  Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
121  pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
122  if ( Aig_ObjEquiv(p, pObj) )
123  {
124  int iObjNew, iNextNew;
125  iObjNew = Abc_Lit2Var(pObj->iData);
126  iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
127  assert( iObjNew > iNextNew );
128  assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
129  pNew->pSibls[iObjNew] = iNextNew;
130  }
131 }
132 Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
133 {
134  Gia_Man_t * pNew;
135  Aig_Obj_t * pObj;
136  int i;
137  assert( p->pEquivs != NULL );
138  // create the new manager
139  pNew = Gia_ManStart( Aig_ManObjNum(p) );
140  pNew->pName = Abc_UtilStrsav( p->pName );
141  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
142  pNew->nConstrs = p->nConstrs;
143  // create room to store equivalences
144  pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
145  // create the PIs
146  Aig_ManCleanData( p );
147  Aig_ManConst1(p)->iData = 1;
148  Aig_ManForEachCi( p, pObj, i )
149  pObj->iData = Gia_ManAppendCi( pNew );
150  // add logic for the POs
151  Aig_ManForEachCo( p, pObj, i )
152  Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
153  Aig_ManForEachCo( p, pObj, i )
154  Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
155  Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
156  assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
157  return pNew;
158 }
159 
160 /**Function*************************************************************
161 
162  Synopsis [Duplicates AIG in the DFS order.]
163 
164  Description []
165 
166  SideEffects []
167 
168  SeeAlso []
169 
170 ***********************************************************************/
171 Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
172 {
173  Gia_Man_t * pNew;
174  Aig_Obj_t * pObj;
175  int i;
176  // create the new manager
177  pNew = Gia_ManStart( Aig_ManObjNum(p) );
178  pNew->pName = Abc_UtilStrsav( p->pName );
179  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
180  pNew->nConstrs = p->nConstrs;
181  // create the PIs
182  Aig_ManCleanData( p );
183  Aig_ManForEachObj( p, pObj, i )
184  {
185  if ( Aig_ObjIsAnd(pObj) )
186  pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
187  else if ( Aig_ObjIsCi(pObj) )
188  pObj->iData = Gia_ManAppendCi( pNew );
189  else if ( Aig_ObjIsCo(pObj) )
190  pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
191  else if ( Aig_ObjIsConst1(pObj) )
192  pObj->iData = 1;
193  else
194  assert( 0 );
195  }
196  Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
197  return pNew;
198 }
199 
200 /**Function*************************************************************
201 
202  Synopsis [Handles choices as additional combinational outputs.]
203 
204  Description []
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
212 {
213  Gia_Man_t * pNew;
214  Aig_Obj_t * pObj;
215  int i;
216  // create the new manager
217  pNew = Gia_ManStart( Aig_ManObjNum(p) );
218  pNew->pName = Abc_UtilStrsav( p->pName );
219  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
220  pNew->nConstrs = p->nConstrs;
221  // create the PIs
222  Aig_ManCleanData( p );
223  Aig_ManConst1(p)->iData = 1;
224  Aig_ManForEachCi( p, pObj, i )
225  pObj->iData = Gia_ManAppendCi( pNew );
226  // add POs corresponding to the nodes with choices
227  Aig_ManForEachNode( p, pObj, i )
228  if ( Aig_ObjRefs(pObj) == 0 )
229  {
230  Gia_ManFromAig_rec( pNew, p, pObj );
231  Gia_ManAppendCo( pNew, pObj->iData );
232  }
233  // add logic for the POs
234  Aig_ManForEachCo( p, pObj, i )
235  Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
236  Aig_ManForEachCo( p, pObj, i )
237  pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
238  Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
239  return pNew;
240 }
241 
242 /**Function*************************************************************
243 
244  Synopsis [Duplicates AIG in the DFS order.]
245 
246  Description []
247 
248  SideEffects []
249 
250  SeeAlso []
251 
252 ***********************************************************************/
253 void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj )
254 {
255  Gia_Obj_t * pNext;
256  if ( ppNodes[Gia_ObjId(p, pObj)] )
257  return;
258  if ( Gia_ObjIsCi(pObj) )
259  ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
260  else
261  {
262  assert( Gia_ObjIsAnd(pObj) );
263  Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
264  Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
265  ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
266  }
267  if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
268  {
269  Aig_Obj_t * pObjNew, * pNextNew;
270  Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
271  pObjNew = ppNodes[Gia_ObjId(p, pObj)];
272  pNextNew = ppNodes[Gia_ObjId(p, pNext)];
273  if ( pNew->pEquivs )
274  pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);
275  }
276 }
277 Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
278 {
279  Aig_Man_t * pNew;
280  Aig_Obj_t ** ppNodes;
281  Gia_Obj_t * pObj;
282  int i;
283  assert( !fChoices || (p->pNexts && p->pReprs) );
284  // create the new manager
285  pNew = Aig_ManStart( Gia_ManAndNum(p) );
286  pNew->pName = Abc_UtilStrsav( p->pName );
287  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
288  pNew->nConstrs = p->nConstrs;
289 // pNew->pSpec = Abc_UtilStrsav( p->pName );
290  // duplicate representation of choice nodes
291  if ( fChoices )
292  pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
293  // create the PIs
294  ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
295  ppNodes[0] = Aig_ManConst0(pNew);
296  Gia_ManForEachCi( p, pObj, i )
297  ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
298  // transfer level
299  if ( p->vLevels )
300  Gia_ManForEachCi( p, pObj, i )
301  Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) );
302  // add logic for the POs
303  Gia_ManForEachCo( p, pObj, i )
304  {
305  Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
306  ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
307  }
308  Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
309  ABC_FREE( ppNodes );
310  return pNew;
311 }
312 
313 /**Function*************************************************************
314 
315  Synopsis [Duplicates AIG in the DFS order.]
316 
317  Description []
318 
319  SideEffects []
320 
321  SeeAlso []
322 
323 ***********************************************************************/
324 Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
325 {
326  Aig_Man_t * pNew;
327  Aig_Obj_t ** ppNodes;
328  Gia_Obj_t * pObj;
329  int i;
330  assert( p->pNexts == NULL && p->pReprs == NULL );
331  assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
332  // create the new manager
333  pNew = Aig_ManStart( Gia_ManAndNum(p) );
334  pNew->pName = Abc_UtilStrsav( p->pName );
335  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
336  pNew->nConstrs = p->nConstrs;
337 // pNew->pSpec = Abc_UtilStrsav( p->pName );
338  // create the PIs
339  ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
340  ppNodes[0] = Aig_ManConst0(pNew);
341  Gia_ManForEachCi( p, pObj, i )
342  ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
343  // add logic for the POs
344  Gia_ManForEachCo( p, pObj, i )
345  {
346  Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
347  if ( i % nOutDelta != 0 )
348  continue;
349  ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
350  }
351  Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
352  ABC_FREE( ppNodes );
353  return pNew;
354 }
355 
356 /**Function*************************************************************
357 
358  Synopsis [Duplicates AIG in the DFS order.]
359 
360  Description []
361 
362  SideEffects []
363 
364  SeeAlso []
365 
366 ***********************************************************************/
367 Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
368 {
369  Aig_Man_t * pNew;
370  Aig_Obj_t ** ppNodes;
371  Gia_Obj_t * pObj;
372  int i;
373  ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
374  // create the new manager
375  pNew = Aig_ManStart( Gia_ManObjNum(p) );
376  pNew->pName = Abc_UtilStrsav( p->pName );
377  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
378  pNew->nConstrs = p->nConstrs;
379  // create the PIs
380  Gia_ManForEachObj( p, pObj, i )
381  {
382  if ( Gia_ObjIsAnd(pObj) )
383  ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
384  else if ( Gia_ObjIsCi(pObj) )
385  ppNodes[i] = Aig_ObjCreateCi( pNew );
386  else if ( Gia_ObjIsCo(pObj) )
387  ppNodes[i] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
388  else if ( Gia_ObjIsConst0(pObj) )
389  ppNodes[i] = Aig_ManConst0(pNew);
390  else
391  assert( 0 );
392  pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
393  assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
394  }
395  Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
396  ABC_FREE( ppNodes );
397  return pNew;
398 }
399 
400 /**Function*************************************************************
401 
402  Synopsis [Duplicates AIG in the DFS order.]
403 
404  Description []
405 
406  SideEffects []
407 
408  SeeAlso []
409 
410 ***********************************************************************/
411 Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
412 {
413  Aig_Man_t * pMan;
414  Gia_Man_t * pGia, * pTemp;
415  pGia = Gia_ManFromAig( p );
416  pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
417  Gia_ManStop( pTemp );
418  pMan = Gia_ManToAig( pGia, 0 );
419  Gia_ManStop( pGia );
420  return pMan;
421 }
422 
423 
424 /**Function*************************************************************
425 
426  Synopsis [Transfers representatives from pGia to pAig.]
427 
428  Description [Assumes that pGia was created from pAig.]
429 
430  SideEffects []
431 
432  SeeAlso []
433 
434 ***********************************************************************/
435 void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
436 {
437  Aig_Obj_t * pObj;
438  Gia_Obj_t * pGiaObj, * pGiaRepr;
439  int i;
440  assert( pAig->pReprs == NULL );
441  assert( pGia->pReprs != NULL );
442  // move pointers from AIG to GIA
443  Aig_ManForEachObj( pAig, pObj, i )
444  {
445  assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
446  pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
447  pGiaObj->Value = i;
448  }
449  // set the pointers to the nodes in AIG
450  Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
451  Gia_ManForEachObj( pGia, pGiaObj, i )
452  {
453  pGiaRepr = Gia_ObjReprObj( pGia, i );
454  if ( pGiaRepr == NULL )
455  continue;
456  Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
457  }
458 }
459 void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
460 {
461  Gia_Obj_t * pGiaObj, * pGiaRepr;
462  int i;
463  assert( pAig->pReprs == NULL );
464  assert( pGia->pReprs != NULL );
465  // set the pointers to the nodes in AIG
466  Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
467  Gia_ManForEachObj( pGia, pGiaObj, i )
468  {
469  pGiaRepr = Gia_ObjReprObj( pGia, i );
470  if ( pGiaRepr == NULL )
471  continue;
472  Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
473  }
474 }
475 
476 /**Function*************************************************************
477 
478  Synopsis [Transfers representatives from pAig to pGia.]
479 
480  Description []
481 
482  SideEffects []
483 
484  SeeAlso []
485 
486 ***********************************************************************/
487 void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
488 {
489  Gia_Obj_t * pObjGia;
490  Aig_Obj_t * pObjAig, * pReprAig;
491  int i;
492  assert( pAig->pReprs != NULL );
493  assert( pGia->pReprs == NULL );
494  assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
495  pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
496  for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
497  Gia_ObjSetRepr( pGia, i, GIA_VOID );
498  // move pointers from GIA to AIG
499  Gia_ManForEachObj( pGia, pObjGia, i )
500  {
501  if ( Gia_ObjIsCo(pObjGia) )
502  continue;
503  assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
504  pObjAig = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
505  pObjAig->iData = i;
506  }
507  Aig_ManForEachObj( pAig, pObjAig, i )
508  {
509  if ( Aig_ObjIsCo(pObjAig) )
510  continue;
511  if ( pAig->pReprs[i] == NULL )
512  continue;
513  pReprAig = pAig->pReprs[i];
514  Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData );
515  }
516  pGia->pNexts = Gia_ManDeriveNexts( pGia );
517 }
518 void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
519 {
520  Aig_Obj_t * pObjAig, * pReprAig;
521  int i;
522  assert( pAig->pReprs != NULL );
523  assert( pGia->pReprs == NULL );
524  assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
525  pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
526  for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
527  Gia_ObjSetRepr( pGia, i, GIA_VOID );
528  Aig_ManForEachObj( pAig, pObjAig, i )
529  {
530  if ( Aig_ObjIsCo(pObjAig) )
531  continue;
532  if ( pAig->pReprs[i] == NULL )
533  continue;
534  pReprAig = pAig->pReprs[i];
535  Gia_ObjSetRepr( pGia, Abc_Lit2Var(pObjAig->iData), Abc_Lit2Var(pReprAig->iData) );
536  }
537  pGia->pNexts = Gia_ManDeriveNexts( pGia );
538 }
539 
540 /**Function*************************************************************
541 
542  Synopsis [Applies DC2 to the GIA manager.]
543 
544  Description []
545 
546  SideEffects []
547 
548  SeeAlso []
549 
550 ***********************************************************************/
551 Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
552 {
553  Gia_Man_t * pGia;
554  Aig_Man_t * pNew, * pTemp;
555  if ( p->pManTime && p->vLevels == NULL )
556  Gia_ManLevelWithBoxes( p );
557  pNew = Gia_ManToAig( p, 0 );
558  pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
559  Aig_ManStop( pTemp );
560  pGia = Gia_ManFromAig( pNew );
561  Aig_ManStop( pNew );
562  Gia_ManTransferTiming( pGia, p );
563  return pGia;
564 }
565 
566 /**Function*************************************************************
567 
568  Synopsis []
569 
570  Description []
571 
572  SideEffects []
573 
574  SeeAlso []
575 
576 ***********************************************************************/
577 Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
578 {
579  Gia_Man_t * pGia;
580  Aig_Man_t * pNew;
581  if ( p->pManTime && p->vLevels == NULL )
582  Gia_ManLevelWithBoxes( p );
583  pNew = Gia_ManToAig( p, 0 );
584  pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
585 // pGia = Gia_ManFromAig( pNew );
586  pGia = Gia_ManFromAigChoices( pNew );
587  Aig_ManStop( pNew );
588  Gia_ManTransferTiming( pGia, p );
589  return pGia;
590 }
591 
592 /**Function*************************************************************
593 
594  Synopsis [Computes equivalences after structural sequential cleanup.]
595 
596  Description []
597 
598  SideEffects []
599 
600  SeeAlso []
601 
602 ***********************************************************************/
603 void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose )
604 {
605  Aig_Man_t * pNew, * pTemp;
606  pNew = Gia_ManToAigSimple( p );
607  pTemp = Aig_ManScl( pNew, fConst, fEquiv, 0, -1, -1, fVerbose, 0 );
608  Gia_ManReprFromAigRepr( pNew, p );
609  Aig_ManStop( pTemp );
610  Aig_ManStop( pNew );
611 }
612 
613 /**Function*************************************************************
614 
615  Synopsis [Solves SAT problem.]
616 
617  Description []
618 
619  SideEffects []
620 
621  SeeAlso []
622 
623 ***********************************************************************/
624 int Gia_ManSolveSat( Gia_Man_t * p )
625 {
626 // extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
627  Aig_Man_t * pNew;
628  int RetValue;//, clk = Abc_Clock();
629  pNew = Gia_ManToAig( p, 0 );
630  RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
631  if ( RetValue == 0 )
632  {
633  Gia_Obj_t * pObj;
634  int i, * pInit = (int *)pNew->pData;
635  Gia_ManConst0(p)->fMark0 = 0;
636  Gia_ManForEachPi( p, pObj, i )
637  pObj->fMark0 = pInit[i];
638  Gia_ManForEachAnd( p, pObj, i )
639  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
640  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
641  Gia_ManForEachPo( p, pObj, i )
642  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
643  Gia_ManForEachPo( p, pObj, i )
644  if ( pObj->fMark0 != 1 )
645  break;
646  if ( i != Gia_ManPoNum(p) )
647  Abc_Print( 1, "Counter-example verification has failed. " );
648 // else
649 // Abc_Print( 1, "Counter-example verification succeeded. " );
650  }
651 /*
652  else if ( RetValue == 1 )
653  Abc_Print( 1, "The SAT problem is unsatisfiable. " );
654  else if ( RetValue == -1 )
655  Abc_Print( 1, "The SAT problem is undecided. " );
656  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
657 */
658  Aig_ManStop( pNew );
659  return RetValue;
660 }
661 
662 
663 ////////////////////////////////////////////////////////////////////////
664 /// END OF FILE ///
665 ////////////////////////////////////////////////////////////////////////
666 
667 
668 ABC_NAMESPACE_IMPL_END
669 
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Gia_ManAppendAnd
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Aig_ObjSetLevel
static int Aig_ObjSetLevel(Aig_Obj_t *pObj, int i)
Definition: aig.h:325
Gia_ManFromAigSwitch
Gia_Man_t * Gia_ManFromAigSwitch(Aig_Man_t *p)
Definition: giaAig.c:211
Gia_ManDeriveReprs
void Gia_ManDeriveReprs(Gia_Man_t *p)
Definition: giaEquiv.c:129
Dar_ManChoiceNew
Aig_Man_t * Dar_ManChoiceNew(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition: darScript.c:849
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Gia_ObjChild1Copy2
static Aig_Obj_t * Gia_ObjChild1Copy2(Aig_Obj_t **ppNodes, Gia_Obj_t *pObj, int Id)
Definition: giaAig.c:37
Gia_ManReprFromAigRepr
void Gia_ManReprFromAigRepr(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:487
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
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
Aig_ManObjNum
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Gia_Man_t_::pSibls
int * pSibls
Definition: gia.h:123
Gia_ManReprToAigRepr
void Gia_ManReprToAigRepr(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:435
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManLevelWithBoxes
int Gia_ManLevelWithBoxes(Gia_Man_t *p)
Definition: giaTim.c:469
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
Gia_ManFromAigSimple
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition: giaAig.c:171
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Dch_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition: dch.h:43
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
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
Gia_Obj_t_
Definition: gia.h:75
Gia_ManFromAigChoices_rec
void Gia_ManFromAigChoices_rec(Gia_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: giaAig.c:113
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
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
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Gia_ObjLevel
static int Gia_ObjLevel(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:501
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ManPerformDch
Gia_Man_t * Gia_ManPerformDch(Gia_Man_t *p, void *pPars)
Definition: giaAig.c:577
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::nConstrs
int nConstrs
Definition: gia.h:117
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Gia_ManReprToAigRepr2
void Gia_ManReprToAigRepr2(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:459
Aig_ManReprStart
void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition: aigRepr.c:45
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Aig_ManScl
Aig_Man_t * Aig_ManScl(Aig_Man_t *pAig, int fLatchConst, int fLatchEqual, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose)
Definition: aigScl.c:650
Gia_ObjChild0Copy2
static Aig_Obj_t * Gia_ObjChild0Copy2(Aig_Obj_t **ppNodes, Gia_Obj_t *pObj, int Id)
Definition: giaAig.c:36
Gia_ManUnrollAndCofactor
Gia_Man_t * Gia_ManUnrollAndCofactor(Gia_Man_t *p, int nFrames, int nFanMax, int fVerbose)
Definition: giaEnable.c:403
Dar_ManCompress2
Aig_Man_t * Dar_ManCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Definition: darScript.c:235
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Aig_ObjEquiv
static Aig_Obj_t * Aig_ObjEquiv(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:328
Gia_ManSeqCleanupClasses
void Gia_ManSeqCleanupClasses(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition: giaAig.c:603
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ManFromAig_rec
void Gia_ManFromAig_rec(Gia_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: giaAig.c:54
Gia_ManToAig
Aig_Man_t * Gia_ManToAig(Gia_Man_t *p, int fChoices)
Definition: giaAig.c:277
Aig_Obj_t_
Definition: aig.h:69
Gia_Man_t_::pManTime
void * pManTime
Definition: gia.h:165
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManTransferTiming
void Gia_ManTransferTiming(Gia_Man_t *p, Gia_Man_t *pGia)
Definition: giaIf.c:1912
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_ObjNextObj
static Gia_Obj_t * Gia_ObjNextObj(Gia_Man_t *p, int Id)
Definition: gia.h:911
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ManDeriveNexts
int * Gia_ManDeriveNexts(Gia_Man_t *p)
Definition: giaEquiv.c:97
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Aig_Obj_t_::iData
int iData
Definition: aig.h:88
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
Gia_ManCofactorAig
Aig_Man_t * Gia_ManCofactorAig(Aig_Man_t *p, int nFrames, int nCofFanLit)
Definition: giaAig.c:411
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ManToAigSkip
Aig_Man_t * Gia_ManToAigSkip(Gia_Man_t *p, int nOutDelta)
Definition: giaAig.c:324
Gia_ManReprFromAigRepr2
void Gia_ManReprFromAigRepr2(Aig_Man_t *pAig, Gia_Man_t *pGia)
Definition: giaAig.c:518
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Gia_ManToAig_rec
void Gia_ManToAig_rec(Aig_Man_t *pNew, Aig_Obj_t **ppNodes, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaAig.c:253
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
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
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
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ManCompress2
Gia_Man_t * Gia_ManCompress2(Gia_Man_t *p, int fUpdateLevel, int fVerbose)
Definition: giaAig.c:551
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Aig_ObjCreateRepr
void Aig_ObjCreateRepr(Aig_Man_t *p, Aig_Obj_t *pNode1, Aig_Obj_t *pNode2)
Definition: aigRepr.c:83
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_Man_t_::vLevels
Vec_Int_t * vLevels
Definition: gia.h:115
Gia_ManSolveSat
int Gia_ManSolveSat(Gia_Man_t *p)
Definition: giaAig.c:624
Gia_ObjChild1Copy
static int Gia_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: giaAig.c:34
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Gia_ObjChild0Copy
static ABC_NAMESPACE_IMPL_START int Gia_ObjChild0Copy(Aig_Obj_t *pObj)
DECLARATIONS ///.
Definition: giaAig.c:33
Gia_Rpr_t_
Definition: gia.h:56
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Fra_FraigSat
int Fra_FraigSat(Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
ITERATORS ///.
Definition: fraCec.c:47
Aig_ObjIsAnd
static int Aig_ObjIsAnd(Aig_Obj_t *pObj)
Definition: aig.h:278
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231
Gia_ManFromAigChoices
Gia_Man_t * Gia_ManFromAigChoices(Aig_Man_t *p)
Definition: giaAig.c:132
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
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