summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaIf.c3
-rw-r--r--src/map/if/if.h3
-rw-r--r--src/map/if/ifDsd.c99
-rw-r--r--src/map/if/ifMap.c1
-rw-r--r--src/map/if/ifSat.c414
-rw-r--r--src/sat/bsat/satSolver.h64
6 files changed, 420 insertions, 164 deletions
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index a494ca8f..f5982ea4 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1528,8 +1528,7 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
If_Man_t * pIfMan;
If_Par_t * pPars = (If_Par_t *)pp;
// disable cut minimization when GIA strucure is needed
-// if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts )
- if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->pLutStruct )
+ if ( !pPars->fDelayOpt && !pPars->fUserRecLib && ((!pPars->fDeriveLuts && !pPars->fUseDsd) || !pPars->pLutStruct) )
pPars->fCutMin = 0;
// reconstruct GIA according to the hierarchy manager
diff --git a/src/map/if/if.h b/src/map/if/if.h
index cf26c53c..8af5cff3 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -574,7 +574,10 @@ extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, i
extern void If_ManImproveMapping( If_Man_t * p );
/*=== ifSat.c ==========================================================*/
extern void * If_ManSatBuildXY( int nLutSize );
+extern void * If_ManSatBuildXYZ( int nLutSize );
+extern void If_ManSatUnbuild( void * p );
extern int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits );
+extern unsigned If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits );
/*=== ifSeq.c =============================================================*/
extern int If_ManPerformMappingSeq( If_Man_t * p );
/*=== ifTime.c ============================================================*/
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 63341ad3..e916f39e 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -67,6 +67,7 @@ struct If_DsdMan_t_
word ** pTtElems; // elementary TTs
Vec_Mem_t * vTtMem; // truth table memory and hash table
Vec_Ptr_t * vTtDecs; // truth table decompositions
+ void * pSat; // SAT solver
int * pSched[16]; // grey code schedules
int nUniqueHits; // statistics
int nUniqueMisses; // statistics
@@ -207,6 +208,8 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
Vec_MemHashAlloc( p->vTtMem, 10000 );
for ( v = 2; v < nVars; v++ )
p->pSched[v] = Extra_GreyCodeSchedule( v );
+ if ( LutSize )
+ p->pSat = If_ManSatBuildXY( LutSize );
return p;
}
void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
@@ -234,6 +237,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
Vec_IntFreeP( &p->vNexts );
Vec_PtrFreeP( &p->vObjs );
Mem_FlexStop( p->pMem, 0 );
+ If_ManSatUnbuild( p->pSat );
ABC_FREE( p->pStore );
ABC_FREE( p->pBins );
ABC_FREE( p );
@@ -618,6 +622,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
p->pStore = Abc_UtilStrsav( pFileName );
RetValue = fread( &Num, 4, 1, pFile );
p->LutSize = Num;
+ p->pSat = If_ManSatBuildXY( p->LutSize );
RetValue = fread( &Num, 4, 1, pFile );
assert( Num >= 2 );
Vec_PtrFillExtra( p->vObjs, Num, NULL );
@@ -770,7 +775,7 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
}
else
If_DsdManComputeTruth_rec( p, iDsd, pRes, pPermLits, &nSupp );
- assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, Abc_Lit2Var(iDsd)) );
+ assert( nSupp == If_DsdVecLitSuppSize(p->vObjs, iDsd) );
return pRes;
}
@@ -785,74 +790,6 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
SeeAlso []
***********************************************************************/
-int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits )
-{
- If_DsdObj_t * pObj;
- int nChildren = 0, pChildren[DAU_MAX_VAR];
- int i, k, Id, iFanin, fCompl = 0;
- if ( Type == IF_DSD_AND )
- {
- for ( k = 0; k < nLits; k++ )
- {
- pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
- if ( Abc_LitIsCompl(pLits[k]) || If_DsdObjType(pObj) != IF_DSD_AND )
- pChildren[nChildren++] = pLits[k];
- else
- If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
- pChildren[nChildren++] = iFanin;
- }
- If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
- }
- else if ( Type == IF_DSD_XOR )
- {
- for ( k = 0; k < nLits; k++ )
- {
- fCompl ^= Abc_LitIsCompl(pLits[k]);
- pObj = If_DsdVecObj( p->vObjs, Abc_LitRegular(pLits[k]) );
- if ( If_DsdObjType(pObj) != IF_DSD_XOR )
- pChildren[nChildren++] = pLits[k];
- else
- If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
- {
- assert( !Abc_LitIsCompl(iFanin) );
- pChildren[nChildren++] = iFanin;
- }
- }
- If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
- }
- else if ( Type == IF_DSD_MUX )
- {
- if ( Abc_LitIsCompl(pLits[0]) )
- {
- pLits[0] = Abc_LitNot(pLits[0]);
- ABC_SWAP( int, pLits[1], pLits[2] );
- }
- if ( Abc_LitIsCompl(pLits[1]) )
- {
- pLits[1] = Abc_LitNot(pLits[1]);
- pLits[2] = Abc_LitNot(pLits[2]);
- fCompl ^= 1;
- }
- for ( k = 0; k < nLits; k++ )
- pChildren[nChildren++] = pLits[k];
- }
- else assert( 0 );
- // create new graph
- Id = If_DsdObjFindOrAdd( p, Type, pChildren, nChildren, NULL );
- return Abc_Var2Lit( Id, fCompl );
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs DSD operation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts )
{
int i, nSSize = 0;
@@ -1290,15 +1227,17 @@ Dau_DecPrintSets( vSets, nFans );
}
return 0;
}
-unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
{
If_DsdObj_t * pObj, * pTemp;
int i, Mask, iFirst;
+/*
if ( 193 == iDsd )
{
int s = 0;
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
}
+*/
pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
if ( fVerbose )
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
@@ -1366,6 +1305,26 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
return 0;
}
+unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
+{
+ unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose );
+/*
+ if ( uSet == 0 )
+ {
+// abctime clk = Abc_Clock();
+ int nVars = If_DsdVecLitSuppSize( p->vObjs, iDsd );
+ word * pRes = If_DsdManComputeTruth( p, iDsd, NULL );
+ uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 );
+ if ( uSet )
+ {
+// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
+// Dau_DecPrintSet( uSet, nVars, 1 );
+ }
+// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+*/
+ return uSet;
+}
/**Function*************************************************************
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 5c23c1b6..959455ae 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -223,7 +223,6 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
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 );
-// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
while ( Vec_IntSize(p->vTtDsds) <= truthId )
{
Vec_IntPush( p->vTtDsds, -1 );
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index cfce7369..a0fc5737 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -53,9 +53,61 @@ void * If_ManSatBuildXY( int nLutSize )
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 );
+ sat_solver_add_mux( p,
+ iVarP0 + m % nMintsL,
+ iVarP1 + 2 * (m / nMintsL) + 1,
+ iVarP1 + 2 * (m / nMintsL),
+ iVarM + m );
return p;
}
+void * If_ManSatBuildXYZ( int nLutSize )
+{
+ int nMintsL = (1 << nLutSize);
+ int nMintsF = (1 << (3 * nLutSize - 2));
+ int nVars = 3 * nMintsL + nMintsF;
+ int iVarP0 = 0; // LUT0 parameters (total nMintsL)
+ int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
+ int iVarP2 = 2 * nMintsL; // LUT2 parameters (total nMintsL)
+ int m,iVarM = 3 * 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_mux41( p,
+ iVarP0 + m % nMintsL,
+ iVarP1 + (m >> nLutSize) % nMintsL,
+ iVarP2 + 4 * (m >> (2 * nLutSize)) + 0,
+ iVarP2 + 4 * (m >> (2 * nLutSize)) + 1,
+ iVarP2 + 4 * (m >> (2 * nLutSize)) + 2,
+ iVarP2 + 4 * (m >> (2 * nLutSize)) + 3,
+ iVarM + m );
+ return p;
+}
+void * If_ManSatBuild55()
+{
+ int nMintsL = 16;
+ int nMintsF = 512;
+ 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++ )
+ {
+ int iVar0 = (((m >> 2) & 7) << 1) | ((m & 3) == 3);
+ int iVar1 = ((m >> 6) & 7);
+ if ( (m >> 5) & 1 )
+ sat_solver_add_mux( p, iVarP0 + iVar0, iVarP1 + 2 * iVar1 + 1, iVarP1 + 2 * iVar1, iVarM + m );
+ else
+ sat_solver_add_buffer( p, iVarP1 + 2 * iVar1, iVarM + m, 0 );
+ }
+ return p;
+}
+void If_ManSatUnbuild( void * p )
+{
+ if ( p )
+ sat_solver_delete( (sat_solver *)p );
+}
/**Function*************************************************************
@@ -183,48 +235,269 @@ int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsig
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 << (1 + nSSet + nFSet));
- for ( m = 0; m < nMintsLNew; m++ )
- if ( sat_solver_var_value(p, nMintsL+m) )
- Abc_TtSetBit( pTFree, m );
- *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
- if ( nVars != 6 )
- return 1;
- // verify the result
- Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
- if ( pTruth[0] != Res )
+ if ( pTBound && pTFree )
{
- Dau_DsdPrintFromTruth( pTruth, nVars );
- Dau_DsdPrintFromTruth( &Res, nVars );
- Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
- Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
- printf( "Verification failed!\n" );
+ // 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 << (1 + nSSet + nFSet));
+ for ( m = 0; m < nMintsLNew; m++ )
+ if ( sat_solver_var_value(p, nMintsL+m) )
+ Abc_TtSetBit( pTFree, m );
+ *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
+ if ( nVars != 6 || nLutSize != 4 )
+ return 1;
+ // verify the result
+ Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
+ if ( pTruth[0] != Res )
+ {
+ Dau_DsdPrintFromTruth( pTruth, nVars );
+ Dau_DsdPrintFromTruth( &Res, nVars );
+ Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
+ Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
+ printf( "Verification failed!\n" );
+ }
}
-/*
- else
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns config string for the given truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned If_ManSatCheckXYall_int( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits )
+{
+ unsigned uSet = 0;
+ int nTotal = 2 * nLutSize - 1;
+ int nShared = nTotal - nVars;
+ int i[6], s[4];
+ assert( nLutSize >= 2 && nLutSize <= 6 );
+ assert( nLutSize < nVars && nVars <= nTotal );
+ assert( nShared >= 0 && nShared < nLutSize - 1 );
+ if ( nLutSize == 2 )
{
-// Kit_DsdPrintFromTruth( (unsigned*)pTBound, nSSet+nBSet ); printf( "\n" );
-// Kit_DsdPrintFromTruth( (unsigned*)pTFree, nSSet+nFSet+1 ); printf( "\n" );
-
- Dau_DsdPrintFromTruth( pTruth, nVars );
- Dau_DsdPrintFromTruth( &Res, nVars );
- Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
- Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
- printf( "Verification OK!\n" );
+ assert( nShared == 0 );
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1]));
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
+ return uSet;
+ }
}
-*/
- return 1;
+ else if ( nLutSize == 3 )
+ {
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
+ return uSet;
+ }
+ if ( nShared < 1 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]]));
+ }
+ }
+ else if ( nLutSize == 4 )
+ {
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
+ return uSet;
+ }
+ if ( nShared < 1 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]]));
+ }
+ if ( nShared < 2 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
+ {
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
+ }
+ }
+ }
+ else if ( nLutSize == 5 )
+ {
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
+ return uSet;
+ }
+ if ( nShared < 1 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]]));
+ }
+ if ( nShared < 2 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
+ }
+ if ( nShared < 3 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ {
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
+ for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
+ }
+ }
+ else if ( nLutSize == 6 )
+ {
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
+ return uSet;
+ }
+ if ( nShared < 1 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]]));
+ }
+ if ( nShared < 2 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
+ }
+ if ( nShared < 3 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
+ for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
+ }
+ if ( nShared < 4 )
+ return 0;
+ for ( i[0] = 0; i[0] < nVars; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+ for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+ for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+ for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
+ {
+ uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
+ for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
+ for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
+ for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
+ for ( s[3] = s[1]+1; s[3] < nLutSize; s[3]++ )
+ if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]])), NULL, NULL, vLits) )
+ return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]]));
+ }
+ }
+ return 0;
+}
+unsigned If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits )
+{
+ unsigned uSet = If_ManSatCheckXYall_int( pSat, nLutSize, pTruth, nVars, vLits );
+// Dau_DecPrintSet( uSet, nVars, 1 );
+ return uSet;
}
/**Function*************************************************************
@@ -268,60 +541,19 @@ void If_ManSatTest2()
void If_ManSatTest()
{
- int nVars = 4;
- int nLutSize = 3;
+ int nVars = 6;
+ int nLutSize = 4;
sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
- word t = 0x183C, * pTruth = &t;
- word uBound, uFree;
- unsigned uSet;
- int RetValue;
+// char * pDsd = "(abcdefg)";
+// char * pDsd = "([a!bc]d!e)";
+ char * pDsd = "0123456789ABCDEF{abcdef}";
+ word * pTruth = Dau_DsdToTruth( pDsd, nVars );
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
-
-
- uSet = (3 << 0) | (1 << 2) | (1 << 4);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 0) | (3 << 2) | (1 << 4);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 0) | (1 << 2) | (3 << 4);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
-
-
- uSet = (3 << 0) | (1 << 2) | (1 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 0) | (3 << 2) | (1 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 0) | (1 << 2) | (3 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
-
-
- uSet = (3 << 0) | (1 << 4) | (1 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 0) | (3 << 4) | (1 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 0) | (1 << 4) | (3 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
-
-
- uSet = (3 << 2) | (1 << 4) | (1 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 2) | (3 << 4) | (1 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
- uSet = (1 << 2) | (1 << 4) | (3 << 6);
- RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
- printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
-
- printf( "\n" );
+// 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);
+ uSet = If_ManSatCheckXYall( p, nLutSize, pTruth, nVars, vLits );
+ Dau_DecPrintSet( uSet, nVars, 1 );
sat_solver_delete(p);
Vec_IntFree( vLits );
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 345bbd28..1003d54a 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -414,6 +414,70 @@ static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, i
assert( Cid );
return 6;
}
+static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3, int iVarZ )
+{
+ lit Lits[4];
+ int Cid;
+ assert( iVarC0 >= 0 && iVarC1 >= 0 && iVarD0 >= 0 && iVarD1 >= 0 && iVarD2 >= 0 && iVarD3 >= 0 && iVarZ >= 0 );
+
+ Lits[0] = toLitCond( iVarD0, 1 );
+ Lits[1] = toLitCond( iVarC0, 0 );
+ Lits[2] = toLitCond( iVarC1, 0 );
+ Lits[3] = toLitCond( iVarZ, 0 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarD1, 1 );
+ Lits[1] = toLitCond( iVarC0, 1 );
+ Lits[2] = toLitCond( iVarC1, 0 );
+ Lits[3] = toLitCond( iVarZ, 0 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarD2, 1 );
+ Lits[1] = toLitCond( iVarC0, 0 );
+ Lits[2] = toLitCond( iVarC1, 1 );
+ Lits[3] = toLitCond( iVarZ, 0 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarD3, 1 );
+ Lits[1] = toLitCond( iVarC0, 1 );
+ Lits[2] = toLitCond( iVarC1, 1 );
+ Lits[3] = toLitCond( iVarZ, 0 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+
+ Lits[0] = toLitCond( iVarD0, 0 );
+ Lits[1] = toLitCond( iVarC0, 0 );
+ Lits[2] = toLitCond( iVarC1, 0 );
+ Lits[3] = toLitCond( iVarZ, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarD1, 0 );
+ Lits[1] = toLitCond( iVarC0, 1 );
+ Lits[2] = toLitCond( iVarC1, 0 );
+ Lits[3] = toLitCond( iVarZ, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarD2, 0 );
+ Lits[1] = toLitCond( iVarC0, 0 );
+ Lits[2] = toLitCond( iVarC1, 1 );
+ Lits[3] = toLitCond( iVarZ, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+
+ Lits[0] = toLitCond( iVarD3, 0 );
+ Lits[1] = toLitCond( iVarC0, 1 );
+ Lits[2] = toLitCond( iVarC1, 1 );
+ Lits[3] = toLitCond( iVarZ, 1 );
+ Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+ assert( Cid );
+ return 8;
+}
static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
{
// F = (a (+) b) * c
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-07 23:33:26 +0000