From ee11ee1833c01a4705b52210e122db298825d388 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 25 Sep 2013 13:18:21 -0700 Subject: Changes to enable decomposition of non-DSD functions. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaUtil.c | 23 +++++++++++++ src/base/abci/abcRec3.c | 10 +++++- src/bool/rsb/rsbDec6.c | 57 ++++++++++++++++++++++++++----- src/misc/extra/extraUtilDsd.c | 79 +++++++++++++++++++++++++++++++++++++++++++ src/misc/vec/vecWrd.h | 18 ++++++++++ 6 files changed, 179 insertions(+), 9 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 70fda8d4..5a6148d0 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1227,6 +1227,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManPrint( Gia_Man_t * p ); extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes ); +extern void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); extern void Gia_ManInvertPos( Gia_Man_t * pAig ); extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index cad6f5ad..cf1aa762 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1194,6 +1194,7 @@ void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj ) Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) ); Gia_ObjPrint( p, pObj ); } + void Gia_ManPrintCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) { if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 ) @@ -1215,6 +1216,28 @@ void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeav Gia_ObjPrint( p, pObj ); } +void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 ) + return; + if ( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) ) + Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes ); + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} +void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + Vec_Int_t * vNodes; + int i; + vNodes = Vec_IntAlloc( 100 ); + Gia_ManPrintCollect2_rec( p, pObj, vNodes ); + printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + Gia_ObjPrint( p, pObj ); + Vec_IntFree( vNodes ); +} + /**Function************************************************************* Synopsis [Complements the constraint outputs.] diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c index cf90a79d..8bf46feb 100644 --- a/src/base/abci/abcRec3.c +++ b/src/base/abci/abcRec3.c @@ -1035,7 +1035,15 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo ); assert( BestPo >= 0 ); pGiaPo = Gia_ManCo( pGia, BestPo ); - +/* +if ( If_CutLeaveNum(pCut) == 6 ) +{ +printf( "\n" ); +Kit_DsdPrintFromTruth( If_CutTruth(pCut), If_CutLeaveNum(pCut) ); printf( "\n" ); +//Gia_ManPrintCo( pGia, pGiaPo ); +Gia_ManPrintCone2( pGia, pGiaPo ); +} +*/ // collect internal nodes into pGia->vTtNodes if ( pGia->vTtNodes == NULL ) pGia->vTtNodes = Vec_IntAlloc( 256 ); diff --git a/src/bool/rsb/rsbDec6.c b/src/bool/rsb/rsbDec6.c index df30eb1a..88644686 100644 --- a/src/bool/rsb/rsbDec6.c +++ b/src/bool/rsb/rsbDec6.c @@ -334,7 +334,7 @@ int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word SeeAlso [] ***********************************************************************/ -unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll ) +unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fFindAll ) { word * pCexes = Vec_WrdArray(p->vCexes); unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats); @@ -365,7 +365,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n pDivs[0] = g[i]; p->vFanins->pArray[0] = i; uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); if ( uTruth ) - return uTruth; + { + if ( fFindAll ) + { + uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 1 ); + Kit_DsdPrintFromTruth( &uTruth, 1 ); printf( " " ); + Vec_IntPrint(p->vFanins); + continue; + } + else + return uTruth; + } if ( nCexes == 64 ) return 0; Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); @@ -388,7 +398,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n pDivs[1] = g[k]; p->vFanins->pArray[1] = k; uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); if ( uTruth ) - return uTruth; + { + if ( fFindAll ) + { + uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 2 ); + Kit_DsdPrintFromTruth( &uTruth, 2 ); printf( " " ); + Vec_IntPrint(p->vFanins); + continue; + } + else + return uTruth; + } if ( nCexes == 64 ) return 0; Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); @@ -414,7 +434,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n pDivs[2] = g[j]; p->vFanins->pArray[2] = j; uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); if ( uTruth ) - return uTruth; + { + if ( fFindAll ) + { + uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 3 ); + Kit_DsdPrintFromTruth( &uTruth, 3 ); printf( " " ); + Vec_IntPrint(p->vFanins); + continue; + } + else + return uTruth; + } if ( nCexes == 64 ) return 0; Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); @@ -443,7 +473,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n pDivs[3] = g[n]; p->vFanins->pArray[3] = n; uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB ); if ( uTruth ) - return uTruth; + { + if ( fFindAll ) + { + uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 4 ); + Kit_DsdPrintFromTruth( &uTruth, 4 ); printf( " " ); + Vec_IntPrint(p->vFanins); + continue; + } + else + return uTruth; + } if ( nCexes == 64 ) return 0; Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB ); @@ -611,7 +651,7 @@ unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, if ( fVerbose ) vTries = Vec_IntAlloc( 100 ); assert( nGs < nGsAll ); - uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll ); + uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll, 0 ); if ( uTruth ) { @@ -653,12 +693,13 @@ Vec_IntFree( vTries ); ***********************************************************************/ int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose ) { - word * pGs[64]; + word * pGs[200]; unsigned uTruthRes; int i, nVars, nGs = Vec_WrdSize(vDivTruths); + assert( nGs < 200 ); for ( i = 0; i < nGs; i++ ) pGs[i] = Vec_WrdEntryP(vDivTruths,i); - uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs ); + uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs, 0 ); if ( uTruthRes == 0 ) return 0; diff --git a/src/misc/extra/extraUtilDsd.c b/src/misc/extra/extraUtilDsd.c index 657808fd..cf1d3ade 100644 --- a/src/misc/extra/extraUtilDsd.c +++ b/src/misc/extra/extraUtilDsd.c @@ -27,6 +27,7 @@ #include "misc/vec/vec.h" #include "misc/vec/vecHsh.h" #include "misc/util/utilTruth.h" +#include "bool/rsb/rsb.h" ABC_NAMESPACE_IMPL_START @@ -1151,6 +1152,84 @@ void Sdm_ManCompareCnfSizes() } */ + +/**Function************************************************************* + + Synopsis [Collect DSD divisors of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sdm_ManDivCollect_rec( word t, Vec_Wrd_t ** pvDivs ) +{ + int i, Config, Counter = 0; + // check if function is decomposable + Config = Sdm_ManCheckDsd6( s_SdmMan, t ); + if ( Config != -1 && (Config >> 17) < 2 ) + return; + for ( i = 0; i < 6; i++ ) + { + if ( !Abc_Tt6HasVar( t, i ) ) + continue; + Sdm_ManDivCollect_rec( Abc_Tt6Cofactor0(t, i), pvDivs ); + Sdm_ManDivCollect_rec( Abc_Tt6Cofactor1(t, i), pvDivs ); + Counter++; + } + if ( Config != -1 && Counter >= 2 && Counter <= 4 ) + { + Vec_WrdPush( pvDivs[Counter], (t & 1) ? ~t : t ); +// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" ); + } +} +void Sdm_ManDivTest() +{ +// word u, t0, t1, t = ABC_CONST(0xB0F0BBFFB0F0BAFE); +// word u, t0, t1, t = ABC_CONST(0x3F1F3F13FFDFFFD3); + word u, t0, t1, t = ABC_CONST(0x3F3FFFFF37003700); + Rsb_Man_t * pManRsb = Rsb_ManAlloc( 6, 200, 3, 1 ); + Vec_Wrd_t * pvDivs[7] = { NULL }; + Vec_Wrd_t * vDivs = Vec_WrdAlloc( 100 ); + int i, RetValue; + + // collect divisors + for ( i = 2; i <= 4; i++ ) + pvDivs[i] = Vec_WrdAlloc( 100 ); + Sdm_ManDivCollect_rec( t, pvDivs ); + for ( i = 2; i <= 4; i++ ) + Vec_WrdUniqify( pvDivs[i] ); + + // prepare the set + vDivs = Vec_WrdAlloc( 100 ); + for ( i = 0; i < 6; i++ ) + Vec_WrdPush( vDivs, s_Truths6[i] ); + for ( i = 2; i <= 4; i++ ) + Vec_WrdAppend( vDivs, pvDivs[i] ); + for ( i = 2; i <= 4; i++ ) + Vec_WrdFree( pvDivs[i] ); + + Vec_WrdForEachEntry( vDivs, u, i ) + { + printf( "%2d : ", i ); + Kit_DsdPrintFromTruth( (unsigned *)&u, 6 ); printf( "\n" ); + } + + RetValue = Rsb_ManPerformResub6( pManRsb, 6, t, vDivs, &t0, &t1, 1 ); + if ( RetValue ) + { + Kit_DsdPrintFromTruth( (unsigned *)&t0, 6 ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ); printf( "\n" ); + printf( "Decomposition exits.\n" ); + } + + + Vec_WrdFree( vDivs ); + Rsb_ManFree( pManRsb ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index 99aa1acb..a5beeb37 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -1120,6 +1120,24 @@ static inline void Vec_WrdSortUnsigned( Vec_Wrd_t * p ) } +/**Function************************************************************* + + Synopsis [Appends the contents of the second vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_WrdAppend( Vec_Wrd_t * vVec1, Vec_Wrd_t * vVec2 ) +{ + word Entry; int i; + Vec_WrdForEachEntry( vVec2, Entry, i ) + Vec_WrdPush( vVec1, Entry ); +} + ABC_NAMESPACE_HEADER_END -- cgit v1.2.3