From b05ee94311ac284de1a658f0c72c8c02a433ed4c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 19 Sep 2014 14:06:51 -0700 Subject: Improvements to Boolean matching. --- src/base/abci/abc.c | 42 ++-- src/map/if/if.h | 2 + src/map/if/ifCut.c | 2 +- src/map/if/ifDsd.c | 5 +- src/map/if/ifMan.c | 17 +- src/map/if/ifMap.c | 19 ++ src/map/if/ifTune.c | 495 ++++++++++++++++++++++++++++++++++++++++------ src/misc/util/utilTruth.h | 69 +++++++ 8 files changed, 563 insertions(+), 88 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b99c1049..db15c678 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15309,7 +15309,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fEnableCheck07 ^= 1; break; case 'i': - pPars->fEnableCheck08 ^= 1; + pPars->fUseCofVars ^= 1; break; case 'k': pPars->fUseDsdTune ^= 1; @@ -15376,7 +15376,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fCutMin = 1; } - if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 ) + if ( pPars->fEnableCheck07 + pPars->fUseCofVars + pPars->fUseDsdTune + (pPars->pLutStruct != NULL) > 1 ) { Abc_Print( -1, "Only one additional check can be performed at the same time.\n" ); return 1; @@ -15391,14 +15391,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncCell = If_CutPerformCheck07; pPars->fCutMin = 1; } - if ( pPars->fEnableCheck08 ) + if ( pPars->fUseCofVars ) { - if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 ) + if ( !(pPars->nLutSize & 1) ) { - Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" ); + Abc_Print( -1, "This feature only works for odd-sized LUTs.\n" ); return 1; } - pPars->pFuncCell = If_CutPerformCheck08; pPars->fCutMin = 1; } if ( pPars->fUseDsdTune ) @@ -15610,7 +15609,7 @@ usage: Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" ); Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); - Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" ); + Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" ); Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" ); Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" ); Abc_Print( -2, "\t-n : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" ); @@ -30984,7 +30983,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgxyojikfuztncvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgxyojfuikztncvh" ) ) != EOF ) { switch ( c ) { @@ -31159,18 +31158,18 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'j': pPars->fEnableCheck07 ^= 1; break; - case 'i': - pPars->fEnableCheck08 ^= 1; - break; - case 'k': - pPars->fUseDsdTune ^= 1; - break; case 'f': pPars->fEnableCheck75 ^= 1; break; case 'u': pPars->fEnableCheck75u ^= 1; break; + case 'i': + pPars->fUseCofVars ^= 1; + break; + case 'k': + pPars->fUseDsdTune ^= 1; + break; case 'z': pPars->fDeriveLuts ^= 1; break; @@ -31247,7 +31246,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fCutMin = 1; } - if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 ) + if ( pPars->fEnableCheck07 + pPars->fUseCofVars + pPars->fUseDsdTune + pPars->fEnableCheck75 + pPars->fEnableCheck75u + (pPars->pLutStruct != NULL) > 1 ) { Abc_Print( -1, "Only one additional check can be performed at the same time.\n" ); return 1; @@ -31262,14 +31261,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncCell = If_CutPerformCheck07; pPars->fCutMin = 1; } - if ( pPars->fEnableCheck08 ) + if ( pPars->fUseCofVars ) { - if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 ) + if ( !(pPars->nLutSize & 1) ) { - Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" ); + Abc_Print( -1, "This feature only works for odd-sized LUTs.\n" ); return 1; } - pPars->pFuncCell = If_CutPerformCheck08; pPars->fCutMin = 1; } if ( pPars->fUseDsdTune ) @@ -31439,7 +31437,7 @@ usage: sprintf(LutSize, "library" ); else sprintf(LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgxyojikfuztncvh]\n" ); + Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgxyojfuikztncvh]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -31467,9 +31465,9 @@ usage: Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" ); Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); - Abc_Print( -2, "\t-i : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" ); Abc_Print( -2, "\t-f : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75? "yes": "no" ); Abc_Print( -2, "\t-u : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" ); + Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" ); Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" ); Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" ); Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" ); @@ -32255,7 +32253,7 @@ usage: Abc_Print( -2, "\t-L num : the fanout limit for coarsening XOR/MUX (num >= 2) [default = %d]\n", pPars->nCoarseLimit ); Abc_Print( -2, "\t-E num : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner ); Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer ); - Abc_Print( -2, "\t-M num : LUT size for the cofactoring (0 <= num <= 100) [default = %d]\n", pPars->nLutSizeMux ); + Abc_Print( -2, "\t-M num : LUT size when cofactoring is performed (0 <= num <= 100) [default = %d]\n", pPars->nLutSizeMux ); // Abc_Print( -2, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" ); Abc_Print( -2, "\t-e : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" ); Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" ); diff --git a/src/map/if/if.h b/src/map/if/if.h index f6849337..a0180563 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -131,6 +131,7 @@ struct If_Par_t_ int fEnableCheck75u;// enable additional checking int fUseDsd; // compute DSD of the cut functions int fUseDsdTune; // use matching based on precomputed manager + int fUseCofVars; // use cofactoring variables int fUseTtPerm; // compute truth tables of the cut functions int fDeriveLuts; // enables deriving LUT structures int fDoAverage; // optimize average rather than maximum level @@ -242,6 +243,7 @@ struct If_Man_t_ Vec_Wec_t * vTtIsops[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD Vec_Int_t * vTtDsds[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD Vec_Str_t * vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations + Vec_Str_t * vTtVars[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into selected vars Hash_IntMan_t * vPairHash; // hashing pairs of truth tables Vec_Int_t * vPairRes; // resulting truth table Vec_Str_t * vPairPerms; // resulting permutation diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index d13d6a49..7b9ad3c1 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -754,7 +754,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut ) if ( !pCut->fUseless && (p->pPars->fUseDsd || p->pPars->fUseBat || p->pPars->pLutStruct || p->pPars->fUserRecLib || - p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || + p->pPars->fEnableCheck07 || p->pPars->fUseCofVars || p->pPars->fUseDsdTune || p->pPars->fEnableCheck75 || p->pPars->fEnableCheck75u) ) { diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 5525678b..51607066 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -2410,7 +2410,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( (i & 0xFF) == 0 ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); nVars = If_DsdObjSuppSize(pObj); if ( nVars <= LutSize ) continue; @@ -2574,7 +2575,7 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, } for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ ) { - if ( (k & 0x3FF) == 0 ) + if ( (k & 0xFF) == 0 ) Extra_ProgressBarUpdate( pProgress, k, NULL ); pObj = If_DsdVecObj( &p->vObjs, k ); nVars = If_DsdObjSuppSize(pObj); diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 0d66814b..472a1b1e 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -125,6 +125,17 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) p->vPairRes = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vPairRes, -1 ); } + if ( pPars->fUseCofVars ) + { + for ( v = 6; v <= Abc_MaxInt(6,p->pPars->nLutSize); v++ ) + { + p->vTtVars[v] = Vec_StrAlloc( 1000 ); + Vec_StrPush( p->vTtVars[v], 0 ); + Vec_StrPush( p->vTtVars[v], 0 ); + } + for ( v = 0; v < 6; v++ ) + p->vTtVars[v] = p->vTtVars[6]; + } if ( pPars->fUseBat ) { // abctime clk = Abc_Clock(); @@ -209,8 +220,8 @@ void If_ManStop( If_Man_t * p ) { for ( i = 0; i <= 16; i++ ) if ( p->nCutsUseless[i] ) - Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) ); - Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) ); + Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/Abc_MaxInt(p->nCutsCount[i],1) ); + Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/Abc_MaxInt(p->nCutsCountAll,1) ); } // if ( p->pPars->fVerbose && p->nCuts5 ) // Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 ); @@ -235,6 +246,8 @@ void If_ManStop( If_Man_t * p ) Vec_IntFreeP( &p->vTtDsds[i] ); for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ ) Vec_StrFreeP( &p->vTtPerms[i] ); + for ( i = 6; i <= Abc_MaxInt(6,p->pPars->nLutSize); i++ ) + Vec_StrFreeP( &p->vTtVars[i] ); Vec_IntFreeP( &p->vCutData ); Vec_IntFreeP( &p->vPairRes ); Vec_StrFreeP( &p->vPairPerms ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 18b1eed2..ae8897e2 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -270,6 +270,25 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep p->nCutsCountAll++; p->nCutsCount[pCut->nLeaves]++; } + else if ( p->pPars->fUseCofVars ) + { + extern int Abc_TtCheckCondDepTest( word * pTruth, int nVars, int nSuppLim ); + int iCofVar = -1, truthId = Abc_Lit2Var(pCut->iCutFunc); + if ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) || Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId) == (char)-1 ) + { + while ( truthId >= Vec_StrSize(p->vTtVars[pCut->nLeaves]) ) + Vec_StrPush( p->vTtVars[pCut->nLeaves], (char)-1 ); + iCofVar = Abc_TtCheckCondDep( If_CutTruthWR(p, pCut), pCut->nLeaves, p->pPars->nLutSize / 2 ); + Vec_StrWriteEntry( p->vTtVars[pCut->nLeaves], truthId, (char)iCofVar ); + } + iCofVar = Vec_StrEntry(p->vTtVars[pCut->nLeaves], truthId); + assert( iCofVar >= 0 && iCofVar <= (int)pCut->nLeaves ); + pCut->fUseless = (int)(iCofVar == (int)pCut->nLeaves && pCut->nLeaves > 0); + p->nCutsUselessAll += pCut->fUseless; + p->nCutsUseless[pCut->nLeaves] += pCut->fUseless; + p->nCutsCountAll++; + p->nCutsCount[pCut->nLeaves]++; + } } // compute the application-specific cost and depth diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 7b3adfec..24260c2a 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -37,14 +37,14 @@ ABC_NAMESPACE_IMPL_START // network types typedef enum { - IF_DSD_NONE = 0, // 0: unknown - IF_DSD_CONST0, // 1: constant - IF_DSD_VAR, // 2: variable - IF_DSD_AND, // 3: AND - IF_DSD_XOR, // 4: XOR - IF_DSD_MUX, // 5: MUX - IF_DSD_PRIME // 6: PRIME -} If_DsdType_t; + IFN_DSD_NONE = 0, // 0: unknown + IFN_DSD_CONST0, // 1: constant + IFN_DSD_VAR, // 2: variable + IFN_DSD_AND, // 3: AND + IFN_DSD_XOR, // 4: XOR + IFN_DSD_MUX, // 5: MUX + IFN_DSD_PRIME // 6: PRIME +} Ifn_DsdType_t; // object types static char * Ifn_Symbs[16] = { @@ -124,7 +124,7 @@ int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars ) p->nPars = p->nObjs; for ( i = p->nInps; i < p->nObjs; i++ ) { - if ( p->Nodes[i].Type != IF_DSD_PRIME ) + if ( p->Nodes[i].Type != IFN_DSD_PRIME ) continue; p->Nodes[i].iFirst = p->nPars; p->nPars += (1 << p->Nodes[i].nFanins); @@ -162,7 +162,7 @@ int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ) { int i, LutSize = 0; for ( i = p->nInps; i < p->nObjs; i++ ) - if ( p->Nodes[i].Type == IF_DSD_PRIME ) + if ( p->Nodes[i].Type == IFN_DSD_PRIME ) LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins ); return LutSize; } @@ -182,9 +182,150 @@ int Ifn_NtkInputNum( Ifn_Ntk_t * p ) SeeAlso [] ***********************************************************************/ +int Ifn_ErrorMessage( const char * format, ... ) +{ + char * pMessage; + va_list args; + va_start( args, format ); + pMessage = vnsprintf( format, args ); + va_end( args ); + printf( "%s", pMessage ); + ABC_FREE( pMessage ); + return 0; +} +int Inf_ManOpenSymb( char * pStr ) +{ + if ( pStr[0] == '(' ) + return 3; + if ( pStr[0] == '[' ) + return 4; + if ( pStr[0] == '<' ) + return 5; + if ( pStr[0] == '{' ) + return 6; + return 0; +} int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs ) { - int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0, RetValue = 1; + int i, nNodes = 0, Marks[32] = {0}, MaxVar = -1, RetValue = 1; + for ( i = 0; pStr[i]; i++ ) + { + if ( Inf_ManOpenSymb(pStr+i) ) + nNodes++; + if ( pStr[i] == ';' || + pStr[i] == '(' || pStr[i] == ')' || + pStr[i] == '[' || pStr[i] == ']' || + pStr[i] == '<' || pStr[i] == '>' || + pStr[i] == '{' || pStr[i] == '}' ) + continue; + if ( pStr[i] >= 'A' && pStr[i] <= 'Z' ) + continue; + if ( pStr[i] >= 'a' && pStr[i] <= 'z' ) + { + MaxVar = Abc_MaxInt( MaxVar, (int)(pStr[i] - 'a') ); + Marks[pStr[i] - 'a'] = 1; + continue; + } + return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] ); + } + for ( i = 0; i <= MaxVar; i++ ) + if ( Marks[i] == 0 ) + return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i ); + *pnInps = MaxVar + 1; + *pnObjs = MaxVar + 1 + nNodes; + return 1; +} +static inline char * Ifn_NtkParseFindClosingParanthesis( char * pStr, char Open, char Close ) +{ + int Counter = 0; + assert( *pStr == Open ); + for ( ; *pStr; pStr++ ) + { + if ( *pStr == Open ) + Counter++; + if ( *pStr == Close ) + Counter--; + if ( Counter == 0 ) + return pStr; + } + return NULL; +} +int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNode ) +{ + Ifn_Obj_t * pObj; + int nFanins = 0, pFanins[IFN_INS]; + int Type = Inf_ManOpenSymb( pStr ); + char * pLim = Ifn_NtkParseFindClosingParanthesis( pStr++, Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] ); + *ppFinal = NULL; + if ( pLim == NULL ) + return Ifn_ErrorMessage( "For symbol \'%c\' cannot find matching symbol \'%c\'.\n", Ifn_Symbs[Type][0], Ifn_Symbs[Type][1] ); + while ( pStr < pLim ) + { + assert( nFanins < IFN_INS ); + if ( pStr[0] >= 'a' && pStr[0] <= 'z' ) + pFanins[nFanins++] = pStr[0] - 'a', pStr++; + else if ( Inf_ManOpenSymb(pStr) ) + { + if ( !Ifn_NtkParseInt_rec( pStr, p, &pStr, piNode ) ) + return 0; + pFanins[nFanins++] = *piNode - 1; + } + else + return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] ); + } + assert( pStr == pLim ); + pObj = p->Nodes + (*piNode)++; + pObj->Type = Type; + assert( pObj->nFanins == 0 ); + pObj->nFanins = nFanins; + memcpy( pObj->Fanins, pFanins, sizeof(int) * nFanins ); + *ppFinal = pLim + 1; + if ( Type == IFN_DSD_MUX && nFanins != 3 ) + return Ifn_ErrorMessage( "MUX should have exactly three fanins.\n" ); + return 1; +} +int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p ) +{ + char * pFinal; int iNode; + if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) ) + return 0; + if ( p->nInps > IFN_INS ) + return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS ); + assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS ); + if ( !Inf_ManOpenSymb(pStr) ) + return Ifn_ErrorMessage( "The first symbol should be one of the symbols: (, [, <, {.\n" ); + iNode = p->nInps; + if ( !Ifn_NtkParseInt_rec( pStr, p, &pFinal, &iNode ) ) + return 0; + if ( pFinal[0] && pFinal[0] != ';' ) + return Ifn_ErrorMessage( "The last symbol should be \';\'.\n" ); + if ( iNode != p->nObjs ) + return Ifn_ErrorMessage( "Mismatch in the number of nodes.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ifn_ManStrType2( char * pStr ) +{ + int i; + for ( i = 0; pStr[i]; i++ ) + if ( pStr[i] == '=' ) + return 1; + return 0; +} +int Ifn_ManStrCheck2( char * pStr, int * pnInps, int * pnObjs ) +{ + int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0; for ( i = 0; pStr[i]; i++ ) { if ( pStr[i] == '=' || pStr[i] == ';' || @@ -201,11 +342,8 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs ) Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a'); continue; } - printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] ); - RetValue = 0; + return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] ); } - if ( !RetValue ) - return 0; for ( i = 0; pStr[i]; i++ ) { if ( pStr[i] == '=' || pStr[i] == ';' || @@ -222,43 +360,27 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs ) Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a'); continue; } - printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] ); - RetValue = 0; + return Ifn_ErrorMessage( "String \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[i] ); } - if ( !RetValue ) - return 0; MaxVar++; MaxDef++; for ( i = 0; i < MaxDef; i++ ) if ( Marks[i] == 0 ) - printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + i ), RetValue = 0; + return Ifn_ErrorMessage( "String \"%s\" has no symbol \'%c\'.\n", pStr, 'a' + i ); for ( i = 0; i < MaxVar; i++ ) if ( Marks[i] == 2 ) - printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + i ), RetValue = 0; + return Ifn_ErrorMessage( "String \"%s\" has definition of input variable \'%c\'.\n", pStr, 'a' + i ); for ( i = MaxVar; i < MaxDef; i++ ) if ( Marks[i] == 1 ) - printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0; - if ( !RetValue ) - return 0; + return Ifn_ErrorMessage( "String \"%s\" has no definition for internal variable \'%c\'.\n", pStr, 'a' + i ); *pnInps = MaxVar; *pnObjs = MaxDef; return 1; } -int Ifn_ErrorMessage( const char * format, ... ) -{ - char * pMessage; - va_list args; - va_start( args, format ); - pMessage = vnsprintf( format, args ); - va_end( args ); - printf( "%s", pMessage ); - ABC_FREE( pMessage ); - return 0; -} -int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p ) +int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p ) { int i, k, n, f, nFans, iFan; - if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) ) + if ( !Ifn_ManStrCheck2(pStr, &p->nInps, &p->nObjs) ) return 0; if ( p->nInps > IFN_INS ) return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS ); @@ -270,25 +392,25 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p ) if ( pStr[k] == 'a' + i && pStr[k+1] == '=' ) break; if ( pStr[k] == 0 ) - return Ifn_ErrorMessage( "Cannot find definition of signal %c.\n", 'a' + i ); + return Ifn_ErrorMessage( "Cannot find definition of signal \'%c\'.\n", 'a' + i ); if ( pStr[k+2] == '(' ) - p->Nodes[i].Type = IF_DSD_AND, Next = ')'; + p->Nodes[i].Type = IFN_DSD_AND, Next = ')'; else if ( pStr[k+2] == '[' ) - p->Nodes[i].Type = IF_DSD_XOR, Next = ']'; + p->Nodes[i].Type = IFN_DSD_XOR, Next = ']'; else if ( pStr[k+2] == '<' ) - p->Nodes[i].Type = IF_DSD_MUX, Next = '>'; + p->Nodes[i].Type = IFN_DSD_MUX, Next = '>'; else if ( pStr[k+2] == '{' ) - p->Nodes[i].Type = IF_DSD_PRIME, Next = '}'; + p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}'; else - return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i ); + return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal \'%c\'.\n", 'a' + i ); for ( n = k + 3; pStr[n]; n++ ) if ( pStr[n] == Next ) break; if ( pStr[n] == 0 ) - return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i ); + return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal \'%c\'.\n", 'a' + i ); nFans = n - k - 3; if ( nFans < 1 || nFans > 8 ) - return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i ); + return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal \'%c\'.\n", 'a' + i ); for ( f = 0; f < nFans; f++ ) { iFan = pStr[k + 3 + f] - 'a'; @@ -298,8 +420,11 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p ) } p->Nodes[i].nFanins = nFans; } - // truth tables - Abc_TtElemInit2( p->pTtElems, p->nInps ); + return 1; +} +void Ifn_NtkParseConstraints( char * pStr, Ifn_Ntk_t * p ) +{ + int i, k; // parse constraints p->nConstr = 0; for ( i = 0; i < p->nInps; i++ ) @@ -311,17 +436,265 @@ int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p ) } // if ( p->nConstr ) // printf( "Total constraints = %d\n", p->nConstr ); - return 1; } + Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) { Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 ); - if ( Ifn_NtkParseInt( pStr, p ) ) - return p; - ABC_FREE( p ); - return NULL; + if ( Ifn_ManStrType2(pStr) ) + { + if ( !Ifn_NtkParseInt2( pStr, p ) ) + { + ABC_FREE( p ); + return NULL; + } + } + else + { + if ( !Ifn_NtkParseInt( pStr, p ) ) + { + ABC_FREE( p ); + return NULL; + } + } + Ifn_NtkParseConstraints( pStr, p ); + Abc_TtElemInit2( p->pTtElems, p->nInps ); + printf( "Finished parsing: " ); Ifn_NtkPrint(p); + return p; } + + +/**Function************************************************************* + + Synopsis [Derive AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + int i, k, iLit, * pVarMap = ABC_FALLOC( int, p->nParsVIni ); + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( "model" ); + Gia_ManHashStart( pNew ); + for ( i = 0; i < p->nInps; i++ ) + pVarMap[i] = Gia_ManAppendCi(pNew); + for ( i = p->nObjs; i < p->nParsVIni; i++ ) + pVarMap[i] = Gia_ManAppendCi(pNew); + for ( i = p->nInps; i < p->nObjs; i++ ) + { + int Type = p->Nodes[i].Type; + int nFans = p->Nodes[i].nFanins; + int * pFans = p->Nodes[i].Fanins; + int iFanin = p->Nodes[i].iFirst; + if ( Type == IFN_DSD_AND ) + { + iLit = 1; + for ( k = 0; k < nFans; k++ ) + iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] ); + pVarMap[i] = iLit; + } + else if ( Type == IFN_DSD_XOR ) + { + iLit = 0; + for ( k = 0; k < nFans; k++ ) + iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] ); + pVarMap[i] = iLit; + } + else if ( Type == IFN_DSD_MUX ) + { + assert( nFans == 3 ); + pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] ); + } + else if ( Type == IFN_DSD_PRIME ) + { + int n, Step, pVarsData[256]; + int nMints = (1 << nFans); + assert( nFans >= 1 && nFans <= 8 ); + for ( k = 0; k < nMints; k++ ) + pVarsData[k] = pVarMap[iFanin + k]; + for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 ) + for ( n = 0; n < nMints; n += Step << 1 ) + pVarsData[n] = Gia_ManHashMux( pNew, pVarMap[pFans[k]], pVarsData[n+Step], pVarsData[n] ); + assert( Step == nMints ); + pVarMap[i] = pVarsData[0]; + } + else assert( 0 ); + } + Gia_ManAppendCo( pNew, pVarMap[p->nObjs-1] ); + ABC_FREE( pVarMap ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + assert( Gia_ManPiNum(pNew) == p->nParsVIni - (p->nObjs - p->nInps) ); + assert( Gia_ManPoNum(pNew) == 1 ); + return pNew; +} +// compute cofactors w.r.t. the first nIns variables +Gia_Man_t * Ifn_ManStrFindCofactors( int nIns, Gia_Man_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, m, nMints = nIns; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + if ( i >= nIns ) + pObj->Value = Gia_ManAppendCi( pNew ); + for ( m = 0; m < nMints; m++ ) + { + Gia_ManForEachCi( p, pObj, i ) + if ( i < nIns ) + pObj->Value = ((m >> i) & 1); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derive SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + pAig->nRegs = 0; + pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); + Aig_ManStop( pAig ); + return pCnf; +} +sat_solver * Ifn_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars ) +{ + sat_solver * pSat; + Gia_Obj_t * pObj; + Cnf_Dat_t * pCnf; + int i; + pCnf = Cnf_DeriveGiaRemapped( p ); + // start the SAT solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + // add timeframe clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + // inputs/outputs + *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) ); + Gia_ManForEachCi( p, pObj, i ) + Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] ); + *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) ); + Gia_ManForEachCo( p, pObj, i ) + Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] ); + Cnf_DataFree( pCnf ); + return pSat; +} +sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars ) +{ + Gia_Man_t * p1, * p2; + sat_solver * pSat = NULL; + *pvPiVars = *pvPoVars = NULL; + p1 = Ifn_ManStrFindModel( p ); +// Gia_AigerWrite( p1, "satbuild.aig", 0, 0 ); + p2 = Ifn_ManStrFindCofactors( p->nInps, p1 ); + Gia_ManStop( p1 ); +// Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 ); + pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars ); + Gia_ManStop( p2 ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ifn_ManSatPrintPerm( char * pPerms, int nVars ) +{ + int i; + for ( i = 0; i < nVars; i++ ) + printf( "%c", 'a' + pPerms[i] ); + printf( "\n" ); +} +int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nVarsAll, Vec_Int_t * vLits ) +{ + int v, Value, m, mNew, nMints = (1 << nVars); + assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) ); + assert( nVars <= nVarsAll ); + // remap minterms + Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 ); + for ( m = 0; m < nMints; m++ ) + { + mNew = 0; + for ( v = 0; v < nVarsAll; v++ ) + { + assert( pPerm[v] < nVars ); + if ( ((m >> pPerm[v]) & 1) ) + mNew |= (1 << v); + } + assert( Vec_IntEntry(vLits, mNew) == -1 ); + Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) ); + } + // find assumptions + v = 0; + Vec_IntForEachEntry( vLits, Value, m ) + if ( Value >= 0 ) + Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) ); + Vec_IntShrink( vLits, v ); + // run SAT solver + Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + return (int)(Value == l_True); +} +void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues ) +{ + int i, iVar; + Vec_IntClear( vValues ); + Vec_IntForEachEntry( vPiVars, iVar, i ) + Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); +} +int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, Vec_Int_t * vValues ) +{ + // extract permutation + int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE]; + for ( i = 0; i < Vec_IntSize(vPiVars); i++ ) + { + pPerm[i] = Abc_TtGetHex( &Perm, i ); + assert( pPerm[i] < nVars ); + } + // perform SAT check + RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, Vec_IntSize(vPiVars), vValues ); + Vec_IntClear( vValues ); + if ( RetValue == 0 ) + return 0; + Ifn_ManSatDeriveOne( pSat, vPiVars, vValues ); + return 1; +} + + /**Function************************************************************* Synopsis [Derive truth table given the configulation values.] @@ -353,24 +726,24 @@ word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues ) int nFans = p->Nodes[i].nFanins; int * pFans = p->Nodes[i].Fanins; word * pTruth = Ifn_ObjTruth( p, i ); - if ( p->Nodes[i].Type == IF_DSD_AND ) + if ( p->Nodes[i].Type == IFN_DSD_AND ) { Abc_TtFill( pTruth, p->nWords ); for ( f = 0; f < nFans; f++ ) Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 ); } - else if ( p->Nodes[i].Type == IF_DSD_XOR ) + else if ( p->Nodes[i].Type == IFN_DSD_XOR ) { Abc_TtClear( pTruth, p->nWords ); for ( f = 0; f < nFans; f++ ) Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 ); } - else if ( p->Nodes[i].Type == IF_DSD_MUX ) + else if ( p->Nodes[i].Type == IFN_DSD_MUX ) { assert( nFans == 3 ); Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords ); } - else if ( p->Nodes[i].Type == IF_DSD_PRIME ) + else if ( p->Nodes[i].Type == IFN_DSD_PRIME ) { int nValues = (1 << nFans); word * pTemp = Ifn_ObjTruth(p, p->nObjs); @@ -573,7 +946,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat ) { int nFans = p->Nodes[i].nFanins; int * pFans = p->Nodes[i].Fanins; - if ( p->Nodes[i].Type == IF_DSD_AND ) + if ( p->Nodes[i].Type == IFN_DSD_AND ) { nLits = 0; pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 ); @@ -590,7 +963,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat ) if ( !Ifn_AddClause( pSat, pLits, pLits + nLits ) ) return 0; } - else if ( p->Nodes[i].Type == IF_DSD_XOR ) + else if ( p->Nodes[i].Type == IFN_DSD_XOR ) { int m, nMints = (1 << (nFans+1)); for ( m = 0; m < nMints; m++ ) @@ -609,7 +982,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat ) return 0; } } - else if ( p->Nodes[i].Type == IF_DSD_MUX ) + else if ( p->Nodes[i].Type == IFN_DSD_MUX ) { pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 ); pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl @@ -635,7 +1008,7 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat ) if ( !Ifn_AddClause( pSat, pLits, pLits + 3 ) ) return 0; } - else if ( p->Nodes[i].Type == IF_DSD_PRIME ) + else if ( p->Nodes[i].Type == IFN_DSD_PRIME ) { int nValues = (1 << nFans); int iParStart = p->Nodes[i].iFirst; @@ -704,7 +1077,7 @@ void Ifn_SatPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat ) for ( v = p->nObjs; v < p->nPars; v++ ) { for ( i = p->nInps; i < p->nObjs; i++ ) - if ( p->Nodes[i].Type == IF_DSD_PRIME && (int)p->Nodes[i].iFirst == v ) + if ( p->Nodes[i].Type == IFN_DSD_PRIME && (int)p->Nodes[i].iFirst == v ) break; if ( i < p->nObjs ) printf( " " ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index 98883748..fbabdbe8 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1011,6 +1011,75 @@ static inline int Abc_Tt6SupportAndSize( word t, int nVars, int * pSuppSize ) return Supp; } +/**Function************************************************************* + + Synopsis [Checks if there is a var whose both cofs have supp <= nSuppLim.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCheckCondDep2( word * pTruth, int nVars, int nSuppLim ) +{ + int v, d, nWords = Abc_TtWordNum(nVars); + if ( nVars <= nSuppLim + 1 ) + return 0; + for ( v = 0; v < nVars; v++ ) + { + int nDep0 = 0, nDep1 = 0; + for ( d = 0; d < nVars; d++ ) + { + if ( v == d ) + continue; + if ( v < d ) + { + nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 0, 2 ); + nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, v, d, 1, 3 ); + } + else // if ( v > d ) + { + nDep0 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 0, 1 ); + nDep1 += !Abc_TtCheckEqualCofs( pTruth, nWords, d, v, 2, 3 ); + } + if ( nDep0 > nSuppLim || nDep1 > nSuppLim ) + break; + } + if ( d == nVars ) + return v; + } + return nVars; +} +static inline int Abc_TtCheckCondDep( word * pTruth, int nVars, int nSuppLim ) +{ + int nVarsMax = 12; + word Cof0[64], Cof1[64]; // pow( 2, nVarsMax-6 ) + int v, d, nWords = Abc_TtWordNum(nVars); + assert( nVars <= nVarsMax ); + if ( nVars <= nSuppLim + 1 ) + return 0; + for ( v = 0; v < nVars; v++ ) + { + int nDep0 = 0, nDep1 = 0; + Abc_TtCofactor0p( Cof0, pTruth, nWords, v ); + Abc_TtCofactor1p( Cof1, pTruth, nWords, v ); + for ( d = 0; d < nVars; d++ ) + { + if ( v == d ) + continue; + nDep0 += Abc_TtHasVar( Cof0, nVars, d ); + nDep1 += Abc_TtHasVar( Cof1, nVars, d ); + if ( nDep0 > nSuppLim || nDep1 > nSuppLim ) + break; + } + if ( d == nVars ) + return v; + } + return nVars; +} + /**Function************************************************************* -- cgit v1.2.3