From f97b8d2882bc69d37e6559a12b9e31a988a7eb97 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 6 Oct 2017 17:16:16 +0300 Subject: Improvements to SAT based SOP computation. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaHash.c | 7 ++++++ src/base/abc/abcUtil.c | 4 ++- src/sat/glucose/AbcGlucose.cpp | 55 ++++++++++++++++++++++++------------------ src/sat/glucose/AbcGlucose.h | 2 +- 5 files changed, 44 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index cbb98d1c..591dd419 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -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_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_ManHashAndMulti2( Gia_Man_t * p, Vec_Int_t * vLits ); /*=== giaIf.c ===========================================================*/ extern void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index c80f9e07..c6067312 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -798,6 +798,13 @@ int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits ) assert( Vec_IntSize(vLits) == 1 ); 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 /// diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index b930e6c5..a63abb9e 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -3235,7 +3235,7 @@ Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk ) Gia_ManStop( pTemp ); return pNew; } -Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ) +Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ) { Abc_Ntk_t * pNtkNew, * pNtk; Vec_Ptr_t * vSops; @@ -3253,6 +3253,8 @@ Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ) pNtk = Abc_NtkCreateFromSops( "top", vSops ); Vec_PtrFree( vSops ); Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); + if ( fClp ) + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "clp; sop" ); Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2" ); pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ); return Abc_NtkStrashToGia( pNtkNew ); diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 1da07b7f..84927daa 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -745,25 +745,25 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) 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 nVars = Vec_IntSize(vVars); + int nVars = Vec_IntCountLarger( vVarMap, -1 ); 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_StrFill( vCube, nVars, '-' ); Vec_StrPrintF( vCube, " 1\n\0" ); while ( 1 ) { - int * pFinal, nFinal, iVar, i; + int * pFinal, nFinal, iVar, i, k = 0; // generate onset minterm int status = bmcg_sat_solver_solve( pSat[1], NULL, 0 ); if ( status == GLUCOSE_UNSAT ) break; assert( status == GLUCOSE_SAT ); 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)) ); // expand against offset if ( fCreatePrime ) @@ -785,9 +785,13 @@ Vec_Str_t * Glucose_GenerateCubes( bmcg_sat_solver * pSat[2], Vec_Int_t * vVars, for ( i = 0; i < nFinal; i++ ) { iVar = Vec_IntEntry(vVarMap, Abc_Lit2Var(pFinal[i])); + if ( iVar == -1 ) + continue; + pFinal[k++] = pFinal[i]; assert( iVar >= 0 && iVar < nVars ); Vec_StrWriteEntry( vCube, iVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) ); } + nFinal = k; Vec_StrAppend( vSop, Vec_StrArray(vCube) ); //printf( "%4d : %s", Count++, Vec_StrArray(vCube) ); // add blocking clause @@ -805,7 +809,7 @@ void Glucose_GenerateSop( Gia_Man_t * p ) // 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*/ ); - 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; assert( Gia_ManCoNum(p) == 1 ); for ( n = 0; n < 2; n++ ) @@ -851,8 +855,9 @@ void Glucose_GenerateSop( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj, int(*pFuncCiToKeep)(int), - Vec_Int_t * vCiSatVarsToKeep, Vec_Int_t * vObjsUsed ) +int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj, + Vec_Int_t * vObjsUsed, Vec_Int_t * vCisUsed, Vec_Int_t * vCiSatVarsToKeep, + int(*pFuncCiToKeep)(void *, int), void * pData ) { Gia_Obj_t * pObj; int iVar; if ( (iVar = Gia_ObjCopyArray(p, iObj)) > 0 ) @@ -864,14 +869,16 @@ int Gia_ManSatAndCollect_rec( Gia_Man_t * p, int iObj, int(*pFuncCiToKeep)(int), assert( Gia_ObjIsCand(pObj) ); if ( Gia_ObjIsAnd(pObj) ) { - Gia_ManSatAndCollect_rec( p, Gia_ObjFaninId0(pObj, iObj), pFuncCiToKeep, vCiSatVarsToKeep, vObjsUsed ); - Gia_ManSatAndCollect_rec( p, Gia_ObjFaninId1(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), vObjsUsed, vCisUsed, vCiSatVarsToKeep, pFuncCiToKeep, pData ); } - else if ( pFuncCiToKeep && pFuncCiToKeep(Gia_ObjCioId(pObj)) ) + else if ( pFuncCiToKeep && pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) ) Vec_IntPush( vCiSatVarsToKeep, iVar ); + if ( vCisUsed && Gia_ObjIsCi(pObj) ) + Vec_IntPush( vCisUsed, 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; 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 } 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 ); - Gia_Man_t * pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop) ); + extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp ); + Gia_Man_t * pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 ); Gia_Obj_t * pObj; int i, Result; assert( Gia_ManPiNum(pMan) == Vec_IntSize(vCiObjIds) ); 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 Gia_ManStop( pMan ); 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 * 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; 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 Gia_ManCleanCopyArray(p); 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 ); 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 Vec_IntForEachEntry( vCiSatVarsToKeep, iVar, i ) Vec_IntWriteEntry( vVarMap, iVar, i ); - vSop = Glucose_GenerateCubes( pSats, vCiSatVarsToKeep, vVarMap ); + vSop = Glucose_GenerateCubes( pSats, vCisUsed, vVarMap ); printf( "%s", Vec_StrArray(vSop) ); // remap SAT vars into obj IDs of CI nodes @@ -957,21 +965,22 @@ cleanup: Gia_ObjSetCopyArray( p, iVar, -1 ); Vec_IntFree( vCiSatVarsToKeep ); Vec_IntFree( vObjsUsed ); + Vec_IntFree( vCisUsed ); Vec_IntFreeP( &vVarMap ); Vec_StrFreeP( &vSop ); 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; } void Glucose_QuantifyAigTest( Gia_Man_t * p ) { 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 ); 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, if ( Vec_IntSize(&p->vCopies) == 0 ) Gia_ManCleanCopyArray(p); Vec_IntPush( vObjsUsed, 0 ); - iSatVar[0] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit0), NULL, NULL, vObjsUsed ); - iSatVar[1] = Gia_ManSatAndCollect_rec( p, Abc_Lit2Var(iLit1), 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), vObjsUsed, NULL, NULL, NULL, NULL ); iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) ); iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) ); Gia_ManQuantLoadCnf( p, vObjsUsed, pSats ); diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index 83ad8dcc..3484c008 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -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_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_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 void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); -- cgit v1.2.3