luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improvements to 'satclp'.

This commit is contained in:
Alan Mishchenko 2015-11-09 08:33:56 -08:00
parent 236118c0b6
commit 58c2584e2a
4 changed files with 57 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/base/abc/abc.h
View File

@ -600,7 +600,7 @@ extern ABC_DLL int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
/*=== abcCollapse.c ==========================================================*/
extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose );
/*=== abcCut.c ==========================================================*/
extern ABC_DLL void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
extern ABC_DLL void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );

25
src/base/abci/abc.c
View File

@ -3125,17 +3125,18 @@ usage:
int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes;
int nCubeLim = 0;
int nBTLimit = 1000000;
int nCostMax = 20000000;
int fCanon = 0;
int fReverse = 0;
int fVerbose = 0;
int nCubeLim = 0;
int nBTLimit = 1000000;
int nCostMax = 20000000;
int fCanon = 0;
int fReverse = 0;
int fCnfShared = 1;
int fVerbose = 0;
int c;
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CLZcrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CLZcrsvh" ) ) != EOF )
{
switch ( c )
{
@ -3178,6 +3179,9 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fReverse ^= 1;
break;
case 's':
fCnfShared ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -3202,11 +3206,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
@ -3219,13 +3223,14 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: satclp [-CLZ num] [-crvh]\n" );
Abc_Print( -2, "usage: satclp [-CLZ num] [-crsvh]\n" );
Abc_Print( -2, "\t performs SAT based collapsing\n" );
Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-Z num : the limit on the cost of the largest output [default = %d]\n", nCostMax );
Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" );
Abc_Print( -2, "\t-r : toggles using reverse veriable ordering [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-s : toggles shared CNF computation [default = %s]\n", fCnfShared? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

64
src/base/abci/abcCollapse.c
View File

@ -598,9 +598,9 @@ Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk )
***********************************************************************/
#define Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
int Abc_NtkCollapseReduce( Vec_Str_t * vSop, Vec_Int_t * vSupp, Vec_Int_t * vClass, Vec_Wec_t * vSupps )
{
int j = 0, k, iVar, nVars = Vec_IntSize(vSupp);
int j = 0, i, k, iCo, iVar, nVars = Vec_IntSize(vSupp);
char * pCube, * pSop = Vec_StrArray(vSop);
Vec_Int_t * vPres = Vec_IntStart( nVars );
Abc_NtkSopForEachCube( pSop, nVars, pCube )
@ -620,11 +620,15 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
Vec_StrWriteEntry( vSop, j++, '\0' );
Vec_StrShrink( vSop, j );
// reduce support
j = 0;
Vec_IntForEachEntry( vSupp, iVar, k )
if ( Vec_IntEntry(vPres, k) )
Vec_IntWriteEntry( vSupp, j++, iVar );
Vec_IntShrink( vSupp, j );
Vec_IntForEachEntry( vClass, iCo, i )
{
j = 0;
vSupp = Vec_WecEntry( vSupps, iCo );
Vec_IntForEachEntry( vSupp, iVar, k )
if ( Vec_IntEntry(vPres, k) )
Vec_IntWriteEntry( vSupp, j++, iVar );
Vec_IntShrink( vSupp, j );
}
Vec_IntFree( vPres );
// if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) )
// printf( "Mismatch!!!\n" );
@ -705,7 +709,7 @@ 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 fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose )
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_Int_t * vClass, Vec_Wec_t * vSupps )
{
Vec_Str_t * vSop;
abctime clk = Abc_Clock();
@ -719,15 +723,15 @@ 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_NtkCollapseReduce( vSop, vSupp, vClass, vSupps );
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 fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose )
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_Int_t * vClass, Vec_Wec_t * vSupps )
{
Vec_Str_t * vSop;
sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
@ -761,15 +765,15 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu
return NULL;
if ( Vec_StrSize(vSop) == 4 ) // constant
Vec_IntClear(vSupp);
// else
// Abc_NtkCollapseCountVars( vSop, vSupp );
else
Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps );
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_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose )
{
ProgressBar * pProgress;
abctime clk = Abc_Clock();
@ -777,8 +781,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;
Cnf_Dat_t * pCnf = NULL;
Vec_Int_t * vMap = NULL;
// derive classes of outputs
vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
if ( fVerbose )
@ -794,8 +798,11 @@ 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 );
if ( fCnfShared )
{
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 );
@ -810,8 +817,10 @@ 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, fCanon, fReverse, vSupp, i ? 0 : fVerbose );
// vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose );
if ( fCnfShared )
vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps );
else
vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps );
if ( vSop == NULL )
goto finish;
assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
@ -820,8 +829,11 @@ 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 );
if ( fCnfShared )
{
Cnf_DataFree( pCnf );
Vec_IntFree( vMap );
}
// derive SOPs for each output
vSops = Vec_PtrStart( Gia_ManCoNum(p) );
Vec_WecForEachLevel ( vClasses, vClass, i )
@ -845,7 +857,7 @@ finish:
Vec_PtrFree( vSopsRepr );
return vSops;
}
Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
Gia_Man_t * pGia;
@ -874,7 +886,7 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
}
}
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
Gia_ManStop( pGia );
if ( vSops == NULL )
{
@ -917,11 +929,11 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
Vec_PtrFree( vSops );
return pNtkNew;
}
Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
assert( Abc_NtkIsStrash(pNtk) );
pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
if ( pNtkNew == NULL )
return NULL;
if ( pNtk->pExdc )

6
src/sat/bmc/bmcClp.c
View File

@ -1103,6 +1103,7 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nV
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 );
@ -1113,7 +1114,6 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nV
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 )
@ -1230,8 +1230,8 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int
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
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 )