summaryrefslogtreecommitdiffstats
path: root/src/map/if
diff options
context:
space:
mode:
Diffstat (limited to 'src/map/if')
-rw-r--r--src/map/if/if.h7
-rw-r--r--src/map/if/ifDsd.c132
-rw-r--r--src/map/if/ifMan.c12
-rw-r--r--src/map/if/ifMap.c26
-rw-r--r--src/map/if/ifSat.c199
5 files changed, 340 insertions, 36 deletions
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
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 20:13:25 +0000