From fe6cb9e891f55e9478d8444ce64fc0cb673bd989 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Aug 2017 14:08:36 +0700 Subject: Experiments with BMC. --- src/sat/bmc/bmcBmcS.c | 78 ++++++++++++++++++++------------------------------- 1 file changed, 31 insertions(+), 47 deletions(-) (limited to 'src/sat/bmc') diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index d4de90f3..170b0318 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -40,6 +40,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define PAR_THR_MAX 100 + typedef struct Bmcs_Man_t_ Bmcs_Man_t; struct Bmcs_Man_t_ { @@ -50,8 +52,7 @@ struct Bmcs_Man_t_ Vec_Ptr_t vGia2Fr; // copies of GIA in each timeframe Vec_Int_t vFr2Sat; // mapping of objects in pFrames into SAT variables Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA - satoko_t * pSat; // SAT solver - satoko_t * pSats[3]; // concurrent SAT solvers + satoko_t * pSats[PAR_THR_MAX]; // concurrent SAT solvers int nSatVars; // number of SAT variables used int fStopNow; // signal when it is time to stop }; @@ -349,39 +350,32 @@ Bmcs_Man_t * Bmcs_ManStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) Vec_IntGrow( &p->vFr2Sat, 3*Gia_ManCiNum(pGia) ); Vec_IntPush( &p->vFr2Sat, 0 ); Vec_IntGrow( &p->vCiMap, 3*Gia_ManCiNum(pGia) ); -#ifdef ABC_USE_PTHREADS - for ( i = 0; i < 3; i++ ) + for ( i = 0; i < pPars->nProcs; i++ ) { - // modify parameters to get different SAT solver instances - opts.f_rst = 0.8 - i * 0.1; - opts.b_rst = 1.4 - i * 0.1; - opts.garbage_max_ratio = (float) 0.3 + i * 0.1; + // modify parameters to get different SAT solvers + opts.f_rst = 0.8 - i * 0.05; + opts.b_rst = 1.4 - i * 0.05; + opts.garbage_max_ratio = (float) 0.3 + i * 0.05; // create SAT solvers p->pSats[i] = satoko_create(); satoko_configure(p->pSats[i], &opts); p->nSatVars = 1; satoko_add_clause( p->pSats[i], &Lit, 1 ); solver_set_stop( p->pSats[i], &p->fStopNow ); } - p->pSat = p->pSats[0]; -#else - p->pSat = satoko_create(); satoko_configure(p->pSat, &opts); - p->nSatVars = 1; - satoko_add_clause( p->pSat, &Lit, 1 ); -#endif // pthreads are used return p; } void Bmcs_ManStop( Bmcs_Man_t * p ) { + int i; Gia_ManStopP( &p->pFrames ); Gia_ManStopP( &p->pClean ); Vec_PtrFreeData( &p->vGia2Fr ); Vec_PtrErase( &p->vGia2Fr ); Vec_IntErase( &p->vFr2Sat ); Vec_IntErase( &p->vCiMap ); - if ( p->pSat ) satoko_destroy( p->pSat ); - if ( p->pSats[0] ) satoko_destroy( p->pSats[0] ); - if ( p->pSats[1] ) satoko_destroy( p->pSats[1] ); - if ( p->pSats[2] ) satoko_destroy( p->pSats[2] ); + for ( i = 0; i < p->pPars->nProcs; i++ ) + if ( p->pSats[i] ) + satoko_destroy( p->pSats[i] ); ABC_FREE( p ); } @@ -541,9 +535,9 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim if ( !p->pPars->fVerbose ) return; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); - Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSat) ); + Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) ); Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses ); - Abc_Print( 1, "Conf =%7.0f. ", (double)satoko_stats(p->pSat).n_conflicts ); + Abc_Print( 1, "Conf =%7.0f. ", (double)satoko_stats(p->pSats[0]).n_conflicts ); if ( p->pPars->nProcs > 1 ) Abc_Print( 1, "S = %3d. ", Solver ); Abc_Print( 1, "%4.0f MB", 1.0*((int)Gia_ManMemory(p->pFrames) + Vec_IntMemory(&p->vFr2Sat))/(1<<20) ); @@ -551,14 +545,14 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim printf( "\n" ); fflush( stdout ); } -Abc_Cex_t * Bmcs_ManGenerateCex( Bmcs_Man_t * p, int i, int f ) +Abc_Cex_t * Bmcs_ManGenerateCex( Bmcs_Man_t * p, int i, int f, int s ) { Abc_Cex_t * pCex = Abc_CexMakeTriv( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), Gia_ManPoNum(p->pGia), f*Gia_ManPoNum(p->pGia)+i ); Gia_Obj_t * pObj; int k; Gia_ManForEachPi( p->pFrames, pObj, k ) { int iSatVar = Vec_IntEntry( &p->vFr2Sat, Gia_ObjId(p->pFrames, pObj) ); - if ( iSatVar > 0 && var_polarity(p->pSat, iSatVar) == LIT_TRUE ) // 1 bit + if ( iSatVar > 0 && var_polarity(p->pSats[s], iSatVar) == LIT_TRUE ) // 1 bit { int iCiId = Vec_IntEntry( &p->vCiMap, 2*k+0 ); int iFrame = Vec_IntEntry( &p->vCiMap, 2*k+1 ); @@ -567,6 +561,13 @@ Abc_Cex_t * Bmcs_ManGenerateCex( Bmcs_Man_t * p, int i, int f ) } return pCex; } +void Bmcs_ManAddCnf( satoko_t * pSat, Cnf_Dat_t * pCnf ) +{ + int i; + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + assert( 0 ); +} int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { abctime clkStart = Abc_Clock(); @@ -585,9 +586,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) continue; } nClauses += pCnf->nClauses; - for ( i = 0; i < pCnf->nClauses; i++ ) - if ( !satoko_add_clause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) - assert( 0 ); + Bmcs_ManAddCnf( p->pSats[0], pCnf ); Cnf_DataFree( pCnf ); assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(pGia) ); for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) @@ -596,9 +595,9 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 ); if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) break; - satoko_assump_push( p->pSat, iLit ); - status = satoko_solve( p->pSat ); - satoko_assump_pop( p->pSat ); + satoko_assump_push( p->pSats[0], iLit ); + status = satoko_solve( p->pSats[0] ); + satoko_assump_pop( p->pSats[0] ); if ( status == SATOKO_UNSAT ) { Bmcs_ManPrintFrame( p, f, nClauses, -1, clkStart ); @@ -610,7 +609,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { RetValue = 0; pPars->iFrame = f; - pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f ); + pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f, 0 ); pPars->nFailOuts++; if ( !pPars->fNotVerbose ) { @@ -654,7 +653,6 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { return Bmcs #else // pthreads are used -#define PAR_THR_MAX 100 typedef struct Par_ThData_t_ { satoko_t * pSat; @@ -691,14 +689,6 @@ void * Bmcs_ManWorkerThread( void * pArg ) return NULL; } -void Bmcs_ManPerform_Add( satoko_t * pSat, Cnf_Dat_t * pCnf ) -{ - int i; - for ( i = 0; i < pCnf->nClauses; i++ ) - if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) - assert( 0 ); -} - int Bmcs_ManPerform_Solve( Bmcs_Man_t * p, int iLit, pthread_t * WorkerThread, Par_ThData_t * ThData, int nProcs, int * pSolver ) { int i, status = -1; @@ -722,11 +712,6 @@ int Bmcs_ManPerform_Solve( Bmcs_Man_t * p, int iLit, pthread_t * WorkerThread, P p->fStopNow = 1; // remember status status = ThData[i].status; - if ( status == 0 ) // SAT - { - assert( p->pSat == NULL ); - p->pSat = p->pSats[i]; - } //printf( "Solver %d returned status %d.\n", i, status ); *pSolver = i; break; @@ -781,8 +766,8 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) } // load CNF into solvers nClauses += pCnf->nClauses; - for ( i = 0; i < 3; i++ ) - Bmcs_ManPerform_Add( p->pSats[i], pCnf ); + for ( i = 0; i < pPars->nProcs; i++ ) + Bmcs_ManAddCnf( p->pSats[i], pCnf ); Cnf_DataFree( pCnf ); // solve outputs assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(pGia) ); @@ -804,7 +789,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { RetValue = 0; pPars->iFrame = f; - pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f ); + pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f, Solver ); pPars->nFailOuts++; if ( !pPars->fNotVerbose ) { @@ -828,7 +813,6 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) ThData[i].pSat = NULL; ThData[i].fWorking = 1; } - p->pSat = NULL; Bmcs_ManStop( p ); if ( RetValue == -1 && !pPars->fNotVerbose ) printf( "No output failed in %d frames. ", f ); -- cgit v1.2.3