diff options
Diffstat (limited to 'src/opt/sfm/sfmSat.c')
| -rw-r--r-- | src/opt/sfm/sfmSat.c | 59 |
1 files changed, 56 insertions, 3 deletions
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index ed2a53c4..6431cd50 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -27,23 +27,76 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static word s_Truths6[6] = { + ABC_CONST(0xAAAAAAAAAAAAAAAA), + ABC_CONST(0xCCCCCCCCCCCCCCCC), + ABC_CONST(0xF0F0F0F0F0F0F0F0), + ABC_CONST(0xFF00FF00FF00FF00), + ABC_CONST(0xFFFF0000FFFF0000), + ABC_CONST(0xFFFFFFFF00000000) +}; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Takes SAT solver and returns interpolant.] - Description [] + Description [If interpolant does not exist, returns diff SAT variables.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Sfm_CreateSatWindow( Sfm_Ntk_t * p ) +word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit ) { + word uTruth = 0, uCube; + int status, i, Div, iVar, nFinal, * pFinal; + int nVars = sat_solver_nvars(pSatOn); + int iNewLit = Abc_Var2Lit( nVars, 0 ); + while ( 1 ) + { + // find onset minterm + status = sat_solver_solve( pSatOn, &iNewLit, &iNewLit + 1, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return SFM_SAT_UNDEC; + if ( status == l_False ) + return uTruth; + assert( status == l_True ); + // collect literals + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vDivs, Div, i ) + Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) ); + // check against offset + status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return SFM_SAT_UNDEC; + if ( status == l_True ) + { + Vec_IntClear( vDiffs ); + for ( i = 0; i < nVars; i++ ) + Vec_IntPush( vDiffs, sat_solver_var_value(pSatOn, i) ^ sat_solver_var_value(pSatOff, i) ); + return SFM_SAT_SAT; + } + assert( status == l_False ); + // compute cube and add clause + nFinal = sat_solver_final( pSatOff, &pFinal ); + uCube = ~(word)0; + Vec_IntClear( vLits ); + Vec_IntPush( vLits, Abc_LitNot(iNewLit) ); + for ( i = 0; i < nFinal; i++ ) + { + Vec_IntPush( vLits, pFinal[i] ); + iVar = Vec_IntFind( vDivs, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 ); + uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar]; + } + uTruth |= uCube; + sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + } + assert( 0 ); return 0; } |