/**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 #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 #include #endif #endif ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// 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 ) { 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 ) { printf( "The problem is SAT without cofactoring.\n" ); return 0; } if ( status == 1 ) { 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(2, 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(2, 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 ( 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 [] ***********************************************************************/ #ifdef ABC_USE_PTHREADS #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 ) { 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 ); // 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 ) { printf( "The problem is SAT without cofactoring.\n" ); return 0; } if ( status == 1 ) { 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(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 ); fflush( stdout ); return RetValue; } int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { 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 ); 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; } #endif /**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 ); } } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END