From 674bcbee379b9dcef418ddb62655ee0d3d59f96c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 30 Sep 2021 18:02:33 -0700 Subject: Various changes. --- abclib.dsp | 8 + src/aig/gia/gia.h | 6 + src/aig/gia/giaDecs.c | 350 ++++++++++++++++++++ src/aig/gia/giaMan.c | 1 + src/aig/gia/giaResub.c | 36 +- src/aig/gia/giaSupps.c | 817 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 2 + src/bool/bdc/bdc.h | 2 + src/bool/bdc/bdcCore.c | 79 +++++ src/bool/kit/kit.h | 2 + src/bool/kit/kitHop.c | 101 ++++++ src/misc/util/utilTruth.h | 48 ++- src/misc/vec/vecHsh.h | 4 + src/misc/vec/vecInt.h | 90 +++++ src/misc/vec/vecQue.h | 4 + src/misc/vec/vecWrd.h | 8 + src/proof/cec/cecSatG2.c | 72 ++++ 17 files changed, 1625 insertions(+), 5 deletions(-) create mode 100644 src/aig/gia/giaDecs.c create mode 100644 src/aig/gia/giaSupps.c diff --git a/abclib.dsp b/abclib.dsp index 424b33f7..1726fb18 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -4915,6 +4915,10 @@ SOURCE=.\src\aig\gia\giaCut.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaDecs.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaDeep.c # End Source File # Begin Source File @@ -5211,6 +5215,10 @@ SOURCE=.\src\aig\gia\giaSupp.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaSupps.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaSweep.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 42eb71d5..51b4b2e3 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -216,6 +216,7 @@ struct Gia_Man_t_ Vec_Wrd_t * vSimsPo; Vec_Int_t * vClassOld; Vec_Int_t * vClassNew; + Vec_Int_t * vPats; // incremental simulation int fIncrSim; int iNextPi; @@ -1275,6 +1276,11 @@ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose ); extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ); +/*=== giaDecs.c ============================================================*/ +extern int Gia_ResubVarNum( Vec_Int_t * vResub ); +extern word Gia_ResubToTruth6( Vec_Int_t * vResub ); +extern int Gia_ManEvalSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int fVerbose ); +extern Vec_Int_t * Gia_ManDeriveSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int Type ); /*=== giaDfs.c ============================================================*/ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); extern void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes ); diff --git a/src/aig/gia/giaDecs.c b/src/aig/gia/giaDecs.c new file mode 100644 index 00000000..343891d5 --- /dev/null +++ b/src/aig/gia/giaDecs.c @@ -0,0 +1,350 @@ +/**CFile**************************************************************** + + FileName [giaDecs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Calling various decomposition engines.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaDecs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig/gia/gia.h" +#include "misc/util/utilTruth.h" +#include "misc/extra/extra.h" +#include "bool/bdc/bdc.h" +#include "bool/kit/kit.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut ); +extern Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc, int Depth ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ResubVarNum( Vec_Int_t * vResub ) +{ + if ( Vec_IntSize(vResub) == 1 ) + return Vec_IntEntryLast(vResub) >= 2; + return Vec_IntEntryLast(vResub)/2 - Vec_IntSize(vResub)/2 - 1; +} +word Gia_ResubToTruth6_rec( Vec_Int_t * vResub, int iNode, int nVars ) +{ + assert( iNode >= 0 && nVars <= 6 ); + if ( iNode < nVars ) + return s_Truths6[iNode]; + else + { + int iLit0 = Vec_IntEntry( vResub, Abc_Var2Lit(iNode-nVars, 0) ); + int iLit1 = Vec_IntEntry( vResub, Abc_Var2Lit(iNode-nVars, 1) ); + word Res0 = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iLit0)-2, nVars ); + word Res1 = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iLit1)-2, nVars ); + Res0 = Abc_LitIsCompl(iLit0) ? ~Res0 : Res0; + Res1 = Abc_LitIsCompl(iLit1) ? ~Res1 : Res1; + return iLit0 > iLit1 ? Res0 ^ Res1 : Res0 & Res1; + } +} +word Gia_ResubToTruth6( Vec_Int_t * vResub ) +{ + word Res; + int iRoot = Vec_IntEntryLast(vResub); + if ( iRoot < 2 ) + return iRoot ? ~(word)0 : 0; + assert( iRoot != 2 && iRoot != 3 ); + Res = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iRoot)-2, Gia_ResubVarNum(vResub) ); + return Abc_LitIsCompl(iRoot) ? ~Res : Res; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Gia_ManDeriveTruths( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords ) +{ + int nTtWords = Abc_Truth6WordNum(Vec_IntSize(vSet)); + int nFuncs = Vec_WrdSize(vIsfs) / 2 / nWords; + Vec_Wrd_t * vRes = Vec_WrdStart( 2 * nFuncs * nTtWords ); + Vec_Wrd_t * vIn = Vec_WrdStart( 64*nWords ), * vOut; + int i, f, m, iObj; word Func; + assert( Vec_IntSize(vSet) <= 64 ); + Vec_IntForEachEntry( vSet, iObj, i ) + Abc_TtCopy( Vec_WrdEntryP(vIn, i*nWords), Vec_WrdEntryP(vSims, Vec_IntEntry(vCands, iObj)*nWords), nWords, 0 ); + vOut = Vec_WrdStart( Vec_WrdSize(vIn) ); + Extra_BitMatrixTransposeP( vIn, nWords, vOut, 1 ); + for ( f = 0; f < nFuncs; f++ ) + { + word * pIsf[2] = { Vec_WrdEntryP(vIsfs, (2*f+0)*nWords), + Vec_WrdEntryP(vIsfs, (2*f+1)*nWords) }; + word * pTruth[2] = { Vec_WrdEntryP(vRes, (2*f+0)*nTtWords), + Vec_WrdEntryP(vRes, (2*f+1)*nTtWords) }; + for ( m = 0; m < 64*nWords; m++ ) + { + int iMint = (int)Vec_WrdEntry(vOut, m); + int Value0 = Abc_TtGetBit( pIsf[0], m ); + int Value1 = Abc_TtGetBit( pIsf[1], m ); + if ( !Value0 && !Value1 ) + continue; + if ( Value0 && Value1 ) + printf( "Internal error: Onset and Offset overlap.\n" ); + assert( !Value0 || !Value1 ); + Abc_TtSetBit( pTruth[Value1], iMint ); + } + if ( Abc_TtCountOnesVecMask(pTruth[0], pTruth[1], nTtWords, 0) ) + printf( "Verification for function %d failed for %d minterm pairs.\n", f, + Abc_TtCountOnesVecMask(pTruth[0], pTruth[1], nTtWords, 0) ); + } + if ( Vec_IntSize(vSet) < 6 ) + Vec_WrdForEachEntry( vRes, Func, i ) + Vec_WrdWriteEntry( vRes, i, Abc_Tt6Stretch(Func, Vec_IntSize(vSet)) ); + Vec_WrdFree( vIn ); + Vec_WrdFree( vOut ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCountResub( Vec_Wrd_t * vTruths, int nVars, int fVerbose ) +{ + Vec_Int_t * vResub; int nNodes; + int nTtWords = Abc_Truth6WordNum(nVars); + int v, nFuncs = Vec_WrdSize(vTruths) / 2 / nTtWords; + Vec_Wrd_t * vElems = Vec_WrdStartTruthTables( nVars ); + Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2 + nVars ); + assert( Vec_WrdSize(vElems) == nTtWords * nVars ); + assert( nFuncs == 1 ); + Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+0)*nTtWords) ); + Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+1)*nTtWords) ); + for ( v = 0; v < nVars; v++ ) + Vec_PtrPush( vDivs, Vec_WrdEntryP(vElems, v*nTtWords) ); + vResub = Gia_ManResubOne( vDivs, nTtWords, 30, 100, 0, 0, 0, fVerbose, NULL, 0 ); + Vec_PtrFree( vDivs ); + Vec_WrdFree( vElems ); + nNodes = Vec_IntSize(vResub) ? Vec_IntSize(vResub)/2 : 999; + Vec_IntFree( vResub ); + return nNodes; +} +Vec_Int_t * Gia_ManDeriveResub( Vec_Wrd_t * vTruths, int nVars ) +{ + Vec_Int_t * vResub; + int nTtWords = Abc_Truth6WordNum(nVars); + int v, nFuncs = Vec_WrdSize(vTruths) / 2 / nTtWords; + Vec_Wrd_t * vElems = Vec_WrdStartTruthTables( nVars ); + Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2 + nVars ); + assert( Vec_WrdSize(vElems) == nTtWords * nVars ); + assert( nFuncs == 1 ); + Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+0)*nTtWords) ); + Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+1)*nTtWords) ); + for ( v = 0; v < nVars; v++ ) + Vec_PtrPush( vDivs, Vec_WrdEntryP(vElems, v*nTtWords) ); + vResub = Gia_ManResubOne( vDivs, nTtWords, 30, 100, 0, 0, 0, 0, NULL, 0 ); + Vec_PtrFree( vDivs ); + Vec_WrdFree( vElems ); + return vResub; +} + +int Gia_ManCountBidec( Vec_Wrd_t * vTruths, int nVars, int fVerbose ) +{ + int nNodes, nTtWords = Abc_Truth6WordNum(nVars); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + Abc_TtOr( pTruth[0], pTruth[0], pTruth[1], nTtWords ); + nNodes = Bdc_ManBidecNodeNum( pTruth[1], pTruth[0], nVars, fVerbose ); + Abc_TtSharp( pTruth[0], pTruth[0], pTruth[1], nTtWords ); + return nNodes; +} +Vec_Int_t * Gia_ManDeriveBidec( Vec_Wrd_t * vTruths, int nVars ) +{ + Vec_Int_t * vRes = NULL; + int nTtWords = Abc_Truth6WordNum(nVars); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + Abc_TtOr( pTruth[0], pTruth[0], pTruth[1], nTtWords ); + vRes = Bdc_ManBidecResub( pTruth[1], pTruth[0], nVars ); + Abc_TtSharp( pTruth[0], pTruth[0], pTruth[1], nTtWords ); + return vRes; +} + +int Gia_ManCountIsop( Vec_Wrd_t * vTruths, int nVars, int fVerbose ) +{ + int nTtWords = Abc_Truth6WordNum(nVars); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + int nNodes = Kit_IsopNodeNum( (unsigned *)pTruth[0], (unsigned *)pTruth[1], nVars, NULL ); + return nNodes; +} +Vec_Int_t * Gia_ManDeriveIsop( Vec_Wrd_t * vTruths, int nVars ) +{ + Vec_Int_t * vRes = NULL; + int nTtWords = Abc_Truth6WordNum(nVars); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + vRes = Kit_IsopResub( (unsigned *)pTruth[0], (unsigned *)pTruth[1], nVars, NULL ); + return vRes; +} + +int Gia_ManCountBdd( Vec_Wrd_t * vTruths, int nVars, int fVerbose ) +{ + extern Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords, int nRounds, int fVerbose ); + int nTtWords = Abc_Truth6WordNum(nVars); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + Gia_Man_t * pGia; int nNodes; + + Abc_TtOr( pTruth[1], pTruth[1], pTruth[0], nTtWords ); + Abc_TtNot( pTruth[0], nTtWords ); + pGia = Gia_TryPermOptNew( pTruth[0], nVars, 1, nTtWords, 50, 0 ); + Abc_TtNot( pTruth[0], nTtWords ); + Abc_TtSharp( pTruth[1], pTruth[1], pTruth[0], nTtWords ); + + nNodes = Gia_ManAndNum(pGia); + Gia_ManStop( pGia ); + return nNodes; +} +Vec_Int_t * Gia_ManDeriveBdd( Vec_Wrd_t * vTruths, int nVars ) +{ + extern Vec_Int_t * Gia_ManToGates( Gia_Man_t * p ); + Vec_Int_t * vRes = NULL; + extern Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords, int nRounds, int fVerbose ); + int nTtWords = Abc_Truth6WordNum(nVars); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + Gia_Man_t * pGia; + + Abc_TtOr( pTruth[1], pTruth[1], pTruth[0], nTtWords ); + Abc_TtNot( pTruth[0], nTtWords ); + pGia = Gia_TryPermOptNew( pTruth[0], nVars, 1, nTtWords, 50, 0 ); + Abc_TtNot( pTruth[0], nTtWords ); + Abc_TtSharp( pTruth[1], pTruth[1], pTruth[0], nTtWords ); + + vRes = Gia_ManToGates( pGia ); + Gia_ManStop( pGia ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManEvalSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int fVerbose ) +{ + Vec_Wrd_t * vTruths = Gia_ManDeriveTruths( p, vSims, vIsfs, vCands, vSet, nWords ); + int nTtWords = Vec_WrdSize(vTruths)/2, nVars = Vec_IntSize(vSet); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + int nNodesResub = Gia_ManCountResub( vTruths, nVars, 0 ); + int nNodesBidec = nVars > 2 ? Gia_ManCountBidec( vTruths, nVars, 0 ) : 999; + int nNodesIsop = nVars > 2 ? Gia_ManCountIsop( vTruths, nVars, 0 ) : 999; + int nNodesBdd = nVars > 2 ? Gia_ManCountBdd( vTruths, nVars, 0 ) : 999; + int nNodesMin = Abc_MinInt( Abc_MinInt(nNodesResub, nNodesBidec), Abc_MinInt(nNodesIsop, nNodesBdd) ); + if ( fVerbose ) + { + printf( "Size = %2d ", nVars ); + printf( "Resub =%3d ", nNodesResub ); + printf( "Bidec =%3d ", nNodesBidec ); + printf( "Isop =%3d ", nNodesIsop ); + printf( "Bdd =%3d ", nNodesBdd ); + Abc_TtIsfPrint( pTruth[0], pTruth[1], nTtWords ); + if ( nVars <= 6 ) + { + printf( " " ); + Extra_PrintHex( stdout, (unsigned*)pTruth[0], nVars ); + printf( " " ); + Extra_PrintHex( stdout, (unsigned*)pTruth[1], nVars ); + } + printf( "\n" ); + } + Vec_WrdFree( vTruths ); + if ( nNodesMin > 500 ) + return -1; + if ( nNodesMin == nNodesResub ) + return (nNodesMin << 2) | 0; + if ( nNodesMin == nNodesBidec ) + return (nNodesMin << 2) | 1; + if ( nNodesMin == nNodesIsop ) + return (nNodesMin << 2) | 2; + if ( nNodesMin == nNodesBdd ) + return (nNodesMin << 2) | 3; + return -1; +} +Vec_Int_t * Gia_ManDeriveSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int Type ) +{ + Vec_Int_t * vRes = NULL; + Vec_Wrd_t * vTruths = Gia_ManDeriveTruths( p, vSims, vIsfs, vCands, vSet, nWords ); + int nTtWords = Vec_WrdSize(vTruths)/2, nVars = Vec_IntSize(vSet); + word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords), + Vec_WrdEntryP(vTruths, 1*nTtWords) }; + if ( Type == 0 ) + vRes = Gia_ManDeriveResub( vTruths, nVars ); + else if ( Type == 1 ) + vRes = Gia_ManDeriveBidec( vTruths, nVars ); + else if ( Type == 2 ) + vRes = Gia_ManDeriveIsop( vTruths, nVars ); + else if ( Type == 3 ) + vRes = Gia_ManDeriveBdd( vTruths, nVars ); + if ( vRes && Gia_ResubVarNum(vRes) <= 6 ) + { + word Func = Gia_ResubToTruth6( vRes ); + assert( !(Func & pTruth[0][0]) ); + assert( !(pTruth[1][0] & ~Func) ); + } + Vec_WrdFree( vTruths ); + return vRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 772dc31a..464835e4 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -94,6 +94,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vStore ); Vec_IntFreeP( &p->vClassNew ); Vec_IntFreeP( &p->vClassOld ); + Vec_IntFreeP( &p->vPats ); Vec_WrdFreeP( &p->vSims ); Vec_WrdFreeP( &p->vSimsT ); Vec_WrdFreeP( &p->vSimsPi ); diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index a5017b7d..33fd5276 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -651,6 +651,37 @@ Gia_Man_t * Gia_ManConstructFromGates2( Vec_Wec_t * vFuncs, Vec_Wec_t * vDivs, i Vec_IntFree( vSupp ); return pNew; } +Vec_Int_t * Gia_ManToGates( Gia_Man_t * p ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 2*Gia_ManAndNum(p) + 1 ); + Gia_Obj_t * pRoot = Gia_ManCo( p, 0 ); + int iRoot = Gia_ObjFaninId0p(p, pRoot) - 1; + int nVars = Gia_ManCiNum(p); + assert( Gia_ManCoNum(p) == 1 ); + if ( iRoot == -1 ) + Vec_IntPush( vRes, Gia_ObjFaninC0(pRoot) ); + else if ( iRoot < nVars ) + Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) ); + else + { + Gia_Obj_t * pObj, * pLast = NULL; int i; + Gia_ManForEachCi( p, pObj, i ) + assert( Gia_ObjId(p, pObj) == i+1 ); + Gia_ManForEachAnd( p, pObj, i ) + { + int iLit0 = Abc_Var2Lit( Gia_ObjFaninId0(pObj, i) - 1, Gia_ObjFaninC0(pObj) ); + int iLit1 = Abc_Var2Lit( Gia_ObjFaninId1(pObj, i) - 1, Gia_ObjFaninC1(pObj) ); + if ( iLit0 > iLit1 ) + iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1; + Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 ); + pLast = pObj; + } + assert( pLast == Gia_ObjFanin0(pRoot) ); + Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Gia_ObjFaninC0(pRoot)) ); + } + assert( Vec_IntSize(vRes) == 2*Gia_ManAndNum(p) + 1 ); + return vRes; +} /**Function************************************************************* @@ -1378,7 +1409,10 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit, int Depth ) if ( iResLit >= 0 ) { int iNode = nVars + Vec_IntSize(p->vGates)/2; - Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); + if ( iDiv < iResLit ) + Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); + else + Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_LitNot(iDiv) ); return Abc_Var2Lit( iNode, fUseOr ); } } diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c new file mode 100644 index 00000000..f95d815d --- /dev/null +++ b/src/aig/gia/giaSupps.c @@ -0,0 +1,817 @@ +/**CFile**************************************************************** + + FileName [giaSupp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Support computation manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig/gia/gia.h" +#include "base/main/mainInt.h" +#include "misc/util/utilTruth.h" +#include "misc/extra/extra.h" +#include "misc/vec/vecHsh.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Supp_Man_t_ Supp_Man_t; +struct Supp_Man_t_ +{ + // user data + int nIters; // optimization rounds + int nRounds; // optimization rounds + int nWords; // the number of simulation words + int nDivWords; // the number of divisor words + Vec_Wrd_t * vIsfs; // functions to synthesize + Vec_Int_t * vCands; // candidate divisors + Vec_Int_t * vWeights; // divisor weights (optional) + Vec_Wrd_t * vSims; // simulation values + Vec_Wrd_t * vSimsC; // simulation values + Gia_Man_t * pGia; // used for object names + // computed data + Vec_Wrd_t * vDivs[2]; // simulation values + Vec_Wrd_t * vPats[2]; // simulation values + Vec_Ptr_t * vMatrix; // simulation values + Vec_Wrd_t * vMask; // simulation values + Vec_Wrd_t * vRowTemp; // simulation values + Vec_Int_t * vCosts; // candidate costs + Hsh_VecMan_t * pHash; // subsets considered + Vec_Wrd_t * vSFuncs; // ISF storage + Vec_Int_t * vSStarts; // subset function starts + Vec_Int_t * vSCount; // subset function count + Vec_Int_t * vSPairs; // subset pair count + Vec_Int_t * vTemp; // temporary + Vec_Int_t * vTempSets; // temporary + Vec_Int_t * vTempPairs; // temporary + Vec_Wec_t * vSolutions; // solutions for each node count +}; + +extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Supp_ManFuncInit( Vec_Wrd_t * vFuncs, int nWords ) +{ + int i, k = 0, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2; + assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) ); + for ( i = 0; i < nFuncs; i++ ) + { + word * pFunc0 = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords); + word * pFunc1 = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords); + if ( Abc_TtIsConst0(pFunc0, nWords) || Abc_TtIsConst0(pFunc1, nWords) ) + continue; + if ( k < i ) Abc_TtCopy( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), pFunc0, nWords, 0 ); + if ( k < i ) Abc_TtCopy( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), pFunc1, nWords, 0 ); + k++; + } + Vec_WrdShrink( vFuncs, 2*k*nWords ); + return k; +} +int Supp_ManCostInit( Vec_Wrd_t * vFuncs, int nWords ) +{ + int Res = 0, i, nFuncs = Vec_WrdSize(vFuncs) / nWords / 2; + assert( 2 * nFuncs * nWords == Vec_WrdSize(vFuncs) ); + for ( i = 0; i < nFuncs; i++ ) + { + word * pFunc0 = Vec_WrdEntryP(vFuncs, (2*i+0)*nWords); + word * pFunc1 = Vec_WrdEntryP(vFuncs, (2*i+1)*nWords); + Res += Abc_TtCountOnesVec(pFunc0, nWords) * Abc_TtCountOnesVec(pFunc1, nWords); + } + assert( nFuncs < 128 ); + assert( Res < (1 << 24) ); + return (nFuncs << 24) | Res; +} +void Supp_ManInit( Supp_Man_t * p ) +{ + int Value, nFuncs, iSet = Hsh_VecManAdd( p->pHash, p->vTemp ); // empty set + assert( iSet == 0 ); + Vec_IntPush( p->vSStarts, Vec_WrdSize(p->vSFuncs) ); + Vec_WrdAppend( p->vSFuncs, p->vIsfs ); + nFuncs = Supp_ManFuncInit( p->vSFuncs, p->nWords ); + assert( Vec_WrdSize(p->vSFuncs) == 2 * nFuncs * p->nWords ); + Value = Supp_ManCostInit(p->vSFuncs, p->nWords); + Vec_IntPush( p->vSCount, Value >> 24 ); + Vec_IntPush( p->vSPairs, Value & 0xFFFFFF ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Supp_DeriveLines( Supp_Man_t * p ) +{ + int n, i, iObj, nWords = p->nWords; + int nDivWords = Abc_Bit6WordNum( Vec_IntSize(p->vCands) ); + for ( n = 0; n < 2; n++ ) + { + p->vDivs[n] = Vec_WrdStart( 64*nWords*nDivWords ); + p->vPats[n] = Vec_WrdStart( 64*nWords*nDivWords ); + if ( p->vSimsC ) + Vec_IntForEachEntry( p->vCands, iObj, i ) + Abc_TtAndSharp( Vec_WrdEntryP(p->vDivs[n], i*nWords), Vec_WrdEntryP(p->vSimsC, iObj*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n ); + else + Vec_IntForEachEntry( p->vCands, iObj, i ) + Abc_TtCopy( Vec_WrdEntryP(p->vDivs[n], i*nWords), Vec_WrdEntryP(p->vSims, iObj*nWords), nWords, !n ); + Extra_BitMatrixTransposeP( p->vDivs[n], nWords, p->vPats[n], nDivWords ); + } + return nDivWords; +} +Supp_Man_t * Supp_ManCreate( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vWeights, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsC, int nWords, Gia_Man_t * pGia, int nIters, int nRounds ) +{ + Supp_Man_t * p = ABC_CALLOC( Supp_Man_t, 1 ); + p->nIters = nIters; + p->nRounds = nRounds; + p->nWords = nWords; + p->vIsfs = vIsfs; + p->vCands = vCands; + p->vWeights = vWeights; + p->vSims = vSims; + p->vSimsC = vSimsC; + p->pGia = pGia; + // computed data + p->nDivWords = Supp_DeriveLines( p ); + p->vMatrix = Vec_PtrAlloc( 100 ); + p->vMask = Vec_WrdAlloc( 100 ); + p->vRowTemp = Vec_WrdStart( 64*p->nDivWords ); + p->vCosts = Vec_IntStart( Vec_IntSize(p->vCands) ); + p->pHash = Hsh_VecManStart( 1000 ); + p->vSFuncs = Vec_WrdAlloc( 1000 ); + p->vSStarts = Vec_IntAlloc( 1000 ); + p->vSCount = Vec_IntAlloc( 1000 ); + p->vSPairs = Vec_IntAlloc( 1000 ); + p->vSolutions = Vec_WecStart( 16 ); + p->vTemp = Vec_IntAlloc( 10 ); + p->vTempSets = Vec_IntAlloc( 10 ); + p->vTempPairs = Vec_IntAlloc( 10 ); + Supp_ManInit( p ); + return p; +} +void Supp_ManCleanMatrix( Supp_Man_t * p ) +{ + Vec_Wrd_t * vTemp; int i; + Vec_PtrForEachEntry( Vec_Wrd_t *, p->vMatrix, vTemp, i ) + Vec_WrdFreeP( &vTemp ); + Vec_PtrClear( p->vMatrix ); +} +void Supp_ManDelete( Supp_Man_t * p ) +{ + Supp_ManCleanMatrix( p ); + Vec_WrdFreeP( &p->vDivs[0] ); + Vec_WrdFreeP( &p->vDivs[1] ); + Vec_WrdFreeP( &p->vPats[0] ); + Vec_WrdFreeP( &p->vPats[1] ); + Vec_PtrFreeP( &p->vMatrix ); + Vec_WrdFreeP( &p->vMask ); + Vec_WrdFreeP( &p->vRowTemp ); + Vec_IntFreeP( &p->vCosts ); + Hsh_VecManStop( p->pHash ); + Vec_WrdFreeP( &p->vSFuncs ); + Vec_IntFreeP( &p->vSStarts ); + Vec_IntFreeP( &p->vSCount ); + Vec_IntFreeP( &p->vSPairs ); + Vec_WecFreeP( &p->vSolutions ); + Vec_IntFreeP( &p->vTemp ); + Vec_IntFreeP( &p->vTempSets ); + Vec_IntFreeP( &p->vTempPairs ); + ABC_FREE( p ); +} +int Supp_ManMemory( Supp_Man_t * p ) +{ + int nMem = sizeof(Supp_Man_t); + nMem += 2*(int)Vec_WrdMemory( p->vDivs[0] ); + nMem += 2*(int)Vec_WrdMemory( p->vPats[0] ); + nMem += (Vec_PtrSize(p->vMatrix)+1)*(int)Vec_WrdMemory( p->vRowTemp ); + nMem += (int)Vec_WrdMemory( p->vMask ); + nMem += (int)Vec_IntMemory( p->vCosts ); + nMem += (int)Hsh_VecManMemory( p->pHash ); + nMem += (int)Vec_WrdMemory( p->vSFuncs ); + nMem += (int)Vec_IntMemory( p->vSStarts ); + nMem += (int)Vec_IntMemory( p->vSCount ); + nMem += (int)Vec_IntMemory( p->vSPairs ); + nMem += (int)Vec_WecMemory( p->vSolutions ); + nMem += (int)Vec_IntMemory( p->vTemp ); + nMem += (int)Vec_IntMemory( p->vTempSets ); + nMem += (int)Vec_IntMemory( p->vTempPairs ); + return nMem; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Supp_ArrayWeight( Vec_Int_t * vRes, Vec_Int_t * vWeights ) +{ + int i, iObj, Cost = 0; + if ( !vWeights ) + return Vec_IntSize(vRes); + Vec_IntForEachEntry( vRes, iObj, i ) + Cost += Vec_IntEntry(vWeights, iObj); + return Cost; +} +int Supp_SetWeight( Supp_Man_t * p, int iSet ) +{ + return Supp_ArrayWeight( Hsh_VecReadEntry(p->pHash, iSet), p->vWeights ); +} +int Supp_SetSize( Supp_Man_t * p, int iSet ) +{ + return Vec_IntSize( Hsh_VecReadEntry(p->pHash, iSet) ); +} +int Supp_SetFuncNum( Supp_Man_t * p, int iSet ) +{ + return Vec_IntEntry(p->vSCount, iSet); +} +int Supp_SetPairNum( Supp_Man_t * p, int iSet ) +{ + return Vec_IntEntry(p->vSPairs, iSet); +} +void Supp_SetConvert( Vec_Int_t * vSet, Vec_Int_t * vCands ) +{ + int i, iObj; + Vec_IntForEachEntry( vSet, iObj, i ) + Vec_IntWriteEntry( vSet, i, Vec_IntEntry(vCands, iObj) ); +} +void Supp_PrintNodes( Gia_Man_t * pGia, Vec_Int_t * vObjs, int Skip, int Limit ) +{ + int i, iObj; + //printf( "Considering %d targets: ", Vec_IntSize(vObjs) ); + Vec_IntForEachEntryStart( vObjs, iObj, i, Skip ) + { + if ( iObj < 0 ) + continue; + printf( "(%d)", iObj ); + if ( pGia && pGia->vWeights && Vec_IntEntry(pGia->vWeights, iObj) > 0 ) + printf( "(%d)", Vec_IntEntry(pGia->vWeights, iObj) ); + if ( pGia ) + printf( " %s ", Gia_ObjName(pGia, iObj)+2 ); + else + printf( " n%d ", iObj ); + if ( i >= Limit ) + { + printf( "... " ); + break; + } + } + printf( "Cost = %d", Supp_ArrayWeight(vObjs, pGia ? pGia->vWeights : NULL) ); + printf( "\n" ); +} +void Supp_PrintOne( Supp_Man_t * p, int iSet ) +{ + Vec_Int_t * vSet = Hsh_VecReadEntry(p->pHash, iSet); + printf( "Set %5d : ", iSet ); + printf( "Funcs %2d ", Supp_SetFuncNum(p, iSet) ); + printf( "Pairs %4d ", Supp_SetPairNum(p, iSet) ); + printf( "Start %8d ", Vec_IntEntry(p->vSStarts, iSet) ); + printf( "Weight %4d ", Supp_ArrayWeight(vSet, p->vWeights) ); + Vec_IntClearAppend( p->vTemp, vSet ); + Supp_SetConvert( p->vTemp, p->vCands ); + Supp_PrintNodes( p->pGia, p->vTemp, 0, 6 ); +} +int Supp_ManRefine1( Supp_Man_t * p, int iSet, int iObj ) +{ + word * pSet = Vec_WrdEntryP( p->vSims, Vec_IntEntry(p->vCands, iObj)*p->nWords ); + word * pIsf; int nFuncs = Vec_IntEntry(p->vSCount, iSet); + int i, n, f, w, nFuncsNew = 0, Mark = Vec_WrdSize(p->vSFuncs), Res = 0; + if ( Vec_WrdSize(p->vSFuncs) + 4*nFuncs*p->nWords > Vec_WrdCap(p->vSFuncs) ) + Vec_WrdGrow( p->vSFuncs, 2*Vec_WrdCap(p->vSFuncs) ); + pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) ); + for ( i = 0; i < nFuncs; i++ ) + { + word * pFunc[2] = { pIsf + (2*i+0)*p->nWords, pIsf + (2*i+1)*p->nWords }; + for ( f = 0; f < 2; f++ ) + { + int nOnes[2], Start = Vec_WrdSize(p->vSFuncs); + for ( n = 0; n < 2; n++ ) + { + word * pLimit = Vec_WrdLimit(p->vSFuncs); + if ( f ) + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[n][w] & pSet[w] ); + else + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[n][w] & ~pSet[w] ); + nOnes[n] = Abc_TtCountOnesVec( pLimit, p->nWords ); + } + if ( nOnes[0] && nOnes[1] ) + Res += nOnes[0] * nOnes[1]; + else + Vec_WrdShrink( p->vSFuncs, Start ); + } + } + assert( Res < (1 << 24) ); + nFuncsNew = (Vec_WrdSize(p->vSFuncs) - Mark)/2/p->nWords; + assert( nFuncsNew < 128 ); + assert( nFuncsNew >= 0 && nFuncsNew <= 2*nFuncs ); + return (nFuncsNew << 24) | Res; +} +void Supp_ManRefine( Supp_Man_t * p, int iSet, int iObj, int * pnFuncs, int * pnPairs ) +{ + word * pDivs0 = Vec_WrdEntryP( p->vDivs[0], iObj*p->nWords ); + word * pDivs1 = Vec_WrdEntryP( p->vDivs[1], iObj*p->nWords ); + word * pIsf; int nFuncs = Supp_SetFuncNum(p, iSet); + int i, f, w, nFuncsNew = 0, Mark = Vec_WrdSize(p->vSFuncs), Res = 0; + if ( Vec_WrdSize(p->vSFuncs) + 6*nFuncs*p->nWords > Vec_WrdCap(p->vSFuncs) ) + Vec_WrdGrow( p->vSFuncs, 2*Vec_WrdCap(p->vSFuncs) ); + if ( Vec_WrdSize(p->vSFuncs) == Vec_IntEntry(p->vSStarts, iSet) ) + pIsf = Vec_WrdLimit( p->vSFuncs ); + else + pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) ); + for ( i = 0; i < nFuncs; i++ ) + { + word * pFunc[2] = { pIsf + (2*i+0)*p->nWords, pIsf + (2*i+1)*p->nWords }; + for ( f = 0; f < 3; f++ ) + { + int nOnes[2], Start = Vec_WrdSize(p->vSFuncs); + word * pLimit[2] = { Vec_WrdLimit(p->vSFuncs), Vec_WrdLimit(p->vSFuncs) + p->nWords }; + if ( f == 0 ) + { + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[0][w] & pDivs0[w] ); + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[1][w] & ~pDivs1[w] ); + } + else if ( f == 1 ) + { + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[0][w] & pDivs1[w] ); + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[1][w] & ~pDivs0[w] ); + } + else + { + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[0][w] & ~pDivs0[w] & ~pDivs1[w] ); + for ( w = 0; w < p->nWords; w++ ) + Vec_WrdPush( p->vSFuncs, pFunc[1][w] ); + } + nOnes[0] = Abc_TtCountOnesVec( pLimit[0], p->nWords ); + nOnes[1] = Abc_TtCountOnesVec( pLimit[1], p->nWords ); + if ( nOnes[0] && nOnes[1] ) + Res += nOnes[0] * nOnes[1]; + else + Vec_WrdShrink( p->vSFuncs, Start ); + } + } + assert( Res < (1 << 24) ); + nFuncsNew = (Vec_WrdSize(p->vSFuncs) - Mark)/2/p->nWords; + *pnFuncs = nFuncsNew; + *pnPairs = Res; +} +int Supp_ManSubsetAdd( Supp_Man_t * p, int iSet, int iObj, int fVerbose ) +{ + int iSetNew, nEntries = Hsh_VecSize( p->pHash ); + Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSet ); + Vec_IntClear( p->vTemp ); + Vec_IntAppend( p->vTemp, vSet ); + Vec_IntPushOrder( p->vTemp, iObj ); + assert( Vec_IntIsOrdered(p->vTemp, 0) ); + iSetNew = Hsh_VecManAdd( p->pHash, p->vTemp ); + if ( iSetNew == nEntries ) // new entry + { + int nFuncs, nPairs; + Vec_IntPush( p->vSStarts, Vec_WrdSize(p->vSFuncs) ); + Supp_ManRefine( p, iSet, iObj, &nFuncs, &nPairs ); + Vec_IntPush( p->vSCount, nFuncs ); + Vec_IntPush( p->vSPairs, nPairs ); + assert( Hsh_VecSize(p->pHash) == Vec_IntSize(p->vSStarts) ); + assert( Hsh_VecSize(p->pHash) == Vec_IntSize(p->vSCount) ); + assert( Hsh_VecSize(p->pHash) == Vec_IntSize(p->vSPairs) ); + if ( Supp_SetFuncNum(p, iSetNew) == 0 && Supp_SetSize(p, iSetNew) < Vec_WecSize(p->vSolutions) ) + Vec_WecPush( p->vSolutions, Supp_SetSize(p, iSetNew), iSetNew ); + if ( fVerbose ) + Supp_PrintOne( p, iSetNew ); + } + return iSetNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Supp_ComputePair1( Supp_Man_t * p, int iSet ) +{ + int Random = 0xFFFFFF & Abc_Random(0); + int nFuncs = Vec_IntEntry(p->vSCount, iSet); + int iFunc = Random % nFuncs; + word * pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) ); + word * pFunc[2] = { pIsf + (2*iFunc+0)*p->nWords, pIsf + (2*iFunc+1)*p->nWords }; + int iBit0 = ((Random >> 16) & 1) ? Abc_TtFindFirstBit2(pFunc[0], p->nWords) : Abc_TtFindLastBit2(pFunc[0], p->nWords); + int iBit1 = ((Random >> 17) & 1) ? Abc_TtFindFirstBit2(pFunc[1], p->nWords) : Abc_TtFindLastBit2(pFunc[1], p->nWords); + if ( 1 ) + { + Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSet ); int i, iObj; + Vec_IntForEachEntry( vSet, iObj, i ) + { + word * pSet = Vec_WrdEntryP( p->vSims, Vec_IntEntry(p->vCands, iObj)*p->nWords ); + assert( Abc_TtGetBit(pSet, iBit0) == Abc_TtGetBit(pSet, iBit1) ); + } + } + return (iBit0 << 16) | iBit1; +} +int Supp_ComputePair( Supp_Man_t * p, int iSet ) +{ + int Random = 0xFFFFFF & Abc_Random(0); + int nFuncs = Vec_IntEntry(p->vSCount, iSet); + int iFunc = Random % nFuncs; + word * pIsf = Vec_WrdEntryP( p->vSFuncs, Vec_IntEntry(p->vSStarts, iSet) ); + word * pFunc[2] = { pIsf + (2*iFunc+0)*p->nWords, pIsf + (2*iFunc+1)*p->nWords }; + int iBit0 = ((Random >> 16) & 1) ? Abc_TtFindFirstBit2(pFunc[0], p->nWords) : Abc_TtFindLastBit2(pFunc[0], p->nWords); + int iBit1 = ((Random >> 17) & 1) ? Abc_TtFindFirstBit2(pFunc[1], p->nWords) : Abc_TtFindLastBit2(pFunc[1], p->nWords); + if ( 1 ) + { + Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSet ); int i, iObj; + Vec_IntForEachEntry( vSet, iObj, i ) + { + word * pSet0 = Vec_WrdEntryP( p->vDivs[0], iObj*p->nWords ); + word * pSet1 = Vec_WrdEntryP( p->vDivs[1], iObj*p->nWords ); + int Value00 = Abc_TtGetBit(pSet0, iBit0); + int Value01 = Abc_TtGetBit(pSet0, iBit1); + int Value10 = Abc_TtGetBit(pSet1, iBit0); + int Value11 = Abc_TtGetBit(pSet1, iBit1); + assert( !Value00 || !Value11 ); + assert( !Value01 || !Value10 ); + } + } + return (iBit0 << 16) | iBit1; +} +Vec_Int_t * Supp_Compute64Pairs( Supp_Man_t * p, Vec_Int_t * vSets ) +{ + int i; + Vec_IntClear( p->vTempPairs ); + for ( i = 0; i < 64; i++ ) + { + int Rand = 0xFFFFFF & Abc_Random(0); + int iSet = Vec_IntEntry( vSets, Rand % Vec_IntSize(vSets) ); + Vec_IntPush( p->vTempPairs, Supp_ComputePair(p, iSet) ); + } + return p->vTempPairs; +} +void Supp_ManFillBlock( Supp_Man_t * p, Vec_Int_t * vPairs, Vec_Wrd_t * vRes ) +{ + int i, Pair; + assert( Vec_IntSize(vPairs) == 64 ); + Vec_IntForEachEntry( vPairs, Pair, i ) + { + int iBit0 = Pair >> 16, iBit1 = Pair & 0xFFFF; + word * pPat00 = Vec_WrdEntryP(p->vPats[0], iBit0*p->nDivWords); + word * pPat01 = Vec_WrdEntryP(p->vPats[0], iBit1*p->nDivWords); + word * pPat10 = Vec_WrdEntryP(p->vPats[1], iBit0*p->nDivWords); + word * pPat11 = Vec_WrdEntryP(p->vPats[1], iBit1*p->nDivWords); + word * pPat = Vec_WrdEntryP(p->vRowTemp, i*p->nDivWords); + Abc_TtAnd( pPat, pPat00, pPat11, p->nDivWords, 0 ); + Abc_TtOrAnd( pPat, pPat01, pPat10, p->nDivWords ); + } + Extra_BitMatrixTransposeP( p->vRowTemp, p->nDivWords, vRes, 1 ); +} +void Supp_ManAddPatterns( Supp_Man_t * p, Vec_Int_t * vSets ) +{ + Vec_Int_t * vPairs = Supp_Compute64Pairs( p, vSets ); + Vec_Wrd_t * vRow = Vec_WrdStart( 64*p->nDivWords ); + Supp_ManFillBlock( p, vPairs, vRow ); + Vec_PtrPush( p->vMatrix, vRow ); +} +Vec_Int_t * Supp_ManCollectOnes( word * pSim, int nWords ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); int i; + for ( i = 0; i < 64*nWords; i++ ) + if ( Abc_TtGetBit(pSim, i) ) + Vec_IntPush( vRes, i ); + return vRes; +} +Vec_Int_t * Supp_Compute64PairsFunc( Supp_Man_t * p, Vec_Int_t * vBits0, Vec_Int_t * vBits1 ) +{ + int i; + Vec_IntClear( p->vTempPairs ); + for ( i = 0; i < 64; i++ ) + { + int Random = 0xFFFFFF & Abc_Random(0); + int iBit0 = Vec_IntEntry( vBits0, (Random & 0xFFF) % Vec_IntSize(vBits0) ); + int iBit1 = Vec_IntEntry( vBits1, (Random >> 12) % Vec_IntSize(vBits1) ); + Vec_IntPush( p->vTempPairs, (iBit0 << 16) | iBit1 ); + } + return p->vTempPairs; +} +void Supp_ManAddPatternsFunc( Supp_Man_t * p, int nBatches ) +{ + int b; + Vec_Int_t * vBits0 = Supp_ManCollectOnes( Vec_WrdEntryP(p->vSFuncs, 0*p->nWords), p->nWords ); + Vec_Int_t * vBits1 = Supp_ManCollectOnes( Vec_WrdEntryP(p->vSFuncs, 1*p->nWords), p->nWords ); + for ( b = 0; b < nBatches; b++ ) + { + Vec_Int_t * vPairs = Supp_Compute64PairsFunc( p, vBits0, vBits1 ); + Vec_Wrd_t * vRow = Vec_WrdStart( 64*p->nDivWords ); + Supp_ManFillBlock( p, vPairs, vRow ); + Vec_PtrPush( p->vMatrix, vRow ); + } + Vec_IntFree( vBits0 ); + Vec_IntFree( vBits1 ); +} +int Supp_FindNextDiv( Supp_Man_t * p, int Pair ) +{ + int iDiv, iBit0 = Pair >> 16, iBit1 = Pair & 0xFFFF; + word * pPat00 = Vec_WrdEntryP(p->vPats[0], iBit0*p->nDivWords); + word * pPat01 = Vec_WrdEntryP(p->vPats[0], iBit1*p->nDivWords); + word * pPat10 = Vec_WrdEntryP(p->vPats[1], iBit0*p->nDivWords); + word * pPat11 = Vec_WrdEntryP(p->vPats[1], iBit1*p->nDivWords); + int iDiv1 = Abc_TtFindFirstAndBit2( pPat00, pPat11, p->nDivWords ); + int iDiv2 = Abc_TtFindFirstAndBit2( pPat01, pPat10, p->nDivWords ); + iDiv1 = iDiv1 == -1 ? ABC_INFINITY : iDiv1; + iDiv2 = iDiv2 == -1 ? ABC_INFINITY : iDiv2; + iDiv = Abc_MinInt( iDiv1, iDiv2 ); + assert( iDiv >= 0 && iDiv < Vec_IntSize(p->vCands) ); + return iDiv; +} +int Supp_ManRandomSolution( Supp_Man_t * p, int iSet, int fVerbose ) +{ + Vec_IntClear( p->vTempSets ); + while ( Supp_SetFuncNum(p, iSet) > 0 ) + { + int Pair = Supp_ComputePair( p, iSet ); + int iDiv = Supp_FindNextDiv( p, Pair ); + iSet = Supp_ManSubsetAdd( p, iSet, iDiv, fVerbose ); + if ( Supp_SetFuncNum(p, iSet) > 0 ) + Vec_IntPush( p->vTempSets, iSet ); + } + if ( Vec_IntSize(p->vTempSets) < 2 ) + return iSet; + Supp_ManAddPatterns( p, p->vTempSets ); + return iSet; +} +int Supp_ManSubsetRemove( Supp_Man_t * p, int iSet, int iPos ) +{ + int i, iSetNew = 0, nSize = Supp_SetSize(p, iSet); + for ( i = 0; i < nSize; i++ ) + if ( i != iPos && Supp_SetFuncNum(p, iSetNew) > 0 ) + iSetNew = Supp_ManSubsetAdd( p, iSetNew, Vec_IntEntry(Hsh_VecReadEntry(p->pHash, iSet), i), 0 ); + return iSetNew; +} +int Supp_ManMinimize( Supp_Man_t * p, int iSet0, int r, int fVerbose ) +{ + int i, nSize = Supp_SetSize(p, iSet0); + Vec_Int_t * vPerm = Vec_IntStartNatural( Supp_SetSize(p, iSet0) ); + Vec_IntRandomizeOrder( vPerm ); + Vec_IntClear( p->vTempSets ); + if ( fVerbose ) + printf( "Removing items from %d:\n", iSet0 ); + // make sure we first try to remove items with higher weight + for ( i = 0; i < nSize; i++ ) + { + int Index = Vec_IntEntry( vPerm, i ); + int iSet = Supp_ManSubsetRemove( p, iSet0, Index ); + if ( fVerbose ) + printf( "Item %2d : ", Index ); + if ( fVerbose ) + Supp_PrintOne( p, iSet ); + if ( Supp_SetFuncNum(p, iSet) == 0 ) + { + Vec_IntFree( vPerm ); + return Supp_ManMinimize( p, iSet, r, fVerbose ); + } + Vec_IntPush( p->vTempSets, iSet ); + } + Supp_ManAddPatterns( p, p->vTempSets ); + Vec_IntFree( vPerm ); + return iSet0; +} +int Supp_ManFindNextObj( Supp_Man_t * p, int fVerbose ) +{ + Vec_Wrd_t * vTemp; int r, k, iDiv; + word Sim, * pMask = Vec_WrdArray(p->vMask); + assert( Vec_WrdSize(p->vMask) == Vec_PtrSize(p->vMatrix) ); + Vec_IntFill( p->vCosts, Vec_IntSize(p->vCosts), 0 ); + Vec_PtrForEachEntry( Vec_Wrd_t *, p->vMatrix, vTemp, r ) + Vec_WrdForEachEntryStop( vTemp, Sim, k, Vec_IntSize(p->vCosts) ) + Vec_IntAddToEntry( p->vCosts, k, Abc_TtCountOnes(Sim & pMask[r]) ); + iDiv = Vec_IntArgMax( p->vCosts ); + if ( fVerbose ) + printf( "Choosing divisor %d with weight %d.\n", iDiv, Vec_IntEntry(p->vCosts, iDiv) ); + Vec_PtrForEachEntry( Vec_Wrd_t *, p->vMatrix, vTemp, r ) + pMask[r] &= ~Vec_WrdEntry( vTemp, iDiv ); + return iDiv; +} +int Supp_ManReconstruct( Supp_Man_t * p, int fVerbose ) +{ + int iSet = 0; + Vec_WrdFill( p->vMask, Vec_PtrSize(p->vMatrix), ~(word)0 ); + if ( fVerbose ) + printf( "\nBuilding a new set:\n" ); + while ( Supp_SetPairNum(p, iSet) ) + { + int iDiv = Supp_ManFindNextObj( p, fVerbose ); + iSet = Supp_ManSubsetAdd( p, iSet, iDiv, fVerbose ); + if ( Abc_TtIsConst0(Vec_WrdArray(p->vMask), Vec_WrdSize(p->vMask)) ) + break; + } + if ( fVerbose ) + printf( "Adding random part:\n" ); + return Supp_ManRandomSolution( p, iSet, fVerbose ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Supp_ManFindBestSolution( Supp_Man_t * p, Vec_Wec_t * vSols, int fVerbose, Vec_Int_t ** pvDivs ) +{ + Vec_Int_t * vLevel, * vRes = NULL; + int i, k, iSet, nFuncs = 0, Count = 0; + int iSolBest = -1, Cost, CostBest = ABC_INFINITY; + Vec_WecForEachLevel( vSols, vLevel, i ) + { + Count += Vec_IntSize(vLevel) > 0; + Vec_IntForEachEntry( vLevel, iSet, k ) + { + if ( fVerbose ) + printf( "%3d : ", nFuncs++ ); + Cost = Gia_ManEvalSolutionOne( p->pGia, p->vSims, p->vIsfs, p->vCands, Hsh_VecReadEntry(p->pHash, iSet), p->nWords, fVerbose ); + if ( Cost == -1 ) + continue; + if ( CostBest > Cost ) + { + CostBest = Cost; + iSolBest = iSet; + } + if ( nFuncs > 5 ) + break; + } + if ( Count == 2 || k < Vec_IntSize(vLevel) ) + break; + } + if ( iSolBest > 0 && (CostBest >> 2) < 50 ) + { + Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSolBest ); int i, iObj; + vRes = Gia_ManDeriveSolutionOne( p->pGia, p->vSims, p->vIsfs, p->vCands, vSet, p->nWords, CostBest & 3 ); + assert( !vRes || Vec_IntSize(vRes) == 2*(CostBest >> 2)+1 ); + if ( vRes && pvDivs ) + { + Vec_IntClear( *pvDivs ); + Vec_IntPushTwo( *pvDivs, -1, -1 ); + Vec_IntForEachEntry( vSet, iObj, i ) + Vec_IntPush( *pvDivs, Vec_IntEntry(p->vCands, iObj) ); + } + } + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Supp_FindGivenOne( Supp_Man_t * p ) +{ + int i, iObj, iSet = 0; + Vec_Int_t * vSet = Vec_IntStart( 2 ); + //extern void Patch_GenerateSet11( Gia_Man_t * p, Vec_Int_t * vDivs, Vec_Int_t * vCands ); + //Patch_GenerateSet11( p->pGia, vSet, p->vCands ); + Vec_IntDrop( vSet, 0 ); + Vec_IntDrop( vSet, 0 ); + Vec_IntForEachEntry( vSet, iObj, i ) + iSet = Supp_ManSubsetAdd( p, iSet, iObj, 1 ); + Vec_IntFree( vSet ); + return iSet; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vWeights, Vec_Wrd_t * vSims, Vec_Wrd_t * vSimsC, int nWords, Gia_Man_t * pGia, Vec_Int_t ** pvDivs, int nIters, int nRounds, int fVerbose ) +{ + int fVeryVerbose = 0; + int i, r, iSet, iBest = -1; + abctime clk = Abc_Clock(); + Vec_Int_t * vRes = NULL; + Supp_Man_t * p = Supp_ManCreate( vIsfs, vCands, vWeights, vSims, vSimsC, nWords, pGia, nIters, nRounds ); + if ( Supp_SetFuncNum(p, 0) == 0 ) + { + Supp_ManDelete( p ); + Vec_IntClear( *pvDivs ); + Vec_IntPushTwo( *pvDivs, -1, -1 ); + vRes = Vec_IntAlloc( 1 ); + Vec_IntPush( vRes, Abc_TtIsConst0(Vec_WrdArray(vIsfs), nWords) ); + return vRes; + } + if ( fVerbose ) + printf( "\nUsing %d divisors with %d words. Problem has %d functions and %d minterm pairs.\n", + Vec_IntSize(p->vCands), p->nWords, Supp_SetFuncNum(p, 0), Supp_SetPairNum(p, 0) ); + //iBest = Supp_FindGivenOne( p ); + if ( iBest == -1 ) + for ( i = 0; i < p->nIters; i++ ) + { + Supp_ManAddPatternsFunc( p, i ); + iSet = Supp_ManRandomSolution( p, 0, fVeryVerbose ); + for ( r = 0; r < p->nRounds; r++ ) + { + if ( fVeryVerbose ) + printf( "\n\nITER %d ROUND %d\n", i, r ); + iSet = Supp_ManMinimize( p, iSet, r, fVeryVerbose ); + if ( iBest == -1 || Supp_SetWeight(p, iBest) > Supp_SetWeight(p, iSet) ) + //if ( Supp_SetSize(p, iBest) > Supp_SetSize(p, iSet) ) + { + if ( fVeryVerbose ) + printf( "\nThe best solution found:\n" ); + if ( fVeryVerbose ) + Supp_PrintOne( p, iSet ); + iBest = iSet; + } + iSet = Supp_ManReconstruct( p, fVeryVerbose ); + } + if ( fVeryVerbose ) + printf( "Matrix size %d.\n", Vec_PtrSize(p->vMatrix) ); + Supp_ManCleanMatrix( p ); + } + if ( fVerbose ) + { + printf( "Explored %d divisor sets. Found %d solutions. Memory usage %.2f MB. ", + Hsh_VecSize(p->pHash), Vec_WecSizeSize(p->vSolutions), 1.0*Supp_ManMemory(p)/(1<<20) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + printf( "The best solution: " ); + if ( iBest == -1 ) + printf( "No solution.\n" ); + else + Supp_PrintOne( p, iBest ); + } + vRes = Supp_ManFindBestSolution( p, p->vSolutions, fVerbose, pvDivs ); + Supp_ManDelete( p ); +// if ( vRes && Vec_IntSize(vRes) == 0 ) +// Vec_IntFreeP( &vRes ); + return vRes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 35ed4ab0..0786ce44 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -16,6 +16,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaCSat2.c \ src/aig/gia/giaCTas.c \ src/aig/gia/giaCut.c \ + src/aig/gia/giaDecs.c \ src/aig/gia/giaDeep.c \ src/aig/gia/giaDfs.c \ src/aig/gia/giaDup.c \ @@ -89,6 +90,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaStr.c \ src/aig/gia/giaSupMin.c \ src/aig/gia/giaSupp.c \ + src/aig/gia/giaSupps.c \ src/aig/gia/giaSweep.c \ src/aig/gia/giaSweeper.c \ src/aig/gia/giaSwitch.c \ diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h index bd0f7d7d..cc3cfeab 100644 --- a/src/bool/bdc/bdc.h +++ b/src/bool/bdc/bdc.h @@ -79,6 +79,8 @@ extern void * Bdc_FuncCopy( Bdc_Fun_t * p ); extern int Bdc_FuncCopyInt( Bdc_Fun_t * p ); extern void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy ); extern void Bdc_FuncSetCopyInt( Bdc_Fun_t * p, int iCopy ); +extern int Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose ); +extern Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars ); /*=== working with saved copies ==========================================*/ static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj ) { return Abc_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); } diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c index 5a7a0c3a..cc94244d 100644 --- a/src/bool/bdc/bdcCore.c +++ b/src/bool/bdc/bdcCore.c @@ -364,6 +364,85 @@ void Bdc_ManDecomposeTest( unsigned uTruth, int nVars ) Bdc_ManFree( p ); } +/**Function************************************************************* + + Synopsis [Performs decomposition of one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bdc_ManBidecNodeNum( word * pFunc, word * pCare, int nVars, int fVerbose ) +{ + int nNodes, nTtWords = Abc_Truth6WordNum(nVars); + Bdc_Man_t * pManDec; + Bdc_Par_t Pars = {0}, * pPars = &Pars; + pPars->nVarsMax = nVars; + pManDec = Bdc_ManAlloc( pPars ); + Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 ); + nNodes = Bdc_ManAndNum( pManDec ); + if ( fVerbose ) + Bdc_ManDecPrint( pManDec ); + Bdc_ManFree( pManDec ); + return nNodes; +} + +/**Function************************************************************* + + Synopsis [Performs decomposition of one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_ManBidecResubInt( Bdc_Man_t * p, Vec_Int_t * vRes ) +{ + int i, iRoot = Bdc_FunId(p,Bdc_Regular(p->pRoot)) - 1; + if ( iRoot == -1 ) + Vec_IntPush( vRes, !Bdc_IsComplement(p->pRoot) ); + else if ( iRoot < p->nVars ) + Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) ); + else + { + for ( i = p->nVars+1; i < p->nNodes; i++ ) + { + Bdc_Fun_t * pNode = p->pNodes + i; + int iLit0 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) - 1, Bdc_IsComplement(pNode->pFan0) ); + int iLit1 = Abc_Var2Lit( Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) - 1, Bdc_IsComplement(pNode->pFan1) ); + if ( iLit0 > iLit1 ) + iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1; + Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 ); + } + assert( 2 + iRoot == p->nNodes ); + Vec_IntPush( vRes, 4 + Abc_Var2Lit(iRoot, Bdc_IsComplement(p->pRoot)) ); + } +} +Vec_Int_t * Bdc_ManBidecResub( word * pFunc, word * pCare, int nVars ) +{ + Vec_Int_t * vRes = NULL; + int nNodes, nTtWords = Abc_Truth6WordNum(nVars); + Bdc_Man_t * pManDec; + Bdc_Par_t Pars = {0}, * pPars = &Pars; + pPars->nVarsMax = nVars; + pManDec = Bdc_ManAlloc( pPars ); + Bdc_ManDecompose( pManDec, (unsigned *)pFunc, (unsigned *)pCare, nVars, NULL, 1000 ); + if ( pManDec->pRoot != NULL ) + { + //Bdc_ManDecPrint( pManDec ); + nNodes = Bdc_ManAndNum( pManDec ); + vRes = Vec_IntAlloc( 2*nNodes + 1 ); + Bdc_ManBidecResubInt( pManDec, vRes ); + assert( Vec_IntSize(vRes) == 2*nNodes + 1 ); + } + Bdc_ManFree( pManDec ); + return vRes; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h index 5436956a..ee82b084 100644 --- a/src/bool/kit/kit.h +++ b/src/bool/kit/kit.h @@ -574,6 +574,8 @@ extern int Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t //extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); //extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); //extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory ); +extern int Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory ); +extern Vec_Int_t * Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory ); /*=== kitIsop.c ==========================================================*/ extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); extern int Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth, int fReturnTt ); diff --git a/src/bool/kit/kitHop.c b/src/bool/kit/kitHop.c index 4ac82ac9..4509dadf 100644 --- a/src/bool/kit/kitHop.c +++ b/src/bool/kit/kitHop.c @@ -125,6 +125,107 @@ int Kit_TruthToGia2( Gia_Man_t * pMan, unsigned * pTruth0, unsigned * pTruth1, i return iLit; } +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory ) +{ + Kit_Graph_t * pGraph; + int nNodes; + // transform truth table into the decomposition tree + if ( vMemory == NULL ) + { + vMemory = Vec_IntAlloc( 0 ); + pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory ); + Vec_IntFree( vMemory ); + } + else + pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory ); + if ( pGraph == NULL ) + { + printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" ); + Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" ); + } + // derive the AIG for the decomposition tree + nNodes = Kit_GraphNodeNum( pGraph ); + Kit_GraphFree( pGraph ); + return nNodes; +} + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_IsopResubInt( Kit_Graph_t * pGraph, Vec_Int_t * vRes ) +{ + int nVars = Kit_GraphLeaveNum(pGraph); + assert( nVars >= 0 && nVars <= pGraph->nSize ); + if ( Kit_GraphIsConst(pGraph) ) + Vec_IntPush( vRes, Kit_GraphIsConst1(pGraph) ); + else if ( Kit_GraphIsVar(pGraph) ) + Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphVarInt(pGraph), Kit_GraphIsComplement(pGraph)) ); + else + { + Kit_Node_t * pNode; int i; + Kit_GraphForEachNode( pGraph, pNode, i ) + { + Kit_Node_t * pFan0 = Kit_GraphNodeFanin0( pGraph, pNode ); + Kit_Node_t * pFan1 = Kit_GraphNodeFanin1( pGraph, pNode ); + int iLit0 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan0), pNode->eEdge0.fCompl ); + int iLit1 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan1), pNode->eEdge1.fCompl ); + if ( iLit0 > iLit1 ) + iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1; + Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 ); + } + assert( pNode == Kit_GraphNode(pGraph, pGraph->eRoot.Node) ); + Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphNodeInt(pGraph, pNode), Kit_GraphIsComplement(pGraph)) ); + } +} +Vec_Int_t * Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory ) +{ + Vec_Int_t * vRes = NULL; + Kit_Graph_t * pGraph; + int nNodes; + // transform truth table into the decomposition tree + if ( vMemory == NULL ) + { + vMemory = Vec_IntAlloc( 0 ); + pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory ); + Vec_IntFree( vMemory ); + } + else + pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory ); + if ( pGraph == NULL ) + { + printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" ); + Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" ); + } + // derive the AIG for the decomposition tree + nNodes = Kit_GraphNodeNum( pGraph ); + vRes = Vec_IntAlloc( 2*nNodes + 1 ); + Kit_IsopResubInt( pGraph, vRes ); + assert( Vec_IntSize(vRes) == 2*nNodes + 1 ); + Kit_GraphFree( pGraph ); + return vRes; +} + /**Function************************************************************* Synopsis [Transforms the decomposition graph into the AIG.] diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 6a98c40f..dbc0e5a0 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -356,6 +356,12 @@ static inline void Abc_TtOrAnd( word * pOut, word * pIn1, word * pIn2, int nWord for ( w = 0; w < nWords; w++ ) pOut[w] |= pIn1[w] & pIn2[w]; } +static inline void Abc_TtSharpOr( word * pOut, word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + pOut[w] = (pOut[w] & ~pIn1[w]) | pIn2[w]; +} static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl ) { int w; @@ -2104,18 +2110,25 @@ static inline int Abc_TtCountOnesVec( word * x, int nWords ) { int w, Count = 0; for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( x[w] ); + if ( x[w] ) + Count += Abc_TtCountOnes( x[w] ); return Count; } static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl ) { int w, Count = 0; if ( fCompl ) + { for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & ~x[w] ); + if ( pMask[w] & ~x[w] ) + Count += Abc_TtCountOnes( pMask[w] & ~x[w] ); + } else + { for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & x[w] ); + if ( pMask[w] & x[w] ) + Count += Abc_TtCountOnes( pMask[w] & x[w] ); + } return Count; } static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int fComp1, word * pMask, int nWords ) @@ -2139,7 +2152,8 @@ static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords ) { int w, Count = 0; for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( x[w] ^ y[w] ); + if ( x[w] ^ y[w] ) + Count += Abc_TtCountOnes( x[w] ^ y[w] ); return Count; } static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords ) @@ -2163,6 +2177,16 @@ static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nW } return Count; } +static inline void Abc_TtIsfPrint( word * pOff, word * pOn, int nWords ) +{ + int nTotal = 64*nWords; + int nOffset = Abc_TtCountOnesVec(pOff, nWords); + int nOnset = Abc_TtCountOnesVec(pOn, nWords); + int nDcset = nTotal - nOffset - nOnset; + printf( "OFF =%6d (%6.2f %%) ", nOffset, 100.0*nOffset/nTotal ); + printf( "ON =%6d (%6.2f %%) ", nOnset, 100.0*nOnset/nTotal ); + printf( "DC =%6d (%6.2f %%)", nDcset, 100.0*nDcset/nTotal ); +} /**Function************************************************************* @@ -2263,6 +2287,22 @@ static inline int Abc_TtFindLastDiffBit2( word * pIn1, word * pIn2, int nWords ) return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]); return -1; } +static inline int Abc_TtFindFirstAndBit2( word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = 0; w < nWords; w++ ) + if ( pIn1[w] & pIn2[w] ) + return 64*w + Abc_Tt6FirstBit(pIn1[w] & pIn2[w]); + return -1; +} +static inline int Abc_TtFindLastAndBit2( word * pIn1, word * pIn2, int nWords ) +{ + int w; + for ( w = nWords - 1; w >= 0; w-- ) + if ( pIn1[w] & pIn2[w] ) + return 64*w + Abc_Tt6LastBit(pIn1[w] & pIn2[w]); + return -1; +} static inline int Abc_TtFindFirstZero( word * pIn, int nVars ) { int w, nWords = Abc_TtWordNum(nVars); diff --git a/src/misc/vec/vecHsh.h b/src/misc/vec/vecHsh.h index 00da8450..b87904a2 100644 --- a/src/misc/vec/vecHsh.h +++ b/src/misc/vec/vecHsh.h @@ -492,6 +492,10 @@ static inline int Hsh_VecSize( Hsh_VecMan_t * p ) { return Vec_IntSize(p->vMap); } +static inline double Hsh_VecManMemory( Hsh_VecMan_t * p ) +{ + return !p ? 0.0 : Vec_IntMemory(p->vTable) + Vec_IntMemory(p->vData) + Vec_IntMemory(p->vMap); +} /**Function************************************************************* diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index df90f73f..e482ef89 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1154,6 +1154,17 @@ static inline int Vec_IntFindMax( Vec_Int_t * p ) Best = p->pArray[i]; return Best; } +static inline int Vec_IntArgMax( Vec_Int_t * p ) +{ + int i, Best, Arg = 0; + if ( p->nSize == 0 ) + return -1; + Best = p->pArray[0]; + for ( i = 1; i < p->nSize; i++ ) + if ( Best < p->pArray[i] ) + Best = p->pArray[i], Arg = i; + return Arg; +} /**Function************************************************************* @@ -1177,6 +1188,17 @@ static inline int Vec_IntFindMin( Vec_Int_t * p ) Best = p->pArray[i]; return Best; } +static inline int Vec_IntArgMin( Vec_Int_t * p ) +{ + int i, Best, Arg = 0; + if ( p->nSize == 0 ) + return 0; + Best = p->pArray[0]; + for ( i = 1; i < p->nSize; i++ ) + if ( Best > p->pArray[i] ) + Best = p->pArray[i], Arg = i; + return Arg; +} /**Function************************************************************* @@ -2149,6 +2171,13 @@ static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 ) SeeAlso [] ***********************************************************************/ +static inline void Vec_IntClearAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) +{ + int Entry, i; + Vec_IntClear( vVec1 ); + Vec_IntForEachEntry( vVec2, Entry, i ) + Vec_IntPush( vVec1, Entry ); +} static inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) { int Entry, i; @@ -2192,6 +2221,67 @@ static inline void Vec_IntRemapArray( Vec_Int_t * vOld2New, Vec_Int_t * vOld, Ve Vec_IntWriteEntry( vNew, iNew, Vec_IntEntry(vOld, iOld) ); } +/**Function************************************************************* + + Synopsis [File interface.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntDumpBin( char * pFileName, Vec_Int_t * p, int fVerbose ) +{ + int RetValue; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + RetValue = fwrite( Vec_IntArray(p), 1, sizeof(int)*Vec_IntSize(p), pFile ); + fclose( pFile ); + if ( RetValue != (int)sizeof(int)*Vec_IntSize(p) ) + printf( "Error reading data from file.\n" ); + if ( fVerbose ) + printf( "Written %d integers into file \"%s\".\n", Vec_IntSize(p), pFileName ); +} +static inline Vec_Int_t * Vec_IntReadBin( char * pFileName, int fVerbose ) +{ + Vec_Int_t * p = NULL; int nSize, RetValue; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return NULL; + } + fseek( pFile, 0, SEEK_END ); + nSize = ftell( pFile ); + if ( nSize == 0 ) + { + printf( "The input file is empty.\n" ); + fclose( pFile ); + return NULL; + } + if ( nSize % sizeof(int) > 0 ) + { + printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", nSize % sizeof(int) ); + fclose( pFile ); + return NULL; + } + rewind( pFile ); + p = Vec_IntStart( nSize/sizeof(int) ); + RetValue = fread( Vec_IntArray(p), 1, nSize, pFile ); + fclose( pFile ); + if ( RetValue != nSize ) + printf( "Error reading data from file.\n" ); + if ( fVerbose ) + printf( "Read %d integers from file \"%s\".\n", nSize/sizeof(int), pFileName ); + return p; +} + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/misc/vec/vecQue.h b/src/misc/vec/vecQue.h index 54a10a29..6a8a68d0 100644 --- a/src/misc/vec/vecQue.h +++ b/src/misc/vec/vecQue.h @@ -119,6 +119,10 @@ static inline void Vec_QueClear( Vec_Que_t * p ) } p->nSize = 1; } +static inline double Vec_QueMemory( Vec_Que_t * p ) +{ + return !p ? 0.0 : 2.0 * sizeof(int) * (size_t)p->nCap + sizeof(Vec_Que_t) ; +} /**Function************************************************************* diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index dd030c1a..32c78626 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -903,6 +903,14 @@ static inline void Vec_WrdInsert( Vec_Wrd_t * p, int iHere, word Entry ) p->pArray[i] = p->pArray[i-1]; p->pArray[i] = Entry; } +static inline void Vec_WrdDrop( Vec_Wrd_t * p, int i ) +{ + int k; + assert( i >= 0 && i < Vec_WrdSize(p) ); + p->nSize--; + for ( k = i; k < p->nSize; k++ ) + p->pArray[k] = p->pArray[k+1]; +} /**Function************************************************************* diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index ae90e7fc..b58aada8 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -98,11 +98,13 @@ struct Cec4_Man_t_ Vec_Int_t * vCands; Vec_Int_t * vVisit; Vec_Int_t * vPat; + Vec_Int_t * vPats; Vec_Int_t * vDisprPairs; Vec_Bit_t * vFails; int iPosRead; // candidate reading position int iPosWrite; // candidate writing position int iLastConst; // last const node proved + int nPatsAll; // refinement Vec_Int_t * vRefClasses; Vec_Int_t * vRefNodes; @@ -145,6 +147,63 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Cec4_EvalCombine( Vec_Int_t * vPats, int nPats, int nInputs, int nWords ) +{ + //Vec_Wrd_t * vSimsPi = Vec_WrdStart( nInputs * nWords ); + Vec_Wrd_t * vSimsPi = Vec_WrdStartRandom( nInputs * nWords ); + int i, k, iPat = 0; + for ( i = 0; i < Vec_IntSize(vPats); ) + { + int Size = Vec_IntEntry(vPats, i); + assert( Size > 0 ); + for ( k = 1; k <= Size; k++ ) + { + int iLit = Vec_IntEntry( vPats, i+k ); + word * pSim; + if ( iLit == 0 ) + continue; + assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs ); + pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords ); + if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) ) + Abc_InfoXorBit( (unsigned*)pSim, iPat ); + } + iPat++; + i += Size + 1; + } + assert( iPat == nPats ); + return vSimsPi; +} +void Cec4_EvalPatterns( Gia_Man_t * p, Vec_Int_t * vPats, int nPats ) +{ + int nWords = Abc_Bit6WordNum(nPats); + Vec_Wrd_t * vSimsPi = Cec4_EvalCombine( vPats, nPats, Gia_ManCiNum(p), nWords ); + Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 ); + int i, Count = 0, nErrors = 0; + for ( i = 0; i < Gia_ManCoNum(p); i++ ) + { + int CountThis = Abc_TtCountOnesVec( Vec_WrdEntryP(vSimsPo, i*nWords), nWords ); + if ( CountThis == 0 ) + continue; + printf( "%d ", CountThis ); + nErrors += CountThis; + Count++; + } + printf( "\nDetected %d error POs with %d errors (average %.2f).\n", Count, nErrors, 1.0*nErrors/Abc_MaxInt(1, Count) ); + Vec_WrdFree( vSimsPi ); + Vec_WrdFree( vSimsPo ); +} + /**Function************************************************************* Synopsis [Default parameter settings.] @@ -198,6 +257,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) p->vCands = Vec_IntAlloc( 100 ); p->vVisit = Vec_IntAlloc( 100 ); p->vPat = Vec_IntAlloc( 100 ); + p->vPats = Vec_IntAlloc( 10000 ); p->vDisprPairs = Vec_IntAlloc( 100 ); p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) ); //pAig->pData = p->pSat; // point AIG manager to the solver @@ -226,6 +286,12 @@ void Cec4_ManDestroy( Cec4_Man_t * p ) ABC_PRTP( "TOTAL ", timeTotal, timeTotal ); fflush( stdout ); } + //printf( "Recorded %d patterns with %d literals (average %.2f).\n", + // p->nPatsAll, Vec_IntSize(p->vPats) - p->nPatsAll, 1.0*Vec_IntSize(p->vPats)/Abc_MaxInt(1, p->nPatsAll)-1 ); + //Cec4_EvalPatterns( p->pAig, p->vPats, p->nPatsAll ); + //Vec_IntFreeP( &p->vPats ); + Vec_IntFreeP( &p->pAig->vPats ); + p->pAig->vPats = p->vPats; Vec_WrdFreeP( &p->pAig->vSims ); Vec_WrdFreeP( &p->pAig->vSimsPi ); Gia_ManCleanMark01( p->pAig ); @@ -1392,6 +1458,9 @@ int Cec4_ManGeneratePatterns( Cec4_Man_t * p ) if ( Res ) { int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat, 1 ); + Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) ); + Vec_IntAppend( p->vPats, p->vPat ); + p->nPatsAll++; //Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand ); Packs += Ret; if ( Ret == 64 * p->pAig->nSimWords ) @@ -1566,6 +1635,9 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) p->pAig->iPatsPi++; Vec_IntForEachEntry( p->vPat, iLit, i ) Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) ); + Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) ); + Vec_IntAppend( p->vPats, p->vPat ); + p->nPatsAll++; //Cec4_ManPackAddPattern( p->pAig, p->vPat, 0 ); //assert( iPatsOld + 1 == p->pAig->iPatsPi ); if ( fEasy ) -- cgit v1.2.3