diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 11:26:40 -0500 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-26 11:26:40 -0500 |
| commit | 59bc3cb9d9593159e586b91520f8224bce3a34b3 (patch) | |
| tree | 8224e5f38ce5ebb5d0ea4d237d91b7d3afe8bf43 | |
| parent | 8e68df2c6a1870dc6d8fb1c06fbeb250a33cbd40 (diff) | |
| download | abc-59bc3cb9d9593159e586b91520f8224bce3a34b3.tar.gz abc-59bc3cb9d9593159e586b91520f8224bce3a34b3.tar.bz2 abc-59bc3cb9d9593159e586b91520f8224bce3a34b3.zip | |
User-controlable SAT sweeper.
| -rw-r--r-- | src/aig/gia/gia.h | 6 | ||||
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 20 |
2 files changed, 15 insertions, 11 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index bf184c8c..e6db1886 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -995,16 +995,16 @@ extern Gia_Man_t * Gia_SweeperStart(); extern void Gia_SweeperStop( Gia_Man_t * p ); extern void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax ); extern void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds ); -extern Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * pGia ); +extern Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p ); extern int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit ); extern int Gia_SweeperProbeFind( Gia_Man_t * p, int iLit ); extern void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId ); extern int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId ); -extern int Gia_SweeperProbeCheckUnsat( Gia_Man_t * p ); extern int Gia_SweeperCondPop( Gia_Man_t * p ); extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId ); -extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames ); +extern int Gia_SweeperCondCheckUnsat( Gia_Man_t * p ); extern int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int ProbeId1, int ProbeId2 ); +extern Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames ); /*=== 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 7d743cbb..773f3f5a 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -181,14 +181,16 @@ void Gia_SweeperStop( Gia_Man_t * pGia ) ***********************************************************************/ void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax ) { - p->nConfMax = nConfMax; + Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; + pSwp->nConfMax = nConfMax; } void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds ) { - p->nTimeOut = nSeconds; + Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; + pSwp->nTimeOut = nSeconds; } -Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * pGia ) +Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p ) { Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; return pSwp->vCexUser; @@ -242,10 +244,6 @@ int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId ) Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; return Vec_IntEntry( pSwp->vProbes, ProbeId ); } -// returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided) -int Gia_SweeperProbeCheckUnsat( Gia_Man_t * p ) -{ -} /**Function************************************************************* @@ -271,6 +269,11 @@ int Gia_SweeperCondPop( Gia_Man_t * p ) Vec_IntPop( pSwp->vCondLits ); return ProbId; } +// returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided) +int Gia_SweeperCondCheckUnsat( Gia_Man_t * p ) +{ + return 0; +} /**Function************************************************************* @@ -565,6 +568,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) clock_t clk; p->nSatCalls++; assert( p->pSat != NULL ); + p->vCexUser = NULL; // get the literals iLitOld = Gia_SweeperProbeLit( pGia, Probe1 ); @@ -575,7 +579,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) // if the literals are opposites, the probes are if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) ) { - Vec_IntFill( p->vSwpCex, Gia_ManPiNum(pGia), 0 ); + Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 0 ); return 0; } // order the literals |