From 4b0c12eb1e03ac863d09efc643d3253c4bfe3af4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 8 Mar 2014 17:09:20 -0800 Subject: Changes to LUT mappers. --- src/map/if/ifSat.c | 159 ----------------------------------------------------- 1 file changed, 159 deletions(-) (limited to 'src/map/if/ifSat.c') diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 9f4ea631..4af55203 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -82,27 +82,6 @@ void * If_ManSatBuildXYZ( int nLutSize ) 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 ) @@ -268,128 +247,6 @@ int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsig } return 1; } -int If_ManSatCheck55( void * pSat, word * pTruth, int nVars, int * pPerm9, word * pTBound, word * pTFree, Vec_Int_t * vLits ) -{ - sat_solver * p = (sat_solver *)pSat; - int v, Value, m, mNew; - int nMintsL = 16; - // remap minterms - Vec_IntFill( vLits, 512, -1 ); - for ( m = 0; m < (1 << nVars); m++ ) - { - mNew = 0; - for ( v = 0; v < 9; v++ ) - { - assert( pPerm9[v] < nVars ); - if ( ((m >> pPerm9[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(2 * nMintsL + m, !Value) ); - Vec_IntShrink( vLits, v ); - // 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; - if ( pTBound && pTFree ) - { - // collect config - *pTBound = 0; - for ( m = 0; m < nMintsL; m++ ) - if ( sat_solver_var_value(p, m) ) - Abc_TtSetBit( pTBound, m ); - *pTBound = Abc_Tt6Stretch( *pTBound, 4 ); - // collect configs - *pTFree = 0; - for ( m = 0; m < nMintsL; m++ ) - if ( sat_solver_var_value(p, nMintsL+m) ) - Abc_TtSetBit( pTFree, m ); - *pTFree = Abc_Tt6Stretch( *pTFree, 4 ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns config string for the given truth table.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned If_ManSatCheck55all_int( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits ) -{ - int Combs[10][5] = { - {0,1,2,3,4}, - {0,2,1,3,4}, - {0,3,1,2,4}, - {0,4,1,2,3}, - {1,2,0,3,4}, - {1,3,0,2,4}, - {1,4,0,2,3}, - {2,3,0,1,4}, - {2,4,0,1,3}, - {3,4,0,1,2} - }; - int pPerm9[9], Mark[9], i[6], k, n, c; - assert( nVars == 9 || nVars == 8 || nVars == 7 ); - 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]++ ) - { - // add remaining ones - n = 5; - for ( k = 0; k < nVars; k++ ) - Mark[k] = 0; - for ( k = 0; k < 5; k++ ) - Mark[i[k]] = 1; - for ( k = 0; k < nVars; k++ ) - if ( Mark[k] == 0 ) - pPerm9[n++] = k; - assert( n == nVars ); - for ( ; n < 9; n++ ) - pPerm9[n] = pPerm9[n-1]; - assert( n == 9 ); - // current ones - for ( c = 0; c < 10; c++ ) - { - for ( n = 0; n < 5; n++ ) - pPerm9[n] = i[Combs[c][n]]; - // try different combinations - for ( k = 5; k < nVars; k++ ) - { - ABC_SWAP( int, pPerm9[5], pPerm9[k] ); - if ( If_ManSatCheck55(pSat, pTruth, nVars, pPerm9, NULL, NULL, vLits) ) - { -// for ( k = 0; k < 9; k++ ) -// printf( "%c", 'a' + pPerm9[k] ); -// printf( "\n" ); - return 1; - } - ABC_SWAP( int, pPerm9[5], pPerm9[k] ); - } - } - } - return 0; -} -unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits ) -{ -// abctime clk = Abc_Clock(); - unsigned Value = If_ManSatCheck55all_int( pSat, pTruth, nVars, vLits ); -// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - return Value; -} /**Function************************************************************* @@ -680,22 +537,6 @@ void If_ManSatTest3() sat_solver_delete(p); Vec_IntFree( vLits ); } -void If_ManSatTest() -{ - int nVars = 9; - sat_solver * p = (sat_solver *)If_ManSatBuild55(); -// char * pDsd = "[([(ab)cde]f)ghi]"; -// char * pDsd = "[([(hi)cde]f)gab]"; - char * pDsd = "[(0123{(hi)cde}f)gab]"; - word * pTruth = Dau_DsdToTruth( pDsd, nVars ); - Vec_Int_t * vLits = Vec_IntAlloc( 1000 ); - if ( If_ManSatCheck55all( p, pTruth, nVars, vLits ) ) - printf( "Found!\n" ); - else - printf( "Not found!\n" ); - sat_solver_delete(p); - Vec_IntFree( vLits ); -} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3