From 9521d1345b364eeb99498dfc0df329375d0ea669 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 28 Oct 2015 13:44:29 -0700 Subject: Improvements to 'satclp'. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaUtil.c | 41 +++++++++++ src/base/abci/abcCollapse.c | 87 ++++++++++++++++++---- src/proof/abs/absRpm.c | 81 +++++++++++++++++++++ src/sat/bmc/bmcClp.c | 171 +++++++++++++++++++++++++++++++++++++++++--- 5 files changed, 356 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 6b801b9e..4ad3e39a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1452,6 +1452,7 @@ extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); extern int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); +extern int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index ae32b91e..ff44eecf 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1141,6 +1141,47 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ) return ConeSize1; } +/**Function************************************************************* + + Synopsis [Returns the number of internal nodes in the MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_NodeCollect_rec( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pNode) ) + return; + Gia_ObjSetTravIdCurrent(p, pNode); + if ( Gia_ObjRefNum(p, pNode) || Gia_ObjIsCi(pNode) ) + { + Vec_IntPush( vSupp, Gia_ObjId(p, pNode) ); + return; + } + assert( Gia_ObjIsAnd(pNode) ); + Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp ); + Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp ); +} +int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp ) +{ + int ConeSize1, ConeSize2; + assert( !Gia_IsComplement(pNode) ); + assert( Gia_ObjIsAnd(pNode) ); + Vec_IntClear( vSupp ); + Gia_ManIncrementTravId( p ); + ConeSize1 = Gia_NodeDeref_rec( p, pNode ); + Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp ); + Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp ); + ConeSize2 = Gia_NodeRef_rec( p, pNode ); + assert( ConeSize1 == ConeSize2 ); + assert( ConeSize1 >= 0 ); + return ConeSize1; +} + /**Function************************************************************* Synopsis [Returns 1 if AIG has dangling nodes.] diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index d1e6be2f..ac7bcdc5 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -581,6 +581,51 @@ Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk ) return pNew; } +/**Function************************************************************* + + Synopsis [Minimize SOP by removing redundant variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#define Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) + +int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp ) +{ + int j = 0, k, iVar, nVars = Vec_IntSize(vSupp); + char * pCube, * pSop = Vec_StrArray(vSop); + Vec_Int_t * vPres = Vec_IntStart( nVars ); + Abc_NtkSopForEachCube( pSop, nVars, pCube ) + for ( k = 0; k < nVars; k++ ) + if ( pCube[k] != '-' ) + Vec_IntWriteEntry( vPres, k, 1 ); + if ( Vec_IntCountZero(vPres) == 0 ) + { + Vec_IntFree( vPres ); + return 0; + } + // reduce cubes + Abc_NtkSopForEachCube( pSop, nVars, pCube ) + for ( k = 0; k < nVars + 3; k++ ) + if ( k >= nVars || Vec_IntEntry(vPres, k) ) + Vec_StrWriteEntry( vSop, j++, pCube[k] ); + Vec_StrWriteEntry( vSop, j++, '\0' ); + Vec_StrShrink( vSop, j ); + // reduce support + j = 0; + Vec_IntForEachEntry( vSupp, iVar, k ) + if ( Vec_IntEntry(vPres, k) ) + Vec_IntWriteEntry( vSupp, j++, iVar ); + Vec_IntShrink( vSupp, j ); + Vec_IntFree( vPres ); + return 1; +} + + /**Function************************************************************* Synopsis [Computes SOPs for each output.] @@ -606,6 +651,10 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit return NULL; if ( Vec_StrSize(vSop) == 4 ) // constant Vec_IntClear(vSupp); + else + Abc_NtkCollapseCountVars( vSop, vSupp ); + if ( fVerbose ) + printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return vSop; @@ -613,27 +662,18 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) { ProgressBar * pProgress; + abctime clk = Abc_Clock(); Vec_Ptr_t * vSops = NULL, * vSopsRepr; Vec_Int_t * vReprs, * vClass, * vReprSuppSizes; int i, k, Entry, iCo, * pOrder; Vec_Wec_t * vClasses; - // check the largest output - if ( nCubeLim > 0 && nCostMax > 0 ) - { - int iCoMax = Gia_ManCoLargestSupp( p, vSupps ); - int iObjMax = Gia_ObjId( p, Gia_ManCo(p, iCoMax) ); - int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) ); - int nNodeMax = Gia_ManConeSize( p, &iObjMax, 1 ); - word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim; - if ( Cost > (word)nCostMax ) - { - printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n", - nNodeMax, nSuppMax, nCubeLim, nCostMax ); - return NULL; - } - } // derive classes of outputs vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 ); + if ( fVerbose ) + { + printf( "Considering %d (out of %d) outputs. ", Vec_WecSize(vClasses), Gia_ManCoNum(p) ); + Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); + } // derive representatives vReprs = Vec_WecCollectFirsts( vClasses ); vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) ); @@ -693,6 +733,23 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in int i, k, iCi; pGia = Abc_NtkClpGia( pNtk ); vSupps = Gia_ManCreateCoSupps( pGia, fVerbose ); + // check the largest output + if ( nCubeLim > 0 && nCostMax > 0 ) + { + int iCoMax = Gia_ManCoLargestSupp( pGia, vSupps ); + int iObjMax = Gia_ObjId( pGia, Gia_ManCo(pGia, iCoMax) ); + int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) ); + int nNodeMax = Gia_ManConeSize( pGia, &iObjMax, 1 ); + word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim; + if ( Cost > (word)nCostMax ) + { + printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n", + nNodeMax, nSuppMax, nCubeLim, nCostMax ); + Gia_ManStop( pGia ); + Vec_WecFree( vSupps ); + return NULL; + } + } pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c index ef5747c1..edcbe7ed 100644 --- a/src/proof/abs/absRpm.c +++ b/src/proof/abs/absRpm.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abs.h" +#include "misc/vec/vecWec.h" ABC_NAMESPACE_IMPL_START @@ -106,6 +107,86 @@ void Gia_ManComputeDoms( Gia_Man_t * p ) Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i ); } } + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Gia_ManCreateSupps( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Obj_t * pObj; int i, Id; + Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntPush( Vec_WecEntry(vSupps, Id), i ); + Gia_ManForEachAnd( p, pObj, Id ) + Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), + Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), + Vec_WecEntry(vSupps, Id) ); +// Gia_ManForEachCo( p, pObj, i ) +// Vec_IntAppend( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) ); + if ( fVerbose ) + Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); + return vSupps; +} +void Gia_ManDomTest( Gia_Man_t * p ) +{ + Vec_Int_t * vDoms = Vec_IntAlloc( 100 ); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + Vec_Wec_t * vSupps = Gia_ManCreateSupps( p, 1 ); + Vec_Wec_t * vDomeds = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pObj, * pDom; int i, Id, nMffcSize; + Gia_ManCreateRefs( p ); + Gia_ManComputeDoms( p ); + Gia_ManForEachCi( p, pObj, i ) + { + if ( Gia_ObjDom(p, pObj) == -1 ) + continue; + for ( pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj)); Gia_ObjIsAnd(pDom); pDom = Gia_ManObj(p, Gia_ObjDom(p, pDom)) ) + Vec_IntPush( Vec_WecEntry(vDomeds, Gia_ObjId(p, pDom)), i ); + } + Gia_ManForEachAnd( p, pObj, i ) + if ( Vec_IntEqual(Vec_WecEntry(vSupps, i), Vec_WecEntry(vDomeds, i)) ) + Vec_IntPush( vDoms, i ); + Vec_WecFree( vSupps ); + Vec_WecFree( vDomeds ); + + // check MFFC sizes + Vec_IntForEachEntry( vDoms, Id, i ) + Gia_ObjRefInc( p, Gia_ManObj(p, Id) ); + Vec_IntForEachEntry( vDoms, Id, i ) + { + nMffcSize = Gia_NodeMffcSizeSupp( p, Gia_ManObj(p, Id), vSupp ); + printf( "%d(%d:%d) ", Id, Vec_IntSize(vSupp), nMffcSize ); + } + printf( "\n" ); + Vec_IntForEachEntry( vDoms, Id, i ) + Gia_ObjRefDec( p, Gia_ManObj(p, Id) ); + +// Vec_IntPrint( vDoms ); + Vec_IntFree( vDoms ); + Vec_IntFree( vSupp ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManTestDoms2( Gia_Man_t * p ) { Vec_Int_t * vNodes; diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 81f81063..826c0a32 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -36,14 +36,158 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [For a given random pattern, compute output change.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_ComputeSimDiff( Gia_Man_t * p, Vec_Int_t * vPat, Vec_Int_t * vPat2 ) +{ + Gia_Obj_t * pObj; + int i, Id; word Sim, Sim0, Sim1; + Gia_ManForEachCiId( p, Id, i ) + { + Sim = Vec_IntEntry(vPat, i) ? ~(word)0 : 0; + Sim ^= (word)1 << (i + 1); + Vec_WrdWriteEntry( p->vSims, Id, Sim ); + } + Gia_ManForEachAnd( p, pObj, i ) + { + Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, i) ); + Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1(pObj, i) ); + Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0; + Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1; + Vec_WrdWriteEntry( p->vSims, i, Sim0 & Sim1 ); + } + Gia_ManForEachCo( p, pObj, i ) + { + Id = Gia_ObjId( p, pObj ); + Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0(pObj, Id) ); + Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0; + Vec_WrdWriteEntry( p->vSims, Id, Sim0 ); + } + pObj = Gia_ManCo( p, 0 ); + Sim = Vec_WrdEntry( p->vSims, Gia_ObjId(p, pObj) ); + Vec_IntClear( vPat2 ); + for ( i = 1; i <= Gia_ManCiNum(p); i++ ) + Vec_IntPush( vPat2, (int)((Sim & 1) ^ ((Sim >> i) & 1)) ); + return (int)(Sim & 1); +} +void Bmc_ComputeSimTest( Gia_Man_t * p ) +{ + int i, v, w, Res, Bit, Bit2, nPats = 256; + int Count[2][64][64] = {{{0}}}; + int PatCount[64][2][2] = {{{0}}}; + int DiffCount[64] = {0}; + Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) ); + Vec_Int_t * vPat2 = Vec_IntAlloc( Gia_ManCiNum(p) ); + Vec_WrdFreeP( &p->vSims ); + p->vSims = Vec_WrdStart( Gia_ManObjNum(p) ); + printf( "Number of patterns = %d.\n", nPats ); + for ( i = 0; i < nPats; i++ ) + { + Vec_IntClear( vPat ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + Vec_IntPush( vPat, rand() & 1 ); + +// Vec_IntForEachEntry( vPat, Bit, v ) +// printf( "%d", Bit ); +// printf( " " ); + + Res = Bmc_ComputeSimDiff( p, vPat, vPat2 ); +// printf( "%d ", Res ); + +// Vec_IntForEachEntry( vPat2, Bit, v ) +// printf( "%d", Bit ); +// printf( "\n" ); + + Vec_IntForEachEntry( vPat, Bit, v ) + PatCount[v][Res][Bit]++; + + Vec_IntForEachEntry( vPat2, Bit, v ) + { + if ( Bit ) + DiffCount[v]++; + Vec_IntForEachEntryStart( vPat2, Bit2, w, v + 1 ) + if ( Bit && Bit2 ) + Count[Res][v][w]++; + } + } + Vec_IntFree( vPat ); + Vec_IntFree( vPat2 ); + Vec_WrdFreeP( &p->vSims ); + + + printf( "\n" ); + printf( " " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3c ", 'a'+v ); + printf( "\n" ); + + printf( "Off0 " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3d ", PatCount[v][0][0] ); + printf( "\n" ); + + printf( "Off1 " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3d ", PatCount[v][0][1] ); + printf( "\n" ); + + printf( "On0 " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3d ", PatCount[v][1][0] ); + printf( "\n" ); + + printf( "On1 " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3d ", PatCount[v][1][1] ); + printf( "\n" ); + printf( "\n" ); + + printf( "Diff " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3d ", DiffCount[v] ); + printf( "\n" ); + printf( "\n" ); + + for ( i = 0; i < 2; i++ ) + { + printf( " " ); + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + printf( "%3c ", 'a'+v ); + printf( "\n" ); + + for ( v = 0; v < Gia_ManCiNum(p); v++ ) + { + printf( " %c ", 'a'+v ); + for ( w = 0; w < Gia_ManCiNum(p); w++ ) + { + if ( Count[i][v][w] ) + printf( "%3d ", Count[i][v][w] ); + else + printf( " . " ); + } + printf( "\n" ); + } + printf( "\n" ); + } +} + + static abctime clkCheck1 = 0; static abctime clkCheck2 = 0; static abctime clkCheckS = 0; static abctime clkCheckU = 0; -// enumerate cubes and literals -#define Bmc_SopForEachCube( pSop, nVars, pCube ) \ - for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) +// iterator thought the cubes +#define Bmc_SopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) /**Function************************************************************* @@ -270,11 +414,6 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * } // if ( pSatOn ) // printf( "\n" ); - // put into new array - Vec_IntClear( vNums ); - Vec_IntForEachEntry( vLits, iLit, n ) - if ( iLit != -1 ) - Vec_IntPush( vNums, n ); return 0; } @@ -311,9 +450,21 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit if ( k == nFinal ) Vec_IntWriteEntry( vLits, i, -1 ); } + Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon ); + } + else + { + Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon ); + Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon ); + } + { + // put into new array + int i, iLit; + Vec_IntClear( vNums ); + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 ) + Vec_IntPush( vNums, i ); } - Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon ); - Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon ); return 0; } -- cgit v1.2.3