From 6f0b87dd5c5c7f4f5dec04e9c146d60188acf3c2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 15 Oct 2011 22:04:05 +0300 Subject: New abstraction code. --- src/aig/gia/gia.h | 2 + src/aig/gia/giaAbs.c | 36 +++ src/aig/gia/giaAig.c | 1 + src/aig/gia/giaDup.c | 117 +++++++--- src/aig/gia/giaMan.c | 46 +++- src/aig/saig/saigAbsGla.c | 542 ++++++++++++++++++++++++++++------------------ 6 files changed, 491 insertions(+), 253 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 2d677638..f53d05f3 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -603,6 +603,7 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); +extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ); @@ -659,6 +660,7 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); +extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index f5327f8f..511f418c 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -366,6 +366,42 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit } +/**Function************************************************************* + + Synopsis [Derive unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars ) +{ + extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ); + Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; + Vec_Int_t * vGateClasses; + Aig_Man_t * pAig; +/* + // check if flop classes are given + if ( pGia->vGateClasses == NULL ) + { + Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" ); + pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) ); + } +*/ + // perform abstraction + pAig = Gia_ManToAigSimple( pGia ); + vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose ); + Aig_ManStop( pAig ); + + // update the map + Vec_IntFreeP( &pGia->vGateClasses ); + pGia->vGateClasses = vGateClasses; + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index a38cf083..221593a1 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -350,6 +350,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ) else assert( 0 ); pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) ); + assert( i == 0 || Aig_ObjId(ppNodes[i]) == i ); } Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); ABC_FREE( ppNodes ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index fdf94837..b879cb05 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1586,8 +1586,8 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) Synopsis [Performs abstraction of the AIG to preserve the included gates.] - Description [The array contains PIs, LOs, and internal nodes included. - 0=unsed, 1=PI, 2=PPI, 3=FF, 4=AND.] + Description [The array contains 1 for those objects (const, RO, AND) + that are included in the abstraction; 0, otherwise.] SideEffects [] @@ -1596,51 +1596,110 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) ***********************************************************************/ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) { + Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes; Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, nFlops = 0; assert( Gia_ManPoNum(p) == 1 ); - Gia_ManFillValue( p ); + assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); + + // create included objects and their fanins + vAssigned = Gia_GlaCollectAssigned( p, vGateClasses ); + + // create additional arrays + vPis = Vec_IntAlloc( 1000 ); + vPPis = Vec_IntAlloc( 1000 ); + vFlops = Vec_IntAlloc( 1000 ); + vNodes = Vec_IntAlloc( 1000 ); + Gia_ManForEachObjVec( vAssigned, p, pObj, i ) + { + if ( Gia_ObjIsPi(p, pObj) ) + Vec_IntPush( vPis, Gia_ObjId(p,pObj) ); + else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) ) + Vec_IntPush( vPPis, Gia_ObjId(p,pObj) ); + else if ( Gia_ObjIsAnd(pObj) ) + Vec_IntPush( vNodes, Gia_ObjId(p,pObj) ); + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vFlops, Gia_ObjId(p,pObj) ); + else assert( Gia_ObjIsConst0(pObj) ); + } + // start the new manager pNew = Gia_ManStart( 5000 ); pNew->pName = Gia_UtilStrsav( p->pName ); - // create PIs + // create constant + Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; - Gia_ManForEachPi( p, pObj, i ) - if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 1 ) - pObj->Value = Gia_ManAppendCi(pNew); + // create PIs + Gia_ManForEachObjVec( vPis, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); // create additional PIs - Gia_ManForEachPi( p, pObj, i ) - if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 2 ) - pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachObjVec( vPPis, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); // create ROs - Gia_ManForEachRo( p, pObj, i ) - if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 ) - pObj->Value = Gia_ManAppendCi(pNew); - // create POs - Gia_ManHashAlloc( pNew ); + Gia_ManForEachObjVec( vFlops, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create internal nodes + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create PO Gia_ManForEachPo( p, pObj, i ) - { - Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - } + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); // create RIs - Gia_ManForEachRo( p, pObj, i ) - if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 ) - { - pObj = Gia_ObjRoToRi(p, pObj); - Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - nFlops++; - } - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, nFlops ); + Gia_ManForEachObjVec( vFlops, p, pObj, i ) + Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) ); + Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) ); // clean up pNew = Gia_ManSeqCleanup( pTemp = pNew ); + assert( Gia_ManObjNum(pTemp) == Gia_ManObjNum(pNew) ); Gia_ManStop( pTemp ); + + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vFlops ); + Vec_IntFree( vNodes ); + Vec_IntFree( vAssigned ); return pNew; } +/**Function************************************************************* + + Synopsis [Returns the array of neighbors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses ) +{ + Vec_Int_t * vAssigned; + Gia_Obj_t * pObj; + int i, Entry; + vAssigned = Vec_IntAlloc( 1000 ); + Vec_IntForEachEntry( vGateClasses, Entry, i ) + { + if ( Entry == 0 ) + continue; + assert( Entry == 1 ); + pObj = Gia_ManObj( p, i ); + Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) ); + if ( Gia_ObjIsAnd(pObj) ) + { + Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) ); + Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) ); + else assert( Gia_ObjIsConst0(pObj) ); + } + Vec_IntUniqify( vAssigned ); + return vAssigned; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index ab0c9bc1..f09ca7b5 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -179,7 +179,8 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) } Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 ); Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); - printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d ", Counter0, Counter1 ); + printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ", + Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) ); if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) printf( "and there are other FF classes..." ); printf( "\n" ); @@ -198,7 +199,10 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) ***********************************************************************/ void Gia_ManPrintGateClasses( Gia_Man_t * p ) { - int i, Counter[5]; + Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes; + Gia_Obj_t * pObj; + int i; + if ( p->vGateClasses == NULL ) return; if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) ) @@ -206,12 +210,38 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p ) printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" ); return; } - for ( i = 0; i < 5; i++ ) - Counter[i] = Vec_IntCountEntry( p->vGateClasses, i ); - printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d AND = %d Unused = %d\n", - Counter[1], Counter[2], Counter[3], Counter[4], Counter[0] ); - if ( Counter[0] + Counter[1] + Counter[2] + Counter[3] + Counter[4] != Gia_ManObjNum(p) ) - printf( "Gia_ManPrintGateClasses(): Mismatch in the object count.\n" ); + + // create included objects and their fanins + vAssigned = Gia_GlaCollectAssigned( p, p->vGateClasses ); + + // create additional arrays + vPis = Vec_IntAlloc( 1000 ); + vPPis = Vec_IntAlloc( 1000 ); + vFlops = Vec_IntAlloc( 1000 ); + vNodes = Vec_IntAlloc( 1000 ); + Gia_ManForEachObjVec( vAssigned, p, pObj, i ) + { + if ( Gia_ObjIsPi(p, pObj) ) + Vec_IntPush( vPis, Gia_ObjId(p,pObj) ); + else if ( !Vec_IntEntry(p->vGateClasses, Gia_ObjId(p,pObj)) ) + Vec_IntPush( vPPis, Gia_ObjId(p,pObj) ); + else if ( Gia_ObjIsAnd(pObj) ) + Vec_IntPush( vNodes, Gia_ObjId(p,pObj) ); + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vFlops, Gia_ObjId(p,pObj) ); + else assert( Gia_ObjIsConst0(pObj) ); + } + + printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n", + Vec_IntSize(vPis), Vec_IntSize(vPPis), + Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), + Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) ); + + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vFlops ); + Vec_IntFree( vNodes ); + Vec_IntFree( vAssigned ); } /**Function************************************************************* diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigAbsGla.c index 3915c24b..5c8263eb 100644 --- a/src/aig/saig/saigAbsGla.c +++ b/src/aig/saig/saigAbsGla.c @@ -37,141 +37,30 @@ struct Aig_GlaMan_t_ int nFramesMax; int fVerbose; // abstraction - Vec_Int_t * vAbstr; // collects objects used in the abstraction - Vec_Int_t * vUsed; // maps object ID into its status (0=unused; 1=used) + Vec_Int_t * vAssigned; // collects objects whose SAT variables have been created + Vec_Int_t * vIncluded; // maps obj ID into its status (0=unused; 1=included in abstraction) + // components Vec_Int_t * vPis; // primary inputs Vec_Int_t * vPPis; // pseudo primary inputs Vec_Int_t * vFlops; // flops Vec_Int_t * vNodes; // nodes // unrolling - int iFrame; int nFrames; Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID) Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID // SAT solver sat_solver * pSat; + // statistics + int timeSat; + int timeRef; + int timeTotal; }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Performs abstraction of the AIG to preserve the included gates.] - - Description [The array contains 1 if the obj is included; 0 otherwise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_GlaDupAbsGates( Aig_Man_t * p, Vec_Int_t * vUsed, int * pnRealPis ) -{ - Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, nFlops = 0, RetValue; - assert( Aig_ManPoNum(p) == 1 ); - // start the new manager - pNew = Aig_ManStart( 5000 ); - pNew->pName = Aig_UtilStrsav( p->pName ); - // create constant - Aig_ManCleanData( p ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - // create PIs - Saig_ManForEachPi( p, pObj, i ) - if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) ) - pObj->pData = Aig_ObjCreatePi(pNew); - if ( pnRealPis ) - *pnRealPis = Aig_ManPiNum(pNew); - // create additional PIs - Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && !Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) ) - pObjLo->pData = Aig_ObjCreatePi(pNew); - Aig_ManForEachNode( p, pObj, i ) - { - if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) && - (!Vec_IntEntry(vUsed, Aig_ObjFaninId0(pObj)) || - !Vec_IntEntry(vUsed, Aig_ObjFaninId1(pObj))) ) - pObj->pData = Aig_ObjCreatePi(pNew); - } - // create ROs - Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) ) - pObjLo->pData = Aig_ObjCreatePi(pNew), nFlops++; - // create internal nodes - Aig_ManForEachNode( p, pObj, i ) - { - if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) && - Vec_IntEntry(vUsed, Aig_ObjFaninId0(pObj)) && - Vec_IntEntry(vUsed, Aig_ObjFaninId1(pObj)) ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - } - // create PO - Saig_ManForEachPo( p, pObj, i ) - pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - // create RIs - Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) ) - pObjLi->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObjLi) ); - Aig_ManSetRegNum( pNew, nFlops ); - // clean up - RetValue = Aig_ManCleanup( pNew ); - assert( RetValue == 0 ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) -{ - Aig_Man_t * pNew; - Aig_Obj_t * pObj; - int i, nFlops = 0, RetValue; - assert( Aig_ManPoNum(p) == 1 ); - // start the new manager - pNew = Aig_ManStart( 5000 ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); - // create constant - Aig_ManCleanData( p->pAig ); - Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); - // create PIs - Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pNew); - // create additional PIs - Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pNew); - // create ROs - Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pNew); - // create internal nodes - Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create PO - Saig_ManForEachPo( p->pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - // create RIs - Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i ) - Saig_ObjLoToLi(p->pAig, pObj)->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(Saig_ObjLoToLi(p->pAig, pObj)) ); - Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) ); - // clean up - RetValue = Aig_ManCleanup( pNew ); - assert( RetValue == 0 ); - return pNew; -} - /**Function************************************************************* Synopsis [Adds constant to the solver.] @@ -183,7 +72,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) +static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) { lit Lit = toLitCond( iVar, fCompl ); if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) @@ -202,7 +91,7 @@ int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) SeeAlso [] ***********************************************************************/ -int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) +static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) { lit Lits[2]; @@ -230,7 +119,7 @@ int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) SeeAlso [] ***********************************************************************/ -int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) +static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) { lit Lits[3]; @@ -253,6 +142,155 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp return 1; } +/**Function************************************************************* + + Synopsis [Returns the array of neighbors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_GlaCollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses ) +{ + Vec_Int_t * vAssigned; + Aig_Obj_t * pObj; + int i, Entry; + vAssigned = Vec_IntAlloc( 1000 ); + Vec_IntForEachEntry( vGateClasses, Entry, i ) + { + if ( Entry == 0 ) + continue; + assert( Entry == 1 ); + pObj = Aig_ManObj( p, i ); + Vec_IntPush( vAssigned, Aig_ObjId(pObj) ); + if ( Aig_ObjIsNode(pObj) ) + { + Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) ); + Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) ); + } + else if ( Saig_ObjIsLo(p, pObj) ) + Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) ); + else assert( Aig_ObjIsConst1(pObj) ); + } + Vec_IntUniqify( vAssigned ); + return vAssigned; +} + +/**Function************************************************************* + + Synopsis [Derives abstraction components (PIs, PPIs, flops, nodes).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) +{ + Aig_Obj_t * pObj; + int i, Entry; +/* + // make sure every neighbor of included objects is assigned a variable + Vec_IntForEachEntry( p->vIncluded, Entry, i ) + { + if ( Entry == 0 ) + continue; + assert( Entry == 1 ); + pObj = Aig_ManObj( p->pAig, i ); + if ( Vec_IntFind( p->vAssigned, Aig_ObjId(pObj) ) == -1 ) + printf( "Aig_GlaCollectAbstr(): Object not found\n" ); + if ( Aig_ObjIsNode(pObj) ) + { + if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 ) + printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" ); + if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId1(pObj) ) == -1 ) + printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" ); + } + else if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + Aig_Obj_t * pObjLi; + pObjLi = Saig_ObjLoToLi(p->pAig, pObj); + if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObjLi) ) == -1 ) + printf( "Aig_GlaCollectAbstr(): Flop's fanin is not found\n" ); + } + else assert( Aig_ObjIsConst1(pObj) ); + } +*/ + Vec_IntClear( p->vPis ); + Vec_IntClear( p->vPPis ); + Vec_IntClear( p->vFlops ); + Vec_IntClear( p->vNodes ); + Vec_IntForEachEntryReverse( p->vAssigned, Entry, i ) + { + pObj = Aig_ManObj( p->pAig, Entry ); + if ( Saig_ObjIsPi(p->pAig, pObj) ) + Vec_IntPush( p->vPis, Aig_ObjId(pObj) ); + else if ( !Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) ) + Vec_IntPush( p->vPPis, Aig_ObjId(pObj) ); + else if ( Aig_ObjIsNode(pObj) ) + Vec_IntPush( p->vNodes, Aig_ObjId(pObj) ); + else if ( Saig_ObjIsLo(p->pAig, pObj) ) + Vec_IntPush( p->vFlops, Aig_ObjId(pObj) ); + else assert( Aig_ObjIsConst1(pObj) ); + } +} + +/**Function************************************************************* + + Synopsis [Derives abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i, nFlops = 0, RetValue; + assert( Saig_ManPoNum(p->pAig) == 1 ); + // start the new manager + pNew = Aig_ManStart( 5000 ); + pNew->pName = Aig_UtilStrsav( p->pAig->pName ); + // create constant + Aig_ManCleanData( p->pAig ); + Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); + // create PIs + Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // create additional PIs + Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // create ROs + Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); + // create internal nodes + Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create PO + Saig_ManForEachPo( p->pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + // create RIs + Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i ) + { + assert( Saig_ObjIsLo(p->pAig, pObj) ); + pObj = Saig_ObjLoToLi( p->pAig, pObj ); + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) ); + // clean up + RetValue = Aig_ManCleanup( pNew ); + assert( RetValue == 0 ); + return pNew; +} /**Function************************************************************* @@ -268,17 +306,15 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) { int i, iVecId, iSatVar; - if ( !Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) ) - { - Vec_IntWriteEntry( p->vUsed, Aig_ObjId(pObj), 1 ); - Vec_IntPush( p->vAbstr, Aig_ObjId(pObj) ); - } + assert( k < p->nFrames ); iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); if ( iVecId == 0 ) { iVecId = Vec_IntSize( p->vVec2Var ) / p->nFrames; for ( i = 0; i < p->nFrames; i++ ) Vec_IntPush( p->vVec2Var, 0 ); + Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId ); + Vec_IntPushOrderReverse( p->vAssigned, Aig_ObjId(pObj) ); } iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k ); if ( iSatVar == 0 ) @@ -304,27 +340,42 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) ***********************************************************************/ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) { - assert( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) ); + if ( k == p->nFrames ) + { + int i, j, nVecIds = Vec_IntSize( p->vVec2Var ) / p->nFrames; + Vec_Int_t * vVec2VarNew = Vec_IntAlloc( 4 * nVecIds * p->nFrames ); + for ( i = 0; i < nVecIds; i++ ) + { + for ( j = 0; j < p->nFrames; j++ ) + Vec_IntPush( vVec2VarNew, Vec_IntEntry( p->vVec2Var, i * p->nFrames + j ) ); + for ( j = 0; j < p->nFrames; j++ ) + Vec_IntPush( vVec2VarNew, i ? 0 : -1 ); + } + Vec_IntFree( p->vVec2Var ); + p->vVec2Var = vVec2VarNew; + p->nFrames *= 2; + } + assert( k < p->nFrames ); + assert( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) ); if ( Aig_ObjIsConst1(pObj) ) return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 0 ); - if ( Saig_ObjIsPi(p->pAig, pObj) ) - return 1; if ( Saig_ObjIsLo(p->pAig, pObj) ) { Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); if ( k == 0 ) + { + Aig_GlaFetchVar( p, Aig_ObjFanin0(pObjLi), 0 ); return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 1 ); - if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObjLi)) ) - return 1; - return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k), Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), Aig_ObjFaninC0(pObjLi) ); + } + return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k), + Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), + Aig_ObjFaninC0(pObjLi) ); } assert( Aig_ObjIsNode(pObj) ); - if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObj)) && Vec_IntEntry(p->vUsed, Aig_ObjFaninId1(pObj)) ) - return 0; return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), - Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), - Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), - Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); + Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), + Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), + Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); } /**Function************************************************************* @@ -344,19 +395,19 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) int i; p = ABC_CALLOC( Aig_GlaMan_t, 1 ); - p->pAig = pAig; - p->vAbstr = Vec_IntAlloc( 1000 ); - p->vUsed = Vec_IntStart( Aig_ManObjNumMax(pAig) ); - p->nFrames = 16; + p->pAig = pAig; + p->vAssigned = Vec_IntAlloc( 1000 ); + p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) ); + p->nFrames = 32; - p->vPis = Vec_IntAlloc( 1000 ); - p->vPPis = Vec_IntAlloc( 1000 ); - p->vFlops = Vec_IntAlloc( 1000 ); - p->vNodes = Vec_IntAlloc( 1000 ); + p->vPis = Vec_IntAlloc( 1000 ); + p->vPPis = Vec_IntAlloc( 1000 ); + p->vFlops = Vec_IntAlloc( 1000 ); + p->vNodes = Vec_IntAlloc( 1000 ); - p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) ); - p->vVec2Var = Vec_IntAlloc( 1 << 20 ); - p->vVar2Inf = Vec_IntAlloc( 1 << 20 ); + p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) ); + p->vVec2Var = Vec_IntAlloc( 1 << 20 ); + p->vVar2Inf = Vec_IntAlloc( 1 << 20 ); // skip first vector ID for ( i = 0; i < p->nFrames; i++ ) @@ -367,7 +418,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) // start the SAT solver p->pSat = sat_solver_new(); - sat_solver_setnvars( p->pSat, 1000 ); + sat_solver_setnvars( p->pSat, 256 ); return p; } @@ -385,8 +436,8 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) ***********************************************************************/ void Aig_GlaManStop( Aig_GlaMan_t * p ) { - Vec_IntFreeP( &p->vAbstr ); - Vec_IntFreeP( &p->vUsed ); + Vec_IntFreeP( &p->vAssigned ); + Vec_IntFreeP( &p->vIncluded ); Vec_IntFreeP( &p->vPis ); Vec_IntFreeP( &p->vPPis ); @@ -413,57 +464,47 @@ void Aig_GlaManStop( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) +Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame ) { - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i; - Vec_IntClear( p->vPis ); - Vec_IntClear( p->vPPis ); - Vec_IntClear( p->vFlops ); - Vec_IntClear( p->vNodes ); - - Saig_ManForEachPi( p->pAig, pObj, i ) - if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) ) - Vec_IntPush( p->vPis, Aig_ObjId(pObj) ); - - Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) - if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObjLo)) ) + Abc_Cex_t * pCex; + Aig_Obj_t * pObj; + int i, f, iVecId, iSatId; + pCex = Abc_CexAlloc( Vec_IntSize(p->vFlops), Vec_IntSize(p->vPis) + Vec_IntSize(p->vPPis), iFrame+1 ); + pCex->iFrame = iFrame; + Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i ) + { + iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); + assert( iVecId > 0 ); + for ( f = 0; f <= iFrame; f++ ) { - if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObjLi)) ) - Vec_IntPush( p->vFlops, Aig_ObjId(pObjLo) ); - else - Vec_IntPush( p->vPPis, Aig_ObjId(pObjLo) ); + iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f ); + if ( iSatId == 0 ) + continue; + assert( iSatId > 0 ); + if ( sat_solver_var_value(p->pSat, iSatId) ) + Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + i ); } - - Aig_ManForEachNode( p->pAig, pObj, i ) - if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) ) + } + Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i ) + { + iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); + assert( iVecId > 0 ); + for ( f = 0; f <= iFrame; f++ ) { - if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObj)) && Vec_IntEntry(p->vUsed, Aig_ObjFaninId1(pObj)) ) - Vec_IntPush( p->vNodes, Aig_ObjId(pObjLo) ); - else - Vec_IntPush( p->vPPis, Aig_ObjId(pObjLo) ); + iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f ); + if ( iSatId == 0 ) + continue; + assert( iSatId > 0 ); + if ( sat_solver_var_value(p->pSat, iSatId) ) + Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Vec_IntSize(p->vPis) + i ); } + } + return pCex; } /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p ) -{ - return NULL; -} - -/**Function************************************************************* - - Synopsis [] + Synopsis [Prints current abstraction statistics.] Description [] @@ -472,45 +513,72 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r ) +void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c ) { - printf( "Fra %3d : Ref %3d : PI =%6d PPI =%6d Flop =%6d Node =%6d\n", - f, r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes) ); + if ( r == 0 ) + printf( "== %3d ==", f ); + else + printf( " " ); + printf( " %4d PI =%6d PPI =%6d FF =%6d Node =%6d Var =%7d Conf =%6d\n", + r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes), v, c ); } /**Function************************************************************* - Synopsis [Perform variable frame abstraction.] + Synopsis [Performs gate-level localization abstraction.] - Description [] + Description [Returns array of objects included in the abstraction. This array + may contain only const1, flop outputs, and internal nodes, that is, objects + that should have clauses added to the SAT solver.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose ) +Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ) { + int nStart = 0; + Vec_Int_t * vResult = NULL; Aig_GlaMan_t * p; Aig_Man_t * pAbs; Aig_Obj_t * pObj; Abc_Cex_t * pCex; - Vec_Int_t * vPPisToRefine; + Vec_Int_t * vPPiRefine; int f, g, r, i, iSatVar, Lit, Entry, RetValue; + int nConfBef, nConfAft, clk, clkTotal = clock(); assert( Saig_ManPoNum(pAig) == 1 ); + if ( fVerbose ) + { + if ( TimeLimit ) + printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit ); + else + printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax ); + } + // start the solver p = Aig_GlaManStart( pAig ); p->nFramesMax = nFramesMax; p->nConfLimit = nConfLimit; p->fVerbose = fVerbose; + // include constant node + Vec_IntWriteEntry( p->vIncluded, 0, 1 ); + Aig_GlaFetchVar( p, Aig_ManConst1(pAig), 0 ); + + // set runtime limit + if ( TimeLimit ) + sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC ); + // iterate over the timeframes for ( f = 0; f < nFramesMax; f++ ) { // initialize abstraction in this timeframe - Aig_ManForEachObjVec( p->vAbstr, pAig, pObj, i ) - Aig_GlaObjAddToSolver( p, pObj, f ); + Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i ) + if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) ) + if ( !Aig_GlaObjAddToSolver( p, pObj, f ) ) + printf( "Error! SAT solver became UNSAT.\n" ); // create output literal to represent property failure pObj = Aig_ManPo( pAig, 0 ); @@ -518,41 +586,83 @@ void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerb Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) ); // try solving the abstraction - Aig_GlaPrintAbstr( p, f, -1 ); + Aig_GlaCollectAbstr( p ); for ( r = 0; r < 1000000; r++ ) { + // try to find a counter-example + clk = clock(); + nConfBef = p->pSat->stats.conflicts; RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + nConfAft = p->pSat->stats.conflicts; + p->timeSat += clock() - clk; if ( RetValue != l_True ) + { + if ( fVerbose ) + { + if ( r == 0 ) + printf( "== %3d ==", f ); + else + printf( " " ); + if ( TimeLimit && clock() > clkTotal + TimeLimit * CLOCKS_PER_SEC ) + printf( " SAT solver timed out after %d seconds.\n", TimeLimit ); + else if ( RetValue != l_False ) + printf( " SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef ); + else + printf( " SAT solver returned UNSAT after %5d conflicts.\n", nConfAft - nConfBef ); + } break; - // derive abstraction - Aig_GlaCollectAbstr( p ); - // derive counter-example - pCex = Aig_GlaDeriveCex( p ); + } + clk = clock(); // derive abstraction pAbs = Aig_GlaDeriveAbs( p ); + // derive counter-example + pCex = Aig_GlaDeriveCex( p, f ); + // verify the counter-example + RetValue = Saig_ManVerifyCex( pAbs, pCex ); + if ( RetValue == 0 ) + printf( "Error! CEX is invalid.\n" ); // perform refinement - vPPisToRefine = Saig_ManCbaFilterInputs( pAig, Vec_IntSize(p->vPis), pCex, 0 ); - // update - Vec_IntForEachEntry( vPPisToRefine, Entry, i ) + vPPiRefine = Saig_ManCbaFilterInputs( pAbs, Vec_IntSize(p->vPis), pCex, 0 ); + Vec_IntForEachEntry( vPPiRefine, Entry, i ) { + pObj = Aig_ManObj( pAig, Vec_IntEntry(p->vPPis, Entry) ); + assert( Aig_ObjIsNode(pObj) || Saig_ObjIsLo(p->pAig, pObj) ); + assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 ); + Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 ); for ( g = 0; g <= f; g++ ) - Aig_GlaObjAddToSolver( p, Aig_ManObj(pAig, Vec_IntEntry(p->vPPis, Entry)), g ); + if ( !Aig_GlaObjAddToSolver( p, pObj, g ) ) + printf( "Error! SAT solver became UNSAT.\n" ); } - Vec_IntFree( vPPisToRefine ); - // print abstraction - Aig_GlaPrintAbstr( p, f, r ); + Vec_IntFree( vPPiRefine ); + Aig_ManStop( pAbs ); + Abc_CexFree( pCex ); + p->timeRef += clock() - clk; + + // prepare abstraction + Aig_GlaCollectAbstr( p ); + if ( fVerbose ) + Aig_GlaPrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef ); } if ( RetValue != l_False ) break; } - Aig_GlaPrintAbstr( p, f, -1 ); + p->timeTotal = clock() - clkTotal; if ( f == nFramesMax ) printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit ); else printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f ); - + // print stats + if ( fVerbose ) + { + ABC_PRTP( "Sat ", p->timeSat, p->timeTotal ); + ABC_PRTP( "Ref ", p->timeRef, p->timeTotal ); + ABC_PRTP( "Total ", p->timeTotal, p->timeTotal ); + } + // prepare return value + vResult = p->vIncluded; p->vIncluded = NULL; Aig_GlaManStop( p ); + return vResult; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3