diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 14:44:59 -0500 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 14:44:59 -0500 |
| commit | 044d2f0aba58fe623496a9ec90d9999c8e8c6875 (patch) | |
| tree | 93377f7180ed6f6e29f710305912f7321352b08b /src/aig/gia | |
| parent | fc77972625311cf73243f3867dec07527721eec7 (diff) | |
| download | abc-044d2f0aba58fe623496a9ec90d9999c8e8c6875.tar.gz abc-044d2f0aba58fe623496a9ec90d9999c8e8c6875.tar.bz2 abc-044d2f0aba58fe623496a9ec90d9999c8e8c6875.zip | |
User-controlable SAT sweeper.
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 9f4ab18b..188a021c 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -211,7 +211,7 @@ int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit ) Vec_IntPush( pSwp->vProbes, iLit ); Vec_IntPush( pSwp->vProbRefs, 1 ); Vec_IntSetEntryFull( pSwp->vLit2Prob, iLit, ProbeId ); // consider hash table in the future -printf( "Creating probe %d with literal %d.\n", ProbeId, iLit ); +//printf( "Creating probe %d with literal %d.\n", ProbeId, iLit ); return ProbeId; } // if probe with this literal (iLit) exists, this procedure increments its reference counter and returns it. @@ -234,7 +234,7 @@ void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId ) Vec_IntWriteEntry( pSwp->vLit2Prob, iLit, -1 ); Vec_IntWriteEntry( pSwp->vProbes, ProbeId, 0 ); // TODO: recycle probe ID -printf( "Deleteing probe %d with literal %d.\n", ProbeId, iLit ); +//printf( "Deleteing probe %d with literal %d.\n", ProbeId, iLit ); } } // returns literal associated with the probe @@ -318,8 +318,14 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; Vec_Int_t * vObjIds; + Vec_Int_t * vValues; int i, ProbeId; assert( Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) ); + // save values + vValues = Vec_IntAlloc( Gia_ManObjNum(p) ); + Gia_ManForEachObj( p, pObj, i ) + Vec_IntPush( vValues, pObj->Value ); + // create new Gia_ManIncrementTravId( p ); vObjIds = Vec_IntAlloc( 1000 ); Vec_IntForEachEntry( vProbeIds, ProbeId, i ) @@ -358,6 +364,10 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V if ( vOutNames ) pNew->vNamesOut = Vec_PtrDupStr( vOutNames ); //Gia_ManPrintStats( pNew, 0, 0, 0 ); + // reset values + Gia_ManForEachObj( p, pObj, i ) + pObj->Value = Vec_IntEntry( vValues, i ); + Vec_IntFree( vValues ); return pNew; } |