diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 7 | ||||
| -rw-r--r-- | src/map/if/if.h | 7 | ||||
| -rw-r--r-- | src/map/if/ifDsd.c | 132 | ||||
| -rw-r--r-- | src/map/if/ifMan.c | 12 | ||||
| -rw-r--r-- | src/map/if/ifMap.c | 26 | ||||
| -rw-r--r-- | src/map/if/ifSat.c | 199 | ||||
| -rw-r--r-- | src/opt/dau/dau.h | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 46 |
8 files changed, 394 insertions, 36 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6db36aa0..b8e41dc0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -974,6 +974,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) { // extern void Dau_DsdTest(); // Dau_DsdTest(); +// extern void If_ManSatTest(); +// If_ManSatTest(); } if ( Sdm_ManCanRead() ) @@ -2274,7 +2276,12 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) // Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); // Abc_Print( -1, "\n" ); if ( fPrintDec )//&&Abc_ObjFaninNum(pObj) <= 6 ) + { + word * pTruthW = (word *)pTruth; + if ( Abc_ObjFaninNum(pObj) < 6 ) + pTruthW[0] = Abc_Tt6Stretch( pTruthW[0], Abc_ObjFaninNum(pObj) ); Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj), 1 ); + } if ( fProfile ) Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) ); else if ( fCofactor ) diff --git a/src/map/if/if.h b/src/map/if/if.h index 41d30da4..13828701 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -55,7 +55,7 @@ ABC_NAMESPACE_HEADER_START // the largest possible user cut cost #define IF_COST_MAX 8191 // ((1<<13)-1) -#define IF_BIG_CHAR 120 +#define IF_BIG_CHAR ((char)120) // object types typedef enum { @@ -233,7 +233,8 @@ struct If_Man_t_ int nCuts5, nCuts5a; If_DsdMan_t * pIfDsdMan; Vec_Mem_t * vTtMem; // truth table memory and hash table - Vec_Int_t * vDsds; // mapping of truth table into DSD + Vec_Int_t * vTtDsds; // mapping of truth table into DSD + Vec_Str_t * vTtPerms; // mapping of truth table into permutations int nBestCutSmall[2]; // timing manager @@ -520,7 +521,7 @@ extern void If_DsdManDump( If_DsdMan_t * p ); extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ); extern void If_DsdManFree( If_DsdMan_t * p ); extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct ); -extern int If_DsdManCheckDec( If_DsdMan_t * pIfMan, int iDsd ); +extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); /*=== ifLib.c =============================================================*/ extern If_LibLut_t * If_LibLutRead( char * FileName ); extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 5c3fecc9..e6c2dfac 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -505,9 +505,10 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId ); if ( *pSpot ) return *pSpot; - if ( truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem)-1 ) + if ( truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) ) { Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits ); + assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 ); Vec_PtrPush( p->vTtDecs, vSets ); // Dau_DecPrintSets( vSets, nLits ); } @@ -533,7 +534,8 @@ void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) ); if ( If_DsdObjType(pObj) == IF_DSD_VAR ) { - int iPermLit = (int)pPermLits[(*pnSupp)++]; + int iPermLit = pPermLits ? (int)pPermLits[*pnSupp] : Abc_Var2Lit(*pnSupp, 0); + (*pnSupp)++; assert( (*pnSupp) <= p->nVars ); Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, fCompl ^ Abc_LitIsCompl(iPermLit) ); return; @@ -589,7 +591,8 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi Abc_TtConst1( pRes, p->nWords ); else if ( pObj->Type == IF_DSD_VAR ) { - int iPermLit = (int)pPermLits[nSupp++]; + int iPermLit = pPermLits ? (int)pPermLits[nSupp] : Abc_Var2Lit(nSupp, 0); + nSupp++; Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) ); } else @@ -923,7 +926,7 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) pSSizes[i] = If_DsdObjSuppSize(pFanin); } // checks if there is a way to package some fanins -int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize ) +int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) { int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; int nFans = If_DsdObjFaninNum(pObj); @@ -953,12 +956,49 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int continue; return (1 << i[0]) | (1 << i[1]) | (1 << i[2]); } + if ( pObj->nFans == 4 ) + return 0; + for ( i[0] = 0; i[0] < nFans; i[0]++ ) + for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ ) + for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ ) + for ( i[3] = i[2]+1; i[3] < nFans; i[3]++ ) + { + SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]] + pSSizes[i[3]]; + SizeOut = pObj->nSupp - SizeIn; + if ( SizeIn > LutSize || SizeOut > LimitOut ) + continue; + return (1 << i[0]) | (1 << i[1]) | (1 << i[2]) | (1 << i[3]); + } return 0; } // checks if there is a way to package some fanins -int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize ) +int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) +{ + int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; + assert( If_DsdObjFaninNum(pObj) == 3 ); + assert( If_DsdObjSuppSize(pObj) > LutSize ); + If_DsdManGetSuppSizes( p, pObj, pSSizes ); + LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1); + assert( LimitOut < LutSize ); + // first input + SizeIn = pSSizes[0] + pSSizes[1]; + SizeOut = pSSizes[2]; + if ( SizeIn <= LutSize && SizeOut <= LimitOut ) + { + return 1; + } + // second input + SizeIn = pSSizes[0] + pSSizes[2]; + SizeOut = pSSizes[1]; + if ( SizeIn <= LutSize && SizeOut <= LimitOut ) + { + return 1; + } + return 0; +} +// checks if there is a way to package some fanins +int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) { - int fVerbose = 0; int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; int truthId = If_DsdObjTruthId( p, pObj ); int nFans = If_DsdObjFaninNum(pObj); @@ -967,10 +1007,10 @@ if ( fVerbose ) printf( "\n" ); if ( fVerbose ) Dau_DecPrintSets( vSets, nFans ); - assert( pObj->nFans > 2 ); + assert( If_DsdObjFaninNum(pObj) > 2 ); assert( If_DsdObjSuppSize(pObj) > LutSize ); If_DsdManGetSuppSizes( p, pObj, pSSizes ); - LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1); + LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1); assert( LimitOut < LutSize ); Vec_IntForEachEntry( vSets, set, i ) { @@ -996,9 +1036,8 @@ Dau_DecPrintSets( vSets, nFans ); } return 0; } -int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize ) +int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) { - int fVerbose = 0; If_DsdObj_t * pObj, * pTemp; int i, Mask; pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) ); if ( fVerbose ) @@ -1022,7 +1061,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize ) If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) ) + if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1034,9 +1073,23 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize ) } } If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) - if ( If_DsdObjType(pTemp) == IF_DSD_PRIME ) + if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize ) + { + if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) + { + if ( fVerbose ) + printf( " " ); + if ( fVerbose ) + Abc_TtPrintBinary( (word *)&Mask, 4 ); + if ( fVerbose ) + printf( " Using multi-input MUX node\n" ); + return 1; + } + } + If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize ) { - if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) ) + if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) { if ( fVerbose ) printf( " " ); @@ -1049,6 +1102,8 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize ) } if ( fVerbose ) printf( " UNDEC\n" ); + +// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); return 0; } int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) @@ -1058,6 +1113,22 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) /**Function************************************************************* + Synopsis [Checks existence of decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) +{ + return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) ); +} + +/**Function************************************************************* + Synopsis [Add the function to the DSD manager.] Description [] @@ -1075,10 +1146,10 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char assert( nLeaves <= DAU_MAX_VAR ); Abc_TtCopy( pCopy, pTruth, p->nWords, 0 ); nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd ); - if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") ) - { +// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") ) +// { // int x = 0; - } +// } if ( nSizeNonDec > 0 ) Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars ); memset( pPerm, 0xFF, nLeaves ); @@ -1096,19 +1167,36 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 ); printf( "\n" ); } - If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) ); - if ( pLutStruct ) + if ( pLutStruct && If_DsdVecObjRef(p->vObjs, Abc_Lit2Var(iDsd)) ) { int LutSize = (int)(pLutStruct[0] - '0'); - assert( pLutStruct[2] == 0 ); - if ( If_DsdManCheckXY( p, iDsd, LutSize ) ) + assert( pLutStruct[2] == 0 ); // XY + if ( !If_DsdManCheckXY( p, iDsd, LutSize, 0 ) ) If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) ); } + If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) ); return iDsd; } -int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) + +/**Function************************************************************* + + Synopsis [Checks existence of decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_DsdManTest() { - return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) ); + Vec_Int_t * vSets; + word t = 0x5277; + t = Abc_Tt6Stretch( t, 4 ); +// word t = 0xD9D900D900D900001010001000100000; + vSets = Dau_DecFindSets( &t, 6 ); + Vec_IntFree( vSets ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index ae7552b3..5025429e 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -86,9 +86,12 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) if ( pPars->fUseDsd ) { p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize ); - p->vDsds = Vec_IntAlloc( 1000 ); - Vec_IntPush( p->vDsds, 0 ); - Vec_IntPush( p->vDsds, 2 ); + p->vTtDsds = Vec_IntAlloc( 1000 ); + Vec_IntPush( p->vTtDsds, 0 ); + Vec_IntPush( p->vTtDsds, 2 ); + p->vTtPerms = Vec_StrAlloc( 10000 ); + Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR ); + Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 ); } // create the constant node p->pConst1 = If_ManSetupObj( p ); @@ -173,7 +176,8 @@ void If_ManStop( If_Man_t * p ) Vec_PtrFreeP( &p->vObjsRev ); Vec_PtrFreeP( &p->vLatchOrder ); Vec_IntFreeP( &p->vLags ); - Vec_IntFreeP( &p->vDsds ); + Vec_IntFreeP( &p->vTtDsds ); + Vec_StrFreeP( &p->vTtPerms ); Vec_MemHashFree( p->vTtMem ); Vec_MemFreeP( &p->vTtMem ); Mem_FixedStop( p->pMemObj, 0 ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 34e83139..c719215f 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -140,7 +140,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep { If_Set_t * pCutSet; If_Cut_t * pCut0, * pCut1, * pCut; - int i, k; + int i, k, v; assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 ); assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 ); @@ -254,20 +254,32 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep if ( p->pPars->fUseDsd ) { int truthId = Abc_Lit2Var(pCut->iCutFunc); - if ( Vec_IntSize(p->vDsds) <= truthId || Vec_IntEntry(p->vDsds, truthId) == -1 ) + if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 ) { pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct ); - while ( Vec_IntSize(p->vDsds) <= truthId ) - Vec_IntPush( p->vDsds, -1 ); - Vec_IntWriteEntry( p->vDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); +// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) ); + while ( Vec_IntSize(p->vTtDsds) <= truthId ) + { + Vec_IntPush( p->vTtDsds, -1 ); + for ( v = 0; v < p->pPars->nLutSize; v++ ) + Vec_StrPush( p->vTtPerms, IF_BIG_CHAR ); + } + Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); + for ( v = 0; v < (int)pCut->nLeaves; v++ ) + Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] ); } else - pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) ); + { + pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) ); + for ( v = 0; v < (int)pCut->nLeaves; v++ ) + pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v ); + } if ( p->pPars->pLutStruct ) { int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ); if ( Value != (int)pCut->fUseless ) - printf( "Difference\n" ); + { + } } } } diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c new file mode 100644 index 00000000..0afe7ea5 --- /dev/null +++ b/src/map/if/ifSat.c @@ -0,0 +1,199 @@ +/**CFile**************************************************************** + + FileName [ifSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [SAT-based evaluation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" +#include "sat/bsat/satSolver.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Builds SAT instance for the given structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * If_ManSatBuildXY( int nLutSize ) +{ + int nMintsL = (1 << nLutSize); + int nMintsF = (1 << (2 * nLutSize - 1)); + int nVars = 2 * nMintsL + nMintsF; + int iVarP0 = 0; // LUT0 parameters (total nMintsL) + int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL) + int m,iVarM = 2 * nMintsL; // MUX vars (total nMintsF) + sat_solver * p = sat_solver_new(); + sat_solver_setnvars( p, nVars ); + for ( m = 0; m < nMintsF; m++ ) + sat_solver_add_mux( p, iVarP0 + m % nMintsL, iVarP1 + 2 * (m / nMintsL) + 1, iVarP1 + 2 * (m / nMintsL), iVarM + m ); + return p; +} + +/**Function************************************************************* + + Synopsis [Returns config string for the given truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ) +{ + int iBSet, nBSet = 0; + int iSSet, nSSet = 0; + int iFSet, nFSet = 0; + int nMintsL = (1 << nLutSize); + int nMintsF = (1 << (2 * nLutSize - 1)); + int v, Value, m, mNew, nMintsFNew, nMintsLNew; + // collect variable sets + Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet ); + assert( nBSet + nSSet + nFSet == nVars ); + // check variable bounds + assert( nSSet + nBSet <= nLutSize ); + assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 ); + nMintsFNew = (1 << (nLutSize + nSSet + nFSet)); + // remap minterms + Vec_IntFill( vLits, nMintsF, -1 ); + for ( m = 0; m < (1 << nVars); m++ ) + { + mNew = iBSet = iSSet = iFSet = 0; + for ( v = 0; v < nVars; v++ ) + { + Value = ((uSet >> (v << 1)) & 3); + if ( Value == 0 ) // FS + { + if ( ((m >> v) & 1) ) + mNew |= 1 << (nLutSize + nSSet + iFSet); + iFSet++; + } + else if ( Value == 1 ) // BS + { + if ( ((m >> v) & 1) ) + mNew |= 1 << (nSSet + iBSet); + iBSet++; + } + else if ( Value == 3 ) // SS + { + if ( ((m >> v) & 1) ) + { + mNew |= 1 << iSSet; + mNew |= 1 << (nLutSize + iSSet); + } + iSSet++; + } + else assert( Value == 0 ); + } + assert( iBSet == nBSet && iFSet == nFSet ); + assert( Vec_IntEntry(vLits, mNew) == -1 ); + Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) ); + } + // find assumptions + v = 0; + Vec_IntForEachEntry( vLits, Value, m ) + { + printf( "%d", (Value >= 0) ? Value : 2 ); + if ( Value >= 0 ) + Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) ); + } + Vec_IntShrink( vLits, v ); + printf( " %d\n", Vec_IntSize(vLits) ); + // run SAT solver + Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + if ( Value != l_True ) + return 0; + // collect config + assert( nSSet + nBSet <= nLutSize ); + *pTBound = 0; + nMintsLNew = (1 << (nSSet + nBSet)); + for ( m = 0; m < nMintsLNew; m++ ) + if ( sat_solver_var_value(p, m) ) + Abc_TtSetBit( pTBound, m ); + *pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet ); + // collect configs + assert( nSSet + nFSet + 1 <= nLutSize ); + *pTFree = 0; + nMintsLNew = (1 << (nSSet + nFSet + 1)); + for ( m = 0; m < nMintsLNew; m++ ) + if ( sat_solver_var_value(p, nMintsL+m) ) + Abc_TtSetBit( pTFree, m ); + *pTFree = Abc_Tt6Stretch( *pTFree, nSSet + nFSet + 1 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Test procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManSatTest() +{ + int nVars = 6; + int nLutSize = 4; + sat_solver * p = If_ManSatBuildXY( nLutSize ); +// char * pDsd = "(abcdefg)"; +// char * pDsd = "([a!bc]d!e)"; + char * pDsd = "0123456789ABCDEF{abcdef}"; + word * pTruth = Dau_DsdToTruth( pDsd, nVars ); + word uBound, uFree; + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); +// unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6); +// unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4); + unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6); + int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); + assert( RetValue ); + +// Abc_TtPrintBinary( pTruth, nVars ); +// Abc_TtPrintBinary( &uBound, nLutSize ); +// Abc_TtPrintBinary( &uFree, nLutSize ); + + Dau_DsdPrintFromTruth( pTruth, nVars ); + Dau_DsdPrintFromTruth( &uBound, nLutSize ); + Dau_DsdPrintFromTruth( &uFree, nLutSize ); + sat_solver_delete(p); + Vec_IntFree( vLits ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index 2e56899b..051abb7d 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -99,6 +99,7 @@ extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, i /*=== dauNonDsd.c ==========================================================*/ extern Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars ); +extern void Dau_DecSortSet( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree ); extern void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars ); extern void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine ); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 0d46b86b..345bbd28 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -368,6 +368,52 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i assert( Cid ); return 4; } +static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, int iVarE, int iVarZ ) +{ + lit Lits[3]; + int Cid; + assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 ); + + Lits[0] = toLitCond( iVarC, 1 ); + Lits[1] = toLitCond( iVarT, 1 ); + Lits[2] = toLitCond( iVarZ, 0 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarC, 1 ); + Lits[1] = toLitCond( iVarT, 0 ); + Lits[2] = toLitCond( iVarZ, 1 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarC, 0 ); + Lits[1] = toLitCond( iVarE, 1 ); + Lits[2] = toLitCond( iVarZ, 0 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarC, 0 ); + Lits[1] = toLitCond( iVarE, 0 ); + Lits[2] = toLitCond( iVarZ, 1 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + if ( iVarT == iVarE ) + return 4; + + Lits[0] = toLitCond( iVarT, 0 ); + Lits[1] = toLitCond( iVarE, 0 ); + Lits[2] = toLitCond( iVarZ, 1 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarT, 1 ); + Lits[1] = toLitCond( iVarE, 1 ); + Lits[2] = toLitCond( iVarZ, 0 ); + Cid = sat_solver_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 6; +} static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC ) { // F = (a (+) b) * c |