diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/gia.h | 7 | ||||
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 68 |
2 files changed, 69 insertions, 6 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 5e1e4793..973d8307 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -995,7 +995,7 @@ extern Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars ); /*=== giaSweeper.c ============================================================*/ extern Gia_Man_t * Gia_SweeperStart( Gia_Man_t * p ); extern void Gia_SweeperStop( Gia_Man_t * p ); -extern int Gia_SweeperIsRunning( Gia_Man_t * pGia ); +extern int Gia_SweeperIsRunning( Gia_Man_t * p ); extern void Gia_SweeperPrintStats( Gia_Man_t * p ); extern void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax ); extern void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds ); @@ -1008,10 +1008,11 @@ extern int Gia_SweeperCondPop( Gia_Man_t * p ); extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId ); extern Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p ); extern int Gia_SweeperCondCheckUnsat( Gia_Man_t * p ); -extern int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int ProbeId1, int ProbeId2 ); +extern int Gia_SweeperCheckEquiv( Gia_Man_t * p, int ProbeId1, int ProbeId2 ); extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames ); extern Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc ); -extern Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ); +extern Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime ); +extern Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbes, char * pCommLime ); /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index ea4c2b0e..67ff6f93 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -859,10 +859,13 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * Vec_Int_t * vOutLits; Gia_Obj_t * pObj; int i; - assert( Vec_IntSize(vProbes) == Gia_ManPiNum(pSrc) ); - assert( pDst->pHTable != NULL ); + assert( Gia_SweeperIsRunning(pDst) ); + if ( vProbes ) + assert( Vec_IntSize(vProbes) == Gia_ManPiNum(pSrc) ); + else + assert( Gia_ManPiNum(pDst) == Gia_ManPiNum(pSrc) ); Gia_ManForEachPi( pSrc, pObj, i ) - pObj->Value = Gia_SweeperProbeLit( pDst, Vec_IntEntry(vProbes, i) ); + pObj->Value = Gia_SweeperProbeLit( pDst, vProbes ? Vec_IntEntry(vProbes, i) : Gia_Obj2Lit(pDst,Gia_ManPi(pDst, i)) ); Gia_ManForEachAnd( pSrc, pObj, i ) pObj->Value = Gia_ManHashAnd( pDst, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); vOutLits = Vec_IntAlloc( Gia_ManPoNum(pSrc) ); @@ -976,6 +979,45 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts ) /**Function************************************************************* + Synopsis [Procedure to perform conditional fraig sweeping on separate logic cones..] + + Description [The procedure takes GIA with the sweeper defined. The sweeper + is assumed to have some conditions currently pushed, which will be used + as constraints for fraig sweeping. The second argument (vProbes) contains + the array of probe IDs pointing to the user's logic cones to be SAT swept. + Finally, the optional command line (pCommLine) is an ABC command line + to be applied to the resulting GIA after SAT sweeping before it is + grafted back into the original GIA manager. The return value is the array + of literals in the original GIA manager, corresponding to the user's + logic cones after sweeping, synthesis and grafting.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbes, char * pCommLime ) +{ + Gia_Man_t * pNew; + Vec_Int_t * vLits; + // sweeper is running + assert( Gia_SweeperIsRunning(p) ); + // sweep the logic + pNew = Gia_SweeperSweep( p, vProbes ); + // execute command line + if ( pCommLime ) + { + // set pNew to be current GIA in ABC + // execute command line pCommLine using Abc_CmdCommandExecute() + // get pNew to be current GIA in ABC + } + vLits = Gia_SweeperGraft( p, NULL, pNew ); + Gia_ManStop( pNew ); + return vLits; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -1056,6 +1098,26 @@ Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVe return pGia; } +/**Function************************************************************* + + Synopsis [Sweeper cleanup.] + + Description [Returns new GIA with sweeper defined, which is the same + as the original sweeper, with all the dangling logic removed and SAT + solver restarted. The probe IDs are guaranteed to have the same logic + functions as in the original manager.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime ) +{ + return NULL; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |