diff options
Diffstat (limited to 'src/proof/cec/cecSplit.c')
| -rw-r--r-- | src/proof/cec/cecSplit.c | 279 |
1 files changed, 250 insertions, 29 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index e04d6224..3e2b70a6 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -21,10 +21,21 @@ #include <math.h> #include "aig/gia/gia.h" #include "aig/gia/giaAig.h" -//#include "bdd/cudd/cuddInt.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver.h" #include "misc/util/utilTruth.h" +//#include "bdd/cudd/cuddInt.h" + +//#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include <pthread.h> +#include <unistd.h> +#endif + +//#endif ABC_NAMESPACE_IMPL_START @@ -222,12 +233,20 @@ int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead ) Cost1 = Gia_ManAndNum(pPart); Gia_ManStop( pPart ); - if ( CostBest > Cost0 + Cost1 ) - CostBest = Cost0 + Cost1, iBest = pOrder[i]; +/* + pPart = Gia_ManDupExist( p, pOrder[i] ); + printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d %6d -> %6d\n", + i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])), + Cost0, Cost1, Cost0+Cost1, Gia_ManAndNum(p), Gia_ManAndNum(pPart) ); + Gia_ManStop( pPart ); +*/ // printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n", // i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])), // Cost0, Cost1, Cost0+Cost1 ); + + if ( CostBest > Cost0 + Cost1 ) + CostBest = Cost0 + Cost1, iBest = pOrder[i]; } ABC_FREE( pOrder ); assert( iBest >= 0 ); @@ -255,27 +274,40 @@ static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p ) Aig_ManStop( pAig ); return pCnf; } -static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut ) +static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut ) { sat_solver * pSat; - Cnf_Dat_t * pCnf; - int i; - pCnf = Cec_GiaDeriveGiaRemapped( p ); + int i, fDerive = (pCnf == NULL); + if ( pCnf == NULL ) + pCnf = Cec_GiaDeriveGiaRemapped( p ); pSat = sat_solver_new(); sat_solver_setnvars( pSat, pCnf->nVars ); for ( i = 0; i < pCnf->nClauses; i++ ) if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - assert( 0 ); + { + // the problem is UNSAT + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + return NULL; + } sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); - Cnf_DataFree( pCnf ); + if ( fDerive ) + Cnf_DataFree( pCnf ); return pSat; } -static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs ) +static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs ) { - sat_solver * pSat = Cec_GiaDeriveSolver( p, nTimeOut ); - int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - *pnVars = sat_solver_nvars( pSat ); - *pnConfs = sat_solver_nconflicts( pSat ); + int status; + sat_solver * pSat = Cec_GiaDeriveSolver( p, pCnf, nTimeOut ); + if ( pSat == NULL ) + { + *pnVars = 0; + *pnConfs = 0; + return 1; + } + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + *pnVars = sat_solver_nvars( pSat ); + *pnConfs = sat_solver_nconflicts( pSat ); sat_solver_delete( pSat ); if ( status == l_Undef ) return -1; @@ -299,9 +331,9 @@ static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, in } */ } -static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs ) +static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs ) { - int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose, pnVars, pnConfs ); + int status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, pnVars, pnConfs ); if ( status == -1 ) { Vec_PtrPush( vStack, p ); @@ -333,13 +365,13 @@ static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack ) SeeAlso [] ***********************************************************************/ -void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUnsat, double Prog, abctime clk ) +void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk ) { printf( "%6d : ", nIter ); printf( "Depth =%3d ", Depth ); printf( "SatVar =%7d ", nVars ); printf( "SatConf =%7d ", nConfs ); - printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" ); + printf( "%s ", fStatus ? (fStatus == 1 ? "UNSAT " : "UNDECIDED") : "SAT " ); printf( "Progress = %.10f ", Prog ); Abc_PrintTime( 1, "Time", clk ); //ABC_PRTr( "Time", Abc_Clock()-clk ); @@ -366,9 +398,9 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ) +int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ) { - abctime clk, clkTotal = Abc_Clock(); + abctime clkTotal = Abc_Clock(); Gia_Man_t * pPart0, * pPart1, * pLast; Vec_Ptr_t * vStack; int nSatVars, nSatConfs, fSatUnsat; @@ -381,13 +413,12 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, p->vCofVars = Vec_IntAlloc( 100 ); // start with the current problem vStack = Vec_PtrAlloc( 1000 ); - clk = Abc_Clock(); - if ( !Cnf_GiaCheckOne(vStack, p, nTimeOut, fVerbose, &nSatVars, &nSatConfs) ) + if ( !Cnf_GiaCheckOne(vStack, p, NULL, nTimeOut, &nSatVars, &nSatConfs) ) RetValue = 0; else { if ( fVerbose ) - Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, 0, 0, Abc_Clock() - clk ); + Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, -1, Progress, Abc_Clock() - clkTotal ); for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ ) { // get the last AIG @@ -403,8 +434,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, Vec_IntPush( pPart0->vCofVars, Abc_Var2Lit(iVar, 1) ); // check this AIG fSatUnsat = Vec_PtrSize(vStack); - clk = Abc_Clock(); - if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose, &nSatVars, &nSatConfs) ) + if ( !Cnf_GiaCheckOne(vStack, pPart0, NULL, nTimeOut, &nSatVars, &nSatConfs) ) { Gia_ManStop( pLast ); RetValue = 0; @@ -414,7 +444,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, if ( fSatUnsat ) Progress += 1.0 / pow(2, Depth + 1); if ( fVerbose ) - Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); + Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat?1:-1, Progress, Abc_Clock() - clkTotal ); // cofactor pPart1 = Gia_ManDupCofactor( pLast, iVar, 1 ); // create variable @@ -424,8 +454,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, Gia_ManStop( pLast ); // check this AIG fSatUnsat = Vec_PtrSize(vStack); - clk = Abc_Clock(); - if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose, &nSatVars, &nSatConfs) ) + if ( !Cnf_GiaCheckOne(vStack, pPart1, NULL, nTimeOut, &nSatVars, &nSatConfs) ) { RetValue = 0; break; @@ -434,7 +463,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, if ( fSatUnsat ) Progress += 1.0 / pow(2, Depth + 1); if ( fVerbose ) - Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); + Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat?1:-1, Progress, Abc_Clock() - clkTotal ); if ( nIterMax && Vec_PtrSize(vStack) >= nIterMax ) break; } @@ -454,6 +483,198 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, return RetValue; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#define PAR_THR_MAX 100 +typedef struct Par_ThData_t_ +{ + Gia_Man_t * p; + Cnf_Dat_t * pCnf; + int nTimeOut; + int fWorking; + int Result; + int nVars; + int nConfs; +} Par_ThData_t; +void * Cec_GiaSplitWorkerThread( void * pArg ) +{ + Par_ThData_t * pThData = (Par_ThData_t *)pArg; + volatile int * pPlace = &pThData->fWorking; + while ( 1 ) + { + while ( *pPlace == 0 ); + assert( pThData->fWorking ); + if ( pThData->p == NULL ) + { + pthread_exit( NULL ); + assert( 0 ); + return NULL; + } + pThData->Result = Cnf_GiaSolveOne( pThData->p, pThData->pCnf, pThData->nTimeOut, &pThData->nVars, &pThData->nConfs ); + pThData->fWorking = 0; + } + assert( 0 ); + return NULL; +} +int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ) +{ + abctime clkTotal = Abc_Clock(); + Par_ThData_t ThData[PAR_THR_MAX]; + pthread_t WorkerThread[PAR_THR_MAX]; + Vec_Ptr_t * vStack; + double Progress = 0; + int i, status, nSatVars, nSatConfs; + int nIter = 0, RetValue = -1, fWorkToDo = 1; + if ( fVerbose ) + printf( "Solving CEC problem by cofactoring with the following parameters:\n" ); + if ( fVerbose ) + printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose ); + if ( nProcs == 1 ) + return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose ); + // subtract manager thread + nProcs--; + assert( nProcs >= 1 && nProcs <= PAR_THR_MAX ); + // check the problem + status = Cnf_GiaSolveOne( p, NULL, nTimeOut, &nSatVars, &nSatConfs ); + if ( fVerbose ) + Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); + if ( status == 0 ) + { + printf( "The problem is SAT.\n" ); + return 0; + } + if ( status == 1 ) + { + printf( "The problem is UNSAT.\n" ); + return 1; + } + assert( status == -1 ); + // create local copy + p = Gia_ManDup( p ); + vStack = Vec_PtrAlloc( 1000 ); + Vec_PtrPush( vStack, p ); + // start cofactored variables + assert( p->vCofVars == NULL ); + p->vCofVars = Vec_IntAlloc( 100 ); + // start threads + for ( i = 0; i < nProcs; i++ ) + { + ThData[i].p = NULL; + ThData[i].pCnf = NULL; + ThData[i].nTimeOut = nTimeOut; + ThData[i].fWorking = 0; + ThData[i].Result = -1; + ThData[i].nVars = -1; + ThData[i].nConfs = -1; + status = pthread_create( WorkerThread + i, NULL,Cec_GiaSplitWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); + } + // look at the threads + while ( fWorkToDo ) + { + fWorkToDo = (int)(Vec_PtrSize(vStack) > 0); + for ( i = 0; i < nProcs; i++ ) + { + // check if this thread is working + if ( ThData[i].fWorking ) + { + fWorkToDo = 1; + continue; + } + // check if this thread has recently finished + if ( ThData[i].p != NULL ) + { + Gia_Man_t * pLast = ThData[i].p; + int Depth = Vec_IntSize(pLast->vCofVars); + if ( fVerbose ) + Cec_GiaSplitPrint( nIter, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal ); + if ( ThData[i].Result == 0 ) // SAT + { + RetValue = 0; + goto finish; + } + if ( ThData[i].Result == -1 ) // UNDEC + { + // determine cofactoring variable + int iVar = Gia_SplitCofVar2( pLast, LookAhead ); + // cofactor + Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 ); + pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 ); + Vec_IntAppend( pPart->vCofVars, pLast->vCofVars ); + Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) ); + Vec_PtrPush( vStack, pPart ); + // cofactor + pPart = Gia_ManDupCofactor( pLast, iVar, 1 ); + pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 ); + Vec_IntAppend( pPart->vCofVars, pLast->vCofVars ); + Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) ); + Vec_PtrPush( vStack, pPart ); + // keep working + fWorkToDo = 1; + nIter++; + } + else + Progress += 1.0 / pow(2, Depth); + Gia_ManStopP( &ThData[i].p ); + if ( ThData[i].pCnf == NULL ) + continue; + Cnf_DataFree( ThData[i].pCnf ); + ThData[i].pCnf = NULL; + } + if ( Vec_PtrSize(vStack) == 0 ) + continue; + // start a new thread + assert( ThData[i].p == NULL ); + ThData[i].p = Vec_PtrPop( vStack ); + ThData[i].pCnf = Cec_GiaDeriveGiaRemapped( ThData[i].p ); + ThData[i].fWorking = 1; + } + if ( nIterMax && nIter >= nIterMax ) + break; + } + if ( !fWorkToDo ) + RetValue = 1; +finish: + // wait till threads finish + for ( i = 0; i < nProcs; i++ ) + if ( ThData[i].fWorking ) + i = 0; + // stop threads + for ( i = 0; i < nProcs; i++ ) + { + assert( !ThData[i].fWorking ); + // cleanup + Gia_ManStopP( &ThData[i].p ); + if ( ThData[i].pCnf == NULL ) + continue; + Cnf_DataFree( ThData[i].pCnf ); + ThData[i].pCnf = NULL; + // stop + ThData[i].p = NULL; + ThData[i].fWorking = 1; + } + // finish + Cec_GiaSplitClean( vStack ); + if ( RetValue == 0 ) + printf( "Problem is SAT " ); + else if ( RetValue == 1 ) + printf( "Problem is UNSAT " ); + else if ( RetValue == -1 ) + printf( "Problem is UNDECIDED " ); + else assert( 0 ); + printf( "after %d case-splits. ", nIter ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |