diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 19:17:59 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 19:17:59 -0700 |
| commit | 3b1ebbaa281578ee8b0ef0e62b495dbbaf1f18e1 (patch) | |
| tree | 0853de28ff7a5406d3c9be2f1a7181d648a640fb /src/aig/gia/giaDup.c | |
| parent | 9e1765216ba5f64d89a0dc93e33fb95c84a0c779 (diff) | |
| download | abc-3b1ebbaa281578ee8b0ef0e62b495dbbaf1f18e1.tar.gz abc-3b1ebbaa281578ee8b0ef0e62b495dbbaf1f18e1.tar.bz2 abc-3b1ebbaa281578ee8b0ef0e62b495dbbaf1f18e1.zip | |
SAT sweeping under constraints.
Diffstat (limited to 'src/aig/gia/giaDup.c')
| -rw-r--r-- | src/aig/gia/giaDup.c | 39 |
1 files changed, 36 insertions, 3 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 92248225..c5e5a0b7 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -974,10 +974,32 @@ void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } +Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew->nConstrs = p->nConstrs; + if ( p->pCexSeq ) + pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); + return pNew; +} /**Function************************************************************* - Synopsis [Duplicates AIG in the DFS order.] + Synopsis [Duplicates the AIG in the DFS order while rehashing.] Description [] @@ -986,7 +1008,16 @@ void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) +void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; @@ -998,11 +1029,13 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew->nConstrs = p->nConstrs; if ( p->pCexSeq ) pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; |