diff options
-rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c | 114 | ||||
-rw-r--r-- | src/sat/bmc/bmcClp.c | 352 |
3 files changed, 457 insertions, 11 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 4ad3e39a..87ce6b91 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1038,6 +1038,8 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ ) #define Gia_ManForEachCiId( p, Id, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((Id) = Gia_ObjId(p, Gia_ManCi(p, i))); i++ ) +#define Gia_ManForEachCiVec( vVec, p, pObj, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManCi(p, Vec_IntEntry(vVec,i))); i++ ) #define Gia_ManForEachCiReverse( p, pObj, i ) \ for ( i = Vec_IntSize(p->vCis) - 1; (i >= 0) && ((pObj) = Gia_ManCi(p, i)); i-- ) #define Gia_ManForEachCo( p, pObj, i ) \ diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index ac7bcdc5..f9b02fda 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -21,6 +21,8 @@ #include "base/abc/abc.h" #include "aig/gia/gia.h" #include "misc/vec/vecWec.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" @@ -535,6 +537,8 @@ extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ); extern int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps ); extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose ); +extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + /**Function************************************************************* Synopsis [Derives GIA for the network.] @@ -622,12 +626,67 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp ) Vec_IntWriteEntry( vSupp, j++, iVar ); Vec_IntShrink( vSupp, j ); Vec_IntFree( vPres ); +// if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) ) +// printf( "Mismatch!!!\n" ); return 1; } /**Function************************************************************* + Synopsis [Derives SAT solver for one output from the shared CNF.] + + Description [] + + SideEffects [] + + 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 ) +{ + int i, k, iObj, status, nVars = 2; + Vec_Int_t * vLits = Vec_IntAlloc( 16 ); + sat_solver * pSat = sat_solver_new(); + if ( ppSat ) *ppSat = sat_solver_new(); + // assign SAT variable numbers + Vec_IntWriteEntry( vMap, iCoObjId, nVars++ ); + Vec_IntForEachEntry( vSupp, iObj, k ) + Vec_IntWriteEntry( vMap, iObj, nVars++ ); + Vec_IntForEachEntry( vAnds, iObj, k ) + if ( pCnf->pObj2Clause[iObj] != -1 ) + 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 ); + Vec_IntPush( vAnds, iCoObjId ); + Vec_IntForEachEntry( vAnds, iObj, k ) + { + int iClaBeg, iClaEnd, * pLit; + if ( pCnf->pObj2Clause[iObj] == -1 ) + continue; + iClaBeg = pCnf->pObj2Clause[iObj]; + iClaEnd = iClaBeg + pCnf->pObj2Count[iObj]; + assert( iClaBeg < iClaEnd ); + for ( i = iClaBeg; i < iClaEnd; i++ ) + { + Vec_IntClear( vLits ); + for ( pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ ) + Vec_IntPush( vLits, Abc_Lit2LitV(Vec_IntArray(vMap), *pLit) ); + 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) ); + } + } + Vec_IntPop( vAnds ); + Vec_IntFree( vLits ); + assert( nVars == sat_solver_nvars(pSat) ); + return pSat; +} + +/**Function************************************************************* + Synopsis [Computes SOPs for each output.] Description [] @@ -651,8 +710,43 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit return NULL; if ( Vec_StrSize(vSop) == 4 ) // constant Vec_IntClear(vSupp); - else - Abc_NtkCollapseCountVars( vSop, vSupp ); +// else +// Abc_NtkCollapseCountVars( vSop, vSupp ); + if ( fVerbose ) + printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); + if ( fVerbose ) + 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 * vSop; + sat_solver * pSat, * pSat2 = 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 ); + int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) ); + Vec_Int_t * vAnds = Vec_IntAlloc( 100 ); + Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 ); + Gia_ManForEachCiVec( vSupp, p, pObj, i ) + Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) ); + Gia_ManIncrementTravId( p ); + Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds ); + assert( Vec_IntSize(vAnds) > 0 ); + pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 ); + 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 ); + sat_solver_delete( pSat ); + sat_solver_delete( pSat2 ); + Vec_IntFree( vAnds ); + if ( vSop == NULL ) + return NULL; + if ( Vec_StrSize(vSop) == 4 ) // constant + Vec_IntClear(vSupp); +// else +// Abc_NtkCollapseCountVars( vSop, vSupp ); if ( fVerbose ) printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); if ( fVerbose ) @@ -667,6 +761,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v Vec_Int_t * vReprs, * vClass, * vReprSuppSizes; int i, k, Entry, iCo, * pOrder; Vec_Wec_t * vClasses; + Cnf_Dat_t * pCnf; + Vec_Int_t * vMap; // derive classes of outputs vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 ); if ( fVerbose ) @@ -682,6 +778,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) ); Vec_IntFree( vReprSuppSizes ); // consider SOPs for representatives + vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 ); vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) ); Extra_ProgressBarUpdate( pProgress, 0, NULL ); @@ -690,7 +788,14 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v int iEntry = pOrder[Vec_IntSize(vReprs) - 1 - i]; int iCoThis = Vec_IntEntry( vReprs, iEntry ); Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis ); - Vec_Str_t * vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp ); + Vec_Str_t * vSop; + if ( Vec_IntSize(vSupp) < 2 ) + { + 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 ); if ( vSop == NULL ) goto finish; assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) ); @@ -699,6 +804,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v Vec_StrFree( vSop ); } Extra_ProgressBarStop( pProgress ); + Cnf_DataFree( pCnf ); + Vec_IntFree( vMap ); // derive SOPs for each output vSops = Vec_PtrStart( Gia_ManCoNum(p) ); Vec_WecForEachLevel ( vClasses, vClass, i ) @@ -787,6 +894,7 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in Vec_IntForEachEntry( vSupp, iCi, k ) Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); pNodeNew->pData = Vec_PtrEntry( vSops, i ); + assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Vec_WecFree( vSupps ); diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index 826c0a32..57138fce 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -355,7 +355,7 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars ) SeeAlso [] ***********************************************************************/ -int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon ) +int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit ) { int fProfile = 0; int k, n, iLit, status; @@ -369,6 +369,7 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * // check if this literal when expanded overlaps with the on-set if ( pSatOn ) { + assert( fOnOffSetLit == -1 ); // it is ok to skip the first round if the literal is positive if ( fCanon && !Abc_LitIsCompl(Save) ) continue; @@ -399,9 +400,13 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * 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 ( status == l_Undef ) return -1; if ( status == l_True ) @@ -428,14 +433,18 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * SeeAlso [] ***********************************************************************/ -int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon ) +int Bmc_CollapseExpand( 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, 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 ); @@ -450,12 +459,12 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit if ( k == nFinal ) Vec_IntWriteEntry( vLits, i, -1 ); } - Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon ); + Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, fOnOffSetLit ); } else { - Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon ); - Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon ); + Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); + Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 ); } { // put into new array @@ -625,7 +634,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f printf( "\n" ); } // expand the values - status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon ); + status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon, -1 ); if ( status < 0 ) { Vec_StrFreeP( &vSop ); @@ -719,7 +728,7 @@ Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa SeeAlso [] ***********************************************************************/ -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 ) { int fVeryVerbose = fVerbose; int nVars = Gia_ManCiNum(p); @@ -805,7 +814,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan } // expand the values if ( fVeryVerbose ) clk = Abc_Clock(); - status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon ); + status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon, -1 ); if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk; if ( status < 0 ) goto cleanup; // timeout @@ -884,6 +893,333 @@ cleanup: 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 ) +{ + 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 ); + Cnf_DataFree( pCnf ); + return vSop; +} + + +/**Function************************************************************* + + Synopsis [This code computes on-set and off-set simultaneously.] + + Description [] + + SideEffects [] + + 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 ) +{ + int fVeryVerbose = fVerbose; + sat_solver * pSat[2] = { pSat1, pSat2 }; + 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[n], 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 + } + // add literals to the solver + status = sat_solver_addclause( pSat[n], pLits, pLits + 1 ); + assert( status ); + // 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[n], 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 ); + status = sat_solver_solve( pSat[n], pLits, pLits + 1, 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[n], iVar)) ); + // expand the values + if ( fVeryVerbose ) clk = Abc_Clock(); +// status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) ); + status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 ); + 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) ); + status = sat_solver_addclause( pSat[n], 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; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |