From 8ed6d8e05f5483cbce7e1256bfce6bdacc085667 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 27 Jul 2011 20:18:14 +0700 Subject: Adding procedures to find the care bits of a counter-example (update). --- src/aig/saig/saig.h | 4 +- src/aig/saig/saigAbs.c | 8 +- src/aig/saig/saigRefSat.c | 662 +++++++++++++++++++++++++++++++++++++++++---- src/aig/saig/saigSimExt2.c | 112 ++++++++ src/base/abci/abc.c | 19 +- 5 files changed, 746 insertions(+), 59 deletions(-) diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 39d11174..315e3a8a 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -176,7 +176,8 @@ extern Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose ); /*=== saigRefSat.c ==========================================================*/ -extern Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); +extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); +extern Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ extern void Saig_ManMarkAutonomous( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ); @@ -192,6 +193,7 @@ extern Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirst extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose ); /*=== saigSimExt.c ==========================================================*/ extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose ); +extern Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose ); /*=== saigSimMv.c ==========================================================*/ extern int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose ); /*=== saigStrSim.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index bed5edaf..3cd508a6 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -225,7 +225,8 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo return NULL; if ( pnUseStart ) *pnUseStart = pAbs->pSeqModel->iFrame; - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose ); +// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); if ( vFlopsNew == NULL ) return NULL; if ( Vec_IntSize(vFlopsNew) == 0 ) @@ -238,7 +239,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo } // vFlopsNew contains PI numbers that should be kept in pAbs if ( fVerbose ) - printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); + printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) ); // add to the abstraction Vec_IntForEachEntry( vFlopsNew, Entry, i ) { @@ -276,7 +277,8 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, if ( fSensePath ) vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); else - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose ); +// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); if ( vFlopsNew == NULL ) { Aig_ManStop( pAbs ); diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index bc053fca..0b3dff23 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.c @@ -40,13 +40,187 @@ struct Saig_RefMan_t_ int fVerbose; // verbose flag // unrolling Aig_Man_t * pFrames; // unrolled timeframes - Vec_Int_t * vMapPiA3F; // mapping of frame PIs into real PIs + Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs }; +// performs ternary simulation +extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Maps array of frame PI IDs into array of original PI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_RefManReason2Inputs( Saig_RefMan_t * p, Vec_Int_t * vReasons ) +{ + Vec_Int_t * vOriginal, * vVisited; + int i, Entry; + vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) ); + vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); + Vec_IntForEachEntry( vReasons, Entry, i ) + { + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); + assert( iInput >= 0 && iInput < Aig_ManPiNum(p->pAig) ); + if ( Vec_IntEntry(vVisited, iInput) == 0 ) + Vec_IntPush( vOriginal, iInput ); + Vec_IntAddToEntry( vVisited, iInput, 1 ); + } + Vec_IntFree( vVisited ); + return vOriginal; +} + +/**Function************************************************************* + + Synopsis [Creates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_RefManReason2Cex( Saig_RefMan_t * p, Vec_Int_t * vReasons ) +{ + Abc_Cex_t * pCare; + int i, Entry, iInput, iFrame; + pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); + memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + Vec_IntForEachEntry( vReasons, Entry, i ) + { + assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); + Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + } + return pCare; +} + +/**Function************************************************************* + + Synopsis [Returns reasons for the property to fail.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + if ( pObj->fPhase ) + { + Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); + Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); + } + else + { + int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; + int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase; + assert( !fPhase0 || !fPhase1 ); + if ( !fPhase0 && fPhase1 ) + Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); + else if ( fPhase0 && !fPhase1 ) + Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); + else + { + int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); + int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); + if ( iPrio0 <= iPrio1 ) + Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); + else + Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); + } + } +} + +/**Function************************************************************* + + Synopsis [Returns reasons for the property to fail.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_RefManFindReason( Saig_RefMan_t * p ) +{ + Aig_Obj_t * pObj; + Vec_Int_t * vPrios, * vPi2Prio, * vReasons; + int i, CountPrios; + + vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) ); + vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) ); + + // set PI values according to CEX + CountPrios = 0; + Aig_ManConst1(p->pFrames)->fPhase = 1; + Aig_ManForEachPi( p->pFrames, pObj, i ) + { + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); + pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + // assign priority + if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 ) + Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ ); +// Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) ); + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); + } +// printf( "Priority numbers = %d.\n", CountPrios ); + Vec_IntFree( vPi2Prio ); + + // traverse and set the priority + Aig_ManForEachNode( p->pFrames, pObj, i ) + { + int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; + int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase; + int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); + int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); + pObj->fPhase = fPhase0 && fPhase1; + if ( fPhase0 && fPhase1 ) // both are one + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) ); + else if ( !fPhase0 && fPhase1 ) + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 ); + else if ( fPhase0 && !fPhase1 ) + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 ); + else // both are zero + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) ); + } + // check the property output + pObj = Aig_ManPo( p->pFrames, 0 ); + assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) ); + + // select the reason + vReasons = Vec_IntAlloc( 100 ); + Aig_ManIncrementTravId( p->pFrames ); + Saig_RefManFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons ); + Vec_IntFree( vPrios ); + return vReasons; +} + + /**Function************************************************************* Synopsis [Collect nodes in the unrolled timeframes.] @@ -86,7 +260,7 @@ void Saig_ManUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiA3F ) +Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A ) { Aig_Man_t * pFrames; // unrolled timeframes Vec_Vec_t * vFrameCos; // the list of COs per frame @@ -100,7 +274,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) ); // map PIs of the unrolled frames into PIs of the original design - *pvMapPiA3F = Vec_IntAlloc( 1000 ); + *pvMapPiF2A = Vec_IntAlloc( 1000 ); // collect COs and Objs visited in each frame vFrameCos = Vec_VecStart( pCex->iFrame+1 ); @@ -149,8 +323,8 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu else { pObj->pData = Aig_ObjCreatePi( pFrames ); - Vec_IntPush( *pvMapPiA3F, Aig_ObjPioNum(pObj) ); - Vec_IntPush( *pvMapPiA3F, f ); + Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) ); + Vec_IntPush( *pvMapPiF2A, f ); } } } @@ -164,6 +338,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu // create output pObj = Aig_ManPo( pAig, pCex->iPo ); Aig_ObjCreatePo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) ); + Aig_ManSetRegNum( pFrames, 0 ); // cleanup Vec_VecFree( vFrameCos ); Vec_VecFree( vFrameObjs ); @@ -192,6 +367,7 @@ Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInput p->pCex = pCex; p->nInputs = nInputs; p->fVerbose = fVerbose; + p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A ); return p; } @@ -209,7 +385,7 @@ Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInput void Saig_RefManStop( Saig_RefMan_t * p ) { Aig_ManStopP( &p->pFrames ); - Vec_IntFreeP( &p->vMapPiA3F ); + Vec_IntFreeP( &p->vMapPiF2A ); ABC_FREE( p ); } @@ -231,8 +407,8 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 ) Aig_ManConst1( p->pFrames )->fPhase = 1; Aig_ManForEachPi( p->pFrames, pObj, i ) { - iInput = Vec_IntEntry( p->vMapPiA3F, 2*i ); - iFrame = Vec_IntEntry( p->vMapPiA3F, 2*i+1 ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); // update value if it is a don't-care if ( pCare && !Aig_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) ) @@ -247,6 +423,41 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 ) return pObj->fPhase; } +/**Function************************************************************* + + Synopsis [Tries to remove literals from abstraction.] + + Description [The literals are sorted more desirable first.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Saig_RefManOrderLiterals( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps ) +{ + Vec_Vec_t * vLits; + Vec_Int_t * vVar2New; + int i, Entry, iInput, iFrame; + // collect literals + vLits = Vec_VecAlloc( 100 ); + vVar2New = Vec_IntStartFull( Saig_ManPiNum(p->pAig) ); + Vec_IntForEachEntry( vAssumps, Entry, i ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); +// Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + if ( Vec_IntEntry( vVar2New, iInput ) == ~0 ) + Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) ); + Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry ); + } + Vec_IntFree( vVar2New ); + return vLits; +} + + /**Function************************************************************* Synopsis [Generate the care set using SAT solver.] @@ -258,19 +469,51 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 ) SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p ) +Abc_Cex_t * Saig_RefManCreateCex( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps ) +{ + Abc_Cex_t * pCare; + int i, Entry, iInput, iFrame; + // create counter-example + pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); + memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + Vec_IntForEachEntry( vAssumps, Entry, i ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); + Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + } + return pCare; +} + +/**Function************************************************************* + + Synopsis [Generate the care set using SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) { int nConfLimit = 1000000; Abc_Cex_t * pCare; Cnf_Dat_t * pCnf; sat_solver * pSat; Aig_Obj_t * pObj; + Vec_Vec_t * vLits = NULL; Vec_Int_t * vAssumps, * vVar2PiId; - int i, f, iInput, iFrame, RetValue, Counter; + int i, k, f = 0, Entry, RetValue, Counter = 0; int nCoreLits, * pCoreLits; + int clk = clock(); // create CNF assert( Aig_ManRegNum(p->pFrames) == 0 ); - pCnf = Cnf_Derive( p->pFrames, 0 ); +// pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow + pCnf = Cnf_DeriveSimple( p->pFrames, 0 ); RetValue = Saig_RefManSetPhases( p, NULL, 0 ); if ( RetValue ) { @@ -286,6 +529,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p ) Cnf_DataFree( pCnf ); return NULL; } +//Abc_PrintTime( 1, "Preparing", clock() - clk ); // look for a true counter-example if ( p->nInputs > 0 ) { @@ -306,16 +550,43 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p ) vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) ); Aig_ManForEachPi( p->pFrames, pObj, i ) { - iInput = Vec_IntEntry( p->vMapPiA3F, 2*i ); - iFrame = Vec_IntEntry( p->vMapPiA3F, 2*i+1 ); + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); // RetValue = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) ); Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) ); Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i ); } + + // reverse the order of assumptions +// if ( fNewOrder ) +// Vec_IntReverseOrder( vAssumps ); + + if ( fNewOrder ) + { + // create literals + vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); + // sort literals + Vec_VecSort( vLits, 1 ); + // save literals + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); + + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "\n" ); + + if ( p->fVerbose ) + printf( "Total PIs = %d. Essential PIs = %d.\n", + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) ); + } + // solve +clk = clock(); RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +//Abc_PrintTime( 1, "Solving", clock() - clk ); if ( RetValue != l_False ) { if ( RetValue == l_True ) @@ -328,46 +599,89 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p ) Vec_IntFree( vVar2PiId ); return NULL; } + assert( RetValue == l_False ); // UNSAT + // get relevant SAT literals nCoreLits = sat_solver_final( pSat, &pCoreLits ); assert( nCoreLits > 0 ); if ( p->fVerbose ) - printf( "Analize final selected %d assumptions out of %d.\n", nCoreLits, Vec_IntSize(vAssumps) ); - // create counter-example - pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); - // set new values + printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n", + nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts ); + + // save literals + Vec_IntClear( vAssumps ); for ( i = 0; i < nCoreLits; i++ ) - { - int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) ); - assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); - iInput = Vec_IntEntry( p->vMapPiA3F, 2*iPiNum ); - iFrame = Vec_IntEntry( p->vMapPiA3F, 2*iPiNum+1 ); - Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); - } + Vec_IntPush( vAssumps, pCoreLits[i] ); + + + // create literals + vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); + // sort literals +// Vec_VecSort( vLits, 0 ); + // save literals + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); + +// for ( i = 0; i < Vec_VecSize(vLits); i++ ) +// printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); +// printf( "\n" ); - // further reduce the CEX - Counter = 0; - for ( i = p->nInputs; i < Saig_ManPiNum(p->pAig); i++ ) + if ( p->fVerbose ) + printf( "Total PIs = %d. Essential PIs = %d.\n", + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) ); +/* + // try assumptions in different order + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts ); + + // create different sets of assumptions + Counter = Vec_VecSize(vLits); + for ( f = 0; f < Vec_VecSize(vLits); f++ ) { - for ( f = 0; f <= pCare->iFrame; f++ ) - if ( Aig_InfoHasBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ) ) - break; - if ( f == pCare->iFrame + 1 ) + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + if ( i != f ) + Vec_IntPush( vAssumps, Entry ); + + // try the new assumptions + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts ); + if ( RetValue != l_False ) continue; - Counter++; - // try removing this input + // UNSAT - remove literals + Vec_IntClear( (Vec_Int_t *)Vec_VecEntry(vLits, f) ); + Counter--; } - if ( p->fVerbose ) - printf( "Essential primary inputs %d out of %d.\n", Counter, Saig_ManPiNum(p->pAig) - p->nInputs ); + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "\n" ); + + if ( p->fVerbose ) + printf( "Total PIs = %d. Essential PIs = %d.\n", + Saig_ManPiNum(p->pAig) - p->nInputs, Counter ); + + // save literals + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); +*/ + // create counter-example + pCare = Saig_RefManCreateCex( p, vVar2PiId, vAssumps ); // cleanup Cnf_DataFree( pCnf ); sat_solver_delete( pSat ); Vec_IntFree( vAssumps ); Vec_IntFree( vVar2PiId ); + Vec_VecFreeP( &vLits ); + // verify counter-example RetValue = Saig_RefManSetPhases( p, pCare, 0 ); if ( RetValue ) @@ -375,10 +689,167 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p ) RetValue = Saig_RefManSetPhases( p, pCare, 1 ); if ( RetValue ) printf( "Reduced CEX verification has failed.\n" ); - return pCare; -} +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) +{ + int nConfLimit = 1000000; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + Vec_Vec_t * vLits; + Vec_Int_t * vReasons, * vAssumps, * vVisited, * vVar2PiId; + int i, k, f, Entry, RetValue, Counter; + + // create CNF and SAT solver + pCnf = Cnf_DeriveSimple( p->pFrames, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + return NULL; + } + + // mark used AIG inputs + vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); + Vec_IntForEachEntry( vAigPis, Entry, i ) + { + assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pAig) ); + Vec_IntWriteEntry( vVisited, Entry, 1 ); + } + + // create assumptions + vVar2PiId = Vec_IntStartFull( pCnf->nVars ); + vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) ); + Aig_ManForEachPi( p->pFrames, pObj, i ) + { + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); + if ( Vec_IntEntry(vVisited, iInput) == 0 ) + continue; + RetValue = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) ); +// Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) ); + Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i ); + } + Vec_IntFree( vVisited ); + + // try assumptions in different order + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts ); + +/* + // AnalizeFinal does not work because it implications propagate directly + // and SAT solver does not kick in (the number of conflicts in 0). + + // count the number of lits in the unsat core + { + int nCoreLits, * pCoreLits; + nCoreLits = sat_solver_final( pSat, &pCoreLits ); + assert( nCoreLits > 0 ); + + // count the number of flops + vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); + for ( i = 0; i < nCoreLits; i++ ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) ); + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); + Vec_IntWriteEntry( vVisited, iInput, 1 ); + } + // count the number of entries + Counter = 0; + Vec_IntForEachEntry( vVisited, Entry, i ) + Counter += Entry; + Vec_IntFree( vVisited ); + +// if ( p->fVerbose ) + printf( "AnalizeFinal: Assumptions %d (out of %d). Essential PIs = %d. Conflicts = %d.\n", + nCoreLits, Vec_IntSize(vAssumps), Counter, (int)pSat->stats.conflicts ); + } +*/ + + // derive literals + vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "\n" ); + + // create different sets of assumptions + Counter = Vec_VecSize(vLits); + for ( f = 0; f < Vec_VecSize(vLits); f++ ) + { + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + if ( i != f ) + Vec_IntPush( vAssumps, Entry ); + + // try the new assumptions + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts ); + if ( RetValue != l_False ) + continue; + + // UNSAT - remove literals + Vec_IntClear( (Vec_Int_t *)Vec_VecEntry(vLits, f) ); + Counter--; + } + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "\n" ); + + // create assumptions + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); + + // try assumptions in different order + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts ); + +// if ( p->fVerbose ) +// printf( "Total PIs = %d. Essential PIs = %d.\n", +// Saig_ManPiNum(p->pAig) - p->nInputs, Counter ); + + + // transform assumptions into reasons + vReasons = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vAssumps, Entry, i ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); + Vec_IntPush( vReasons, iPiNum ); + } + + // cleanup + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + Vec_IntFree( vAssumps ); + Vec_IntFree( vVar2PiId ); + Vec_VecFreeP( &vLits ); + + return vReasons; +} /**Function************************************************************* @@ -393,32 +864,119 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p ) SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ) +Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose ) { - Abc_Cex_t * pCare = NULL; + Saig_RefMan_t * p; + Vec_Int_t * vReasons; + Abc_Cex_t * pCare; int clk = clock(); - Saig_RefMan_t * p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose ); - p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiA3F ); -if ( p->fVerbose ) + + clk = clock(); + p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose ); + vReasons = Saig_RefManFindReason( p ); + +if ( fVerbose ) Aig_ManPrintStats( p->pFrames ); -if ( p->fVerbose ) -Abc_PrintTime( 1, "Frames", clock() - clk ); +// if ( fVerbose ) + { + Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons ); + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + + Vec_IntFree( vRes ); + +/* + //////////////////////////////////// + Vec_IntFree( vReasons ); + vReasons = Saig_RefManRefineWithSat( p, vRes ); + //////////////////////////////////// + + Vec_IntFree( vRes ); + vRes = Saig_RefManReason2Inputs( p, vReasons ); + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); + + Vec_IntFree( vRes ); +ABC_PRT( "Time", clock() - clk ); +*/ + } - clk = clock(); - pCare = Saig_RefManRunSat( p ); + pCare = Saig_RefManReason2Cex( p, vReasons ); + Vec_IntFree( vReasons ); Saig_RefManStop( p ); -if ( p->fVerbose ) -Abc_PrintTime( 1, "Filter", clock() - clk ); - -if ( p->fVerbose ) +if ( fVerbose ) Abc_CexPrintStats( pCex ); -if ( p->fVerbose ) +if ( fVerbose ) Abc_CexPrintStats( pCare ); + return pCare; } +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) +{ + Saig_RefMan_t * p; + Vec_Int_t * vRes, * vReasons; + int clk; + if ( Saig_ManPiNum(pAig) != pCex->nPis ) + { + printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", + Aig_ManPiNum(pAig), pCex->nPis ); + return NULL; + } + +clk = clock(); + + p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose ); + vReasons = Saig_RefManFindReason( p ); + vRes = Saig_RefManReason2Inputs( p, vReasons ); + +// if ( fVerbose ) + { + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + } + +/* + //////////////////////////////////// + Vec_IntFree( vReasons ); + vReasons = Saig_RefManRefineWithSat( p, vRes ); + //////////////////////////////////// + + // derive new result + Vec_IntFree( vRes ); + vRes = Saig_RefManReason2Inputs( p, vReasons ); +// if ( fVerbose ) + { + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + } +*/ + + Vec_IntFree( vReasons ); + Saig_RefManStop( p ); + return vRes; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c index cb5d3b77..3d9cc88a 100644 --- a/src/aig/saig/saigSimExt2.c +++ b/src/aig/saig/saigSimExt2.c @@ -360,6 +360,118 @@ ABC_PRT( "Time", clock() - clk ); return vRes; } + + + + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +{ + Abc_Cex_t * pCare; + Aig_Obj_t * pObj; + Vec_Int_t * vRes, * vResInv; + int i, f, Value; +// assert( Aig_ManRegNum(p) > 0 ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + // start simulation data + Value = Saig_ManSimDataInit2( p, pCex, vSimInfo ); + assert( Value == SAIG_ONE_NEW ); + // derive implications of constants and primary inputs + Saig_ManForEachLo( p, pObj, i ) + Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo ); + for ( f = pCex->iFrame; f >= 0; f-- ) + { + Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo ); + for ( i = 0; i < iFirstFlopPi; i++ ) + Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo ); + } + // recursively compute justification + Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); + + // create CEX + pCare = Abc_CexDup( pCex, pCex->nRegs ); + memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + + // select the result + vRes = Vec_IntAlloc( 1000 ); + vResInv = Vec_IntAlloc( 1000 ); + for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) + { + int fFound = 0; + for ( f = pCex->iFrame; f >= 0; f-- ) + { + Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f ); + if ( Saig_ManSimInfo2IsOld( Value ) ) + { + fFound = 1; + Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ); + } + } + if ( fFound ) + Vec_IntPush( vRes, i ); + else + Vec_IntPush( vResInv, i ); + } + // resimulate to make sure it is valid + Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); + assert( Value == SAIG_ONE ); + Vec_IntFree( vResInv ); + Vec_IntFree( vRes ); + + return pCare; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose ) +{ + Abc_Cex_t * pCare; + Vec_Ptr_t * vSimInfo; + int clk; + if ( Saig_ManPiNum(p) != pCex->nPis ) + { + printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", + Aig_ManPiNum(p), pCex->nPis ); + return NULL; + } + Aig_ManFanoutStart( p ); + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); + Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); + +clk = clock(); + pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); + if ( fVerbose ) + { +// printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); +Abc_CexPrintStats( pCex ); +Abc_CexPrintStats( pCare ); +ABC_PRT( "Time", clock() - clk ); + } + + Vec_PtrFree( vSimInfo ); + Aig_ManFanoutStop( p ); + return pCare; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index aa6ec83c..581af654 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8626,11 +8626,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) int nLeafMax = 10; int nDivMax = 50; int nDecMax = 3; + int fNewAlgo = 0; + int fNewOrder = 0; int fVerbose = 0; int fVeryVerbose = 0; int c; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNaovwh" ) ) != EOF ) { switch ( c ) { @@ -8678,6 +8680,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nDecMax < 0 ) goto usage; break; + case 'a': + fNewAlgo ^= 1; + break; + case 'o': + fNewOrder ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -8770,7 +8778,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Cex_t * pNew; Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, 0 ); + if ( fNewAlgo ) + pNew = Saig_ManFindCexCareBitsSense( pAig, pAbc->pCex, 0, fVerbose ); + else + pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, fNewOrder, fVerbose ); Aig_ManStop( pAig ); Abc_FrameReplaceCex( pAbc, &pNew ); } @@ -8779,12 +8790,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: test [-CKDN] [-vwh] \n" ); + Abc_Print( -2, "usage: test [-CKDN] [-aovwh] \n" ); Abc_Print( -2, "\t testbench for new procedures\n" ); Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax ); Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax ); Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax ); Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax ); + Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle using new ordering [default = %s]\n", fNewOrder? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); -- cgit v1.2.3