| /**CFile**************************************************************** |
| |
| FileName [cecSplit.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Combinational equivalence checking.] |
| |
| Synopsis [Cofactoring for combinational miters.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: cecSplit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include <math.h> |
| #include "aig/gia/gia.h" |
| #include "aig/gia/giaAig.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 |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #ifndef ABC_USE_PTHREADS |
| |
| int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } |
| |
| #else // pthreads are used |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #if 0 // BDD code |
| |
| /**Function************************************************************* |
| |
| Synopsis [Permute primary inputs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| DdManager * Gia_ManBuildBdd( Gia_Man_t * p, Vec_Ptr_t ** pvNodes, int nSkip ) |
| { |
| abctime clk = Abc_Clock(); |
| DdManager * dd; |
| DdNode * bBdd, * bBdd0, * bBdd1; |
| Vec_Ptr_t * vNodes; |
| Gia_Obj_t * pObj; |
| int i; |
| vNodes = Vec_PtrStart( Gia_ManObjNum(p) ); |
| dd = Cudd_Init( Gia_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); |
| // Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); |
| bBdd = Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd ); |
| Vec_PtrWriteEntry( vNodes, 0, bBdd ); |
| Gia_ManForEachPi( p, pObj, i ) |
| { |
| bBdd = i > nSkip ? Cudd_bddIthVar(dd, i) : Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd ); |
| Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd ); |
| } |
| Gia_ManForEachAnd( p, pObj, i ) |
| { |
| bBdd0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) ); |
| bBdd1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) ); |
| bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd ); |
| Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd ); |
| if ( i % 10 == 0 ) |
| printf( "%d ", i ); |
| // if ( i == 3000 ) |
| // break; |
| } |
| printf( "\n" ); |
| Gia_ManForEachPo( p, pObj, i ) |
| { |
| bBdd = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj))), Gia_ObjFaninC0(pObj) ); Cudd_Ref( bBdd ); |
| Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd ); |
| } |
| if ( bBdd == Cudd_ReadLogicZero(dd) ) |
| printf( "Equivalent!\n" ); |
| else |
| printf( "Not tquivalent!\n" ); |
| if ( pvNodes ) |
| *pvNodes = vNodes; |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| return dd; |
| } |
| void Gia_ManDerefBdd( DdManager * dd, Vec_Ptr_t * vNodes ) |
| { |
| DdNode * bBdd; |
| int i; |
| Vec_PtrForEachEntry( DdNode *, vNodes, bBdd, i ) |
| if ( bBdd ) |
| Cudd_RecursiveDeref( dd, bBdd ); |
| if ( Cudd_CheckZeroRef(dd) > 0 ) |
| printf( "The number of referenced nodes = %d\n", Cudd_CheckZeroRef(dd) ); |
| Cudd_PrintInfo( dd, stdout ); |
| Cudd_Quit( dd ); |
| } |
| void Gia_ManBuildBddTest( Gia_Man_t * p ) |
| { |
| Vec_Ptr_t * vNodes; |
| DdManager * dd = Gia_ManBuildBdd( p, &vNodes, 50 ); |
| Gia_ManDerefBdd( dd, vNodes ); |
| } |
| |
| #endif // BDD code |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Cec_GiaSplitExplore( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj, * pFan0, * pFan1; |
| int i, Counter = 0; |
| assert( p->pMuxes == NULL ); |
| ABC_FREE( p->pRefs ); |
| Gia_ManCreateRefs( p ); |
| Gia_ManForEachAnd( p, pObj, i ) |
| { |
| if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) |
| continue; |
| if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 && |
| Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 ) |
| continue; |
| printf( "%5d : ", Counter++ ); |
| printf( "%2d %2d ", Gia_ObjRefNum(p, Gia_Regular(pFan0)), Gia_ObjRefNum(p, Gia_Regular(pFan1)) ); |
| printf( "%2d %2d \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find cofactoring variable.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Gia_PermuteSpecialOrder( Gia_Man_t * p ) |
| { |
| Vec_Int_t * vPerm; |
| Gia_Obj_t * pObj; |
| int i, * pOrder; |
| Gia_ManCreateRefs( p ); |
| vPerm = Vec_IntAlloc( Gia_ManPiNum(p) ); |
| Gia_ManForEachPi( p, pObj, i ) |
| Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) ); |
| pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 ); |
| Vec_IntFree( vPerm ); |
| return pOrder; |
| } |
| Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pNew; |
| Vec_Int_t * vPerm; |
| int * pOrder = Gia_PermuteSpecialOrder( p ); |
| vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) ); |
| pNew = Gia_ManDupPerm( p, vPerm ); |
| Vec_IntFree( vPerm ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find cofactoring variable.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_SplitCofVar2( Gia_Man_t * p, int * pnFanouts, int * pnCost ) |
| { |
| Gia_Obj_t * pObj; |
| int i, iBest = -1, CostBest = -1; |
| if ( p->pRefs == NULL ) |
| Gia_ManCreateRefs( p ); |
| Gia_ManForEachPi( p, pObj, i ) |
| if ( CostBest < Gia_ObjRefNum(p, pObj) ) |
| iBest = i, CostBest = Gia_ObjRefNum(p, pObj); |
| assert( iBest >= 0 ); |
| *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest)); |
| *pnCost = -1; |
| return iBest; |
| } |
| int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead, int * pnFanouts, int * pnCost ) |
| { |
| Gia_Man_t * pPart; |
| int Cost0, Cost1, CostBest = ABC_INFINITY; |
| int * pOrder, i, iBest = -1; |
| if ( LookAhead == 1 ) |
| return Gia_SplitCofVar2( p, pnFanouts, pnCost ); |
| pOrder = Gia_PermuteSpecialOrder( p ); |
| LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) ); |
| for ( i = 0; i < LookAhead; i++ ) |
| { |
| pPart = Gia_ManDupCofactorVar( p, pOrder[i], 0 ); |
| Cost0 = Gia_ManAndNum(pPart); |
| Gia_ManStop( pPart ); |
| |
| pPart = Gia_ManDupCofactorVar( p, pOrder[i], 1 ); |
| 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 ); |
| */ |
| } |
| ABC_FREE( pOrder ); |
| assert( iBest >= 0 ); |
| *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest)); |
| *pnCost = CostBest; |
| return iBest; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Cec_SplitDeriveModel( Gia_Man_t * p, Cnf_Dat_t * pCnf, sat_solver * pSat ) |
| { |
| Abc_Cex_t * pCex; |
| Gia_Obj_t * pObj; |
| int i, iLit, * pModel; |
| pModel = ABC_CALLOC( int, Gia_ManPiNum(p) ); |
| Gia_ManForEachPi( p, pObj, i ) |
| pModel[i] = sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(p, pObj)]); |
| if ( p->vCofVars ) |
| Vec_IntForEachEntry( p->vCofVars, iLit, i ) |
| pModel[Abc_Lit2Var(iLit)] = !Abc_LitIsCompl(iLit); |
| pCex = Abc_CexCreate( 0, Gia_ManPiNum(p), pModel, 0, 0, 0 ); |
| ABC_FREE( pModel ); |
| return pCex; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p ) |
| { |
| Cnf_Dat_t * pCnf; |
| Aig_Man_t * pAig = Gia_ManToAigSimple( p ); |
| pAig->nRegs = 0; |
| pCnf = Cnf_Derive( pAig, 0 );//Aig_ManCoNum(pAig) ); |
| Aig_ManStop( pAig ); |
| return pCnf; |
| } |
| static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut ) |
| { |
| sat_solver * pSat; |
| int i; |
| 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] ) ) |
| { |
| // the problem is UNSAT |
| sat_solver_delete( pSat ); |
| return NULL; |
| } |
| sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); |
| return pSat; |
| } |
| static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs ) |
| { |
| 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 ); |
| if ( status == l_True ) |
| p->pCexComb = Cec_SplitDeriveModel( p, pCnf, pSat ); |
| sat_solver_delete( pSat ); |
| if ( status == l_Undef ) |
| return -1; |
| if ( status == l_False ) |
| return 1; |
| return 0; |
| } |
| static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack ) |
| { |
| Gia_Man_t * pNew; |
| int i; |
| Vec_PtrForEachEntry( Gia_Man_t *, vStack, pNew, i ) |
| Gia_ManStop( pNew ); |
| Vec_PtrFree( vStack ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk ) |
| { |
| printf( "%4d : ", nIter ); |
| printf( "Depth =%3d ", Depth ); |
| printf( "SatVar =%7d ", nVars ); |
| printf( "SatConf =%7d ", nConfs ); |
| printf( "%s ", fStatus ? (fStatus == 1 ? "UNSAT " : "UNDECIDED") : "SAT " ); |
| printf( "Solved %8.4f %% ", 100*Prog ); |
| Abc_PrintTime( 1, "Time", clk ); |
| //ABC_PRTr( "Time", Abc_Clock()-clk ); |
| fflush( stdout ); |
| } |
| void Cec_GiaSplitPrintRefs( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| if ( p->pRefs == NULL ) |
| Gia_ManCreateRefs( p ); |
| Gia_ManForEachPi( p, pObj, i ) |
| printf( "%d ", Gia_ObjRefNum(p, pObj) ); |
| printf( "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) |
| { |
| abctime clkTotal = Abc_Clock(); |
| Vec_Ptr_t * vStack; |
| Cnf_Dat_t * pCnf; |
| int nSatVars, nSatConfs; |
| int nIter, status, RetValue = -1; |
| double Progress = 0; |
| // check the problem |
| pCnf = Cec_GiaDeriveGiaRemapped( p ); |
| status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs ); |
| Cnf_DataFree( pCnf ); |
| if ( fVerbose ) |
| Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); |
| if ( status == 0 ) |
| { |
| if ( !fSilent ) |
| printf( "The problem is SAT without cofactoring.\n" ); |
| return 0; |
| } |
| if ( status == 1 ) |
| { |
| if ( !fSilent ) |
| printf( "The problem is UNSAT without cofactoring.\n" ); |
| return 1; |
| } |
| assert( status == -1 ); |
| // create local copy |
| vStack = Vec_PtrAlloc( 1000 ); |
| Vec_PtrPush( vStack, Gia_ManDup(p) ); |
| // start with the current problem |
| for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ ) |
| { |
| // get the last AIG |
| Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); |
| // determine cofactoring variable |
| int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0); |
| int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost ); |
| // cofactor |
| Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 ); |
| if ( pLast->vCofVars == NULL ) |
| pLast->vCofVars = Vec_IntAlloc( 100 ); |
| // print results |
| if ( fVeryVerbose ) |
| { |
| // Cec_GiaSplitPrintRefs( pLast ); |
| printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n", |
| iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) ); |
| // Cec_GiaSplitPrintRefs( pPart ); |
| } |
| // create variable |
| pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 ); |
| Vec_IntAppend( pPart->vCofVars, pLast->vCofVars ); |
| Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) ); |
| // solve the problem |
| pCnf = Cec_GiaDeriveGiaRemapped( pPart ); |
| status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs ); |
| Cnf_DataFree( pCnf ); |
| if ( status == 1 ) |
| Progress += 1.0 / pow((double)2, (double)Depth); |
| if ( fVerbose ) |
| Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); |
| if ( status == 0 ) // SAT |
| { |
| p->pCexComb = pPart->pCexComb; pPart->pCexComb = NULL; |
| Gia_ManStop( pLast ); |
| Gia_ManStop( pPart ); |
| RetValue = 0; |
| break; |
| } |
| if ( status == 1 ) // UNSAT |
| Gia_ManStop( pPart ); |
| else // UNDEC |
| Vec_PtrPush( vStack, pPart ); |
| // cofactor |
| pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 ); |
| // create variable |
| pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 ); |
| Vec_IntAppend( pPart->vCofVars, pLast->vCofVars ); |
| Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 0) ); |
| Gia_ManStop( pLast ); |
| // solve the problem |
| pCnf = Cec_GiaDeriveGiaRemapped( pPart ); |
| status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs ); |
| Cnf_DataFree( pCnf ); |
| if ( status == 1 ) |
| Progress += 1.0 / pow((double)2, (double)Depth); |
| if ( fVerbose ) |
| Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); |
| if ( status == 0 ) // SAT |
| { |
| p->pCexComb = pPart->pCexComb; pPart->pCexComb = NULL; |
| Gia_ManStop( pPart ); |
| RetValue = 0; |
| break; |
| } |
| if ( status == 1 ) // UNSAT |
| Gia_ManStop( pPart ); |
| else // UNDEC |
| Vec_PtrPush( vStack, pPart ); |
| if ( nIterMax && nIter >= nIterMax ) |
| break; |
| } |
| if ( Vec_PtrSize(vStack) == 0 ) |
| RetValue = 1; |
| // finish |
| Cec_GiaSplitClean( vStack ); |
| if ( !fSilent ) |
| { |
| 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 ); |
| fflush( stdout ); |
| } |
| 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 iThread; |
| 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_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) |
| { |
| abctime clkTotal = Abc_Clock(); |
| Par_ThData_t ThData[PAR_THR_MAX]; |
| pthread_t WorkerThread[PAR_THR_MAX]; |
| Vec_Ptr_t * vStack; |
| Cnf_Dat_t * pCnf; |
| double Progress = 0; |
| int i, status, nSatVars, nSatConfs; |
| int nIter = 0, RetValue = -1, fWorkToDo = 1; |
| Abc_CexFreeP( &p->pCexComb ); |
| 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 ); |
| fflush( stdout ); |
| if ( nProcs == 1 ) |
| return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent ); |
| // subtract manager thread |
| nProcs--; |
| assert( nProcs >= 1 && nProcs <= PAR_THR_MAX ); |
| // check the problem |
| pCnf = Cec_GiaDeriveGiaRemapped( p ); |
| status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs ); |
| Cnf_DataFree( pCnf ); |
| if ( fVerbose && status != -1 ) |
| Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); |
| if ( status == 0 ) |
| { |
| if ( !fSilent ) |
| printf( "The problem is SAT without cofactoring.\n" ); |
| return 0; |
| } |
| if ( status == 1 ) |
| { |
| if ( !fSilent ) |
| printf( "The problem is UNSAT without cofactoring.\n" ); |
| return 1; |
| } |
| assert( status == -1 ); |
| // create local copy |
| vStack = Vec_PtrAlloc( 1000 ); |
| Vec_PtrPush( vStack, Gia_ManDup(p) ); |
| // start threads |
| for ( i = 0; i < nProcs; i++ ) |
| { |
| ThData[i].p = NULL; |
| ThData[i].pCnf = NULL; |
| ThData[i].iThread = i; |
| 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 = pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0; |
| if ( pLast->vCofVars == NULL ) |
| pLast->vCofVars = Vec_IntAlloc( 100 ); |
| if ( fVerbose ) |
| Cec_GiaSplitPrint( i+1, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal ); |
| if ( ThData[i].Result == 0 ) // SAT |
| { |
| p->pCexComb = pLast->pCexComb; pLast->pCexComb = NULL; |
| RetValue = 0; |
| goto finish; |
| } |
| if ( ThData[i].Result == -1 ) // UNDEC |
| { |
| // determine cofactoring variable |
| int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost ); |
| // cofactor |
| Gia_Man_t * pPart = Gia_ManDupCofactorVar( 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 ); |
| // print results |
| if ( fVeryVerbose ) |
| { |
| // Cec_GiaSplitPrintRefs( pLast ); |
| printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n", |
| iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) ); |
| // Cec_GiaSplitPrintRefs( pPart ); |
| } |
| // cofactor |
| pPart = Gia_ManDupCofactorVar( 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((double)2, (double)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 = (Gia_Man_t*)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 ( !fSilent ) |
| { |
| 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 ); |
| fflush( stdout ); |
| } |
| return RetValue; |
| } |
| int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) |
| { |
| Abc_Cex_t * pCex = NULL; |
| Gia_Man_t * pOne; |
| Gia_Obj_t * pObj; |
| int i, RetValue1, fOneUndef = 0, RetValue = -1; |
| Abc_CexFreeP( &p->pCexComb ); |
| Gia_ManForEachPo( p, pObj, i ) |
| { |
| pOne = Gia_ManDupOutputGroup( p, i, i+1 ); |
| if ( fVerbose ) |
| printf( "\nSolving output %d:\n", i ); |
| RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent ); |
| Gia_ManStop( pOne ); |
| // collect the result |
| if ( RetValue1 == 0 && RetValue == -1 ) |
| { |
| pCex = pOne->pCexComb; pOne->pCexComb = NULL; |
| pCex->iPo = i; |
| RetValue = 0; |
| } |
| if ( RetValue1 == -1 ) |
| fOneUndef = 1; |
| } |
| if ( RetValue == -1 ) |
| RetValue = fOneUndef ? -1 : 1; |
| else |
| p->pCexComb = pCex; |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Print stats about cofactoring variables.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Cec_GiaPrintCofStats( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pCof0, * pCof1; |
| Gia_Obj_t * pObj, * pFan0, * pFan1, * pCtrl; |
| Vec_Int_t * vMarks; |
| int i, Count = 0; |
| vMarks = Vec_IntStart( Gia_ManObjNum(p) ); |
| Gia_ManForEachAnd( p, pObj, i ) |
| { |
| if ( !Gia_ObjIsMuxType(pObj) ) |
| continue; |
| if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) |
| continue; |
| pCtrl = Gia_ObjRecognizeMux( pObj, &pFan1, &pFan0 ); |
| pCtrl = Gia_Regular(pCtrl); |
| Vec_IntAddToEntry( vMarks, Gia_ObjId(p, pCtrl), 1 ); |
| } |
| printf( "The AIG with %d candidate nodes (PI+AND) has %d unique MUX control drivers:\n", |
| Gia_ManCandNum(p), Vec_IntCountPositive(vMarks) ); |
| Gia_ManLevelNum( p ); |
| Gia_ManForEachCand( p, pObj, i ) |
| { |
| if ( !Vec_IntEntry(vMarks, i) ) |
| continue; |
| pCof0 = Gia_ManDupCofactorObj( p, i, 0 ); |
| pCof1 = Gia_ManDupCofactorObj( p, i, 1 ); |
| printf( "%6d : ", Count++ ); |
| printf( "Obj = %6d ", i ); |
| printf( "MUX refs = %5d ", Vec_IntEntry(vMarks, i) ); |
| printf( "Level = %5d ", Gia_ObjLevelId(p, i) ); |
| printf( "Cof0 = %7d ", Gia_ManAndNum(pCof0) ); |
| printf( "Cof1 = %7d ", Gia_ManAndNum(pCof1) ); |
| printf( "\n" ); |
| Gia_ManStop( pCof0 ); |
| Gia_ManStop( pCof1 ); |
| } |
| Vec_IntFree( vMarks ); |
| } |
| void Cec_GiaPrintCofStats2( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pCof0, * pCof1; |
| Gia_Obj_t * pObj; |
| int i; |
| Gia_ManLevelNum( p ); |
| Gia_ManCreateRefs( p ); |
| Gia_ManForEachPi( p, pObj, i ) |
| { |
| pCof0 = Gia_ManDupCofactorVar( p, i, 0 ); |
| pCof1 = Gia_ManDupCofactorVar( p, i, 1 ); |
| printf( "PI %5d : ", i ); |
| printf( "Refs = %5d ", Gia_ObjRefNum(p, pObj) ); |
| printf( "Cof0 = %7d ", Gia_ManAndNum(pCof0) ); |
| printf( "Cof1 = %7d ", Gia_ManAndNum(pCof1) ); |
| printf( "\n" ); |
| Gia_ManStop( pCof0 ); |
| Gia_ManStop( pCof1 ); |
| } |
| } |
| |
| #endif // pthreads are used |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
