Skip to content

A
abc
Commit f97b8d28 by Alan Mishchenko
Options

Improvements to SAT based SOP computation.

parent 02972e53
Showing with 44 additions and 25 deletions
src/aig/gia/gia.h
...@@ -1353,6 +1353,7 @@ extern void Gia_ManHashProfile( Gia_Man_t * p ); ...@@ -1353,6 +1353,7 @@ extern void Gia_ManHashProfile( Gia_Man_t * p );
extern int Gia_ManHashLookupInt( Gia_Man_t * p, int iLit0, int iLit1 ); extern int Gia_ManHashLookupInt( Gia_Man_t * p, int iLit0, int iLit1 );
extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ); extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ); extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits );
extern int Gia_ManHashAndMulti2( Gia_Man_t * p, Vec_Int_t * vLits );
/*=== giaIf.c ===========================================================*/ /*=== giaIf.c ===========================================================*/
extern void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ); extern void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile );
extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p );
......
src/aig/gia/giaHash.c
...@@ -798,6 +798,13 @@ int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ) ...@@ -798,6 +798,13 @@ int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits )
assert( Vec_IntSize(vLits) == 1 ); assert( Vec_IntSize(vLits) == 1 );
return Vec_IntEntry(vLits, 0); return Vec_IntEntry(vLits, 0);
} }
int Gia_ManHashAndMulti2( Gia_Man_t * p, Vec_Int_t * vLits )
{
int i, iLit, iRes = 1;
Vec_IntForEachEntry( vLits, iLit, i )
iRes = Gia_ManHashAnd( p, iRes, iLit );
return iRes;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/base/abc/abcUtil.c
...@@ -3235,7 +3235,7 @@ Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk ) ...@@ -3235,7 +3235,7 @@ Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk )
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
return pNew; return pNew;
} }
Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ) Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp )
{ {
Abc_Ntk_t * pNtkNew, * pNtk; Abc_Ntk_t * pNtkNew, * pNtk;
Vec_Ptr_t * vSops; Vec_Ptr_t * vSops;
...@@ -3253,6 +3253,8 @@ Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ) ...@@ -3253,6 +3253,8 @@ Gia_Man_t * Abc_SopSynthesizeOne( char * pSop )
pNtk = Abc_NtkCreateFromSops( "top", vSops ); pNtk = Abc_NtkCreateFromSops( "top", vSops );
Vec_PtrFree( vSops ); Vec_PtrFree( vSops );
Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk );
if ( fClp )
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "clp; sop" );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2" ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2" );
pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ); pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() );
return Abc_NtkStrashToGia( pNtkNew ); return Abc_NtkStrashToGia( pNtkNew );
......
src/sat/glucose/AbcGlucose.cpp
...@@ -745,25 +745,25 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) ...@@ -745,25 +745,25 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vVars, Vec_Int_t * vVarMap ) Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vAllVars, Vec_Int_t * vVarMap )
{ {
int fCreatePrime = 1; int fCreatePrime = 1;
int nVars = Vec_IntSize(vVars); int nVars = Vec_IntCountLarger( vVarMap, -1 );
Vec_Str_t * vSop = Vec_StrAlloc( 1000 ); Vec_Str_t * vSop = Vec_StrAlloc( 1000 );
Vec_Int_t * vLits = Vec_IntAlloc( nVars ); Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vAllVars) );
Vec_Str_t * vCube = Vec_StrAlloc( nVars + 4 ); Vec_Str_t * vCube = Vec_StrAlloc( nVars + 4 );
Vec_StrFill( vCube, nVars, '-' ); Vec_StrFill( vCube, nVars, '-' );
Vec_StrPrintF( vCube, " 1\n\0" ); Vec_StrPrintF( vCube, " 1\n\0" );
while ( 1 ) while ( 1 )
{ {
int * pFinal, nFinal, iVar, i; int * pFinal, nFinal, iVar, i, k = 0;
// generate onset minterm // generate onset minterm
int status = bmcg_sat_solver_solve( pSat[1], NULL, 0 ); int status = bmcg_sat_solver_solve( pSat[1], NULL, 0 );
if ( status == GLUCOSE_UNSAT ) if ( status == GLUCOSE_UNSAT )
break; break;
assert( status == GLUCOSE_SAT ); assert( status == GLUCOSE_SAT );
Vec_IntClear( vLits ); Vec_IntClear( vLits );
Vec_IntForEachEntry( vVars, iVar, i ) Vec_IntForEachEntry( vAllVars, iVar, i )
Vec_IntPush( vLits, Abc_Var2Lit(iVar, !bmcg_sat_solver_read_cex_varvalue(pSat[1], iVar)) ); Vec_IntPush( vLits, Abc_Var2Lit(iVar, !bmcg_sat_solver_read_cex_varvalue(pSat[1], iVar)) );
// expand against offset // expand against offset
if ( fCreatePrime ) if ( fCreatePrime )
...@@ -785,9 +785,13 @@ Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vVars, ...@@ -785,9 +785,13 @@ Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vVars,
for ( i = 0; i < nFinal; i++ ) for ( i = 0; i < nFinal; i++ )
{ {
iVar = Vec_IntEntry(vVarMap, Abc_Lit2Var(pFinal[i])); iVar = Vec_IntEntry(vVarMap, Abc_Lit2Var(pFinal[i]));
if ( iVar == -1 )
continue;
pFinal[k++] = pFinal[i];
assert( iVar >= 0 && iVar < nVars ); assert( iVar >= 0 && iVar < nVars );
Vec_StrWriteEntry( vCube, iVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) ); Vec_StrWriteEntry( vCube, iVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) );
} }
nFinal = k;
Vec_StrAppend( vSop, Vec_StrArray(vCube) ); Vec_StrAppend( vSop, Vec_StrArray(vCube) );
//printf( "%4d : %s", Count++, Vec_StrArray(vCube) ); //printf( "%4d : %s", Count++, Vec_StrArray(vCube) );
// add blocking clause // add blocking clause
...@@ -805,7 +809,7 @@ void Glucose_GenerateSop( Gia_Man_t * p ) ...@@ -805,7 +809,7 @@ void Glucose_GenerateSop( Gia_Man_t * p )
// generate CNF for the on-set and off-set // generate CNF for the on-set and off-set
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ ); Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ );
int i,n,nVars = Gia_ManCiNum(p), Lit;//, Count = 0; int i, n, nVars = Gia_ManCiNum(p), Lit;//, Count = 0;
int iFirstVar = pCnf->nVars - nVars; int iFirstVar = pCnf->nVars - nVars;
assert( Gia_ManCoNum(p) == 1 ); assert( Gia_ManCoNum(p) == 1 );
for ( n = 0; n < 2; n++ ) for ( n = 0; n < 2; n++ )
...@@ -851,8 +855,9 @@ void Glucose_GenerateSop( Gia_Man_t * p ) ...@@ -851,8 +855,9 @@ void Glucose_GenerateSop( Gia_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj, int(*pFuncCiToKeep)(int), int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj,
Vec_Int_t * vCiSatVarsToKeep, Vec_Int_t * vObjsUsed ) Vec_Int_t * vObjsUsed, Vec_Int_t * vCisUsed, Vec_Int_t * vCiSatVarsToKeep,
int(*pFuncCiToKeep)(void *, int), void * pData )
{ {
Gia_Obj_t * pObj; int iVar; Gia_Obj_t * pObj; int iVar;
if ( (iVar = Gia_ObjCopyArray(p, iObj)) > 0 ) if ( (iVar = Gia_ObjCopyArray(p, iObj)) > 0 )
...@@ -864,14 +869,16 @@ int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj, int(*pFuncCiToKeep)(int), ...@@ -864,14 +869,16 @@ int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj, int(*pFuncCiToKeep)(int),
assert( Gia_ObjIsCand(pObj) ); assert( Gia_ObjIsCand(pObj) );
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
{ {
Gia_ManSatAndCollect_rec( p, Gia_ObjFaninId0(pObj, iObj), pFuncCiToKeep, vCiSatVarsToKeep, vObjsUsed ); Gia_ManSatAndCollect_rec( p, Gia_ObjFaninId0(pObj, iObj), vObjsUsed, vCisUsed, vCiSatVarsToKeep, pFuncCiToKeep, pData );
Gia_ManSatAndCollect_rec( p, Gia_ObjFaninId1(pObj, iObj), pFuncCiToKeep, vCiSatVarsToKeep, vObjsUsed ); Gia_ManSatAndCollect_rec( p, Gia_ObjFaninId1(pObj, iObj), vObjsUsed, vCisUsed, vCiSatVarsToKeep, pFuncCiToKeep, pData );
} }
else if ( pFuncCiToKeep && pFuncCiToKeep(Gia_ObjCioId(pObj)) ) else if ( pFuncCiToKeep && pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
Vec_IntPush( vCiSatVarsToKeep, iVar ); Vec_IntPush( vCiSatVarsToKeep, iVar );
if ( vCisUsed && Gia_ObjIsCi(pObj) )
Vec_IntPush( vCisUsed, iVar );
return iVar; return iVar;
} }
void Gia_ManQuantLoadCnf( Gia_Man_t * p, Vec_Int_t * vObjsUsed, bmcg_sat_solver * pSats[2] ) void Gia_ManQuantLoadCnf( Gia_Man_t * p, Vec_Int_t * vObjsUsed, bmcg_sat_solver * pSats[] )
{ {
Gia_Obj_t * pObj; int i; Gia_Obj_t * pObj; int i;
bmcg_sat_solver_set_nvars( pSats[0], Vec_IntSize(vObjsUsed) ); bmcg_sat_solver_set_nvars( pSats[0], Vec_IntSize(vObjsUsed) );
...@@ -891,8 +898,8 @@ void Gia_ManQuantLoadCnf( Gia_Man_t * p, Vec_Int_t * vObjsUsed, bmcg_sat_solver ...@@ -891,8 +898,8 @@ void Gia_ManQuantLoadCnf( Gia_Man_t * p, Vec_Int_t * vObjsUsed, bmcg_sat_solver
} }
int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, int fHash ) int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, int fHash )
{ {
extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ); extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
Gia_Man_t * pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop) ); Gia_Man_t * pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 );
Gia_Obj_t * pObj; int i, Result; Gia_Obj_t * pObj; int i, Result;
assert( Gia_ManPiNum(pMan) == Vec_IntSize(vCiObjIds) ); assert( Gia_ManPiNum(pMan) == Vec_IntSize(vCiObjIds) );
Gia_ManConst0(pMan)->Value = 0; Gia_ManConst0(pMan)->Value = 0;
...@@ -908,10 +915,11 @@ int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, in ...@@ -908,10 +915,11 @@ int Gia_ManFactorSop( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, in
Gia_ManStop( pMan ); Gia_ManStop( pMan );
return Result; return Result;
} }
int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[2], Gia_Man_t * p, int iLit, int(*pFuncCiToKeep)(int), int fHash ) int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData )
{ {
Vec_Int_t * vCiSatVarsToKeep = Vec_IntAlloc( 100 ); Vec_Int_t * vCiSatVarsToKeep = Vec_IntAlloc( 100 );
Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 );
Vec_Int_t * vCisUsed = Vec_IntAlloc( 100 );
Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL; Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL;
int i, iVar, iVarLast, Lit, RetValue, Result = -1; int i, iVar, iVarLast, Lit, RetValue, Result = -1;
...@@ -919,7 +927,7 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[2], Gia_Man_t * p, int iLi ...@@ -919,7 +927,7 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[2], Gia_Man_t * p, int iLi
Gia_ManCleanCopyArray(p); Gia_ManCleanCopyArray(p);
Vec_IntPush( vObjsUsed, 0 ); Vec_IntPush( vObjsUsed, 0 );
iVarLast = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit), pFuncCiToKeep, vCiSatVarsToKeep, vObjsUsed ); iVarLast = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit), vObjsUsed, vCisUsed, vCiSatVarsToKeep, pFuncCiToKeep, pData );
Gia_ManQuantLoadCnf( p, vObjsUsed, pSats ); Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) ); Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) );
...@@ -943,7 +951,7 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[2], Gia_Man_t * p, int iLi ...@@ -943,7 +951,7 @@ int bmcg_sat_solver_quantify( bmcg_sat_solver * pSats[2], Gia_Man_t * p, int iLi
Vec_IntForEachEntry( vCiSatVarsToKeep, iVar, i ) Vec_IntForEachEntry( vCiSatVarsToKeep, iVar, i )
Vec_IntWriteEntry( vVarMap, iVar, i ); Vec_IntWriteEntry( vVarMap, iVar, i );
vSop = Glucose_GenerateCubes( pSats, vCiSatVarsToKeep, vVarMap ); vSop = Glucose_GenerateCubes( pSats, vCisUsed, vVarMap );
printf( "%s", Vec_StrArray(vSop) ); printf( "%s", Vec_StrArray(vSop) );
// remap SAT vars into obj IDs of CI nodes // remap SAT vars into obj IDs of CI nodes
...@@ -957,21 +965,22 @@ cleanup: ...@@ -957,21 +965,22 @@ cleanup:
Gia_ObjSetCopyArray( p, iVar, -1 ); Gia_ObjSetCopyArray( p, iVar, -1 );
Vec_IntFree( vCiSatVarsToKeep ); Vec_IntFree( vCiSatVarsToKeep );
Vec_IntFree( vObjsUsed ); Vec_IntFree( vObjsUsed );
Vec_IntFree( vCisUsed );
Vec_IntFreeP( &vVarMap ); Vec_IntFreeP( &vVarMap );
Vec_StrFreeP( &vSop ); Vec_StrFreeP( &vSop );
return Abc_LitNotCond( Result, Abc_LitIsCompl(iLit) ); return Abc_LitNotCond( Result, Abc_LitIsCompl(iLit) );
} }
int Gia_ManCiIsToKeep( int i ) int Gia_ManCiIsToKeep( void * pData, int i )
{ {
return i & 1; return i % 5 != 0;
// return 1; // return 1;
} }
void Glucose_QuantifyAigTest( Gia_Man_t * p ) void Glucose_QuantifyAigTest( Gia_Man_t * p )
{ {
bmcg_sat_solver * pSats[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() }; bmcg_sat_solver * pSats[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() };
int iRes = bmcg_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), Gia_ManCiIsToKeep, 0 ); int iRes = bmcg_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep, NULL );
Gia_ManAppendCo( p, iRes ); Gia_ManAppendCo( p, iRes );
bmcg_sat_solver_stop( pSats[0] ); bmcg_sat_solver_stop( pSats[0] );
...@@ -997,8 +1006,8 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p, ...@@ -997,8 +1006,8 @@ int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * pSat, Gia_Man_t * p,
if ( Vec_IntSize(&p->vCopies) == 0 ) if ( Vec_IntSize(&p->vCopies) == 0 )
Gia_ManCleanCopyArray(p); Gia_ManCleanCopyArray(p);
Vec_IntPush( vObjsUsed, 0 ); Vec_IntPush( vObjsUsed, 0 );
iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), NULL, NULL, vObjsUsed ); iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), vObjsUsed, NULL, NULL, NULL, NULL );
iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), NULL, NULL, vObjsUsed ); iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), vObjsUsed, NULL, NULL, NULL, NULL );
iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) ); iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) );
iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) ); iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) );
Gia_ManQuantLoadCnf( p, vObjsUsed, pSats ); Gia_ManQuantLoadCnf( p, vObjsUsed, pSats );
......
src/sat/glucose/AbcGlucose.h
...@@ -93,7 +93,7 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s ); ...@@ -93,7 +93,7 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s );
extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s );
extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot );
extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[2], Gia_Man_t * p, int iLit, int(*pFuncCiToKeep)(int), int fHash ); extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData );
extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment