mirror of https://github.com/YosysHQ/abc.git
Improvements to 'satclp' (unfinished).
This commit is contained in:
Alan Mishchenko
parent
dd365cbaf3
commit
e50fc467fd
|
|
@ -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)) );
|
||||
|
|
|
|||
|
|
@ -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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
Loading…
Reference in New Issue