From 3b1ebbaa281578ee8b0ef0e62b495dbbaf1f18e1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 28 Apr 2013 19:17:59 -0700 Subject: SAT sweeping under constraints. --- src/proof/ssc/sscCore.c | 12 +++++++++--- src/proof/ssc/sscInt.h | 1 + src/proof/ssc/sscSim.c | 45 ++++++++++++++++++++++++++++++++++++++++----- src/proof/ssc/sscUtil.c | 20 ++++++++++++++------ 4 files changed, 64 insertions(+), 14 deletions(-) (limited to 'src/proof') diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index b29a0193..55f0e140 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -83,8 +83,9 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar p->pPars = pPars; p->pAig = pAig; p->pCare = pCare; - p->pFraig = Gia_ManDup( p->pCare ); - Gia_ManHashStart( p->pFraig ); + p->pFraig = Gia_ManDupDfs( p->pCare ); + assert( p->pFraig->pHTable == NULL ); + assert( !Gia_ManHasDangling(p->pFraig) ); Gia_ManInvertPos( p->pFraig ); Ssc_ManStartSolver( p ); if ( p->pSat == NULL ) @@ -170,6 +171,8 @@ clk = clock(); p = Ssc_ManStart( pAig, pCare, pPars ); if ( p == NULL ) return Gia_ManDup( pAig ); + if ( p->pPars->fVerbose ) + printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 10), 640 ); // perform simulation if ( Gia_ManAndNum(pCare) == 0 ) // no constraints { @@ -189,6 +192,9 @@ p->timeSimInit += clock() - clk; Gia_ManConst0(pAig)->Value = 0; Gia_ManForEachCi( pAig, pObj, i ) pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) ); +// Gia_ManLevelNum(pAig); + // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart) + Gia_ManHashStart( p->pFraig ); // perform sweeping Ssc_GiaResetPiPattern( pAig, pPars->nWords ); Ssc_GiaSavePiPattern( pAig, p->vPivot ); @@ -207,6 +213,7 @@ clk = clock(); Ssc_GiaResetPiPattern( pAig, pPars->nWords ); Ssc_GiaSavePiPattern( pAig, p->vPivot ); p->timeSimSat += clock() - clk; +//printf( "\n" ); } if ( Gia_ObjIsAnd(pObj) ) pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -272,7 +279,6 @@ p->timeSimSat += clock() - clk; // count the number of representatives if ( pPars->fVerbose ) { -// Gia_ManEquivPrintClasses( pAig, 0, 0 ); Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult), 100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) ); diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h index f0a556a6..1226f4ee 100644 --- a/src/proof/ssc/sscInt.h +++ b/src/proof/ssc/sscInt.h @@ -116,6 +116,7 @@ extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_ extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat ); extern void Ssc_GiaSimRound( Gia_Man_t * p ); extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ); +extern int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords ); /*=== sscUtil.c ===================================================*/ extern Gia_Man_t * Ssc_GenerateOneHot( int nVars ); diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c index 9a2c1033..d28db432 100644 --- a/src/proof/ssc/sscSim.c +++ b/src/proof/ssc/sscSim.c @@ -82,6 +82,24 @@ static inline int Ssc_SimFindBit( word * pSim, int nWords ) return -1; } +static inline int Ssc_SimCountBitsWord( word x ) +{ + x = x - ((x >> 1) & ABC_CONST(0x5555555555555555)); + x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333)); + x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F); + x = x + (x >> 8); + x = x + (x >> 16); + x = x + (x >> 32); + return (int)(x & 0xFF); +} +static inline int Ssc_SimCountBits( word * pSim, int nWords ) +{ + int w, Counter = 0; + for ( w = 0; w < nWords; w++ ) + Counter += Ssc_SimCountBitsWord(pSim[w]); + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -245,6 +263,14 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) Vec_IntPush( vInit, Abc_InfoHasBit((unsigned *)Gia_ObjSimObj(p, pObj), iBit) ); return vInit; } +Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ) +{ + Vec_Int_t * vInit; + Ssc_GiaRandomPiPattern( p, 1, NULL ); + Ssc_GiaSimRound( p ); + vInit = Ssc_GiaGetOneSim( p ); + return vInit; +} /**Function************************************************************* @@ -257,13 +283,22 @@ Vec_Int_t * Ssc_GiaGetOneSim( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ) +int Ssc_GiaCountCaresSim( Gia_Man_t * p ) { - Vec_Int_t * vInit; - Ssc_GiaRandomPiPattern( p, 1, NULL ); + Gia_Obj_t * pObj; + int i, Count, nWords = Gia_ObjSimWords( p ); + word * pRes = ABC_FALLOC( word, nWords ); + Gia_ManForEachPo( p, pObj, i ) + Ssc_SimAnd( pRes, pRes, Gia_ObjSimObj(p, pObj), nWords, 0, 0 ); + Count = Ssc_SimCountBits( pRes, nWords ); + ABC_FREE( pRes ); + return Count; +} +int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords ) +{ + Ssc_GiaRandomPiPattern( p, nWords, NULL ); Ssc_GiaSimRound( p ); - vInit = Ssc_GiaGetOneSim( p ); - return vInit; + return Ssc_GiaCountCaresSim( p ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/ssc/sscUtil.c b/src/proof/ssc/sscUtil.c index 0ced578f..52aea52c 100644 --- a/src/proof/ssc/sscUtil.c +++ b/src/proof/ssc/sscUtil.c @@ -52,6 +52,7 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p ) Gia_Obj_t * pObj; Vec_Int_t * vLits, * vKeep; sat_solver * pSat; + int ConstLit = Abc_Var2Lit(pDat->pVarNums[0], 0); int i, status;//, Count = 0; Aig_ManStop( pMan ); @@ -75,10 +76,10 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p ) return NULL; } } + Cnf_DataFree( pDat ); status = sat_solver_simplify( pSat ); if ( status == 0 ) { - Cnf_DataFree( pDat ); sat_solver_delete( pSat ); Vec_IntFree( vLits ); return NULL; @@ -92,17 +93,15 @@ Gia_Man_t * Gia_ManDropContained( Gia_Man_t * p ) status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits,i)) ); if ( status == l_False ) - Vec_IntWriteEntry( vLits, i, Abc_Var2Lit(pDat->pVarNums[0], 0) ); // const1 SAT var is always true + Vec_IntWriteEntry( vLits, i, ConstLit ); // const1 SAT var is always true else { assert( status = l_True ); Vec_IntPush( vKeep, i ); } } - Cnf_DataFree( pDat ); sat_solver_delete( pSat ); Vec_IntFree( vLits ); - if ( Vec_IntSize(vKeep) == Gia_ManPoNum(p) ) { Vec_IntFree( vKeep ); @@ -140,19 +139,28 @@ Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p ) return pTemp; Ssc_ManSetDefaultParams( pPars ); pPars->fAppend = 1; - pPars->fVerbose = 1; + pPars->fVerbose = 0; pTemp->nConstrs = Gia_ManPoNum(pTemp) - 1; for ( i = 0; i < Gia_ManPoNum(pTemp); i++ ) { + // move i-th PO forward Gia_ManSwapPos( pTemp, i ); + pTemp = Gia_ManDupDfs( pAux = pTemp ); + Gia_ManStop( pAux ); + // minimize this PO pTemp = Ssc_PerformSweepingConstr( pAux = pTemp, pPars ); Gia_ManStop( pAux ); - pTemp = Gia_ManDupNormalize( pAux = pTemp ); + pTemp = Gia_ManDupDfs( pAux = pTemp ); Gia_ManStop( pAux ); + // move i-th PO back Gia_ManSwapPos( pTemp, i ); + pTemp = Gia_ManDupDfs( pAux = pTemp ); + Gia_ManStop( pAux ); + // report results printf( "AIG%3d : ", i ); Gia_ManPrintStats( pTemp, 0, 0, 0 ); } + pTemp->nConstrs = 0; return pTemp; } -- cgit v1.2.3