giaAig.c 21.7 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**CFile****************************************************************

  FileName    [giaAig.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Transformation between AIG manager.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: giaAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

Alan Mishchenko committed
21
#include "giaAig.h"
22 23 24
#include "proof/fra/fra.h"
#include "proof/dch/dch.h"
#include "opt/dar/dar.h"
25 26 27

ABC_NAMESPACE_IMPL_START

Alan Mishchenko committed
28 29 30 31 32

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

33 34
static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj )  { return Abc_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj )  { return Abc_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
Alan Mishchenko committed
35 36 37 38 39 40 41 42 43 44

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) ); }
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) ); }

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

45
  Synopsis    [Duplicates AIG in the DFS order.]
Alan Mishchenko committed
46 47 48 49 50 51 52 53

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
54
void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
Alan Mishchenko committed
55
{
Alan Mishchenko committed
56 57
    Aig_Obj_t * pNext;
    if ( pObj->iData )
Alan Mishchenko committed
58 59
        return;
    assert( Aig_ObjIsNode(pObj) );
Alan Mishchenko committed
60 61
    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
Alan Mishchenko committed
62
    pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
Alan Mishchenko committed
63 64 65 66
    if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
    {
        int iObjNew, iNextNew;
        Gia_ManFromAig_rec( pNew, p, pNext );
67 68
        iObjNew  = Abc_Lit2Var(pObj->iData);
        iNextNew = Abc_Lit2Var(pNext->iData);
Alan Mishchenko committed
69 70 71
        if ( pNew->pNexts )
            pNew->pNexts[iObjNew] = iNextNew;        
    }
Alan Mishchenko committed
72
}
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // create the new manager
    pNew = Gia_ManStart( Aig_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
    // create room to store equivalences
    if ( p->pEquivs )
        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->iData = 1;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Gia_ManAppendCi( pNew );
    // add logic for the POs
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    if ( pNew->pNexts )
        Gia_ManDeriveReprs( pNew );
    return pNew;
}
Alan Mishchenko committed
101 102 103 104 105 106 107 108 109 110 111 112

/**Function*************************************************************

  Synopsis    [Duplicates AIG in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
    if ( pObj == NULL || pObj->iData )
        return;
    assert( Aig_ObjIsNode(pObj) );
    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
    pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
    if ( Aig_ObjEquiv(p, pObj) )
    {
        int iObjNew, iNextNew;
        iObjNew  = Abc_Lit2Var(pObj->iData);
        iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
        assert( iObjNew > iNextNew );
        assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
        pNew->pSibls[iObjNew] = iNextNew;        
    }
}
Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
Alan Mishchenko committed
133 134 135 136
{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
137
    assert( p->pEquivs != NULL );
Alan Mishchenko committed
138 139
    // create the new manager
    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;
Alan Mishchenko committed
143
    // create room to store equivalences
144
    pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
Alan Mishchenko committed
145 146 147
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->iData = 1;
148
    Aig_ManForEachCi( p, pObj, i )
Alan Mishchenko committed
149
        pObj->iData = Gia_ManAppendCi( pNew );
Alan Mishchenko committed
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 )
Alan Mishchenko committed
154 155
        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
156
    //assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
Alan Mishchenko committed
157 158 159 160 161
    return pNew;
}

/**Function*************************************************************

Alan Mishchenko committed
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
  Synopsis    [Duplicates AIG in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // create the new manager
    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;
Alan Mishchenko committed
181 182 183 184 185 186
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjIsAnd(pObj) )
            pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
187
        else if ( Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
188
            pObj->iData = Gia_ManAppendCi( pNew );
189
        else if ( Aig_ObjIsCo(pObj) )
Alan Mishchenko committed
190 191 192 193 194 195 196 197 198 199 200 201
            pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
        else if ( Aig_ObjIsConst1(pObj) )
            pObj->iData = 1;
        else
            assert( 0 );
    }
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    return pNew;
}

/**Function*************************************************************

Alan Mishchenko committed
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
  Synopsis    [Handles choices as additional combinational outputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // create the new manager
    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;
Alan Mishchenko committed
221 222 223
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->iData = 1;
224
    Aig_ManForEachCi( p, pObj, i )
Alan Mishchenko committed
225 226 227 228 229
        pObj->iData = Gia_ManAppendCi( pNew );
    // add POs corresponding to the nodes with choices
    Aig_ManForEachNode( p, pObj, i )
        if ( Aig_ObjRefs(pObj) == 0 )
        {
Alan Mishchenko committed
230
            Gia_ManFromAig_rec( pNew, p, pObj );        
Alan Mishchenko committed
231 232 233
            Gia_ManAppendCo( pNew, pObj->iData );
        }
    // add logic for the POs
234
    Aig_ManForEachCo( p, pObj, i )
Alan Mishchenko committed
235
        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
236
    Aig_ManForEachCo( p, pObj, i )
237
        pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
Alan Mishchenko committed
238 239 240 241 242 243
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    return pNew;
}

/**Function*************************************************************

244
  Synopsis    [Duplicates AIG in the DFS order.]
Alan Mishchenko committed
245 246 247 248 249 250 251 252 253 254

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Alan Mishchenko committed
255
    Gia_Obj_t * pNext;
Alan Mishchenko committed
256 257 258
    if ( ppNodes[Gia_ObjId(p, pObj)] )
        return;
    if ( Gia_ObjIsCi(pObj) )
259
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
Alan Mishchenko committed
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
    else
    {
        assert( Gia_ObjIsAnd(pObj) );
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
        ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
    }
    if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
    {
        Aig_Obj_t * pObjNew, * pNextNew;
        Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
        pObjNew  = ppNodes[Gia_ObjId(p, pObj)];
        pNextNew = ppNodes[Gia_ObjId(p, pNext)];
        if ( pNew->pEquivs )
            pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
Alan Mishchenko committed
275 276
    }
}
Alan Mishchenko committed
277
Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
Alan Mishchenko committed
278 279 280 281 282
{
    Aig_Man_t * pNew;
    Aig_Obj_t ** ppNodes;
    Gia_Obj_t * pObj;
    int i;
Alan Mishchenko committed
283
    assert( !fChoices || (p->pNexts && p->pReprs) );
Alan Mishchenko committed
284 285
    // create the new manager
    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 );
Alan Mishchenko committed
290 291 292
    // duplicate representation of choice nodes
    if ( fChoices )
        pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
Alan Mishchenko committed
293
    // create the PIs
Alan Mishchenko committed
294
    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
Alan Mishchenko committed
295 296
    ppNodes[0] = Aig_ManConst0(pNew);
    Gia_ManForEachCi( p, pObj, i )
297
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
298 299 300 301
    // transfer level
    if ( p->vLevels )
    Gia_ManForEachCi( p, pObj, i )
        Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) );
Alan Mishchenko committed
302 303 304 305
    // add logic for the POs
    Gia_ManForEachCo( p, pObj, i )
    {
        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)) );
Alan Mishchenko committed
307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333
    }
    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    ABC_FREE( ppNodes );
    return pNew;
}

/**Function*************************************************************

  Synopsis    [Duplicates AIG in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
{
    Aig_Man_t * pNew;
    Aig_Obj_t ** ppNodes;
    Gia_Obj_t * pObj;
    int i;
    assert( p->pNexts == NULL && p->pReprs == NULL );
    assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
    // create the new manager
    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 );
Alan Mishchenko committed
338 339 340 341
    // create the PIs
    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
    ppNodes[0] = Aig_ManConst0(pNew);
    Gia_ManForEachCi( p, pObj, i )
342
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
Alan Mishchenko committed
343 344 345 346 347 348
    // add logic for the POs
    Gia_ManForEachCo( p, pObj, i )
    {
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
        if ( i % nOutDelta != 0 )
            continue;
349
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
Alan Mishchenko committed
350 351 352 353 354 355
    }
    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    ABC_FREE( ppNodes );
    return pNew;
}

Alan Mishchenko committed
356 357 358 359 360 361 362 363 364 365 366
/**Function*************************************************************

  Synopsis    [Duplicates AIG in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
367 368 369 370 371 372
Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
{
    Aig_Man_t * pNew;
    Aig_Obj_t ** ppNodes;
    Gia_Obj_t * pObj;
    int i;
373
    ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
374 375
    // create the new manager
    pNew = Aig_ManStart( Gia_ManObjNum(p) );
376
    pNew->pName = Abc_UtilStrsav( p->pName );
377
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
378 379 380 381 382 383 384
    pNew->nConstrs = p->nConstrs;
    // create the PIs
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
        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 389 390 391
        else if ( Gia_ObjIsConst0(pObj) )
            ppNodes[i] = Aig_ManConst0(pNew);
        else
            assert( 0 );
392
        pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
Alan Mishchenko committed
393
        assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410
    }
    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    ABC_FREE( ppNodes );
    return pNew;
}

/**Function*************************************************************

  Synopsis    [Duplicates AIG in the DFS order.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
411 412 413 414 415 416 417
Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
{
    Aig_Man_t * pMan;
    Gia_Man_t * pGia, * pTemp;
    pGia = Gia_ManFromAig( p );
    pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
    Gia_ManStop( pTemp );
Alan Mishchenko committed
418
    pMan = Gia_ManToAig( pGia, 0 );
Alan Mishchenko committed
419 420 421 422
    Gia_ManStop( pGia );
    return pMan;
}

Alan Mishchenko committed
423 424 425 426 427

/**Function*************************************************************

  Synopsis    [Transfers representatives from pGia to pAig.]

428
  Description [Assumes that pGia was created from pAig.]
Alan Mishchenko committed
429 430 431 432 433 434
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
435
void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
Alan Mishchenko committed
436 437 438 439
{
    Aig_Obj_t * pObj;
    Gia_Obj_t * pGiaObj, * pGiaRepr;
    int i;
440
    assert( pAig->pReprs == NULL );
Alan Mishchenko committed
441 442
    assert( pGia->pReprs != NULL );
    // move pointers from AIG to GIA
443
    Aig_ManForEachObj( pAig, pObj, i )
Alan Mishchenko committed
444
    {
445 446
        assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
        pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
Alan Mishchenko committed
447 448 449
        pGiaObj->Value = i;
    }
    // set the pointers to the nodes in AIG
450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    Gia_ManForEachObj( pGia, pGiaObj, i )
    {
        pGiaRepr = Gia_ObjReprObj( pGia, i );
        if ( pGiaRepr == NULL )
            continue;
        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
    }
}
void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
{
    Gia_Obj_t * pGiaObj, * pGiaRepr;
    int i;
    assert( pAig->pReprs == NULL );
    assert( pGia->pReprs != NULL );
    // set the pointers to the nodes in AIG
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Alan Mishchenko committed
467 468 469 470 471
    Gia_ManForEachObj( pGia, pGiaObj, i )
    {
        pGiaRepr = Gia_ObjReprObj( pGia, i );
        if ( pGiaRepr == NULL )
            continue;
472
        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
Alan Mishchenko committed
473 474 475
    }
}

Alan Mishchenko committed
476 477
/**Function*************************************************************

478
  Synopsis    [Transfers representatives from pAig to pGia.]
Alan Mishchenko committed
479 480 481 482 483 484 485 486

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
487
void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
Alan Mishchenko committed
488
{
489 490 491 492 493
    Gia_Obj_t * pObjGia; 
    Aig_Obj_t * pObjAig, * pReprAig;
    int i;
    assert( pAig->pReprs != NULL );
    assert( pGia->pReprs == NULL );
494
    assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
495 496 497
    pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
    for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
        Gia_ObjSetRepr( pGia, i, GIA_VOID );
498
    // move pointers from GIA to AIG
499 500 501 502
    Gia_ManForEachObj( pGia, pObjGia, i )
    {
        if ( Gia_ObjIsCo(pObjGia) )
            continue;
503 504
        assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
        pObjAig  = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
505 506 507 508
        pObjAig->iData = i;
    }
    Aig_ManForEachObj( pAig, pObjAig, i )
    {
509
        if ( Aig_ObjIsCo(pObjAig) )
510 511 512 513 514 515 516 517
            continue;
        if ( pAig->pReprs[i] == NULL )
            continue;
        pReprAig = pAig->pReprs[i];
        Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData );
    }
    pGia->pNexts = Gia_ManDeriveNexts( pGia );
}
518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538
void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
{
    Aig_Obj_t * pObjAig, * pReprAig;
    int i;
    assert( pAig->pReprs != NULL );
    assert( pGia->pReprs == NULL );
    assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
    pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
    for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
        Gia_ObjSetRepr( pGia, i, GIA_VOID );
    Aig_ManForEachObj( pAig, pObjAig, i )
    {
        if ( Aig_ObjIsCo(pObjAig) )
            continue;
        if ( pAig->pReprs[i] == NULL )
            continue;
        pReprAig = pAig->pReprs[i];
        Gia_ObjSetRepr( pGia, Abc_Lit2Var(pObjAig->iData), Abc_Lit2Var(pReprAig->iData) );
    }
    pGia->pNexts = Gia_ManDeriveNexts( pGia );
}
539 540 541 542 543 544 545 546 547 548 549 550 551 552

/**Function*************************************************************

  Synopsis    [Applies DC2 to the GIA manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose )
{
Alan Mishchenko committed
553 554
    Gia_Man_t * pGia;
    Aig_Man_t * pNew, * pTemp;
555 556
    if ( p->pManTime && p->vLevels == NULL )
        Gia_ManLevelWithBoxes( p );
Alan Mishchenko committed
557
    pNew = Gia_ManToAig( p, 0 );
558
    pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
Alan Mishchenko committed
559 560 561
    Aig_ManStop( pTemp );
    pGia = Gia_ManFromAig( pNew );
    Aig_ManStop( pNew );
562
    Gia_ManTransferTiming( pGia, p );
Alan Mishchenko committed
563 564 565
    return pGia;
}

566 567 568 569 570 571 572 573 574 575 576 577 578 579 580
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
{
    Gia_Man_t * pGia;
    Aig_Man_t * pNew;
581 582
    if ( p->pManTime && p->vLevels == NULL )
        Gia_ManLevelWithBoxes( p );
583 584
    pNew = Gia_ManToAig( p, 0 );
    pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
585 586
//    pGia = Gia_ManFromAig( pNew );
    pGia = Gia_ManFromAigChoices( pNew );
587
    Aig_ManStop( pNew );
588
    Gia_ManTransferTiming( pGia, p );
589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606
    return pGia;
}

/**Function*************************************************************

  Synopsis    [Computes equivalences after structural sequential cleanup.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose )
{
    Aig_Man_t * pNew, * pTemp;
    pNew  = Gia_ManToAigSimple( p );
607
    pTemp = Aig_ManScl( pNew, fConst, fEquiv, 0, -1, -1, fVerbose, 0 );
608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625
    Gia_ManReprFromAigRepr( pNew, p );
    Aig_ManStop( pTemp );
    Aig_ManStop( pNew );
}

/**Function*************************************************************

  Synopsis    [Solves SAT problem.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManSolveSat( Gia_Man_t * p )
{
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 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655
    if ( RetValue == 0 )
    {
        Gia_Obj_t * pObj;
        int i, * pInit = (int *)pNew->pData;
        Gia_ManConst0(p)->fMark0 = 0;
        Gia_ManForEachPi( p, pObj, i )
            pObj->fMark0 = pInit[i];
        Gia_ManForEachAnd( p, pObj, i )
            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
        Gia_ManForEachPo( p, pObj, i )
            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
        Gia_ManForEachPo( p, pObj, i )
            if ( pObj->fMark0 != 1 )
                break;
        if ( i != Gia_ManPoNum(p) )
            Abc_Print( 1, "Counter-example verification has failed.  " );
//        else
//            Abc_Print( 1, "Counter-example verification succeeded.  " );
    }
/*
    else if ( RetValue == 1 )
        Abc_Print( 1, "The SAT problem is unsatisfiable.  " );
    else if ( RetValue == -1 )
        Abc_Print( 1, "The SAT problem is undecided.  " );
656
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
657 658 659 660 661 662
*/
    Aig_ManStop( pNew );
    return RetValue;
}


Alan Mishchenko committed
663 664 665 666 667
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


668 669
ABC_NAMESPACE_IMPL_END