| /**CFile**************************************************************** | |
| FileName [sbdLut.c] | |
| SystemName [ABC: Logic synthesis and verification system.] | |
| PackageName [SAT-based optimization using internal don't-cares.] | |
| Synopsis [CNF computation.] | |
| Author [Alan Mishchenko] | |
| Affiliation [UC Berkeley] | |
| Date [Ver. 1.0. Started - June 20, 2005.] | |
| Revision [$Id: sbdLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] | |
| ***********************************************************************/ | |
| #include "sbdInt.h" | |
| #include "misc/util/utilTruth.h" | |
| ABC_NAMESPACE_IMPL_START | |
| //////////////////////////////////////////////////////////////////////// | |
| /// DECLARATIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| //////////////////////////////////////////////////////////////////////// | |
| /// FUNCTION DEFINITIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| // count the number of parameter variables in the structure | |
| int Sbd_ProblemCountParams( int nStrs, Sbd_Str_t * pStr0 ) | |
| { | |
| Sbd_Str_t * pStr; int nPars = 0; | |
| for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) | |
| nPars += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns; | |
| return nPars; | |
| } | |
| // add clauses for the structure | |
| int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) | |
| { | |
| // variable order: inputs, structure outputs, parameters | |
| Sbd_Str_t * pStr; | |
| int VarOut = nVars; | |
| int VarPar = nVars + nStrs; | |
| int m, k, n, status, pLits[SBD_SIZE_MAX+2]; | |
| //printf( "Start par = %d. ", VarPar ); | |
| for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ ) | |
| { | |
| if ( pStr->fLut ) | |
| { | |
| int nMints = 1 << pStr->nVarIns; | |
| assert( pStr->nVarIns <= 6 ); | |
| for ( m = 0; m < nMints; m++, VarPar++ ) | |
| { | |
| for ( k = 0; k < pStr->nVarIns; k++ ) | |
| pLits[k] = Abc_Var2Lit( pVars[pStr->VarIns[k]], (m >> k) & 1 ); | |
| for ( n = 0; n < 2; n++ ) | |
| { | |
| pLits[pStr->nVarIns] = Abc_Var2Lit( pVars[VarPar], n ); | |
| pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n ); | |
| status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 ); | |
| if ( !status ) | |
| return 0; | |
| } | |
| } | |
| } | |
| else | |
| { | |
| assert( pStr->nVarIns <= SBD_DIV_MAX ); | |
| for ( k = 0; k < pStr->nVarIns; k++, VarPar++ ) | |
| { | |
| for ( n = 0; n < 2; n++ ) | |
| { | |
| pLits[0] = Abc_Var2Lit( pVars[VarPar], 1 ); | |
| pLits[1] = Abc_Var2Lit( pVars[VarOut], n ); | |
| pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n ); | |
| status = sat_solver_addclause( pSat, pLits, pLits + 3 ); | |
| if ( !status ) | |
| return 0; | |
| } | |
| } | |
| } | |
| } | |
| return 1; | |
| } | |
| void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) | |
| { | |
| Sbd_Str_t * pStr; | |
| int VarPar = nVars + nStrs; | |
| int m, m2, status, pLits[SBD_DIV_MAX]; | |
| // make sure selector parameters are mutually exclusive | |
| for ( pStr = pStr0; pStr < pStr0 + nStrs; VarPar += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns, pStr++ ) | |
| { | |
| if ( pStr->fLut ) | |
| continue; | |
| // one variable should be selected | |
| assert( pStr->nVarIns <= SBD_DIV_MAX ); | |
| for ( m = 0; m < pStr->nVarIns; m++ ) | |
| pLits[m] = Abc_Var2Lit( pVars[VarPar + m], 0 ); | |
| status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns ); | |
| assert( status ); | |
| // two variables cannot be selected | |
| for ( m = 0; m < pStr->nVarIns; m++ ) | |
| for ( m2 = m+1; m2 < pStr->nVarIns; m2++ ) | |
| { | |
| pLits[0] = Abc_Var2Lit( pVars[VarPar + m], 1 ); | |
| pLits[1] = Abc_Var2Lit( pVars[VarPar + m2], 1 ); | |
| status = sat_solver_addclause( pSat, pLits, pLits + 2 ); | |
| assert( status ); | |
| } | |
| } | |
| } | |
| void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits ) | |
| { | |
| Sbd_Str_t * pStr; | |
| int m, nIters, iLit = 0; | |
| printf( "Solution found:\n" ); | |
| for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) | |
| { | |
| nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns; | |
| printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", (int)(pStr-pStr0) ); | |
| for ( m = 0; m < nIters; m++, iLit++ ) | |
| printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) ); | |
| printf( " {" ); | |
| for ( m = 0; m < pStr->nVarIns; m++ ) | |
| printf( " %d", pStr->VarIns[m] ); | |
| printf( " }\n" ); | |
| } | |
| assert( iLit == Vec_IntSize(vLits) ); | |
| } | |
| void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits ) | |
| { | |
| Sbd_Str_t * pStr; | |
| int m, nIters, iLit = 0; | |
| for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) | |
| { | |
| pStr->Res = 0; | |
| if ( pStr->fLut ) | |
| { | |
| nIters = 1 << pStr->nVarIns; | |
| for ( m = 0; m < nIters; m++, iLit++ ) | |
| if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) ) | |
| Abc_TtSetBit( &pStr->Res, m ); | |
| pStr->Res = Abc_Tt6Stretch( pStr->Res, pStr->nVarIns ); | |
| } | |
| else | |
| { | |
| nIters = 0; | |
| for ( m = 0; m < pStr->nVarIns; m++, iLit++ ) | |
| if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) ) | |
| { | |
| pStr->Res = pStr->VarIns[m]; | |
| nIters++; | |
| } | |
| assert( nIters == 1 ); | |
| } | |
| } | |
| assert( iLit == Vec_IntSize(vLits) ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Solves QBF problem for the given window.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors, | |
| int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, | |
| Vec_Int_t * vTfo, Vec_Int_t * vRoots, | |
| Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 ) // divisors, structures | |
| { | |
| extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ); | |
| int fVerbose = 0; | |
| abctime clk = Abc_Clock(); | |
| Vec_Int_t * vLits = Vec_IntAlloc( 100 ); | |
| sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 ); | |
| sat_solver * pSatQbf = sat_solver_new(); | |
| int nVars = Vec_IntSize( vDivSet ); | |
| int nPars = Sbd_ProblemCountParams( nStrs, pStr0 ); | |
| int VarCecOut = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots); | |
| int VarCecPar = VarCecOut + nStrs; | |
| int VarQbfPar = 0; | |
| int VarQbfFree = nPars; | |
| int pVarsCec[256]; | |
| int pVarsQbf[256]; | |
| int i, iVar, iLit, nIters; | |
| int RetValue = 0; | |
| assert( Vec_IntSize(vDivSet) <= SBD_DIV_MAX ); | |
| assert( nVars + nStrs + nPars <= 256 ); | |
| // collect CEC variables | |
| Vec_IntForEachEntry( vDivSet, iVar, i ) | |
| pVarsCec[i] = iVar; | |
| for ( i = 0; i < nStrs; i++ ) | |
| pVarsCec[nVars + i] = VarCecOut + i; | |
| for ( i = 0; i < nPars; i++ ) | |
| pVarsCec[nVars + nStrs + i] = VarCecPar + i; | |
| // collect QBF variables | |
| for ( i = 0; i < nVars + nStrs; i++ ) | |
| pVarsQbf[i] = -1; | |
| for ( i = 0; i < nPars; i++ ) | |
| pVarsQbf[nVars + nStrs + i] = VarQbfPar + i; | |
| // add clauses to the CEC problem | |
| Sbd_ProblemAddClauses( pSatCec, nVars, nStrs, pVarsCec, pStr0 ); | |
| // create QBF solver | |
| sat_solver_setnvars( pSatQbf, 1000 ); | |
| Sbd_ProblemAddClausesInit( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ); | |
| // assume all parameter variables are 0 | |
| Vec_IntClear( vLits ); | |
| for ( i = 0; i < nPars; i++ ) | |
| Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) ); | |
| for ( nIters = 0; nIters < (1 << nVars); nIters++ ) | |
| { | |
| // check if these parameters solve the problem | |
| int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 ); | |
| if ( status == l_False ) // solution found | |
| break; | |
| assert( status == l_True ); | |
| if ( fVerbose ) | |
| { | |
| printf( "Iter %3d : ", nIters ); | |
| for ( i = 0; i < nPars; i++ ) | |
| printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) ); | |
| printf( " " ); | |
| } | |
| Vec_IntClear( vLits ); | |
| // create new QBF variables | |
| for ( i = 0; i < nVars + nStrs; i++ ) | |
| pVarsQbf[i] = VarQbfFree++; | |
| // set their values | |
| Vec_IntForEachEntry( vDivSet, iVar, i ) | |
| { | |
| iLit = Abc_Var2Lit( pVarsQbf[i], !sat_solver_var_value(pSatCec, iVar) ); | |
| status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 ); | |
| assert( status ); | |
| if ( fVerbose ) | |
| printf( "%d", sat_solver_var_value(pSatCec, iVar) ); | |
| } | |
| iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) ); | |
| status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 ); | |
| assert( status ); | |
| if ( fVerbose ) | |
| printf( " %d\n", !sat_solver_var_value(pSatCec, VarCecOut) ); | |
| // add clauses to the QBF problem | |
| if ( !Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ) ) | |
| break; // solution does not exist | |
| // check if solution still exists | |
| status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 ); | |
| if ( status == l_False ) // solution does not exist | |
| break; | |
| assert( status == l_True ); | |
| // find the new values of parameters | |
| assert( Vec_IntSize(vLits) == 0 ); | |
| for ( i = 0; i < nPars; i++ ) | |
| Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, !sat_solver_var_value(pSatQbf, VarQbfPar + i)) ); | |
| } | |
| if ( Vec_IntSize(vLits) > 0 ) | |
| { | |
| //Sbd_ProblemPrintSolution( nStrs, pStr0, vLits ); | |
| Sbd_ProblemCollectSolution( nStrs, pStr0, vLits ); | |
| RetValue = 1; | |
| } | |
| sat_solver_delete( pSatCec ); | |
| sat_solver_delete( pSatQbf ); | |
| Vec_IntFree( vLits ); | |
| if ( fVerbose ) | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| return RetValue; | |
| } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// END OF FILE /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END | |