diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index f9b02fdac..653618c59 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -643,12 +643,15 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp ) SeeAlso [] ***********************************************************************/ -sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat ) +sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat1, sat_solver ** ppSat2, sat_solver ** ppSat3 ) { int i, k, iObj, status, nVars = 2; +// int i, k, iObj, status, nVars = 1; Vec_Int_t * vLits = Vec_IntAlloc( 16 ); sat_solver * pSat = sat_solver_new(); - if ( ppSat ) *ppSat = sat_solver_new(); + if ( ppSat1 ) *ppSat1 = sat_solver_new(); + if ( ppSat2 ) *ppSat2 = sat_solver_new(); + if ( ppSat3 ) *ppSat3 = sat_solver_new(); // assign SAT variable numbers Vec_IntWriteEntry( vMap, iCoObjId, nVars++ ); Vec_IntForEachEntry( vSupp, iObj, k ) @@ -656,9 +659,13 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_ Vec_IntForEachEntry( vAnds, iObj, k ) if ( pCnf->pObj2Clause[iObj] != -1 ) Vec_IntWriteEntry( vMap, iObj, nVars++ ); +// Vec_IntForEachEntry( vSupp, iObj, k ) +// Vec_IntWriteEntry( vMap, iObj, nVars++ ); // create clauses for the internal nodes and for the output sat_solver_setnvars( pSat, nVars ); - if ( ppSat ) sat_solver_setnvars( *ppSat, nVars ); + if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars ); + if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars ); + if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars ); Vec_IntPush( vAnds, iCoObjId ); Vec_IntForEachEntry( vAnds, iObj, k ) { @@ -676,7 +683,9 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); assert( status ); (void) status; - if ( ppSat ) sat_solver_addclause( *ppSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); } } Vec_IntPop( vAnds ); @@ -696,15 +705,15 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_ SeeAlso [] ***********************************************************************/ -Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp ) +Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose ) { Vec_Str_t * vSop; abctime clk = Abc_Clock(); - extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); Gia_Man_t * pGia = Gia_ManDupCones( p, &iCo, 1, 1 ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) ); - vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + vSop = Bmc_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); if ( vSop == NULL ) return NULL; @@ -718,13 +727,15 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return vSop; } -Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap ) +Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose ) { Vec_Str_t * vSop; - sat_solver * pSat, * pSat2 = NULL; + sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL; Gia_Obj_t * pObj; abctime clk = Abc_Clock(); - extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) ); Vec_Int_t * vAnds = Vec_IntAlloc( 100 ); Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 ); @@ -733,13 +744,18 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu Gia_ManIncrementTravId( p ); Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds ); assert( Vec_IntSize(vAnds) > 0 ); - pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 ); +// pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 ); + pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL ); Vec_IntFree( vSuppObjs ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) ); - vSop = Bmc_CollapseOne_int( pSat, pSat2, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); +// vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); +// vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); sat_solver_delete( pSat ); - sat_solver_delete( pSat2 ); + if ( pSat1 ) sat_solver_delete( pSat1 ); + if ( pSat2 ) sat_solver_delete( pSat2 ); + if ( pSat3 ) sat_solver_delete( pSat3 ); Vec_IntFree( vAnds ); if ( vSop == NULL ) return NULL; @@ -794,8 +810,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 ); continue; } -// vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp ); - vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp, vMap ); + vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose ); +// vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose ); if ( vSop == NULL ) goto finish; assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) ); diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 57138fce3..fbff76795 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -396,17 +396,17 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * Vec_IntWriteEntry( vLits, k, -1 ); // put into new array Vec_IntClear( vTemp ); + if ( fOnOffSetLit >= 0 ) + Vec_IntPush( vTemp, fOnOffSetLit ); Vec_IntForEachEntry( vLits, iLit, n ) if ( iLit != -1 ) Vec_IntPush( vTemp, iLit ); // check against offset - if ( fOnOffSetLit >= 0 ) - Vec_IntPush( vTemp, fOnOffSetLit ); if ( fProfile ) clk = Abc_Clock(); status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); if ( fProfile ) clkCheck2 += Abc_Clock() - clk; - if ( fOnOffSetLit >= 0 ) - Vec_IntPop( vTemp ); +// if ( fOnOffSetLit >= 0 ) +// Vec_IntPop( vTemp ); if ( status == l_Undef ) return -1; if ( status == l_True ) @@ -477,6 +477,105 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit return 0; } +int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ) +{ + // perform one quick reduction if it is non-canonical + if ( !fCanon ) + { + int i, k, iLit, j, iNum, status, nFinal, * pFinal; + + // check against offset + if ( fOnOffSetLit >= 0 ) + Vec_IntPush( vLits, fOnOffSetLit ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); + if ( fOnOffSetLit >= 0 ) + Vec_IntPop( vLits ); + if ( status == l_Undef ) + return -1; + assert( status == l_False ); + + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + Vec_IntClear( vNums ); + Vec_IntClear( vTemp ); + if ( fOnOffSetLit >= 0 ) + { + //Vec_IntPush( vNums, -1 ); + Vec_IntPush( vTemp, fOnOffSetLit ); + } + Vec_IntForEachEntry( vLits, iLit, i ) + { + for ( k = 0; k < nFinal; k++ ) + if ( iLit == Abc_LitNot(pFinal[k]) ) + break; + if ( k == nFinal ) + continue; + Vec_IntPush( vNums, i ); + Vec_IntPush( vTemp, iLit ); + } + + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -1; + assert( status == l_False ); + + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + j = 0; + Vec_IntForEachEntry( vTemp, iLit, i ) + { + if ( iLit == fOnOffSetLit ) + continue; + for ( k = 0; k < nFinal; k++ ) + if ( iLit == Abc_LitNot(pFinal[k]) ) + break; + if ( k == nFinal ) + continue; + Vec_IntWriteEntry( vNums, j++, Vec_IntEntry(vNums, i) ); + } + Vec_IntShrink( vNums, j ); + + + // try removing each literal + for ( i = 0; i < Vec_IntSize(vNums); i++ ) + { + Vec_IntClear( vTemp ); + if ( fOnOffSetLit >= 0 ) + Vec_IntPush( vTemp, fOnOffSetLit ); + Vec_IntForEachEntry( vNums, iNum, k ) + if ( k != i ) + Vec_IntPush( vTemp, Vec_IntEntry(vLits, iNum) ); + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -1; + if ( status == l_True ) + continue; + // remove literal + Vec_IntDrop( vNums, i ); + i--; + } + } + else + { + Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + } +/* + { + // put into new array + int i, iLit; + Vec_IntClear( vNums ); + Vec_IntForEachEntry( vLits, iLit, i ) + if ( iLit != -1 ) + Vec_IntPush( vNums, i ); + //printf( "%d(%d) ", Vec_IntSize(vNums), Vec_IntSize(vLits) ); + } +*/ + return 0; +} + /**Function************************************************************* Synopsis [Returns SAT solver in the 'sat' state with the given assignment.] @@ -658,8 +757,8 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f else Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); } - if ( fVerbose ) - printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start ); + //if ( fVerbose ) + // printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start ); Count++; // add cube status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) ); @@ -687,7 +786,7 @@ cleanup: Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars ); return vSop; } -Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { Vec_Str_t * vSopOn, * vSopOff; int nCubesOn = ABC_INFINITY; @@ -728,13 +827,11 @@ Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa SeeAlso [] ***********************************************************************/ -Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat0, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { int fVeryVerbose = fVerbose; - int nVars = Gia_ManCiNum(p); - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); - sat_solver * pSat[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) }; - sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) }; + sat_solver * pSat[2] = { pSat0, pSat1 }; + sat_solver * pSatClean[2] = { pSat2, pSat3 }; Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) }; Vec_Int_t * vVars = Vec_IntAlloc( nVars ); @@ -746,7 +843,8 @@ Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa int fComplete[2] = {0}; // collect CI variables - iCiVarBeg = pCnf->nVars - nVars;// - 1; +// iCiVarBeg = pCnf->nVars - nVars;// - 1; + iCiVarBeg = sat_solver_nvars(pSat0) - nVars; if ( fReverse ) for ( v = nVars - 1; v >= 0; v-- ) Vec_IntPush( vVars, iCiVarBeg + v ); @@ -855,11 +953,6 @@ cleanup: Vec_IntFree( vLitsC[1] ); Vec_IntFree( vNums ); Vec_IntFree( vCube ); - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat[0] ); - sat_solver_delete( pSat[1] ); - sat_solver_delete( pSatClean[0] ); - sat_solver_delete( pSatClean[1] ); assert( !fComplete[0] || !fComplete[1] ); if ( fComplete[0] || fComplete[1] ) // one of the cover is computed { @@ -892,167 +985,18 @@ cleanup: Vec_StrFreeP( &vSop[1] ); return vRes; } - -/**Function************************************************************* - - Synopsis [This code computes on-set and off-set simultaneously.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) -{ - int fVeryVerbose = fVerbose; - Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; - Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 ); - Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 ); - Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 ); - Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 ); - int n, v, iVar, pLits[2], iCube = 0, Start, status; - abctime clk = 0, Time[2][2] = {{0}}; - int fComplete[2] = {0}; - // variables - int iOutVar = 2; - int iOOVars[2] = {0, 1}; -// int iOutVar = 1; -// int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1}; - - // collect CI variables (0 = onset enable, 1 = offset enable, 2 = output) - int iCiVarBeg = 3; -// int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars; - if ( fReverse ) - for ( v = nVars - 1; v >= 0; v-- ) - Vec_IntPush( vVars, iCiVarBeg + v ); - else - for ( v = 0; v < nVars; v++ ) - Vec_IntPush( vVars, iCiVarBeg + v ); - - // check that on-set/off-set is sat - for ( n = 0; n < 2; n++ ) - { - pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0 - status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 ); - if ( status == l_Undef ) - goto cleanup; // timeout - if ( status == l_False ) - { - Vec_StrClear( vSop[0] ); - Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" ); - Vec_StrPush( vSop[0], '\0' ); - fComplete[0] = 1; - goto cleanup; // const0/1 - } - // start cover - Vec_StrPush( vSop[n], '\0' ); - } - - // compute cube pairs - for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ ) - { - for ( n = 0; n < 2; n++ ) - { - if ( fVeryVerbose ) clk = Abc_Clock(); - // get the assignment - sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); - pLits[0] = Abc_Var2Lit( iOutVar, n ); // set output - pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses - status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); - if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk; - if ( status == l_Undef ) - goto cleanup; // timeout - if ( status == l_False ) - { - fComplete[n] = 1; - break; - } - // collect values - Vec_IntClear( vLits ); - Vec_IntForEachEntry( vVars, iVar, v ) - Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) ); - // expand the values - if ( fVeryVerbose ) clk = Abc_Clock(); - status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); - if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk; - if ( status < 0 ) - goto cleanup; // timeout - // collect cube - Vec_StrPop( vSop[n] ); - Start = Vec_StrSize( vSop[n] ); - Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' ); - Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' ); - Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') ); - Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' ); - Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' ); - Vec_IntClear( vCube ); - Vec_IntForEachEntry( vNums, iVar, v ) - { - int iLit = Vec_IntEntry( vLits, iVar ); - Vec_IntPush( vCube, Abc_LitNot(iLit) ); - if ( fReverse ) - Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) ); - else - Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); - } - // add cube - Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); - status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); - if ( status == 0 ) - { - fComplete[n] = 1; - break; - } - assert( status == 1 ); - } - if ( fComplete[0] || fComplete[1] ) - break; - } -cleanup: - Vec_IntFree( vVars ); - Vec_IntFree( vLits ); - Vec_IntFree( vNums ); - Vec_IntFree( vCube ); - assert( !fComplete[0] || !fComplete[1] ); - if ( fComplete[0] || fComplete[1] ) // one of the cover is computed - { - vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL; - if ( iCube > 1 ) -// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); - Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); - } - if ( fVeryVerbose ) - { - int fProfile = 0; - printf( "Processed output with %d supp vars. ", nVars ); - if ( vRes == NULL ) - printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim ); - else - printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) ); - Abc_PrintTime( 1, "Onset minterm", Time[0][0] ); - Abc_PrintTime( 1, "Onset expand ", Time[0][1] ); - Abc_PrintTime( 1, "Offset minterm", Time[1][0] ); - Abc_PrintTime( 1, "Offset expand ", Time[1][1] ); - if ( fProfile ) - { - Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0; - Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0; - Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0; - Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0; - } - } - Vec_StrFreeP( &vSop[0] ); - Vec_StrFreeP( &vSop[1] ); - return vRes; -} -Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); - sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); - Vec_Str_t * vSop = Bmc_CollapseOne_int2( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); - sat_solver_delete( pSat ); + sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + sat_solver * pSat3 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + Vec_Str_t * vSop = Bmc_CollapseOne_int3( pSat0, pSat1, pSat2, pSat3, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + sat_solver_delete( pSat0 ); + sat_solver_delete( pSat1 ); + sat_solver_delete( pSat2 ); + sat_solver_delete( pSat3 ); Cnf_DataFree( pCnf ); return vSop; } @@ -1069,7 +1013,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan SeeAlso [] ***********************************************************************/ -Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { int fVeryVerbose = fVerbose; sat_solver * pSat[2] = { pSat1, pSat2 }; @@ -1220,6 +1164,171 @@ cleanup: return vRes; } + +/**Function************************************************************* + + Synopsis [This code computes on-set and off-set simultaneously.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +{ + int fVeryVerbose = fVerbose; + Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL; + Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 ); + Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 ); + Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 ); + Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 ); + int n, v, iVar, pLits[2], iCube = 0, Start, status; + abctime clk = 0, Time[2][2] = {{0}}; + int fComplete[2] = {0}; + // variables + int iOutVar = 2; + int iOOVars[2] = {0, 1}; +// int iOutVar = 1; +// int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1}; + + // collect CI variables (0 = onset enable, 1 = offset enable, 2 = output) + int iCiVarBeg = 3; +// int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars; + if ( fReverse ) + for ( v = nVars - 1; v >= 0; v-- ) + Vec_IntPush( vVars, iCiVarBeg + v ); + else + for ( v = 0; v < nVars; v++ ) + Vec_IntPush( vVars, iCiVarBeg + v ); + + // check that on-set/off-set is sat + for ( n = 0; n < 2; n++ ) + { + pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0 + status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + goto cleanup; // timeout + if ( status == l_False ) + { + Vec_StrClear( vSop[0] ); + Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" ); + Vec_StrPush( vSop[0], '\0' ); + fComplete[0] = 1; + goto cleanup; // const0/1 + } + // start cover + Vec_StrPush( vSop[n], '\0' ); + } + + // compute cube pairs + for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ ) + { + for ( n = 0; n < 2; n++ ) + { + if ( fVeryVerbose ) clk = Abc_Clock(); + // get the assignment + sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); + pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses + pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output + status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); + if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk; + if ( status == l_Undef ) + goto cleanup; // timeout + if ( status == l_False ) + { + fComplete[n] = 1; + break; + } + // collect values + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vVars, iVar, v ) + Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) ); + // expand the values + if ( fVeryVerbose ) clk = Abc_Clock(); + status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); + if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk; + if ( status < 0 ) + goto cleanup; // timeout + // collect cube + Vec_StrPop( vSop[n] ); + Start = Vec_StrSize( vSop[n] ); + Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' ); + Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' ); + Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') ); + Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' ); + Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' ); + Vec_IntClear( vCube ); + Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) ); + Vec_IntForEachEntry( vNums, iVar, v ) + { + int iLit = Vec_IntEntry( vLits, iVar ); + Vec_IntPush( vCube, Abc_LitNot(iLit) ); + if ( fReverse ) + Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) ); + else + Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); + } + // add cube + status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) ); + if ( status == 0 ) + { + fComplete[n] = 1; + break; + } + assert( status == 1 ); + } + if ( fComplete[0] || fComplete[1] ) + break; + } +cleanup: + Vec_IntFree( vVars ); + Vec_IntFree( vLits ); + Vec_IntFree( vNums ); + Vec_IntFree( vCube ); + assert( !fComplete[0] || !fComplete[1] ); + if ( fComplete[0] || fComplete[1] ) // one of the cover is computed + { + vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL; + if ( iCube > 1 ) +// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); + Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); + } + if ( fVeryVerbose ) + { + int fProfile = 0; + printf( "Processed output with %d supp vars. ", nVars ); + if ( vRes == NULL ) + printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim ); + else + printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) ); + Abc_PrintTime( 1, "Onset minterm", Time[0][0] ); + Abc_PrintTime( 1, "Onset expand ", Time[0][1] ); + Abc_PrintTime( 1, "Offset minterm", Time[1][0] ); + Abc_PrintTime( 1, "Offset expand ", Time[1][1] ); + if ( fProfile ) + { + Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0; + Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0; + Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0; + Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0; + } + } + Vec_StrFreeP( &vSop[0] ); + Vec_StrFreeP( &vSop[1] ); + return vRes; +} +Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) +{ + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return vSop; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////