From 1485e63ae3cc36d2840b5c2d1d7da38a88ee8928 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 7 Jan 2020 01:36:06 +0200 Subject: Allowing nodes and boxes to have more than 6 inputs in mfs2 and &mfs. --- src/opt/sfm/sfm.h | 2 +- src/opt/sfm/sfmCnf.c | 61 +++++++++++++++++++++++++++++++++++++++++++--------- src/opt/sfm/sfmInt.h | 4 +++- src/opt/sfm/sfmLib.c | 2 +- src/opt/sfm/sfmNtk.c | 11 +++++++--- src/opt/sfm/sfmSat.c | 1 + 6 files changed, 65 insertions(+), 16 deletions(-) (limited to 'src/opt') diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index 002778dc..1aa8b7d0 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -87,7 +87,7 @@ struct Sfm_Par_t_ extern void Sfm_ParSetDefault( Sfm_Par_t * pPars ); extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ); /*=== sfmNtk.c ==========================================================*/ -extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths ); +extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); extern void Sfm_NtkFree( Sfm_Ntk_t * p ); extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ); extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c index ce2f34b8..f6d434f8 100644 --- a/src/opt/sfm/sfmCnf.c +++ b/src/opt/sfm/sfmCnf.c @@ -68,24 +68,63 @@ void Sfm_PrintCnf( Vec_Str_t * vCnf ) SeeAlso [] ***********************************************************************/ -int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) +int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ) { + int w, nWords = Abc_Truth6WordNum( nVars ); Vec_StrClear( vCnf ); - if ( Truth == 0 || ~Truth == 0 ) + if ( nVars <= 6 ) { -// assert( nVars == 0 ); - Vec_StrPush( vCnf, (char)(Truth == 0) ); - Vec_StrPush( vCnf, (char)-1 ); - return 1; + if ( Truth == 0 || ~Truth == 0 ) + { + //assert( nVars == 0 ); + Vec_StrPush( vCnf, (char)(Truth == 0) ); + Vec_StrPush( vCnf, (char)-1 ); + return 1; + } + } + else + { + // const0 + for ( w = 0; w < nWords; w++ ) + if ( pTruth[w] ) + break; + if ( w == nWords ) + { + Vec_StrPush( vCnf, (char)1 ); + Vec_StrPush( vCnf, (char)-1 ); + return 1; + } + // const1 + for ( w = 0; w < nWords; w++ ) + if ( ~pTruth[w] ) + break; + if ( w == nWords ) + { + Vec_StrPush( vCnf, (char)0 ); + Vec_StrPush( vCnf, (char)-1 ); + return 1; + } } - else { int i, k, c, RetValue, Literal, Cube, nCubes = 0; assert( nVars > 0 ); for ( c = 0; c < 2; c ++ ) { - Truth = c ? ~Truth : Truth; - RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); + if ( nVars <= 6 ) + { + Truth = c ? ~Truth : Truth; + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 ); + } + else + { + if ( c ) + for ( k = 0; k < nWords; k++ ) + pTruth[k] = ~pTruth[k]; + RetValue = Kit_TruthIsop( (unsigned *)pTruth, nVars, vCover, 0 ); + if ( c ) + for ( k = 0; k < nWords; k++ ) + pTruth[k] = ~pTruth[k]; + } assert( RetValue == 0 ); nCubes += Vec_IntSize( vCover ); Vec_IntForEachEntry( vCover, Cube, i ) @@ -129,7 +168,9 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ) vCnfs = Vec_WecStart( p->nObjs ); Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos ) { - nCubes = Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); + int Offset = Vec_IntEntry( p->vStarts, i ); + word * pRes = Vec_WrdSize(p->vTruths2) ? Vec_WrdEntryP( p->vTruths2, Offset ) : NULL; + nCubes = Sfm_TruthToCnf( uTruth, pRes, Sfm_ObjFaninNum(p, i), p->vCover, vCnf ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) ); diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index 2b96d4bd..80edd54d 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -81,6 +81,8 @@ struct Sfm_Ntk_t_ Vec_Str_t * vEmpty; // transparent objects Vec_Wrd_t * vTruths; // truth tables Vec_Wec_t vFanins; // fanins + Vec_Int_t * vStarts; // offsets + Vec_Wrd_t * vTruths2; // truth tables (large) // attributes Vec_Wec_t vFanouts; // fanouts Vec_Int_t vLevels; // logic level @@ -195,7 +197,7 @@ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); /*=== sfmCnf.c ==========================================================*/ extern void Sfm_PrintCnf( Vec_Str_t * vCnf ); -extern int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ); +extern int Sfm_TruthToCnf( word Truth, word * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ); extern Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p ); extern void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar ); /*=== sfmCore.c ==========================================================*/ diff --git a/src/opt/sfm/sfmLib.c b/src/opt/sfm/sfmLib.c index afb4a48d..18ba0971 100644 --- a/src/opt/sfm/sfmLib.c +++ b/src/opt/sfm/sfmLib.c @@ -107,7 +107,7 @@ void Sfm_DecCreateCnf( Vec_Int_t * vGateSizes, Vec_Wrd_t * vGateFuncs, Vec_Wec_t vCover = Vec_IntAlloc( 100 ); Vec_WrdForEachEntry( vGateFuncs, uTruth, i ) { - nCubes = Sfm_TruthToCnf( uTruth, Vec_IntEntry(vGateSizes, i), vCover, vCnf ); + nCubes = Sfm_TruthToCnf( uTruth, NULL, Vec_IntEntry(vGateSizes, i), vCover, vCnf ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vGateCnfs, i ); Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) ); memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), (size_t)Vec_StrSize(vCnf) ); diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 1ded0ede..d410aa0b 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v SeeAlso [] ***********************************************************************/ -Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths ) +Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) { Sfm_Ntk_t * p; Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed ); @@ -178,6 +178,8 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t p->vEmpty = vEmpty; p->vTruths = vTruths; p->vFanins = *vFanins; + p->vStarts = vStarts; + p->vTruths2 = vTruths2; ABC_FREE( vFanins ); // attributes Sfm_CreateFanout( &p->vFanins, &p->vFanouts ); @@ -217,6 +219,8 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) Vec_StrFreeP( &p->vEmpty ); Vec_WrdFree( p->vTruths ); Vec_WecErase( &p->vFanins ); + Vec_IntFree( p->vStarts ); + Vec_WrdFree( p->vTruths2 ); // attributes Vec_WecErase( &p->vFanouts ); ABC_FREE( p->vLevels.pArray ); @@ -316,6 +320,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth int iFanin = Sfm_ObjFanin( p, iNode, f ); assert( Sfm_ObjIsNode(p, iNode) ); assert( iFanin != iFaninNew ); + assert( Sfm_ObjFaninNum(p, iNode) <= 6 ); if ( uTruth == 0 || ~uTruth == 0 ) { Sfm_ObjForEachFanin( p, iNode, iFanin, f ) @@ -341,7 +346,7 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth Sfm_NtkUpdateLevelR_rec( p, iFanin ); // update truth table Vec_WrdWriteEntry( p->vTruths, iNode, uTruth ); - Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); + Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); } /**Function************************************************************* @@ -361,7 +366,7 @@ Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ) } word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ) { - return Vec_WrdEntryP( p->vTruths, i ); + return Sfm_ObjFaninNum(p, i) <= 6 ? Vec_WrdEntryP( p->vTruths, i ) : Vec_WrdEntryP( p->vTruths2, Vec_IntEntry(p->vStarts, i) ); } int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ) { diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index 8bcb7f8a..6ccdd903 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -167,6 +167,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) sat_solver_setnvars( p->pSat, nVars + 1 ); pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1 pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit + assert( Vec_IntSize(p->vDivIds) <= 6 ); while ( 1 ) { // find onset minterm -- cgit v1.2.3